# On Church's Thesis in Cubical Assemblies

arXiv: https://arxiv.org/abs/1905.03014 · HTML: https://mlsanity.com/paper/1905.03014/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 May 2019.

## Built on by (most cited first, 1 of 1)

- [Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions](https://mlsanity.com/paper/2307.15543/) (2023)

## 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.