Authors
A.W. Swan
T. Uemura
Date (dd-mm-yyyy)
2019-05-09
Title
On Church's Thesis in Cubical Assemblies
Publication Year
2019-05-09
Document type
Working paper
Abstract
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.
Permalink
https://hdl.handle.net/11245.1/79eb8b20-7871-4cf9-87b6-f1975e73af8d