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.

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.

Equations

$$\prod _{f:\mathbb{N}\to \mathbb{N}}\sum _{e:\mathbb{N}}\prod _{x:\mathbb{N}}\sum _{z:\mathbb{N}}T(e,x,z)\wedge U(z)=f(x)$$

$$\prod _{f:\mathbb{N}\to \mathbb{N}}\Vert \sum _{e:\mathbb{N}}\prod _{x:\mathbb{N}}\sum _{z:\mathbb{N}}T(e,x,z)\times U(z)=f(x)\Vert$$

$${\left(\mathcal{C}/\Gamma \right)}^{\mathrm{op}}\ni (f:\Delta \to \Gamma )\mapsto E(\Delta ,X\cdot f)\in \mathbf{Set}$$

$$\begin{gathered} \text{inferrule}\Gamma ⊢{\mathcal{J}}_1 \\ \dots \\ \Gamma ⊢{\mathcal{J}}_n\Gamma ⊢A({\mathcal{J}}_1,\dots ,{\mathcal{J}}_n) \end{gathered}$$

$${\mathcal{U}}_0:{\mathcal{U}}_1:{\mathcal{U}}_2:\dots$$

$$X\times 2$$

$$R$$

$$S$$

$$S(a,f,f^{\prime },b,0)$$

$$S(a,f,f^{\prime },b,1)$$

$$s(\mathsf{ext}(a,f))$$

$$s(\mathsf{isext}(a,f,b)(i))$$

$$X$$

$$u(j,\ast ):\equiv \{\begin{array}{ll}\mathsf{pastecone}(t_A(a),\mathsf{inr}(t_B(b),i),t\circ f\circ t_B^{-1})& j=0\\ \mathsf{pastecone}(a,\mathsf{inr}(b,i),t\circ f)& \phi =\top \\ \mathsf{pastecone}(t_A(a),\mathsf{inl}(\ast ),t\circ f\circ t_B^{-1})& i=0\\ t(f(p(a,b,j)))& i=1\end{array}$$

$$\mathsf{ext}(a,f)$$

$$\mathsf{isext}(a,f,b)(i)$$

$$R$$

$$S$$

$$s(\mathsf{pastecone}(a,\mathsf{inl}(\ast ),f))$$

$$s(\mathsf{pastecone}(a,\mathsf{inr}(b,i),f))$$

$$\prod _{g:e\to d}{N}_0(e,f\circ g{)}^{X(f\circ g,\Gamma (f\circ g)(\gamma ),Y(g)(y))}$$

$${\forall }_{f:\mathbb{N}\to \mathbb{N}}{\exists }_{e:\mathbb{N}}{\forall }_{x:\mathbb{N}}{\exists }_{z:\mathbb{N}}T(e,x,z)\wedge U(z)=f(x)$$

$$\prod _{f:\mathbb{N}\to \mathbb{N}}\Vert \sum _{e:\mathbb{N}}\prod _{x:\mathbb{N}}\sum _{z:\mathbb{N}}T(e,x,z)\times U(z)=f(x)\Vert .$$

$$\Gamma ⊢\prod _{a:A}\mathsf{isEquiv}(\lambda (x:X).\lambda (b:B(a)).x)$$

$$U_B\equiv \{X:U\mid {\mathsf{isNull}}_B(X)\}.$$

$$({\mathcal{L}}_B\Vert X\Vert \to Z)$$

$$\simeq (X\to Z).$$

$$\Gamma ⊢{\mathsf{isNull}}_B(X)\to {\mathsf{isNull}}_B(Y)\to {\mathsf{isNull}}_B(X+Y).$$

$$X+Y$$

$${\forall }_{\alpha :\mathbb{N}\to 2}\neg \neg ({\exists }_{n:\mathbb{N}}\alpha (n))\to {\exists }_{n:\mathbb{N}}\alpha (n)$$

$$\prod _{\alpha :\mathbb{N}\to 2}\prod _{p:({\prod }_{n:\mathbb{N}}\alpha (n)\to 0)\to 0}\Vert \sum _{n:\mathbb{N}}\alpha (n)\Vert .$$

$$B^{\prime }(\mathsf{inl}(a))$$

$$B^{\prime }(\mathsf{inr}(x))$$

$$\prod _{f:\mathbb{N}\to \mathbb{N}}\Vert \sum _{e:\mathbb{N}}\prod _{x:\mathbb{N}}\sum _{z:\mathbb{N}}T(e,x,z)\times U(z)=f(x)\Vert .$$

Full text

We show that nevertheless Church’s thesis is consistent with univalent type theory by constructing a reflective subuniverse of cubical assemblies where it holds.

1 Introduction

One of the main branches of constructive mathematics is that of recursive or “Russian” constructivism, where to justify the existence of mathematical objects, one must show how to compute them. A rather extreme interpretation of this philosophy is the axiom of Church’s thesis, which states that all functions from $\mathbb{N}$ to $\mathbb{N}$ are computable. Despite (or perhaps because) of its highly non-classical nature it has been well studied by logicians and turns out to be consistent with a wide variety of formal theories for constructive mathematics. This is usually proved using realizability models based on computable functions, starting with Kleene’s model of Heyting arithmetic[Kle45], but with many later variants and generalisations. See for example [TvD88, Chapter 4, Section 4] for a standard reference.

When interpreting Church’s thesis in type theory an additional complication is introduced. Logical statements are usually interpreted in type theory using the propositions-as-types interpretation. Applying this to Church’s thesis would give us the type below.

[TABLE]

However it is straightforward to use function extensionality to show that this type is empty.111Surprisingly, however, this version is consistent with intensional type theory as long as one drops the $\xi$ rule, which was proved by Ishihara, Maietti, Maschio and Streicher in [IMMS18]. They leave the case where one has the $\xi$ rule but not function extensionality open and to the authors’ knowledge it remains an open problem. It is therefore impossible in any case to show that the above “untruncated” version of Church’s thesis is consistent with univalence, since univalence implies function extensionality [Uni13, Theorem 4.9.4].

To have any hope of showing Church’s thesis is consistent with univalence we need a different formulation. We will use the interpretation of logical statements advocated in [Uni13, Section 3.7], and commonly used in homotopy type theory and elsewhere. In this approach one uses the higher inductive type of propositional truncation at disjunction and existential quantifiers, which ensures that the resulting type is always an hproposition (i.e. that any two of its elements are equal). This yields the following version of Church’s thesis, which is the one we will study here.

[TABLE]

It is well known that Church’s thesis holds in the internal logic of Hyland’s effective topos (see for instance [vO08, Section 3.1] for a standard reference). Similar arguments show that in fact it already holds in its simpler subcategory of assemblies, and even in cubical assemblies, when they are viewed as regular locally cartesian closed categories and thereby, following Awodey and Bauer in [AB04] or Maietti in [Mai05] as models of extensional type theory with propositional truncation. However, the interpretation of cubical type theory in cubical assemblies due to the second author [Uem18] is very different to the interpretation of extensional type theory. We draw attention in particular to the fact that for extensional type theory hpropositions are implemented as maps where in the internal logic each fibre has at most one element.222Equivalently, the map is a monomorphism, and for this reason hpropositions are sometimes referred to as mono types. On the other hand in the interpretation of cubical type theory, each fibre can have multiple elements as long as any two elements are joined by a path, telling us to always treat them as “propositionally equal.” For propositional truncation we don’t strictly identify elements by quotienting, but instead add new paths. Our first result is that Church’s thesis is in fact false in the interpretation of cubical type theory in cubical assemblies, even though it holds in the internal logic.

To show Church’s thesis is consistent with univalence we will combine cubical assemblies with the work of Rijke, Shulman and Spitters on modalities and $\Sigma$-closed reflective subuniverses in [RSS17]. We will construct a reflective subuniverse where Church’s thesis is forced to hold, and then use properties of cubical assemblies to show that this reflective subuniverse is non trivial. Our model can also be viewed as a kind of stack model akin to those used by Coquand for various independence and consistency results, including the independence of countable choice from homotopy type theory [Coq18], although our formulation will be quite different to Coquand’s.

Acknowledgements

The first author is grateful for some helpful discussions on higher inductive types with Simon Huber, Anders Mörtberg and Christian Sattler at the Hausdorff Research Institute for Mathematics during the trimester program Types, Sets and Constructions. The second author is supported by the research programme “The Computational Content of Homotopy Type Theory” with project number 613.001.602, which is financed by the Netherlands Organisation for Scientific Research (NWO). We are grateful to Benno van den Berg for helpful comments and corrections.

2 Models of Type Theories

In this paper we use models of different kinds of type theory: extensional dependent type theory; intensional dependent type theory (with the univalence axiom). All of them are based on the notion of a category with families [Dyb96].

Definition 2.1**.**

Let $\mathcal{C}$ be a category. A cwf-structure over $\mathcal{C}$ is a pair $(T,E)$ of presheaves $T:\mathcal{C}^{\mathrm{op}}\to\mathbf{Set}$ and $E:\left(\int_{\mathcal{C}}T\right)^{\mathrm{op}}\to\mathbf{Set}$ such that, for any object $\Gamma\in\mathcal{C}$ and element $X\in T(\Gamma)$, the presheaf

[TABLE]

is representable. The representing object for this presheaf is denoted by $\chi(X):\{X\}\to\Gamma$ or $\chi(X):\Gamma.X\to\Gamma$. A category with families, cwf in short, is a triple $\mathcal{E}=(\mathbb{C}^{\mathcal{E}},\mathbb{T}^{\mathcal{E}},\mathbb{E}^{\mathcal{E}})$ such that $\mathbb{C}^{\mathcal{E}}$ is a category with a terminal object and $(\mathbb{T}^{\mathcal{E}},\mathbb{E}^{\mathcal{E}})$ is a cwf-structure over $\mathbb{C}^{\mathcal{E}}$.

In general a model $\mathcal{E}$ of a type theory consists of a category with families $(\mathbb{C}^{\mathcal{E}},\mathbb{T}^{\mathcal{E}},\mathbb{E}^{\mathcal{E}})$ and algebraic operations on the presheaves $\mathbb{T}^{\mathcal{E}}$ and $\mathbb{E}^{\mathcal{E}}$. An object $\Gamma$ of $\mathbb{C}^{\mathcal{E}}$ is called a context. An element $X$ of $\mathbb{T}^{\mathcal{E}}(\Gamma)$ is called a type and written $\Gamma\vdash_{\mathcal{E}}X$. An element $a$ of $\mathbb{E}^{\mathcal{E}}(\Gamma,X)$ is called an element of type $X$ and written $\Gamma\vdash_{\mathcal{E}}a:X$. The subscript of $\vdash_{\mathcal{E}}$ is omitted when the model $\mathcal{E}$ is clear from the context. An algebraic operation on those presheaves is expressed by the schema

[TABLE]

where $\Gamma\vdash\mathcal{J}_{j}$ and $\Gamma\vdash A(\mathcal{J}_{1},\dots,\mathcal{J}_{n})$ are either of the form $\Gamma.X_{1}.\dots.X_{m}\vdash Y$ or of the form $\Gamma.X_{1}.\dots.X_{m}\vdash b:Y$ with $(\Gamma\vdash X_{1}),\dots,(\Gamma.X_{1}.\dots.X_{m-1}\vdash X_{m})$. In this schema we always assume that the operation $A(\mathcal{J}_{1},\dots,\mathcal{J}_{n})$ is stable under reindexing: if $f:\Delta\to\Gamma$ is a morphism in $\mathbb{C}^{\mathcal{E}}$, then we have $A(\mathcal{J}_{1},\dots,\mathcal{J}_{n})\cdot f=A(\mathcal{J}_{1}\cdot f,\dots,\mathcal{J}_{n}\cdot f)$.

Example 2.2*.*

Let $\mathcal{E}$ be a cwf. We say $\mathcal{E}$ supports dependent product types if it has operations {mathpar} \inferruleΓ⊢X

Γ.X ⊢Y Γ⊢Π(X, Y) \inferruleΓ⊢X

Γ.X ⊢Y

Γ.X ⊢b : Y Γ⊢λ(X, Y, b) : Π(X, Y)

such that the map $\mathbb{E}(\Gamma.X,Y)\ni b\mapsto\lambda(X,Y,b)\in\mathbb{E}(\Gamma,\Pi(X,Y))$ is bijective.

It is a kind of routine to describe other type constructors such as dependent sum types, extensional and intensional identity types, inductive types, higher inductive types and universes.

For a model $\mathcal{E}$ of a type theory, we denote by $[\![-]\!]^{\mathcal{E}}$ the interpretation of the type theory in the model $\mathcal{E}$.

Definition 2.3**.**

By a model of univalent type theory we mean a cwf that supports dependent product types, dependent sum type, intensional identity types, unit type, finite coproducts, natural numbers, propositional truncation and a countable chain

[TABLE]

of univalent universes.

2.1 Internal Languages

Formally we will work with models of type theories, but we will construct types and terms of those models in a syntactic way using their internal languages. Let $\mathcal{E}=(\mathbb{C}^{\mathcal{E}},\mathbb{T}^{\mathcal{E}},\mathbb{E}^{\mathcal{E}},\dots)$ be a model of a type theory. For a context $\Gamma\in\mathbb{C}^{\mathcal{E}}$ and a type $\Gamma\vdash X$, we introduce a variable $x$ and write $(\Gamma,x:X)$ for the context $\Gamma.X$. For another type $\Gamma\vdash Y$, the weakening $\Gamma,x:X\vdash Y$ is interpreted as the reindexing $\Gamma.X\vdash Y\cdot\chi(X)$. For an element $\Gamma\vdash a:X$ and a type $\Gamma,x:X\vdash Y(x)$, the substitution $\Gamma\vdash Y(a)$ is interpreted as the reindexing $\Gamma\vdash Y\cdot\bar{a}$, where $\bar{a}:\Gamma\to\Gamma.X$ is the section of $\Gamma.X\to\Gamma$ corresponding to the element $\Gamma\vdash a:X$. All type and term constructors of the type theory are soundly interpreted in $\mathcal{E}$ in a natural way. Note that types and terms built in the internal language are stable under reindexing.

2.2 $W$-types with Reductions

We will later use $W$-types with reductions to construct higher inductive types. So that we can use them internally in type theory we give below a new, split formulation. This is based on the non-dependent special case of the version in [Swa18].

Let $\mathcal{E}=(\mathbb{C}^{\mathcal{E}},\mathbb{T}^{\mathcal{E}},\mathbb{E}^{\mathcal{E}},\dots)$ be a model of a type theory with dependent product types, dependent sum types and extensional identity types. Suppose that $\mathcal{E}$ has types $1\vdash\mathbb{F}$ and $\varphi:\mathbb{F}\vdash[\varphi]$ such that $\varphi:\mathbb{F},x:[\varphi],y:[\varphi]\vdash x=y$. We call an element of $\mathbb{F}$ a cofibrant proposition. We often omit $[-]$ and regard an element $\varphi:\mathbb{F}$ itself as a type. A cofibrant polynomial with reductions over a context $\Gamma\in\mathbb{C}^{\mathcal{E}}$ consists of the following data:

• •

a type $\Gamma\vdash Y$ of constructors;

• •

a type $\Gamma,y:Y\vdash X(y)$ of arities;

• •

a cofibrant proposition $\Gamma,y:Y\vdash R(y):\mathbb{F}$ together with an element $\Gamma,y:Y,r:R(y)\vdash k(y,r):X(y)$ which we refer to as the reductions.

An algebra for a cofibrant polynomial with reductions $(Y,X,R,k)$ over $\Gamma\in\mathbb{C}^{\mathcal{E}}$ is a type $\Gamma\vdash W$ together with an element $\Gamma,y:Y,\alpha:X(y)\to W\vdash s(y,\alpha):W$ such that $\Gamma,y:Y,\alpha:X(y)\to W,r:R(y)\vdash s(y,\alpha)=\alpha(k(y,r))$. Algebras for $(Y,X,R,k)$ form a category in the obvious way and we say $\mathcal{E}$ supports cofibrant $W$-types with reductions if every cofibrant polynomial with reductions has an initial algebra preserved by reindexing.

3 Orton-Pitts Construction

Assumption 3.1**.**

Let $\mathcal{E}$ be a model of dependent type theory that supports dependent product types, dependent sum types, extensional identity types, unit type, finite colimits, natural numbers, propositional truncation and a countable chain of universes. We further assume that every context $\Gamma\in\mathbb{C}^{\mathcal{E}}$ is isomorphic to $1.X$ for some type $X$ over the terminal object $1$. Suppose the following:

• •

$\mathcal{E}$ has a type $1\vdash\mathbb{I}$ equipped with two constants [math] and $1$ and two binary operators $\sqcap$ and $\sqcup$;

• •

$\mathcal{E}$ has types $1\vdash\mathbb{F}$ and $\varphi:\mathbb{F}\vdash[\varphi]$ such that $\varphi:\mathbb{F},x:[\varphi],y:[\varphi]\vdash x=y$. An element of $\mathbb{F}$ is called a cofibrant proposition. We often omit $[-]$ and regard an element $\varphi:\mathbb{F}$ itself as a type;

• •

$\mathbb{I}$ and $\mathbb{F}$ satisfy $\mathtt{ax_{1}}$–$\mathtt{ax_{9}}$ given by Orton and Pitts [OP18];

• •

$\mathbb{F}$ satisfies propositional extensionality: $\prod_{\varphi,\psi:\mathbb{F}}(\varphi\Leftrightarrow\psi)\Rightarrow(\varphi=\psi)$;

• •

the exponential functor $(-)^{\mathbb{I}}:\mathbb{C}^{\mathcal{E}}\to\mathbb{C}^{\mathcal{E}}$ has a right adjoint;

• •

$\mathcal{E}$ supports cofibrant $W$-types with reductions.

Note that the axioms in [OP18] are written in the internal language of an elementary topos, but they are easily translated into dependent type theory with $\mathbb{I}$ and $\mathbb{F}$ as above. We require propositional extensionality which trivially holds when $\mathbb{F}$ is a subobject of the subobject classifier of an elementary topos.

Under these assumptions, we will build a model $\widetilde{\mathcal{E}}$ of univalent type theory as follows:

• •

the base category $\mathbb{C}^{\widetilde{\mathcal{E}}}$ is that of $\mathcal{E}$;

• •

the types $\Gamma\vdash_{\widetilde{\mathcal{E}}}X$ are the types $\Gamma\vdash_{\mathcal{E}}X$ equipped with a “fibration structure”;

• •

the elements $\Gamma\vdash_{\widetilde{\mathcal{E}}}a:X$ are the elements $\Gamma\vdash_{\mathcal{E}}a:X$ of the underlying type $X$ in $\mathcal{E}$;

By the construction given in [OP18], this model $\widetilde{\mathcal{E}}$ supports dependent product types, dependent sum types, identity types, unit type, finite coproducts and natural numbers. For a countable chain of univalent universes, use the right adjoint to $(-)^{\mathbb{I}}$ as in [LOPS18]. It remains to show that $\widetilde{\mathcal{E}}$ supports propositional truncation, which will be proved in Section 3.1 using cofibrant $W$-types with reductions. We call a model of univalent type theory of the form $\widetilde{\mathcal{E}}$ an Orton-Pitts model.

3.1 Higher Inductive Types in Orton-Pitts Models

We are still working with a model $\mathcal{E}$ of type theory that satisfies Assumption 3.1. We will show how to construct higher inductive types in $\widetilde{\mathcal{E}}$. Our techniques are fairly general, although we will focus on the HITs that we will need for the main theorem. The techniques developed by Coquand Huber and Mörtberg in [CHM18] are already very close to working in arbitrary Orton-Pitts models. The only exception is that the underlying objects for the HITs are given by certain initial algebras, which are constructed directly for cubical sets. This definition doesn’t quite work for cubical assemblies for two reasons. Firstly we are using a different cube category, and secondly we are working internally in assemblies. Rather than proving the same results again for cubical assemblies we will use a more general approach based on $W$-types with reductions that covers both cases. The first author already showed in [Swa18, Section 4] that (non-split) $W$-types with locally decidable reductions can be constructed in any category of presheaf assemblies and we’ll see later how to ensure that we get in fact split $W$-types with reductions in presheaf assemblies.

Finally, we will also make some minor adjustments related to the fact that we do not assume the interval object has reversals.

When we construct higher inductive types, we will use formulations based on $\mathsf{Path}$ types, following Coquand, Huber and Mörtberg. Technically these formulations can only be stated in cubical type theory, and not in intensional type theory in general. However, it is straightforward to derive versions based on $\mathsf{Id}$ types using the equivalence of $\mathsf{Path}$ and $\mathsf{Id}$ types, which are then valid in $\widetilde{\mathcal{E}}$. We note that although computation rules hold definitionally for both point and path constructors for the $\mathsf{Path}$ type versions, after translating to $\mathsf{Id}$ types, the definitional equality only holds for point constructors. However, neither definitional equality will be needed for our end result.

Definition 3.2**.**

Given a type $\Gamma\vdash_{\mathcal{E}}A$, we define the local fibrant replacement of $A$, $\mathsf{LFR}(A)$ to be the $W$-type with reductions defined as follows.

• •

When $a:A$, we add an element $\mathsf{inc}(a)$ to $\mathsf{LFR}(A)$.

• •

When $\varphi:\mathbb{F}$, $\epsilon\in\{0,1\}$ and $u:\sum_{i:\mathbb{I}}((i=\epsilon)\vee\varphi)\;\to\;\mathsf{LFR}(A)$, we add an element $\mathsf{hcomp}(\varphi,\epsilon,u)$ to $\mathsf{LFR}(A)$.

• •

If $p:\varphi$ and $\epsilon$ and $u$ are as above then $\mathsf{hcomp}(\varphi,\epsilon,u)$ reduces to $u(1-\epsilon,p)$.

Formally, we define the constructors $Y$ to be the coproduct $A+(\mathbb{F}\times 2)$. We take the arity $X(\mathsf{inl}(a))$ to be the empty type for $a:A$ and $X(\varphi,\epsilon)$ to be $\sum_{i:\mathbb{I}}\varphi\vee(i=\epsilon)$ for $(\varphi,\epsilon):\mathbb{F}\times 2$. We take the reductions $R(\mathsf{inl}(a))$ to be $\bot$ for $a:A$ and $R(\varphi,\epsilon)$ to be $\varphi$ together with the map $p:\varphi\vdash(1-\epsilon,p):\sum_{i:\mathbb{I}}\varphi\vee(i=\epsilon)$.

Theorem 3.3**.**

The model $\widetilde{\mathcal{E}}$ supports suspensions.

Proof.

Suppose we are given a type $\Gamma\vdash_{\widetilde{\mathcal{E}}}X$. We first construct the naïve suspension, $\mathsf{Susp}_{0}(X)$ as the pushout below.

[TABLE]

We next take the local fibrant replacement, to get $\mathsf{LFR}(\mathsf{Susp}_{0}(X))$. This is then an initial $\mathsf{Susp}(X)$ algebra, as defined by Coquand, Huber and Mörtberg in [CHM18, Section 2.2] and so we can then proceed with the same proof as they do there. ∎

Theorem 3.4**.**

The model $\widetilde{\mathcal{E}}$ supports propositional truncation.

Proof.

Suppose we are given a type $\Gamma\vdash_{\widetilde{\mathcal{E}}}A$. We first define the underlying object of $\|A\|$ to be the $W$-type with reductions defined as follows.

• •

When $a:A$, we add an element $\mathsf{inc}(a)$ to $\|A\|$.

• •

When $\varphi:\mathbb{F}$, $\epsilon\in\{0,1\}$ and $u:\sum_{i:\mathbb{I}}((i=\epsilon)\vee\varphi)\;\to\;\|A\|$, we add an element $\mathsf{hcomp}(\varphi,\epsilon,u)$ to $\|A\|$.

• •

If $p:\varphi$ and $\epsilon$ and $u$ are as above then $\mathsf{hcomp}(\varphi,\epsilon,u)$ reduces to $u(1-\epsilon,p)$.

• •

If $x,y:\|A\|$ and $i:\mathbb{I}$, then $\|A\|$ contains an element of the form $\mathsf{sq}(x,y,i)$.

• •

If $x,y,i$ are as above and $i=0$, then $\mathsf{sq}(x,y,i)$ reduces to $x$.

• •

If $x,y,i$ are as above and $i=1$, then $\mathsf{sq}(x,y,i)$ reduces to $y$.

Formally, we define this by taking the coproduct of two polynomials with reductions. The first is the one we used before for $\mathsf{LFR}$. The second has constructors $Y:=\mathbb{I}$, with the arity defined by $X(i):=2$, and reductions $R(i):=(i=0)\lor(i=1)$ together with the map $p:(i=0)\lor(i=1)\vdash k(p):2$ defined by $k(p)=0$ if $p:i=0$ and $k(p)=1$ if $p:i=1$.

The remainder of the proof is the same as the syntactic description of propositional truncation by Coquand, Huber and Mörtberg in [CHM18, Section 3.3.4]. ∎

We now construct a new higher inductive type, which is a simplified version of the higher inductive type $\mathcal{J}_{F}$ defined by Rijke, Shulman and Spitters in [RSS17, Section 2.2]. Given families of types $\Gamma\vdash_{\widetilde{\mathcal{E}}}A$ and $\Gamma,a:A\vdash_{\widetilde{\mathcal{E}}}B(a)$ we will construct a higher inductive type $\mathcal{K}^{\Gamma}_{B}$ defined as follows.

• •

When $a:A$ and $f:B(a)\to\mathcal{K}_{B}$, we add an element $\mathsf{ext}(a,f)$ to $\mathcal{K}_{B}$.

• •

When $a:A$, $f:B(a)\to\mathcal{K}_{B}$ and $b:B(a)$ we add an element $\mathsf{isext}(a,f,b)$ to $\mathsf{Path}(\mathsf{ext}(a,f),f(b))$.

We require that $\mathcal{K}_{B}$ satisfies the following elimination rule. Suppose we are given a family of types $\Gamma,x:\mathcal{K}_{B}\vdash_{\widetilde{\mathcal{E}}}P(x)$ together with the terms below.

[TABLE]

Suppose further that $S$ satisfies the equalities

[TABLE]

Then we have a choice of term $\Gamma,x:\mathcal{K}_{B}\vdash s(x):P(x)$ satisfying the following computation rules for $a:A$, $f:B(a)\to\mathcal{K}_{B}$ and $b:B(a)$.

[TABLE]

Moreover the choice of term is strictly preserved by reindexing.

We use the techniques developed by Coquand, Huber and Mörtberg together with $W$-types with reductions for constructing the actual objects. In order to give $\mathcal{K}^{\Gamma}_{B}$ the structure of a fibration we need to define a composition operator. We will do this by freely adding an $\mathsf{hcomp}$ operator, and then combining it with a transport operator, which we will explicitly define.

Definition 3.5**.**

Let $\Gamma\vdash_{\mathcal{E}}X$ be a type. We define the naïve cone, $\mathsf{Cone}(X)$ to be the following pushout333Pushout in the usual categorical sense, not the homotopy pushout..

[TABLE]

We can now define $\mathcal{K}^{\Gamma}_{B}$ to be the following $W$-type with reductions.

• •

When $a:A$, $c:\mathsf{Cone}(B(a))$ and $f:B(a)\to\mathcal{K}_{B}$, we add an element $\mathsf{pastecone}(a,c,f)$ to $\mathcal{K}_{B}$.

• •

If $a,c,f$ are as above and $c$ is of the form $\mathsf{inr}(b,1)$ for $b:B(a)$, then $\mathsf{pastecone}(a,c,f)$ reduces to $f(b)$.

• •

When $\varphi:\mathbb{F}$ and $u:\sum_{i:\mathbb{I}}((i=0)\vee\varphi)\;\to\;\mathcal{K}_{B}$, we add an element $\mathsf{hcomp}(\varphi,u)$ to $\mathcal{K}_{B}$.

• •

If $p:\varphi$ and $u$ is as above then $\mathsf{hcomp}(\varphi,u)$ reduces to $u(1,p)$.

To check that this really is a $W$-type with reductions, we need to define the polynomial with reductions. We take it to be the coproduct of the following two polynomials with reductions.

We define the first component of the coproduct as follows. We take the constructors $Y$ to be $\sum_{a:A}\mathsf{Cone}(B(a))$ and the arities $X(a,c)$ to be $B(a)$. We take the reductions $R(a,\mathsf{inl}(\ast))$ to be $\bot$ and $R(a,\mathsf{inr}(b,i))$ to be $(i=1)$ together with the map $R(a,\mathsf{inr}(b,i))\vdash b:B(a)$. Note that $R:\left(\sum_{a:A}\mathsf{Cone}(B(a))\right)\to\mathbb{F}$ is well-defined because we have $(0=1)=\bot$ by propositional extensionality.

The second component in the coproduct is the polynomial with reductions that we used for local fibrant replacement.

Lemma 3.6**.**

We construct a transport operator for $\mathcal{K}^{\Gamma}_{B}$, in the sense defined in [CHM18, Definition 2.3].

Proof.

Suppose we are given $\varphi:\mathbb{F}$ and a path $\gamma$ in $\Gamma$ which is constant on $\varphi$. We need to define a transport operator, which is a map $t:\mathcal{K}_{B(\gamma(0))}\to\mathcal{K}_{B(\gamma(1))}$ such that $t$ is the identity when $\varphi$ is true. Formally this map can be defined by giving an appropriate algebra structure on $\mathcal{K}_{B(\gamma(1))}$ and then using the initiality of $\mathcal{K}_{B(\gamma(0))}$. However, for clarity we will present the proof as an argument by higher recursion on the definition of $\mathcal{K}_{B(\gamma(0))}$.

We need to show how to define $t(\mathsf{pastecone}(a,c,f))$ and $t(\mathsf{hcomp}(\psi,u))$, and then check that the definition respects the reduction equations. For the latter we define the transport operator so that it preserves the $\mathsf{hcomp}$ structure, which determines it uniquely, following [CHM18]. For the former, we recall that $\mathsf{Cone}(B(a))$ was defined as a pushout, and so we can split into a further two cases. Either $c$ is of the form $\mathsf{inl}(\ast)$, or it is of the form $\mathsf{inr}(b,i)$ where $b:B(a)$ and $i:\mathbb{I}$. Now in addition to the reduction equation, we have to also satisfy $t(\mathsf{inl}(\ast))=t(\mathsf{inr}(b,0))$ in order to eliminate out of the pushout.

Write $t_{A}$ for the transport $A(\gamma(0))\to A(\gamma(1))$ and $t_{B}$ for the transport $\prod_{a:A(\Gamma(0))}B(a)\to B(t_{A}(a))$ ensuring that $t_{A}(a)=a$ and $t_{B}(b)=b$ when $\varphi=\top$, for all $a:A(\gamma(0))$ and $b:B(a)$. Write $t_{B}^{-1}$ for the homotopy inverse $\prod_{a:A(\Gamma(0))}B(t_{A}(a))\to B(a)$, again ensuring that $t_{B}^{-1}(b)=b$ when $\varphi=\top$. Since we are only guaranteed the existence of a homotopy inverse, not a strict inverse, we don’t necessarily have $t_{B}^{-1}\circ t_{B}=1_{B(a)}$. We can however construct paths $p:\prod_{a:A(\Gamma(0))}\prod_{b:B(a)}\mathbb{I}\to B(a)$ satisfying for all $a:A(\Gamma(0))$ and $b:B(a)$ that $p(a,b,0)=t_{B}^{-1}(t_{B}(b))$ and $p(a,b,1)=b$. Furthermore, we may assume that for any $a,b$ and $i$, if $\varphi=\top$ then $p(a,b,i)=b$.

We define $t(\mathsf{pastecone}(a,\mathsf{inl}(\ast),f))$ to be of the form $\mathsf{pastecone}(t_{A}(a),\mathsf{inl}(\ast),f^{\prime})$, where we still need to define a function $f^{\prime}:B(t_{A}(a))\to\mathcal{K}_{B(\gamma(1))}$. Note that we may assume by recursion that for each $b:B(a)$, $t(f(b))$ has already been defined and belongs to $\mathcal{K}_{B(\gamma(1))}$. Hence we can simply define $f^{\prime}$ to be $t\circ f\circ t_{B}^{-1}$.

The obvious first attempt at defining $t(\mathsf{pastecone}(a,\mathsf{inr}(b,i),f))$, would be $\mathsf{pastecone}(t_{A}(a),\mathsf{inr}(t_{B}(b),i),t\circ f\circ t_{B}^{-1})$. Note however that this does not satisfy the reduction equations. This is because when $i=1$, $\mathsf{pastecone}(a,\mathsf{inr}(b,i),f)$ reduces to $f(b)$ and $\mathsf{pastecone}(t_{A}(a),\mathsf{inr}(t_{B}(b),i),t\circ f\circ t_{B}^{-1})$ reduces to $t(f(t_{B}^{-1}(t_{B}(b))))$ which is not necessarily strictly equal to $t(f(b))$. We fix this using the $\mathsf{hcomp}$ constructor, following the construction of homotopy pushouts in [CHM18, Section 2.3]. We define $\psi:\mathbb{F}$ to be $\varphi\vee(i=0)\vee(i=1)$. We then define $u:\sum_{j:\mathbb{I}}(\psi\vee(j=0))\to\mathcal{K}_{B(\gamma(a))}$ as follows.

[TABLE]

We then define $t(\mathsf{pastecone}(a,\mathsf{inr}(b,i),f))$ to be $\mathsf{hcomp}(\psi,0,u)$. The reduction equation for $\mathsf{hcomp}$ then ensures that we do satisfy the reduction equation for $\mathsf{pastecone}$ and also retain the necessary equations for the pushout and furthermore ensures that the resulting map $t:\mathcal{K}_{B(\gamma(0))}\to\mathcal{K}_{B(\gamma(1))}$ is a transport operator. ∎

Theorem 3.7**.**

We construct a fibration structure for each $\mathcal{K}_{B}$, which is strictly preserved by reindexing.

Proof.

By lemma 3.6 and [CHM18, Lemma 2.5]. ∎

Lemma 3.8**.**

We construct terms $\mathsf{ext}$ and $\mathsf{isext}$ for $\mathcal{K}_{B}$ that satisfy the appropriate equations.

Proof.

[TABLE]

∎

Lemma 3.9**.**

$\mathcal{K}_{B}$* satisfies the necessary induction principle.*

Proof.

Suppose we are given a family of types $\Gamma,x:\mathcal{K}_{B}\vdash_{\widetilde{\mathcal{E}}}P(x)$ together with the terms below.

[TABLE]

We need to define a term $\Gamma,x:\mathcal{K}_{B}\vdash s(x):P(x)$ satisfying the appropriate equalities. We define $s$ by higher recursion on the construction of $\mathcal{K}_{B}$. We first deal with the case $s(\mathsf{pastecone}(a,c,f))$. Recalling that $\mathsf{Cone}(B(a))$ is defined as a pushout, we can split into the two cases $c=\mathsf{inl}(\ast)$ and $c=\mathsf{inr}(b,i)$ for some $b:B(a)$ and $i:\mathbb{I}$.

We define

[TABLE]

It is straightforward to check that this does preserve the reduction and pushout equations and so does give a well defined map. One can show it is a section again by higher recursion and the computation rules are satisfied by definition.

Finally, to define $s(\mathsf{hcomp}(\varphi,u))$ we use the fibration structure on $\Gamma,x:\mathcal{K}_{B}\vdash_{\mathcal{E}}P(x)$. ∎

3.2 Internal Cubical Models

Let $\mathcal{S}$ be a model of dependent type theory with dependent product types, dependent sum types, extensional identity types, unit type, finite colimits, $W$-types and a countable chain of universes. We also assume that every context of $\mathcal{S}$ is isomorphic to $1.X$ for some type $1\vdash_{\mathcal{S}}X$. In particular, the category $\mathbb{C}^{\mathcal{S}}$ is finitely complete so that internal categories in $\mathbb{C}^{\mathcal{S}}$ make sense. Let $\Box$ denote the internal category in $\mathbb{C}^{\mathcal{S}}$ in which the objects are the natural numbers and the morphisms from $n$ to $m$ are the order-preserving functions $\mathbf{2}^{n}\to\mathbf{2}^{m}$. Note that $\mathcal{S}$ has a natural number object since it has $W$-types. We will refer to internal presheaves over $\Box$ as internal cubical objects.

Theorem 3.10**.**

Under those assumptions, the category of internal cubical objects in $\mathcal{S}$ is part of a model of type theory that satisfies Assumption 3.1.

Example 3.11*.*

Let $\mathcal{A}$ be a partial combinatory algebra. It is well-known that the category $\mathbf{Asm}(\mathcal{A})$ of assemblies on $\mathcal{A}$ is part of a model of type theory with dependent product types, dependent sum types, extensional identity types, unit type, finite colimits. It is also known that $\mathbf{Asm}(\mathcal{A})$ has $W$-types (an explicit construction is found in [vdB06, Section 2.2]). Assuming a countable chain of Grothendieck universes in the set theory, $\mathbf{Asm}(\mathcal{A})$ has a countable chain of universes. Thus the category $\mathbf{CAsm}(\mathcal{A})$ of internal cubical objects in $\mathbf{Asm}(\mathcal{A})$ is part of a model of type theory that satisfies Assumption 3.1.

It is shown in [OP18] that, when $\mathcal{S}=\mathbf{Set}$, the category of presheaves over $\Box$ satisfies all the axioms of Orton and Pitts if we take $\mathbb{F}$ to be the presheaf of locally decidable propositions. The proof works for an arbitrary $\mathcal{S}$ and one can show that the category of internal cubical objects in $\mathcal{S}$ is part of a model of type theory satisfying Assumption 3.1 except the existence of cofibrant $W$-types with reductions (see also [Uem18]). To construct cofibrant $W$-types with reductions, we recall the following from [Swa18].

Theorem 3.12**.**

Let $\mathcal{E}$ be a locally cartesian closed category with finite colimits and disjoint coproducts and $W$-types, and let $\mathbf{C}$ be an internal category in $\mathcal{E}$. Then the category $\mathcal{P}(\mathbf{C})$ of internal presheaves over $\mathbf{C}$ has all locally decidable $W$-types with reductions.

We furthermore observe that one can show that this construction is stable under pullback up to isomorphism using a technique similar to the one used by Gambino and Hyland for ordinary $W$-types. The reason is that pointed polynomial endofunctors are stable under pullback because they are constructed from $\Sigma$ types, $\Pi$ types and pushouts, all of which are preserved by pullback, and in locally cartesian closed categories the initial algebras of such pointed endofunctors are also stable under pullback. However, to ensure that the construction is strictly preserved requires a little more work.

We show how to use the non split version above to construct split $W$-types with reductions. The essential idea is to carry out the construction given above “pointwise,” expanding out the method suggested by Coquand, Huber and Mörtberg in [CHM18, Section 2.2]. Since we define cubical sets here as a category of presheaves in the usual, contravariant sense, we work with contravariant presheaves here, although the original proof in [Swa18] is phrased in terms of covariant presheaves. We also make minor adjustments to fit with the “split” version appearing in section 2.2.

Suppose that we are given a context $\Gamma\in\mathcal{P}(\mathbf{C})$ together with a type $Y\in\mathcal{P}(\int_{\mathbf{C}}\Gamma)$, a type $X\in\mathcal{P}(\int_{C}\{Y\})$, a locally decidable monomorphism $R\rightarrowtail Y$ and a map $k:\prod_{y:R}X(y)$ over $\int_{\mathbf{C}}\Gamma$.

We need to show how to define a strict version of the $W$-type with reductions $W(Y,X,R)$. We will refer to the new strict version as $W^{\prime}(Y,X,R)$. This should be an element of $\mathcal{P}(\int_{\mathbf{C}}\Gamma)$, so in particular we need to define a family of types $W^{\prime}(Y,X,R)(c,\gamma)$ indexed by objects $c$ of $\mathbf{C}$ and elements $\gamma:\Gamma(c)$.

We fix such a $c$ and $\gamma$. We first note that we have a a locally decidable polynomial with reductions $Y_{\gamma},X_{\gamma},R_{\gamma}$ in the internal presheaf category $\mathcal{P}(\int_{\mathbf{C}}\mathbf{C}(-,c))$ given by reindexing along the map $\mathbf{C}(-,c)\to\Gamma$ given by Yoneda. We then carry out the “non strict” construction to get a presheaf $W(Y_{\gamma},X_{\gamma},R_{\gamma})$ on $\int_{\mathbf{C}}\mathbf{C}(-,c)$ and finally we define $W^{\prime}(Y,X,R)(c,\gamma)$ to be $W(Y_{\gamma},X_{\gamma},R_{\gamma})(c,1_{c})$.

For completeness, we unfold the definitions to obtain the following explicit description of $W^{\prime}(Y,X,R)(c,\gamma)$. We first define the dependent $W$-type $N_{0}$ of normal forms indexed by the objects $(d,f)$ of $\int_{\mathbf{C}}\mathbf{C}(-,c)$.

If $(d,f)$ is an object of $\int_{\mathbf{C}}\mathbf{C}(-,c)$ we add an element to $N_{0}(d,f)$ of the form $\sup(y,\alpha)$ whenever $y$ is an element of $Y(d,\Gamma(f)(\gamma))$ that does not belong to the subobject $R(d,\Gamma(f)(\gamma))$ and $\alpha$ is an element of the following type.

[TABLE]

The next step is to define maps $N_{0}(d,f)\to N_{0}(e,f\circ g)$ whenever $g\colon e\to d$ and $f\colon d\to c$ in $\mathbf{C}$. Say that we are given an element of $N_{0}(d,f)$ of the form $\sup(y,\alpha)$. We recall that $N_{0}(g)(\sup(y,\alpha))$ is defined by splitting into cases depending on whether or not $y$ belongs to the subobject $R(d,\Gamma(f)(\gamma))$. If it does, we define $N_{0}(g)(\sup(y,\alpha))$ to be $\alpha(g,k(y))$. Otherwise, we define $N_{0}(g)(\sup(y,\alpha))$ to be $\sup(Y(g)(y),\alpha^{\prime})$ where $\alpha^{\prime}(h,x)$ is defined to be $\alpha(g\circ h,x)$.

We then define $N(d,f)$ for each $f:d\to c$ to be the subobject of $N_{0}(d,f)$ consisting of hereditarily natural elements and verify that this does indeed define a presheaf on $\int_{\mathbf{C}}\mathbf{C}(-,c)$. But this is identical to [Swa18, Section 4] so we omit the details.

If we then define $W^{\prime}(Y,X,R)(c,\gamma)$ to be $N(c,1_{c})$, then this is strictly stable under reindexing by definition.

One can construct by recursion an isomorphism between $N(d,f)$ and $W(Y,X,R)(d,\Gamma(f)(\gamma))$ for each $f:d\to c$. In particular this gives us an isomorphism between $N(c,1_{c})$ and $W(Y,X,R)(c,\gamma)$, and so we have a canonical isomorphism between $W^{\prime}(Y,X,R)(c,\gamma)$ and $W(Y,X,R)(c,\gamma)$. It follows that we can assign an initial algebra structure to $W^{\prime}(Y,X,R)(c,\gamma)$ by transferring the algebra structure on $W(Y,X,R)(c,\gamma)$ via the isomorphism.

3.3 Discrete Types

We introduce a class of types in an Orton-Pitts model for future use. Let $\mathcal{E}$ be a model of type theory satisfying Assumption 3.1.

Definition 3.13**.**

A type $1\vdash X$ is said to be discrete if the map $\lambda x.\lambda i.x:X\to X^{\mathbb{I}}$ is an isomorphism.

The proofs of the following propositions are found in [Uem18].

Proposition 3.14**.**

Every discrete type $1\vdash X$ carries a fibration structure.

Proposition 3.15**.**

If a type $1\vdash X$ has decidable equality, then it is discrete.

Corollary 3.16**.**

The natural number object in $\mathcal{E}$ is discrete.

4 Church’s Thesis

We consider a dependent type theory with dependent product types, dependent sum types, identity types, unit type, disjoint finite coproducts, propositional truncation and natural numbers. In such a dependent type theory, one can define Kleene’s computation predicate $T(e,x,z)$ and result extraction function $U(z)$ as primitive recursive functions $T:\mathbb{N}\times\mathbb{N}\times\mathbb{N}\to\mathbf{2}$ and $U:\mathbb{N}\to\mathbb{N}$. The statement $T(e,x,z)$ means that $z$ codes a computation on Turing machine $e$ with input $x$ and $U(z)$ is the output of the computation. Church’s Thesis is the following axiom.

[TABLE]

Since the type $\sum_{z:\mathbb{N}}T(e,x,z)\times U(z)=f(x)$ is a proposition, Church’s Thesis is equivalent to the type

[TABLE]

4.1 Failure of Church’s Thesis in Internal Cubical Models

Let $\mathcal{S}$ be a model of type theory as in Section 3.2. We have seen that the category $\mathcal{P}(\Box)$ of internal cubical objects in $\mathcal{S}$ is part of a model of type theory satisfying Assumption 3.1. In this section we show the following theorem.

Theorem 4.1**.**

The negation of Church’s Thesis holds in the model of univalent type theory $\widetilde{\mathcal{P}(\Box)}$.

To prove Theorem 4.1, we recall from [Uem18] the notion of a codiscrete presheaf. The constant presheaf functor $\Delta:\mathcal{S}\to\mathcal{P}(\Box)$ extends to a morphism of cwf’s and preserves (at least up to isomorphism) several type constructors. Here we only need the following.

Proposition 4.2**.**

The morphism $\Delta:\mathcal{S}\to\mathcal{P}(\Box)$ of cwf’s preserves dependent product types, dependent sum types, extensional identity types and natural number objects.

A constant presheaf $\Delta X$ is regarded as a type in $\widetilde{\mathcal{P}(\Box)}$ by the following proposition and Proposition 3.14.

Proposition 4.3**.**

Constant presheaves are discrete.

For types $1\vdash_{\mathcal{S}}X$ and $x:X\vdash_{\mathcal{S}}Y(x)$, one can define a type $x:\Delta X\vdash_{\mathcal{P}(\Box)}\nabla_{X}Y(x)$ called the codiscrete presheaf which has the following properties.

Proposition 4.4**.**

$\nabla_{X}$* is the right adjoint to the evaluation functor $(-)_{0}$ at $0\in\Box$: for any type $x:\Delta X\vdash_{\mathcal{P}(\Box)}Z(x)$, we have a natural bijection between the set of elements $x:\Delta X,z:Z(x)\vdash_{\mathcal{P}(\Box)}b:\nabla_{X}Y(x)$ and the set of elements $x:X,z:Z_{0}(x)\vdash_{\mathcal{S}}b:Y(x)$. Note that $(\Delta X)_{0}=X$ and thus $Z_{0}$ is a type in $\mathcal{S}$ over $X$.*

Proposition 4.5**.**

For a type $x:X\vdash_{\mathcal{S}}Y(x)$, the type $x:\Delta X\vdash_{\mathcal{P}(\Box)}\nabla_{X}Y(x)$ has a composition structure and is a proposition in $\widetilde{\mathcal{P}(\Box)}$.

Proof of Theorem 4.1.

We define types $f:\mathbb{N}\to\mathbb{N}\vdash C^{\prime}(f):\equiv\sum_{e:\mathbb{N}}\prod_{x:\mathbb{N}}\sum_{z:\mathbb{N}}T(e,x,z)\times U(x)=f(x)$ and $f:\mathbb{N}\to\mathbb{N}\vdash C(f):\equiv\left\|C^{\prime}(f)\right\|$. Let $N$ denote the natural number object in $\mathcal{S}$. Then Church’s Thesis is interpreted in $\widetilde{\mathcal{P}(\Box)}$ as $\prod_{f:\Delta(N\to N)}[\![C]\!]^{\widetilde{\mathcal{P}(\Box)}}(f)$ by Proposition 4.2. We will construct two functions in $\widetilde{\mathcal{P}(\Box)}$:

• •

$\prod_{f:\Delta(N\to N)}[\![C]\!]^{\widetilde{\mathcal{P}(\Box)}}(f)\to\nabla_{N\to N}[\![C^{\prime}]\!]^{\mathcal{S}}(f)$;

• •

$\left(\prod_{f:\Delta(N\to N)}\nabla_{N\to N}[\![C^{\prime}]\!]^{\mathcal{S}}(f)\right)\to\mathbf{0}$.

Then we readily get a function $\left(\prod_{f:\Delta(N\to N)}[\![C]\!]^{\widetilde{\mathcal{P}(\Box)}}(f)\right)\to\mathbf{0}$.

For the former one it suffices to give a function $[\![C^{\prime}]\!]^{\widetilde{\mathcal{P}(\Box)}}(f)\to\nabla_{N\to N}[\![C^{\prime}]\!]^{\mathcal{S}}(f)$ for all $f:\Delta(N\to N)$ by the recursion principle of the propositional truncation because the codomain is a proposition by Proposition 4.5. By the adjunction $(-)_{0}\dashv\nabla_{N\to N}$ it suffices to give a function $[\![C^{\prime}]\!]^{\widetilde{\mathcal{P}(\Box)}}_{0}\to[\![C^{\prime}]\!]^{\mathcal{S}}$ but we have an isomorphism $[\![C^{\prime}]\!]^{\widetilde{\mathcal{P}(\Box)}}\cong(\Delta[\![C^{\prime}]\!]^{\mathcal{S}})_{0}=[\![C^{\prime}]\!]^{\mathcal{S}}$ by Proposition 4.2.

For the latter function, observe that $\prod_{f:\Delta(N\to N)}\nabla_{N\to N}[\![C^{\prime}]\!]^{\mathcal{S}}(f)\cong\nabla_{1}\left(\prod_{f:N\to N}[\![C^{\prime}]\!]^{\mathcal{S}}(f)\right)$ and that $\nabla_{1}\mathbf{0}\cong\mathbf{0}$. Then we apply $\nabla_{1}$ to the function $\left(\prod_{f:N\to N}[\![C^{\prime}]\!]^{\mathcal{S}}(f)\right)\to\mathbf{0}$ in $\mathcal{S}$ obtained from the inconsistency of Church’s Thesis with the axiom of choice and function extensionality. ∎

5 Null Types

Let $\mathcal{E}$ be a model of univalent type theory. Based on Rijke, Shulman and Spitters’ null types [RSS17] we define a notion of null structure as follows.

Let $a:A\vdash B(a)$ be a proposition in $\mathcal{E}$. For a type $\Gamma\vdash X$ in $\mathcal{E}$, we define a proposition $\Gamma\vdash\mathsf{isNull}_{B}(X)$ as

[TABLE]

and call a term of $\mathsf{isNull}_{B}(X)$ a $B$-null structure on $X$. A $B$-null type is a type $\Gamma\vdash X$ equipped with a $B$-null structure $n$ on $X$. That is, a $B$-null type has a witness that the canonical map $X\to X^{B(a)}$ is an equivalence for each $a$.

Definition 5.1**.**

We define a cwf $\mathcal{E}_{B}$ as follows:

• •

the contexts are those of $\mathcal{E}$;

• •

the types are the $B$-null types in $\mathcal{E}$;

• •

the elements of $\Gamma\vdash_{\mathcal{E}_{B}}X$ are those of the underlying type $X$ in $\mathcal{E}$.

We have the obvious forgetful morphism $\mathcal{E}_{B}\to\mathcal{E}$ of cwf’s.

For a proposition $a:A\vdash B(a)$, a nullification operator assigns

• •

each type $\Gamma\vdash X$ a $B$-null type $\Gamma\vdash\mathcal{L}_{B}X$ and an element $\Gamma\vdash\eta_{X}:X\to\mathcal{L}_{B}X$; and

• •

each pair of type $\Gamma\vdash X$ and $B$-null type $\Gamma\vdash Y$ an element $\Gamma\vdash e:\mathsf{isEquiv}(\lambda(f:\mathcal{L}_{B}X\to Y).f\circ\eta_{X}$.

We also require that a nullification operator is preserved by reindexing.

We review some properties of null types. See [RSS17] for further details.

Proposition 5.2**.**

Let $\Gamma\vdash X$ and $\Gamma,x:X\vdash Y(x)$ be types in $\mathcal{E}$.

• •

There exists a term of type $\Gamma\vdash(\prod_{x:X}\mathsf{isNull}_{B}(Y(x)))\to\mathsf{isNull}_{B}(\prod_{x:X}Y(x))$.

• •

There exists a term of type $\Gamma\vdash\mathsf{isNull}_{B}(X)\to(\prod_{x:X}\mathsf{isNull}_{B}(Y(x)))\to\mathsf{isNull}_{B}(\sum_{x:X}Y(x))$.

• •

There exists a term of type $\Gamma\vdash\mathsf{isNull}_{B}(X)\to\prod_{x_{0},x_{1}:X}\mathsf{isNull}_{B}(\mathsf{Id}_{X}(x_{0},x_{1}))$.

Consequently, $\mathcal{E}_{B}$ supports dependent product, dependent sum and intensional identity types preserved by the morphism $\mathcal{E}_{B}\to\mathcal{E}$.

For a universe $U$ we define a subuniverse $U_{B}$ of $U$ as

[TABLE]

Proposition 5.3**.**

The universe $U_{B}$ has a $B$-null structure.

Proof.

Our condition that each $B(a)$ is a proposition corresponds to Rijke, Shulman and Spitters’ notion of topological modality. They prove in [RSS17, Corollary 3.11 and Theorem 3.12] that for any such modality the universe of modal types is itself modal. ∎

Proposition 5.4**.**

If a nullification operator $\mathcal{L}_{B}$ exists, then it preserves propositions.

Proof.

This is true for any modality by [RSS17, Lemma 1.28]. ∎

Corollary 5.5**.**

Suppose that $\mathcal{E}$ has a nullification operator $\mathcal{L}_{B}$. Then $a:A\vdash\mathcal{L}_{B}B(a)$ is contractible.

Proof.

Since $\mathcal{L}_{B}B(a)$ is a proposition, it suffices to find an element of $\prod_{a:A}\mathcal{L}_{B}B(a)$. Assume that $a:A$ is given. Since $\mathcal{L}_{B}B(a)$ is $B$-null, it is enough to give a function $B(a)\to\mathcal{L}_{B}B(a)$, so take the constructor $\eta_{B(a)}:B(a)\to\mathcal{L}_{B}B(a)$. ∎

Corollary 5.6**.**

Suppose that $\mathcal{E}$ has a nullification operator $\mathcal{L}_{B}$. Then $X\mapsto\mathcal{L}_{B}\left\|X\right\|$ gives propositional truncation in the model $\mathcal{E}_{B}$.

Proof.

By Proposition 5.4, $\mathcal{L}_{B}\left\|X\right\|$ is a proposition. For any $B$-null proposition $Z$, we have equivalences

[TABLE]

∎

5.1 Null Types in Orton-Pitts Models

Let $\widetilde{\mathcal{E}}$ be an Orton-Pitts model.

Definition 5.7**.**

A type $a:A\vdash B(a)$ in $\mathcal{E}$ or $\widetilde{\mathcal{E}}$ is said to be well-supported if the propositional truncation $a:A\vdash_{\mathcal{E}}\left\|B(a)\right\|$ taken in the model $\mathcal{E}$ of extensional dependent type theory is inhabited.

Proposition 5.8**.**

Let $1\vdash_{\mathcal{E}}X$ be a type and $a:A\vdash_{\widetilde{\mathcal{E}}}B(a)$ a proposition. If $X$ is discrete and $B$ is well-supported, then $X$ has a $B$-null structure.

Proof.

We show that, for any $a:A$, the function $k_{a}:\equiv\lambda x.\lambda b.x:X\to(B(a)\to X)$ is an isomorphism in the internal language of $\mathcal{E}$. Since $B$ is well-supported, $k_{a}$ is injective. To prove surjectivity we assume that $f:B(a)\to X$ is given. By the well-supportedness of $B$ there exists some element $b:B(a)$. We show that $f=k_{a}(f(b))$. Assume $b^{\prime}:B(a)$ is given. Since $B$ is a proposition in $\widetilde{E}$ we have a path $p:\mathbb{I}\to B(a)$ such that $p0=b^{\prime}$ and $p1=b$. By the discreteness of $X$ the path $f\circ p:\mathbb{I}\to X$ is constant, which implies that $f(b^{\prime})=f(b)$. Hence we have $f=k_{a}(f(b))$ by function extensionality. ∎

We easily deduce the following corollaries.

Corollary 5.9**.**

If $B$ is well-supported, then $\mathbf{0}$ has a $B$-null structure.

Corollary 5.10**.**

If $B$ is well-supported, then $\mathbb{N}$ has a $B$-null structure.

Proposition 5.11**.**

Let $a:A\vdash_{\widetilde{\mathcal{E}}}B(a)$ be a proposition and $\Gamma\vdash_{\widetilde{\mathcal{E}}}X$ and $\Gamma\vdash_{\widetilde{\mathcal{E}}}Y$ types. Then there exists a term of type

[TABLE]

Proof.

We proceed in the internal language of $\mathcal{E}$. Suppose that $X$ and $Y$ has a $B$-null structure. Assume that $a:A$ is given. Since the function $(X+Y)\to(B(a)\to(X+Y))$ factors as

[TABLE]

it suffices to show that the function $\Phi:((B(a)\to X)+(B(a)\to Y))\to(B(a)\to(X+Y))$ is an isomorphism. The injectivity of $\Phi$ follows from the well-supportedness of $B$. To prove the surjectivity we assume that $f:B(a)\to(X+Y)$ is given. We show that $(\forall_{b:B(a)}fb\in X)\lor(\forall_{b:B(a)}fb\in Y)$. Since $B$ is well-supported, there exists some element $b_{0}:B(a)$. We know that $fb_{0}\in X\lor fb_{0}\in Y$. Suppose that $fb_{0}\in X$. Assume $b:B(a)$ is given. Since $B$ is a proposition in $\widetilde{\mathcal{E}}$, we have a path $p:\mathbb{I}\to B(a)$ such that $p0=b_{0}$ and $p1=b$. Since the exponential functor $(-)^{\mathbb{I}}$ preserves colimits because it has a right adjoint, we have $(\forall_{i:\mathbb{I}}f(pi)\in X)\lor(\forall_{i:\mathbb{I}}f(pi)\in Y)$. Now $f(p0)\in X$ and thus we have $\forall_{i:\mathbb{I}}f(pi)\in X$. In particular, $fb\in X$. In a similar manner, we have $\forall_{b:B(a)}fb\in Y$ assuming $fb_{0}\in Y$. Hence we get $(\forall_{b:B(a)}fb\in X)\lor(\forall_{b:B(a)}fb\in Y)$. ∎

By Corollary 3.16, Propositions 5.2, 5.8 and 5.11, for any type $X$ defined in dependent type theory only using dependent product types, dependent sum types, identity types, unit type, disjoint finite coproducts and natural numbers, the interpretation $[\![X]\!]^{\widetilde{\mathcal{E}}}$ has a $B$-null structure for any well-supported proposition $B$ in $\widetilde{\mathcal{E}}$. In particular, if $[\![X]\!]^{\widetilde{\mathcal{E}}}$ is inhabited, then so is $[\![X]\!]^{\widetilde{\mathcal{E}}_{B}}$ for any well-supported proposition $B$ in $\widetilde{\mathcal{E}}$.

Example 5.12*.*

Markov’s Principle is the following axiom.

[TABLE]

It is equivalent to the type

[TABLE]

For a decidable predicate $\alpha:\mathbb{N}\to\mathbf{2}$, the proposition $\left\|\sum_{n:\mathbb{N}}\alpha(n)\right\|$ is equivalent to the type $\sum_{n:\mathbb{N}}\alpha(n)\times\prod_{k:\mathbb{N}}\alpha(k)\to n\leq k$ which is defined without propositional truncation. Hence, if the model $\mathcal{E}$ of extensional dependent type theory satisfies Markov’s Principle, then so does the model $\widetilde{\mathcal{E}}_{B}$ of univalent type theory for any well-supported proposition $B$ in $\widetilde{\mathcal{E}}$.

We now show how to define nullification operators in Orton-Pitts models. Following Rijke, Shulman and Spitters in [RSS17, Section 2.2] we will first define an operator $\mathcal{J}_{B}$, although we will only consider the case of nullification, since that is all we need here.

Lemma 5.13**.**

For types $a:A\vdash_{\widetilde{\mathcal{E}}}B(a)$ and $\Gamma\vdash_{\widetilde{\mathcal{E}}}X$, we have the higher inductive $\mathcal{J}_{B}(X)$ defined as follows.

• •

When $x:X$, then $\mathcal{J}_{B}(X)$ contains an element $\alpha^{B}_{X}(x)$.

• •

When $a:A$ and $f:B(a)\to\mathcal{K}_{B}$, then $\mathcal{J}_{B}(X)$ contains an element $\mathsf{ext}(a,f)$.

• •

When $a:A$, $f:B(a)\to\mathcal{K}_{B}$ and $b:B(a)$ then $\mathsf{Id}(\mathsf{ext}(a,f),f(b))$ contains an element $\mathsf{isext}(a,f,b)$.

Proof.

$\mathcal{J}_{B}(X)$ differs from $\mathcal{K}_{B}$ by having an extra point constructor $\alpha^{B}_{X}:X\to\mathcal{J}_{B}(X)$.

We define $A^{\prime}$ to be the type $A+X$ and define the family of types $a:A^{\prime}\vdash B^{\prime}(a)$ as follows.

[TABLE]

We can then take $\mathcal{J}_{B}(X)$ to be $\mathcal{K}_{B^{\prime}}$, as defined in section 3.1. We take $\alpha^{B}_{X}(x)$ to be $\mathsf{ext}(\mathsf{inr}(x),\bot_{\mathcal{K}_{B}})$ where $\bot_{\mathcal{K}_{B}}$ is the unique map from [math] to $\mathcal{K}_{B}$. ∎

Theorem 5.14**.**

$\widetilde{\mathcal{E}}$* has a nullification operator $\mathcal{L}_{B}$ for every type $a:A\vdash_{\widetilde{\mathcal{E}}}B(a)$.*

Proof.

This follows from [RSS17, Theorem 2.16], observing that for the case of nullification the pushout appearing there is just a suspension, which we have already shown how to implement in theorem 3.3, and we showed in lemma 5.13 how to implement their $\mathcal{J}$ operator. ∎

6 Church’s Thesis in Null Types

Consider a dependent type theory with dependent product types, dependent sum types, identity types, unit type, disjoint finite coproducts, propositional truncation and natural numbers. Let $a:A\vdash B(a)$ be a type in this type theory where $A$ and $B$ are definable only using dependent product types, dependent sum types, identity type of $\mathbf{2}$, unit type, finite coproducts and natural numbers. We define $a:A\vdash C(a):=\left\|B(a)\right\|$. For an Orton-Pitts model $\widetilde{\mathcal{E}}$, the underlying types of the interpretations $[\![A]\!]^{\widetilde{\mathcal{E}}}$ and $[\![B]\!]^{\widetilde{\mathcal{E}}}$ are $[\![A]\!]^{\mathcal{E}}$ and $[\![B]\!]^{\mathcal{E}}$ respectively.

Theorem 6.1**.**

Let $\widetilde{\mathcal{E}}$ be an Orton-Pitts model. Suppose that $[\![B]\!]^{\widetilde{\mathcal{E}}}$ is well-supported. Then the proposition $C$ holds in the model of univalent type theory $\widetilde{\mathcal{E}}_{[\![C]\!]^{\widetilde{\mathcal{E}}}}$.

Proof.

Let $D=[\![C]\!]^{\widetilde{\mathcal{E}}}$. By assumption $[\![B]\!]^{\widetilde{\mathcal{E}}}$ is well-supported and so is its truncation $D$. By Corollary 3.16 and Propositions 5.2, 5.8 and 5.11, $[\![A]\!]^{\widetilde{\mathcal{E}}}$ and $[\![B]\!]^{\widetilde{\mathcal{E}}}$ have $D$-null structures. Hence we have $[\![C]\!]^{\widetilde{\mathcal{E}}_{D}}=\mathcal{L}_{D}[\![C]\!]^{\widetilde{\mathcal{E}}}$ by Corollary 5.6, and this type is inhabited by Corollary 5.5. ∎

Corollary 6.2**.**

Let $\mathcal{S}$ be a model of type theory as in Section 3.2. If the proposition $C$ holds in $\mathcal{S}$, then $C$ also holds in the model of univalent type theory $\widetilde{\mathcal{E}}_{[\![C]\!]^{\widetilde{\mathcal{E}}}}$ where $\mathcal{E}=\mathcal{P}(\Box)$.

Proof.

Since $C=\left\|B\right\|$ holds in $\mathcal{S}$, the type $[\![B]\!]^{\mathcal{S}}$ is well-supported. Then $[\![B]\!]^{\widetilde{\mathcal{E}}}=[\![B]\!]^{\mathcal{E}}$ is also well-supported because the constant presheaf functor $\mathcal{S}\to\mathcal{E}$ preserves all structures of the type theory. Then use Theorem 6.1. ∎

Example 6.3*.*

Recall that Church’s Thesis is equivalent to the type

[TABLE]

Also note that the equality of natural numbers is decidable, and thus there exists a function $=_{\mathbb{N}}:\mathbb{N}\to\mathbb{N}\to\mathbf{2}$ such that the type $U(z)=f(x)$ is equivalent to $(U(z)=_{\mathbb{N}}f(x))=1$. Therefore Church’s Thesis is equivalent to a type of the form

[TABLE]

with a type $a:A\vdash B(a)$ definable only using dependent product types, dependent sum types, identity of $\mathbf{2}$, unit type, finite coproducts and natural numbers. Since Church’s Thesis holds in the category $\mathbf{Asm}(\mathcal{K}_{1})$ of assemblies on Kleene’s first model $\mathcal{K}_{1}$, by Corollary 6.2 the model of univalent type theory $\widetilde{\mathcal{E}}_{[\![C]\!]^{\widetilde{\mathcal{E}}}}$ satisfies Church’s Thesis where $\mathcal{E}=\mathbf{CAsm}(\mathcal{K}_{1})$.

We can now prove our second main result, which informally says that univalent type theory is consistent with the main principles of Recursive Constructive Mathematics.

Theorem 6.4**.**

Martin-Löf type theory remains consistent when all of the following extra structure and axioms are added.

Propositional truncation. 2. 2.

The axiom of univalence. 3. 3.

Church’s Thesis. 4. 4.

Markov’s Principle.

Proof.

We prove consistency by constructing a model where all of the above holds and where there is no element of type $\bot$. Consider the Orton-Pitts model $\widetilde{\mathcal{E}}$ with $\mathcal{E}=\mathbf{CAsm}(\mathcal{K}_{1})$. We have seen that $\widetilde{\mathcal{E}}$ satisfies Church’s Thesis in Example 6.3. It remains to show that $\widetilde{\mathcal{E}}$ satisfies Markov’s Principle and $\bot$ is empty in this model.

Using well supportness again, and example 5.12 we see that to show Markov’s principle holds, it suffices to show it holds in cubical assemblies (as a model of extensional type theory). Again, we observe that the type corresponding to Markov’s principle is preserved by the constant presheaves functor, and so it suffices to show that Markov’s principle holds in assemblies, which is again a standard argument.

Using well supportness once more, and corollary 5.9 we see that $\bot$ is the same in null types as in cubical assemblies. It follows that it has no global sections, i.e. there is no element of type $\bot$ in the model. ∎

We can use Theorem 6.1 for other principles.

Example 6.5*.*

Brouwer’s Continuity Principle is the following axiom.

[TABLE]

The standard ordering $<$ on $\mathbb{N}$ is decidable, and thus Brouwer’s Continuity Principle is an instance of Theorem 6.1.

We obtain a new proof of the following result originally proved by Coquand using cubical stacks [Coq18]444Coquand’s proof can also be said to use reflective subuniverses, although in a very different way to our proof.. See also [CMR17] for an earlier stack model based on groupoids.

Theorem 6.6**.**

Martin-Löf type theory remains consistent when all of the following extra structure and axioms are added.

Propositional truncation. 2. 2.

The axiom of univalence. 3. 3.

Brouwer’s Continuity Principle.

Proof.

This is the same as for theorem 6.4. See e.g. [vO08, Proposition 3.1.6] for a proof that Brouwer’s principle holds in the the effective topos (the same proof applies for assemblies). ∎

7 Conclusion and Further Work

We have constructed a model of type theory that satisfies the main axiom of homotopy type theory (univalence) and the main axioms of recursive constructive mathematics (Church’s thesis and Markov’s principle). However, in both fields there are additional axioms that are natural to consider, but which we have left for future work.

With regards to homotopy type theory, we expect that the remaining higher inductive types appearing in [Uni13] can be implemented following the technique suggested in [RSS17, Remark 3.23] together with the technique of [CHM18] for constructing the necessary higher inductive types in cubical assemblies.

The situation with the remaining axioms of recursive constructive mathematics is more difficult. The axiom of countable choice is often included, but it is unclear whether countable choice holds in our model, or how to adjust the model to ensure countable choice does hold. The other main axiom of recursive constructive mathematics is extended Church’s thesis, which states that certain partial functions from $\mathbb{N}$ to $\mathbb{N}$ are computable. The main issue here is that it is unclear what is the most natural way to formulate partial functions in homotopy type theory. Much progress on this has been made by Escardó and Knapp in [EK17]. However, as they show, a weak form of countable choice is needed for their definition to work as expected. We expect that for any reasonable formulation of extended Church’s thesis Theorem 6.1 can be used to construct a model where it holds.

Another open problem is to find a good definition of $(\infty,1)$-effective topos, which should be to the effective topos what $(\infty,1)$-toposes are to Grothendieck toposes. In particular the effective topos should be recovered as the localisation of the hsets in the $(\infty,1)$-effective topos, and commonly seen theorems and definitions in the effective topos should be special cases of corresponding higher versions. One possible definition is cubical assemblies. We can now see another possibility in the form of reflective subuniverses of cubical assemblies. However, our definition is dependent on particular a choice of axioms that satisfy the necessary conditions to apply Theorem 6.1, so we leave open the problem of finding a “natural” definition that satisfies axioms such as Church’s thesis without needing to ensure they hold in the definition.