On Church's Thesis in Cubical Assemblies

Andrew Swan, Taichi Uemura

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 tha…