On Church's Thesis in Cubical Assemblies
Not on the map. Why?
Abstract (arXiv)
We show that Church's thesis, the axiom stating that all functions on the naturals are computable, does not hold in the cubical assemblies model of cubical type theory. We show that nevertheless Church's thesis is consistent with univalent type theory by constructing a reflective subuniverse of cubical assemblies where it holds.
Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). First posted on arXiv 8 May 2019.
Builds on
No reference list yet.
Built on by
Citing papers per year: 2023: 1.
1 paper.