# On Church's Thesis in Cubical Assemblies

## TL;DR

This paper investigates Church's thesis within cubical assemblies, demonstrating its failure in the model but establishing its consistency through a specialized subuniverse.

## Contribution

It shows that Church's thesis does not hold in cubical assemblies but remains consistent with univalent type theory via a constructed reflective subuniverse.

## Key findings

- Church's thesis fails in cubical assemblies
- Church's thesis is consistent with univalent type theory
- A reflective subuniverse where Church's thesis holds is constructed

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