Cubical type theory provides a constructive justification of
homotopy type theory and satisfies canonicity: every natural number
is convertible to a numeral.  A crucial ingredient of cubical type
theory is a path lifting operation which is explained
computationally by induction on the type involving several
non-canonical choices.  In this paper we show by a sconing argument
that if we remove these equations for the path lifting operation
from the system, we still retain homotopy canonicity: every
natural number is path equal to a numeral.

§ INTRODUCTION

This paper is a contribution to the analysis of the computational content of the univalence axiom [34] (and higher inductive types).
In previous work [2, 4, 5, 6, 23], various presheaf models of this axiom have been described in a constructive meta theory.
In this formalism, the notion of fibrant type is stated as a refinement of the path lifting operation where one not only provides one of the endpoints but also a partial lift (for a suitable notion of partiality).
This generalized form of path lifting operation  is a way to state a homotopy extension property, which was recognized very early (see, [10]) as a key for an abstract development of algebraic topology.
The axiom of univalence is then captured by a suitable equivalence extension operation (the “glueing” operation), which expresses that we can extend a partially defined equivalence of a given total codomain to a total equivalence.
These presheaf models suggest possible extensions of type theory where we manipulate higher dimensional objects [2, 5].
One can define a notion of reduction and prove canonicity for this extension [16]: any closed term of type $\iN$
(natural number) is convertible to a numeral.
There are however several non-canonical choices when defining the path lifting operation
by induction on the type, which produce different notion of convertibility.
[For instance, the definition of this operation for “glue” types is different in [5] and [23].]
A natural question is how essential these non-canonical choices are: can it be that a closed
term of type $\iN$, defined without use of such non-canonical reduction rules, becomes convertible to $0$ for one choice and $1$ for another?
The main result of this paper, the homotopy canonicity theorem, implies that this cannot be the case.
the value of a term is independent of these non-canonical choices.
Homotopy canoncity states that, even without providing reduction rules for path lifting operations at type formers,
we still have that any closed term of type $\iN$ is path equal to a
(We cannot hope to have convertibility anymore with these path lifting constant.)
We can then see this numeral as the “value” of the given term.

Our proof of the homotopy canonicity can be seen as a proof-relevant extension of the reducibility or computability method, going back to the work of Gödel [14] and Tait [32].
It is however best expressed in an algebraic setting.
We first define a general notion of model, called cubical category with families, defined as a category with families [8] with certain special operations internal to presheaves over a category $\cal{C}$ (such as a cube category) with respect to the parameters of an interval $\II$ and an object of cofibrant propositions $\FF$.

We describe the term model and how to re-interpret the cubical presheaf models as cubical categories with families.
The computability method can then be expressed as a general operation (called “sconing”) which applied to an arbitrary model ${\cal M}$ produces a new model $\MM^*$ with a strict morphism $\MM^* \to \MM$.
Homotopy canonicity is obtained by applying this general operation to the initial model, which we conjecture to be the term model.
This construction associates to a (for simplicity, closed) type $A$ a predicate $A'$ on the closed terms $|A|$, and each closed term $u$ a proof $u'$ of $A' u$.
The main rules in the closed case are summarized in <ref>.

We explain next how a similar method can be used to prove canonicity when we add computation
rules of filling at type formers (using as primitive the operation of composition).
This was originally proved by [16]. The main advantage of the present
approach is that we don't need to define an auxiliary reduction relation, and that it is independent
of the exact choice of the equational presentation of cubical type theory.

Some extensions and variations are then described:

* Our development extends uniformly to identity types and higher inductive types (using the methods of [6]) (<ref>).

* Our development applies equally to the case where one treats univalence instead of glue types as primitive (<ref>).
We expect that a similar sconing argument (glueing along a global sections functor to simplicial sets) works to establish homotopy canonicity for the initial split univalent simplicial tribe in the setting of Joyal [17].

* Assuming excluded middle, a version of the simplicial set model [18] forms an instance of our development, and distributive lattice cubical type theory interprets in it (<ref>).

Using our technique, one may also reprove canonicity for ordinary Martin-Löf type theory with inductive families in a reduction-free way.

Shulman [27] proves homotopy canonicity for homotopy type theory with a truncatedness assumption using the sconing technique.
This proof was one starting point for the present work.
Some of his constructions may be simplified using our techniques, for example the construction of the natural number type in the sconing.

$\iPi(A,B)'(w)$     =     $\Pi (u: |A|)\Pi (u': A'u). B'uu'(\iapp(w,u))$

$\iSigma(A,B)'(w)$     =     $\Sigma (u': A'(\ifst (w))). B'(\ifst (w))\,u'\,(\isnd (w))$

$\ifill_{\psi,b}(u)'$     =     $\fillop_{\psi,b}(u')$

$\iPath(A,a_0,a_1)'(w)$     =     $\Path_{\lambda i.A'\,i\,(\ipapp(w,i))}\,a_0'\,a_1'$

$\iGlue(A,\psi\mapsto (B,w))'v$     =     $\Glue~(A'(\iapp(\iunglue,v)))~[\psi\mapsto (B'v, (w'.1\,v, \ldots))]$

The main rules for the sconing model

*Parametricity interpretation

As pointed out in [7], there is a strong analogy between proving canonicity via (Artin) glueing and parametricity.
For readers more familiar with parametricity than the general (Artin) glueing technique, we motivate our proof by briefly presenting a parametricity interpretation [3] of cubical type theory [5].
The parametricity interpretation is a purely syntactical interpretation which associates by structural induction a family $A'\,x$ where $x:A$ to any type $A$ and a term $t' : A'\,t$ to any term $t : A$.
In general, if $A$ is defined over the context $x_1:A_1,\dots,x_n:A_n$, then $A'(x_1,x_1,\dots,x_n,x_n')$ will be defined over the context $x_1:A_1,x_1':A_1'\,x_1,x_2:A_2(x_1),x_2':A_2'(x_1,x_1')\,x_2',\dots$.
The interpretation of $\Pi$, $\Sigma$, and universes is the same as for ordinary type theory.
For instance,

\[
(\Pi (x:A)B)'\,w = \Pi (x:A)(x':A'x).B'(x,x')\,(w\,x)
\]

with $(\lambda (x:A).t)' = \lambda (x:A)(x':A'x).t'$ and $(t\,u)' = t'\,u\,u'$.

For inductive types, we use the “inductive-style” interpretation [3], so that for instance $N'\,x$ is the inductive family with constructors $0'$ of type $N'\,0$ and $S'$ of type $\Pi (x:N).N'x \to N'\,(S\,x)$. (The other “deductive-style” presentation will not work for the canonicity proof.)

This interpretation works as well for cubical type theory.
There is a natural interpretation of path types: $(\Path\,A\,a_0\,a_1)'\,\omega$ is $\Path^i\,(A'\,(\omega~i))\,a'_0\,a'_1$ given $a_0'$ in $A'\,a_0$ and $a_1'$ in $A'\,a_1$.
We also take $(\angles{i}\,t)' = \angles{i}\,t'$ and $(t\,r)' = t'\,r$ for $r:\II$.

Consider $T = \Glue\,A\,[\psi \mapsto (B,w)]$ where $A$ is a “total” type and $w$ a “partial” equivalence between $B$ and $A$ of extent $\psi$, so a pair of $w.1 : B \to A$ and $w.2$ proving that $w.1$ is an equivalence. We define $T'\,u = \Glue\,A'\,(\unglue\,u)\,[\psi \mapsto (B'\,u,(w.1'\,u,c\,u)]$. We have $\unglue : T \to A$ and we can then define $\unglue' : \Pi (u:T). T'\,u \to A'\,(\unglue~u)$ by $\unglue'\,u\,u' = \unglue~u'$.
For this, we need to build a proof $c\,u$ that $w.1'~u$ is an equivalence.
This is possible by showing that the map $\Sigma (y:B) B'y \to \Sigma (x:A) A'\,x$ sending $(u,u')$ to $(w.1\,u,w.1'\,u\,u')$ is an equivalence.
We can then use Theorem 4.7.7 of [33] about equivalences on total spaces.

There is a problem however at this point: this interpretation does not need to validate the computation rules for the filling operation of the “Glue” type.
We can notice however that this problem is solved (in a somewhat trivial way) if we consider a system where the filling operation is given as a primitive constant, without any computation rule.

One way to understand the parametricity interpretation is that it is (Artin) glueing of the syntactic model along the identity map.
For proving canonicity, we instead glue the initial model with the cubical set model along the global section functor.
As in [7], we think that this interpretation is best described in an algebraic way, using what is essentially a generalized algebraic presentation of type theory.

We work in a constructive set theory (as presented in [1]) with a sufficiently long cumulative hierarchy of Grothendieck universes.
However, our constructions are not specific to this setting and can be
replayed in other constructive metatheories such as extensional type
theory.  In <ref>, we assume classical logic for the discussion of models in simplicial sets.

§ CUBICAL CATEGORIES WITH FAMILIES

We first recall the notion of categories with families (cwf) [8]
with $\Pi$- and $\Sigma$-types, universes and natural number types.  This notion
can be interpreted in any presheaf model. In a presheaf model however, we can consider
new operations. A cubical cwf will be such a cwf in a presheaf model
with extra operations which make use of an interval
presheaf $\II$ and a type of cofibrant propositions $\FF$ as introduced in [6, 23].

§.§ Category with families

Categories with families form an algebraic notion of model of type theory.
In order to later model universes à la Russell, we define them in a stratified manner where instead of a single presheaf of types, we specify a filtration of presheaves of “small” types.
[We note that this non-algebraic aspect of the definition does not interfere with the otherwise algebraic character and that subsets and the equality of sets $\Elem(\Gamma, \iU_n) = \Type_n$ below could in principle be replaced by injections and natural isomorphisms, respectively.]
The length of the filtration is not essential: we have chosen $1 + \omega$ so that we may specify constructions just at the top level.

A category with families (cwf) consists of the following data.

* We have a category of contexts $\Con$ and substitutions $\Subst(\Delta, \Gamma)$ from $\Delta$ to $\Gamma$ in $\Con$.
The identity substitution on $\Gamma$ in $\Con$ is written $\id$, and the composition of $\delta$ in $\Subst(\Theta, \Delta)$ and $\sigma$ in $\Subst(\Delta, \Gamma)$ is written $\sigma \delta$.

* We have a presheaf $\Type$ of types over the category of contexts.
The action of $\sigma$ in $\Subst(\Delta, \Gamma)$ on a type $A$ over $\Gamma$ is written $A \sigma$.
We have a cumulative sequence of subpresheaves $\Type_n$ of types of level $n$ of $\Type$ where $n$ is a natural number.

* We have a presheaf $\Elem$ of elements over the category of elements of $\Type$, a type $\Elem(\Gamma, A)$ for $A$ in $\Type(\Gamma)$ with $a \sigma$ in $\Elem(\Delta, A \sigma)$ for $a$ in $\Elem(\Gamma, A)$ and $\sigma$ in $\Subst(\Delta, \Gamma)$ satisfying evident laws.

* We have a terminal context $1$, with the unique element of $\Subst(\Gamma, 1)$ written $()$.

* Given $A$ in $\Type(\Gamma)$, we have a context extension $\Gamma.A$.
There is a projection $\pp$ in $\Subst(\Gamma.A, \Gamma)$ and a generic term $\qq$ in $\Elem(\Gamma.A, A\pp)$.
Given $\sigma$ in $\Subst(\Delta, \Gamma)$, $A$ in $\Type(\Gamma)$, and $a$ in $\Elem(\Delta, A \sigma)$ we have a substitution extension $(\sigma, a)$ in $\Subst(\Delta, \Gamma.A)$.
These operations satisfy $\pp (\sigma, a) = \sigma$, $\qq (\sigma, a) = a$, and $(\pp \sigma, \qq \sigma) = \sigma$.
Thus, every element of $\Subst(\Delta, \Gamma.A)$ is uniquely of the form $(\sigma, a)$ with $\sigma$ and $a$ as above.

We introduce some shorthand notation related to substitution.
Given $\sigma$ in $\Subst(\Delta, \Gamma)$ and $A$ in $\Type(\Gamma)$, we write $\sigma^+ = (\sigma \pp, \qq)$ in $\Subst(\Delta.A \sigma, \Gamma.A)$.
Given $a$ in $\Elem(\Gamma, A)$, we write $\subst{a} = (\id, a)$ in $\Subst(\Gamma, \Gamma.A)$.
Thus, given $B$ in $\Type_n(\Gamma.A)$ and $a$ in $\Elem(\Gamma, A)$, we have $B \subst{a}$ in $\Type(\Gamma)$.
Given furthermore $b$ in $\Elem(\Gamma.A, B)$, we have $b \subst{a}$ in $\Elem(\Gamma, B\subst{a})$.
We extend this notation to several arguments: given $a_i$ in $\Elem(\Gamma, A_i)$ for $1 \leq i \leq k$, we write $\subst{a_1, \ldots, a_k}$ for $[a_k] [a_{k-1} \pp] \cdots [a_1 \pp \ldots \pp]$ in
$\Subst(\Gamma, \Gamma.A_1.\ldots.A_k)$.

Note that we could take a different equational presentation. For instance, the presentation in
[9] takes as primitive the operations $\sigma^+$ and $[u]$ and defines
then $(sigma,u)$ as a derived operation $(\sigma,u) = \sigma^+[u]$. It is a strength of the present
approach to canonicity proof to be independent of this choice.

Given a cwf as above, we define what it means to have the following type formers.
In addition to the specified laws, all specified operations are furthermore required to be stable under substitution in the evident manner.

* Dependent products.

For $A$ in $\Type(\Gamma)$ and $B$ in $\Type(\Gamma.A)$, we have $\iPi(A, B)$ in $\Type(\Gamma)$, of level $n$ if $A$ and $B$ are.
Given $b$ in $\Elem(\Gamma.A, B)$, we have the abstraction $\ilambda(b)$ in $\Elem(\Gamma, \iPi(A, B))$.
Given $c$ in $\Elem(\Gamma, \iPi(A, B))$ and $a$ in $\Elem(\Gamma, A)$, we have the application $\iapp(c, a)$ in $\Elem(\Gamma, B \subst{a})$.
These operations satisfy $\iapp(\ilambda(b), a) = b \subst{a}$ and $\ilambda(\iapp(c \pp, \qq)) = c$.

Given $A$ and $B$ in $\Type(\Gamma)$ we write $A \to B$ for $\iPi(A, B \pp)$.

* Dependent sums.

For $A$ in $\Type(\Gamma)$ and $B$ in $\Type(\Gamma.A)$, we have $\iSigma(A, B)$ in $\Type(\Gamma)$, of level $n$ if $A$ and $B$ are.
Given $a$ in $\Elem(\Gamma, A)$ and $b$ in $\Elem(\Gamma, B \subst{a})$, we have the pairing $\ipair(a, b)$ in $\Elem(\Gamma, \iSigma(A, B))$.
Given $c$ in $\Elem(\Gamma, \iSigma(A, B))$, we have the first projection $\ifst(c)$ in $\Elem(\Gamma, A)$ and second projection $\isnd(c)$ in $\Elem(\Gamma, B \subst{\ifst(c)})$.
These operations satisfy $\ifst(\ipair(a, b)) = a$, $\isnd(\ipair(a, b)) = b$, and $\ipair(\ifst(c), \isnd(c)) = c$.
Thus, every element of $\Elem(\Gamma, \iSigma(A, B))$ is uniquely of the form $\ipair(a, b)$ with $a$ and $b$ as above.

Given $A$ and $B$ in $\Type(\Gamma)$ we write $A \times B$ for $\iSigma(A, B \pp)$.

* Universes.
We have $\iU_n$ in $\Type_{n+1}(\Gamma)$ such that $\Type_n(\Gamma) = \Elem(\Gamma, \iU_n)$, and the action of substitutions on $\Elem(\Gamma, \iU_n)$ is compatible with that on $\Type_n(\Gamma)$.

* Natural numbers.
We have $\iN$ in $\Type_0(\Gamma)$ with zero $\izero$ in $\Elem(\Gamma, \iN)$ and successor $\isucc(n)$ in $\Elem(\Gamma, \iN)$ for $n$ in $\Elem(\Gamma, \iN)$.
Given $P$ in $\Type(\Gamma.\iN)$, $z$ in $\Elem(\Gamma, P[\izero])$, $s$ in $\Elem(\Gamma.\iN.P, P (\pp, S(\qq)) \pp)$, and $n : \Elem(\Gamma, \iN)$, we have the elimination $\inatrec(P, z, s, n)$ in $\Elem(\Gamma, P[n])$ with $\inatrec(P, z, s, \izero) = z$, $\inatrec(P, z, s, \isucc(n)) = s[n, \inatrec(P, z, s, n)]$.

A structured cwf is a cwf with type formers as above.

A (strict) morphism $\mathcal{M} \to \mathcal{N}$ of cwfs is defined in the evident manner and consists of a functor $F \co \Con_{\mathcal{M}} \to \Con_{\mathcal{N}}$ and natural transformations $u \co \Type_{\mathcal{M}} \to \Type_{\mathcal{N}} F$ and $v \co \Elem_{\mathcal{M}} \to \Elem_{\mathcal{N}} (F, u)$ such that $v$ restricts to types of level $n$ and the terminal context and context extension is preserved strictly.
A morphism $\mathcal{M} \to \mathcal{N}$ of structured cwfs additionally preserves the operations of the above type formers.
We obtain a category of structured cwfs.

§.§ Internal language of presheaves

For the rest of the paper, we fix a category $\mathcal{C}$ in the lowest Grothendieck universe.
As in [2, 23, 21], we will use the language of extensional type theory (with subtypes) to describe constructions in the presheaf topos over $\mathcal{C}$.

In the interpretation of this language, a context is a presheaf $A$ over $\mathcal{C}$, a type $B$ over $A$ is a presheaf over the category of elements of $A$, and an element of $B$ is a section.
A global type is a type in the global context, a presheaf over $\mathcal{C}$.
Similarly, a global element of a global type is a section of that presheaf.

Given a dependent type $B$ over a type $A$, we think of $B$ as a family of types $B\,a$ indexed by elements $a$ of $A$.
We have the usual dependent sum $\Sigma(a:A).B(a)$ and dependent product $\Pi(a:A).B\,a$, with projections of $s : \Sigma(a:A).B\,a$ written $s.1$ and $s.2$ and application of $f : \Pi(a:A). B\,a$ to $a : A$ written $f\,a$.
We also the categorical pairing $\angles{f, g} : X \to \Sigma(a:A).B\,$ given $f : X \to A$ and $g : \Pi(x:X). B\,(f\,a)$ and other commonly used notations.
The hierarchy of Grothendieck universes in the ambient set theory gives rise to a cumulative hierarchy $\U_0, \U_1, \ldots, \U_\omega$ of universes à la Russell.
We model propositions as subtypes of a fixed type $1$ with unique element $\TT$.
We have subuniverses $\Omega_i \subseteq \U_i$ of propositions for $i \in \braces{0, 1 \ldots, \omega}$.

When working in this internal language, we refer to the types as “sets” to avoid ambiguity with the types of (internal) cwfs we will be considering.

§.§ Cubical categories with families

We now work internally to presheaves over $\mathcal{C}$.
We assume the following:

* an interval $\II : \U_0$ with endpoints $0, 1 : \II$,

* an object $\FF : \U_0$ of cofibrant propositions with a monomorphism $[-] : \FF \to \Omega_0$.

As in [6, 23], a partial element of a set $T$ is given by an element $\phi$ in $\FF$ and a function $[\phi] \to T$.
We say that a total element $v$ of $T$ extends such a partial element $\phi, u$ if we have $[\phi] \to u\,\TT = v$.

Given $A : \II \to \U_\omega$, we write $\hasFill(A)$ for the set of operations taking as inputs $\phi$ in $\FF$, $b \in \braces{0, 1}$, and a partial section $u$ in $\Pi (i : \II). [\phi] \vee (i = b) \to A\,i$ and producing an extension of $u$ to a total section in $\Pi (i:\II)\, A\,i$.
Given a set $X$ and $Y : X \to \U_\omega$, we write $\Fill(X, Y)$ for the set of filling structures on $Y$, producing an element of $\hasFill(Y \cc x)$ for $x$ in $\II \to X$.
Given $s$ in $\Fill(X, Y)$ and $x, \phi, b, u$ as above, we write $s(x, \phi, b\ u)$ for the resulting total section in $\Pi (i:\II). Y\,(x\,i)$.

We now interpret the definitions of <ref> in the internal language of the presheaf topos.
A cubical cwf is a structured cwf denoted as before that additionally has the following cubical operations and type formers.
Again, all specified operations are required to be stable under substitution.

* Filling operation.
We have $\ifill$ in $\Fill(\Type(\Gamma), \lambda A. \Elem(\Gamma, A))$ for $\Gamma$ in $\Con$.
Let us spell out stability under substitution: given $A \co \II \to \Type(\Gamma)$, $\phi$ in $\FF$, $b \in \braces{0, 1}$, $u$ in $\Pi(i:\II).\, [\phi] \vee (i = b) \to \Elem(\Gamma, A\,i)$, and $\sigma$ in $\Subst(\Delta, \Gamma)$ and $r : \II$, we have $(\ifill(A, \phi, b, u)\,r) \sigma = \ifill(\lambda i.\, (A\, i) \sigma, \phi, b, \lambda i\,x.\, (u\,i\,x) \sigma)\,r$.

Note that we do not include computation rules for $\ifill$ at type formers.
This corresponds to our decision to treat $\ifill$ as a non-canonical operation.

* Dependent path types.
Given $A$ in $\II \to \Type(\Gamma)$ with $a_b$ in $\Elem(\Gamma, A b)$ for $b \in \braces{0, 1}$, we have a type $\iPath(A, a_0, a_1)$ in $\Type(\Gamma)$, of level $n$ if $A$ is.
Given $u$ in $\Pi(i:\II).\Elem(\Gamma, A i)$, we have the path abstraction $\ipabs(u)$ in $\Elem(\Gamma, \iPath(A, u\,0, u\,1))$.
Given $p$ in $\Elem(\Gamma, \iPath(A, a_0, a_1))$ and $i$ in $\II$, we have the path application $\ipapp(p, r)$ in $\Elem(\Gamma, A i)$.
These operations satisfy the laws $\ipapp(p, b) = a_b$ for

$b \in \braces{0, 1}$, $\ipapp(\ipabs(u), i) = u\,i$,  and $\ipabs(\lambda i.\, \ipapp(p, i)) = p$.
Thus, every element of $\Elem(\Gamma, \iPath(A, a_0, a_1))$ is uniquely of the form $\ipabs(u)$ with $u$ in $\Pi(i:\II).\Elem(\Gamma, A i)$ such that $u\,0 = a_0$ and $u\,1 = a_1$.

Using path types, we define $\iisContr(A)$ in $\Type(\Gamma)$ for $A$ in $\Type(\Gamma)$ as well as $\iisEquiv$ in $\Type(\Gamma.A \to B)$ and $\iEquiv$ in $\Type(\Gamma)$ for $A, B$ in $\Type(\Gamma)$ as in [5].
These notions are used in the following type former, which extends any partially defined equivalence (given total codomain) to a totally defined function.

* Glue types.
Given $A$ in $\Type(\Gamma)$, $\phi$ in $\FF$, $T$ in $[\phi] \to \Type(\Gamma)$ and $e : [\phi] \to \Elem(\Gamma, \Equiv(T \TT, A))$, we have the glueing $\iGlue(A, \phi, T, e)$ in $\Type(\Gamma)$, equal to $T$ on $[\phi]$ and of level $n$ if $A$ and $T$ are.
We have $\iunglue$ in $\Elem(\Gamma, \Glue(A, \phi, T, e) \to A)$ such that $\iunglue = \ifst(e)\,\TT$ on $[\phi]$.
Given $a$ in $\Elem(\Gamma, A)$ and $t$ in $[\phi] \to \Elem(\Gamma, T)$ such that $\iapp(\ifst(e)\,\TT, t\,\TT) = a$ on $[\phi]$, we have $\iglue(a, t)$ in $\Elem(\Gamma, \Glue(A, \phi, T, e))$ equal to $t$ on $[\phi]$.
These operations satisfy $\iapp(\iunglue, \iglue(a, t)) = a$ and $\iglue(\iapp(\iunglue, u), \lambda x. u) = u$.
Thus, every element of $\Elem(\Gamma, \iGlue(A, \phi, T, e))$ is uniquely of the form $\iglue(a, t)$ with $a$ and $t$ as above.

The notion of morphism of structured cwfs lifts to an evident notion of morphism of cubical cwfs.
We obtain, internally to presheaves over $\mathcal{C}$, a category of cubical cwfs.
We now lift this category of cubical cwfs from the internal language to the ambient theory by interpreting it in the global context: externally, a cubical cwf (relative to the chosen base category $\mathcal{C}$, interval $\II$, and cofibrant propositions $\FF$) consists of a presheaf $\Con$ over $\mathcal{C}$, a presheaf $\Type$ over the category of elements of $\Con$, .

Fix a cubical cwf as above.
Assume that $\II$ has a connection algebra structure and that $\FF$ forms a sublattice of $\Omega_0$ that contains the interval endpoint inclusions.
As in [5], it is then possible in the above context of the glue type former to construct an element of $\Elem(\Gamma, \iisEquiv[\iunglue])$.

From this, one derives an element of $\Elem(\Gamma, \iUnivalence_n)$ where $\iUnivalence_n = \iPi(\iU_n, \iisContr(\iSigma(\iU_n, \iEquiv(\qq, \qq \pp))))$ for $n \geq 0$, univalence is provable.
One may also show that the path type applied to constant families $\II \to \Type(\Gamma)$ interprets the rules of identity types of Martin-Löf with the computation rule for the eliminator $\iJ$ replaced by a propositional equality.
Thus, we obtain an interpretation of univalent type theory with identity types with propositional computation in any cubical cwf.

§ TWO EXAMPLES OF CUBICAL CWFS

In this section we give two examples of cubical cwfs: a term model and
a particular cubical cwfs formulated in a constructive metatheory, the
latter with extra assumptions on $\II$ and $\FF$.

§.§ Term model

We sketch how to give a cubical cwf $\Syn$ built from syntax, and
refer the reader to <ref> for more details.  All our
judgments will be indexed by an object $X$ of $\mathcal{C}$ and given
a judgment $\Gamma \der_X \JJ$ and $f \co Y \to X$ in $\mathcal{C}$ we
get $\Gamma f \der_Y \JJ f$.  Here, $f$ acts on expressions as an
implicit substitution, while for substitutions on object variables we
will use explicit substitutions.

The forms of judgment are:

Γ_X A
Γ_X A = B
Γ_X t : A
Γ_X t = u : A
σΔ→_X Γ
The main rules are given in the appendix.  This then induces a cubical
cwf $\Syn$ by taking, say, the presheaf of contexts at stage $X$ to be
equivalence classes of $\Gamma$ for $\Gamma \der_X$ where the
equivalence relation is judgmental equality.

Some rules are a priori infinitary, but in some cases (such as the one
considered in [5]) it is possible to present the rules in a
finitary way.

This formal system expresses the laws of cubical cwfs in rule form. It defines
the term model.  Following [29, 24] developed in an
intuitionistic framework, we conjecture that this can be interpreted in an
arbitrary cubical cwf in the usual way:

With chosen parameters $\mathcal{C}, \II, \FF$, the cubical cwf $\Syn$ is initial in the category of cubical cwfs.

However, our canonicity result is orthogonal to this conjecture: It is a result about the initial model, without need for an explicit description of this model as a term model.

§.§ Developments in presheaves over $\mathcal{C}$

We now assume that $\II$ and $\FF$ satisfy the axioms $\mathtt{ax_1}, \ldots, \mathtt{ax_9}$ of [23], internally to presheaves over $\mathcal{C}$.
We also make an external assumption, namely that the endofunctor on presheaves over $\mathcal{C}$ of exponentiation with $\II$ has a right adjoint $R$ that preserves global types of level $n$.
This is the case if $\II$ is representable and $\mathcal{C}$ is closed under finite products.

Most of the arguments will be done in the internal language of the presheaf topos.
At certain points however, we need to consider the set of global sections of a global type $F$; we denote this by $\Box F$.
We stress that statements involving $\Box$ are external, not to be interpreted in the internal language.
Crucially, the adjunction $(-)^\II \dashv R$ cannot be made internal [21].

Recall the global type $\hasFill : \U_\omega^\II \to \U_\omega$ from <ref>.
Taking the slice over $\U_\omega$, the adjunction $(-)^\II \dashv R$ descends to an adjunction between categories of types over $\U_\omega$ and $\U_\omega^\II$.
Applying the right adjoint of this adjunction to $\hasFill$, we obtain global $\CC : \U_\omega \to \U_\omega$ such that naturally in a global type $X$ with global $Y : X \to \U_\omega$, global elements of $\Pi(x : X^\II). \hasFill(Y \cc x)$ are in bijection with global elements of $\Pi(x : X). \CC(Y\,x)$.
Given a global type $X$ and global $Y : X \to \U_\omega$, we thus have a logical equivalence (maps back and forth)

\begin{equation} \label{C-vs-fill-external}
\Box \Fill(X, Y) \longleftrightarrow \Box \Pi(x:X)\,\CC(Y\,x)
\end{equation}

natural in $X$.
[We record only the logical equivalence instead of an isomorphism so that it will be easier to apply our constructions in situations where the right adjoint $R$ fails to exist, see <ref>.
Naturality is only used at a one point below, for the forward map, to construct suitable elements of $C$ applied to glueings.]
Note that $\CC$ descends to $\CC : \U_n \to \U_n$ for $n \geq 0$.
We write $\Ufib_i = \Sigma(A:\U_i)\,\CC(A)$ for $i \in \braces{0, 1, \ldots, \omega}$; we call $\Ufib_i$ a universe of fibrant sets.
Now set $X = \Ufib_\omega$ and $Y(A, c) = A$ in (<ref>).
We trivially have $\Box \Pi(x:X)\,\CC(Y\,x)$, thus get

\begin{equation} \label{U-fib-has-fill}
\fillop : \Fill(\Ufib_\omega, \lambda(A, c). A)

This is essentially the counit of the adjunction defining $\CC$.
Note that [21] use modal extensions of type theory to perform this reasoning internal to presheaves over $\mathcal{C}$.

Internally, a map $\Fill(X, Y) \to \Pi(x:X)\,\CC(Y\,x)$ does not generally exist for a set $X$ and $Y : X \to \U_\omega$ as for $X = 1$ one would derive a filling structure for any “homogeneously fibrant” set, which is impossible (see <cit.>).

However, from (<ref>) we get a map $\Pi(x:X)\,\CC(Y\,x) \to \Fill(X, Y)$ natural in $X$ using closure of filling structures under substitution (see below).

We recall some constructions of [5, 23] in the internal language.

* Given $A : \II \to \U_\omega$ and $a_b : A_b$ for $b \in \braces{0, 1}$, dependent paths $\Path_A\,a_0\,a_1$ are the set of maps $p : \Pi(i : \II). A\,i$ such that $p\,0 = a_0$ and $p\,1 = a_1$.
We use the same notation for non-dependent paths.

* For $A : \U_\omega$, we have a set $\isContr(A)$ of witnesses of contractibility, defined using paths.

* Given $A, B : \U_\omega$ with $f : A \to B$, we have the set $\isEquiv(f)$ with elements witnessing that $f$ is an equivalence, defined using contractibility of homotopy fibers.
We write $\Equiv(A, B) = \Sigma(f : A \to B). \isEquiv(f)$.

* Given $A : \U_\omega$, $\phi : \FF$, $B : [\phi] \to \U_\omega$, and $e : [\phi] \to \Equiv(B\,\TT, A)$, the glueing $\Glue\,A\,[\phi \mapsto (B, e)]$ consists of elements $\glue\,a\,[\phi \mapsto b]$ with $a : A$ and $b : [\phi] \to B$ such that $e.1\,(b\,\TT) = a$ on $[\phi]$ and is defined in such a way that $\Glue\,A\,[\phi \mapsto (B, e)] = T\,\TT$ and $\glue\,a\,[\phi \mapsto b] = b\,\TT$ on $[\phi]$.
The canonical map $\unglue : \Glue\,A\,[\phi \mapsto (B, e)] \to A$ is an equivalence.

These operations are valued in $\U_n$ if their inputs are.
We further recall basic facts from [23] about filling structures in the internal language.

* Filling structures are closed under substitution: given $f : X' \to X$ and $Y \co X \to \U_\omega$, any element of $\Fill(X, Y)$ induces an element of $\Fill(X', Y \cc f)$, naturally in $X'$.

* Filling structures are closed under exponentiation: given sets $S, X$ and $Y \co X \to \U_\omega$, any element of $\Fill(X, Y)$ induces an element of $\Fill(X^S, \lambda x. \Pi(s:S). Y(x\,s))$, naturally in $S$.

* Filling structures are closed under $\Pi, \Sigma, \Path, \Glue$.
for dependent products, given $A : \Gamma \to \U_\omega$ with $\Fill(\Gamma, A)$ and $B : \Pi(\rho : \Gamma). A\,\rho \to \U_\omega$ with $\Fill(\Sigma(\rho : \Gamma). A\,\rho, \lambda(\rho, a). B\,\rho\,a)$, we have $\Fill(\Gamma, \lambda(\rho : \Gamma). \Pi(a : A\,\rho). B\,\rho\,a)$.

From the last point, we deduce using that $\CC$ is closed under $\Pi, \Sigma, \Path, \Glue$, and that $\CC(A)$ implies $\CC(A^S)$ for $A, S : \U_\omega$.
[Note that naturality in $S$ of the latter operation is used in substitutional stability of universes in the sconing in <ref>.]
Let us explain this in the case of dependent products.
We apply (<ref>) with a suitable “generic context” $X = \Sigma((A, c) : \Ufib_\omega). A \to \Ufib_\omega$ and $Y((A, c), \angles{B, d}) = \Pi(a:A). B\,a$.
Using the map of <ref> and closure of filling structures under dependent product, we have $\Box \Fill(X, Y)$ and can conclude $\CC(\Pi(a:A). B\,a)$ for $(A, c) : \Ufib_\omega$ and $\angles{B, d} : A \to \Ufib_\omega$.
Note that in the case of $\Glue$ with $(A, c) : \Ufib_\omega$, $\phi : \FF$, $\angles{B, d} : [\phi] \to \Ufib_\omega$, and $e : [\phi] \to \Equiv(B\,\TT, A)$, naturality of the forward map of (<ref>) is needed to see that the element $c : \CC(\Glue\,A\,[\phi \mapsto (B, e)])$ constructed in the same fashion as above for dependent products equals $d\,\TT : C(B\,\TT)$ on $[\phi]$.

We apply (<ref>) with a suitable “generic context” $X = \Sigma((A, c) : \Ufib_\omega))(\phi : \F)(T : [\phi] \to \Ufib_\omega). [\phi] \to \Equiv(T\,\TT, A)$ and $Y(A, \phi, T, e) = \Glue\A\,(\phi \mapsto (T, e))$.

X = Σ(A : _ω)(ϕ: )(B : [ϕ] →_ω)(e : [ϕ] →(B , A))
Y(A, ϕ, B, e) =  A (ϕ↦(B, e))

X' = Σ(A : _ω)(B : _ω)(e : (B , A))
Y'(A, B, e) = B

X” = _ωY”(B) = B

f : X' →X
f(A, B, e) = (A, ⊤, λx. B, λx. e)

g : X' →X”
g(A, B, e) = B

c : Fill(X, Y)
c” : Fill(X”, Y”)

the restrictions of c along f and c” along g to Fill(X', Y') agree

using naturality of

As in [5, 23, 21], glueing shows $\Fill(1, \Ufib_n)$ for $n \geq 0$.
Using (<ref>), we conclude $\CC(\Ufib_n)$.

Let $\mathbb{N}$ denote the natural number object in presheaves over $\mathcal{C}$, the constant presheaf with value the natural numbers.
From [5, 23], we have $\Fill(1, \mathbb{N})$.
Using (<ref>), we conclude $\CC(\mathbb{N})$.

We justify fibrant indexed inductive sets in <ref>.

§.§ Standard model

Making the same assumptions on $\mathcal{C}, \II, \FF$ as in <ref>, we can now specify the standard model $\Std$ of cubical type theory in the sense of the current paper as a cubical cwf (with respect to parameters $\mathcal{C}, \II, \FF$) purely using the internal language of the presheaf topos.
The cwf is induced by the family over $\Ufib_\omega$ given by the first projection as follows.

* The category of contexts is $\U_{\omega}$, with $\Subst(\Delta, \Gamma)$ the functions from $\Delta$ to $\Gamma$.

* The types over $\Gamma$ are maps from $\Gamma$ to $\Ufib_\omega$; a type $\angles{A, p}$ is of level $n$ if $A$ is in $\Gamma \to \U_n$.
This is clearly functorial in $\Gamma$.

* The elements of $\angles{A, p} : \Gamma \to \Ufib_\omega$ are $\Pi(\rho:\Gamma).A\,\rho$.
This is clearly functorial in $\Gamma$.

* The terminal context is given by $1$.

* The context extension of $\Gamma$ by $\angles{A, p}$ is given by $\Sigma(\rho:\Gamma). A \, \rho$, with $\pp, \qq$ given by projections and substitution extension given by pairing.

We briefly go through the necessary type formers and operations, omitting evident details.

* The dependent product of $\angles{A, c} : \Gamma \to \Ufib_\omega$ and $\angles{B, d} : \Sigma(\rho : \Gamma). A\,\rho \to \Ufib_\omega$ is $\angles{\lambda \rho. \Pi(a : A\,\rho). B(\rho, a), e}$ where $e\,\rho : \CC(\Pi(a : A\,\rho). B(\rho, a))$ is induced by $c\,\rho : \CC(A\,\rho)$ and $d\,\rho\,a : \CC(B(\rho, a))$ for $a : A$ as discussed above.

* The dependent sum of $\angles{A, c} : \Gamma \to \Ufib_\omega$ and $\angles{B, d} : \Sigma(\rho : \Gamma). A\,\rho \to \Ufib_\omega$ is $\angles{\lambda \rho. \Sigma(a : A\,\rho). B(\rho, a), e}$ where $e$ is induced by $c$ and $d$.

* The universe $\iU_n : \Gamma \to \Ufib_{n+1}$ is constantly $(\Ufib_n, c)$ with $c : \CC(\Ufib_n)$ as above.

* The natural number type $\iN : \Gamma \to \Ufib_0$ is constantly $(\mathbb{N}, c)$ with $c : \CC(\mathbb{N})$ as above.
The zero and successor constructors and eliminator are given by the corresponding features of the natural number object $\mathbb{N}$.

We now turn to the cubical aspects.

* The filling operation $\ifill : \Fill(\Gamma \to \Ufib_\omega, \lambda \angles{A, p}. \Pi(\rho : \Gamma). A\,\rho)$ is derived from (<ref>) by closure of filling structures under exponentiation.

* Given $\angles{A, c} : \II \to \Gamma \to \Sigma(A : \U_\omega)\, \CC(A)$ and $a_b : \Pi(\rho : \Gamma). A\,b\,\rho$ for $b \in \braces{0, 1}$, we define $\iPath(A, a_0, a_1) : \Gamma \to \Sigma(A : \U_\omega)\, \CC(A)$ as $\angles{\Pi(\rho : \Gamma). \Path_{\lambda i. A\,i\,\rho}\,c_0\,c_1), d}$ where $d\,\rho : \CC(\Path_{\lambda i. A\,i\,\rho}\,c_0\,c_1))$ induced by $\lambda i. c\,i\,\rho$.

Before defining glue types, we note that the notions $\iisContr$ and $\iisEquiv$ in the cubical cwf we are defining correspond to the notions $\isContr$ and $\isEquiv$.
For example, given a type $A : \Gamma \to \Ufib_\omega$, then the elements of $\iisContr(A)$, given by $\Pi(\rho : \Gamma).\,\iisContr(A).1\,\rho$, are in bijection with $\Pi(\rho : \Gamma). \isContr(A.1\,\rho)$ naturally in $\Gamma$.

* Given $\angles{A, c} : \Gamma \to \Ufib_\omega$, $\phi : \FF$, $\angles{T, d} : [\phi] \to \Gamma \to \Ufib_\omega$ and $e : [\phi] \to \iEquiv(T\,\TT, A)$, we define $\iGlue(\angles{A, c}, \phi, \angles{T, d}, e) : \Gamma \to \Ufib_\omega$ as $\lambda \rho. (\Glue\,(A\,\rho) [\phi \mapsto (T\,\TT\,\rho, e'\,\TT\,\rho)], q\,\rho)$ where $e'\,\TT\,\rho : \Equiv(T\,\TT\,\rho, A\,\rho)$ is induced by $e\,\TT\,\rho$ and $q\,\rho$ is induced by $c\,\rho$ and $\lambda x. d\,x\,\rho$.

We have thus verified the following statement.

Assuming the parameters $\mathcal{C}, \II, \FF$ satisfy the assumptions of <ref>, the standard model $\Std$ forms a cubical cwf.

§ SCONING

We make the same assumptions on our parameters $\mathcal{C}, \II, \FF$ as in <ref>.
Let $\MM$ be a cubical cwf (with respect to these parameters) denoted $\Con, \Subst, \ldots$ as in <ref>.
We assume that $\MM$ is size-compatible with the standard model, by which we mean $\Subst(\Delta, \Gamma) : \U_\omega$ for all $\Gamma, \Delta$ and $\Elem(\Gamma, A) : \U_i$ for $i \in \braces{0, 1, \ldots, \omega}$ and all $\Gamma$ and $A : \Type_i(\Gamma)$.
We will then define a new cubical cwf $\MM^*$ denoted $\Con^*, \Subst^*, \ldots$, the (Artin) glueing of $\MM$ with the standard model $\Std$ along an (internal) global sections functor, the sconing of $\MM$.

Recall from <ref> the operation $\ifill$ of $\MM$.
Instantiating it to the terminal context, we get $\Box \Fill(\Type(1), \lambda A. \Elem(1, A))$.
Using the forward direction of <ref>, we thus have an internal operation $k : \Pi(A : \Type(1)). \CC(\Elem(1, A))$.

From now on, we will work in the internal language of presheaves over $\mathcal{C}$.
We start by defining a global sections operation $\verts{-}$ mapping contexts, types, and elements of $\MM$ to those of $\Std$.

* Given $\Gamma : \Con$, we define $\verts{\Gamma} : \U_\omega$ as the set of substitutions $\Subst(1, \Gamma)$.
Given a substitution $\sigma : \Subst(\Delta, \Gamma)$, we define $\verts{\sigma} : \verts{\Delta} \to \verts{\Gamma}$ as $\verts{\sigma} \rho = \sigma \rho$.
This evidently defines a functor.

* Given $A : \Type(\Gamma)$, we define $\verts{A} : \verts{\Gamma} \to \Ufib_\omega$ as $\verts{A}\,\rho = (\Elem(1, A \rho), k\, (A\, \rho))$.
This evidently natural in $\Gamma$.
If $A$ is of level $n$, then $|A| : \verts{\Gamma} \to \Ufib_n$.

* Given $a : \Elem(\Gamma, A)$ we define $\verts{a} : \Pi(\rho : \Gamma).\,(\verts{A}\,\rho).1$ as $\verts{a}\,\rho = a \rho$.
This is evidently natural in $\Gamma$.

Note that $\verts{-}$ preserves the terminal context and context extension up to canonical isomorphism in the category of contexts.
One could thus call $\verts{-}$ an (internal) pseudomorphism cwfs from $\MM$ to $\Std$.
The sconing $\MM^*$ will be defined as essentially the (Artin) glueing along this pseudomorphism, but we will be as explicit as possible and not define (Artin) glueing at the level of generality of an abstract pseudomorphism.

For convenience, we also just write $\verts{A} : \verts{\Gamma} \to \U_\omega$ instead of $\lambda \rho.\, (\verts{A}\,\rho).1$, implicitly applying the first projection.
We also write just $\verts{A}$ for $\verts{A}~\verts{()}$ if $\Gamma$ is the terminal context.

§.§ Contexts, substitutions, types and elements

We start by defining the cwf $\MM^*$.

* A context $(\Gamma, \Gamma') : \Con^*$ consists of a context $\Gamma : \Con$ in $\MM$ and a family $\Gamma'$ over $\verts{\Gamma}$ (which in the context of Artin glueing should be thought of as a substitution in $\Std$ from some context to $\verts{\Gamma}$).
We think of $\Gamma'$ as a proof-relevant computability predicate.
A substitution $(\sigma, \sigma') : \Subst^*((\Delta, \Delta'), (\Gamma, \Gamma'))$ consists of a substitution $\sigma : \Delta \to \Gamma$ in $\MM$ and a map $\sigma' : \Pi(\nu : \verts{\Delta}). \Delta'(\nu) \to \Gamma'(\sigma \nu)$.
This evidently has the structure of a category.

* A type $(A, A') : \Type^*(\Gamma, \Gamma')$ consists of a type $A : \Type(\Gamma)$ in $\MM$ and

\[
A' : \Pi(\rho : \verts{\Gamma})(\rho' : \Gamma'\,\rho). \verts{A}\,\rho \to \Ufib_\omega

We think of $A'$ as a fibrant proof-relevant computability family on $A$.
In the abstract context of Artin glueing for cwfs, we should think of it as an element of $\Type(\Sigma(\rho : \verts{\Gamma})(\rho' : \Gamma'\,\rho). \verts{A}\, \rho)$ in $\Std$, but this point of view is not compatible with the universes à la Russell we are going to model.
Recalling $\Ufib_\omega = \Sigma(X : \U_\omega). C(X)$, we also write $\angles{A', \fib_{A'}}$ instead of $A'$ if we want to directly access the family and split off its proof of fibrancy.

The type $(A, A')$ is of level $n$ if $A$ and $A'$ are.

The action of a substitution $(\sigma, \sigma') : \Subst^*((\Delta, \Delta'), (\Gamma, \Gamma'))$ on $(A, A')$ is given by

\[
(A \sigma, \lambda \nu\,\nu'\,a. A'\,(\sigma \nu)\,(\sigma'\,\nu\,\nu')\, a).
\]

* An element $(a, a') : \Elem^*((\Gamma, \Gamma'), (A, \angles{A', \fib_{A'}}))$ consists of $a : \Elem(\Gamma, A)$ in $\MM$ and

\[
a' : \Pi(\rho : \verts{\Gamma})(\rho' : \Gamma'\,\rho).\,A'(\rho, \rho', a \rho)

In the context of Artin glueing (with types in $\MM^*$ presented correspondingly), this should be thought of as an element $a' : \Elem(\Sigma(\rho : \verts{\Gamma}). \Gamma'\,\rho, \lambda(\rho, \rho'). A'(\rho, \rho', \verts{a}\,\rho))$ of $\Std$.

The action of a substitution $(\sigma, \sigma') : \Subst^*((\Delta, \Delta'), (\Gamma, \Gamma'))$ on the element $(a, a')$ is given by $(a \sigma, \lambda \nu\,\nu'. a'\,\sigma \nu\,(\sigma'\,\nu\,\nu'))$.

* The terminal context is given by $(1, 1')$ defined by $1'\,() = 1$.

* The extension in $\MM^*$  of a context $(\Gamma, \Gamma')$ by a type $(A, A')$ is given by $(\Gamma.A, (\Gamma.A)')$ where $(\Gamma.A')(\rho, a) = \Sigma(\rho' : \Gamma'\,\rho).\,(A'\,\rho\,\rho'\,a).1$.
The projection $\pp^* : \Subst^*((\Gamma, \Gamma').(A, A'), (\Gamma, \Gamma'))$ is $(\pp, \pp')$ where $\pp'\,(\rho, a)\,(\rho', a') = \rho'$ and the generic term $\qq^* : \Elem((\Gamma, \Gamma').(A, A') \pp^*)$ is $(\qq, \qq')$ where $\qq'\,(\rho, a)\,(\rho', a') = a'$.
The extension of $(\sigma, \sigma') : \Subst^*((\Delta, \Delta'), (\Gamma, \Gamma'))$ with $(a, a') : \Elem^*((\Delta, \Delta'), (A, A')(\sigma, \sigma'))$ is $((\sigma, a), \lambda \nu\,\nu'. (\sigma'\,\nu\,\nu', a'\,\nu\,\nu'))$.

§.§ Type formers and operations

§.§.§ Dependent products

Let $(A, \angles{A', \fib_{A'}}) : \Type^*(\Gamma, \Gamma')$ and $(B, \angles{B', \fib_{B'}}) : \Type^*((\Gamma, \Gamma').(A, \angles{A', \fib_{A'}}))$.
We define the dependent product $\iPi^*((A, \angles{A', \fib_{A'}}), (B, \angles{B', \fib_{B'}})) = (\iPi(A, B), \angles{\iPi(A, B)', \fib_{\iPi(A, B)'}})$ where

\[
\iPi(A, B)'(\rho, \rho', f) = \Pi(a : \verts{A}\,\rho)(a' : A'\,\rho\,\rho'\,a). B'\,(\rho, a)\,(\rho', a')\,(\iapp(f, a))
\]

and $\fib_{\iPi(A, B)'}(\rho, \rho', f)$ is given by closure of $\CC$ under dependent product applied to $(\verts{A}\,\rho).2$, $\fib_{A'}\,\rho\,\rho'\,a$ for $a : \verts{A}\,\rho$, and $\fib_{B'}\,(\rho, a)\,(\rho', a')\,(\iapp(f, a))$ for additionally $a' : A'\,\rho\,\rho'\,a$.

Given an element $(b, b')$ of $(B, \angles{B', d}))$ in $\MM^*$, we define the abstraction $\iabs^*(b, b') = (\iabs(b), \iabs(b)')$ where
\iabs(b)'\,\rho\,\rho'\,a\,a' = b'\,(\rho, a)\,(\rho', a')

Given elements $(f, f')$ of $\iPi^*((A, \angles{A', c}), (B, \angles{B', d}))$ and $(a, a')$ of $(A, \angles{A', \fib_{A'}}))$ in $\MM^*$, we define the application $\iapp^*((f, f'), (a, a')) = (\iapp(f, a), \iapp(f, a)')$ where
\iapp(f, a)'\,\rho\,\rho' = f'\,\rho\,\rho'\,a\rho\,(a'\,\rho\,\rho')

§.§.§ Dependent sums

Let $(A, \angles{A', \fib_{A'}}) : \Type^*(\Gamma, \Gamma')$ and $(B,
\angles{B', \fib_{B'}}) : \Type^* ((\Gamma, \Gamma').(A, \angles{A', \fib_{A'}}))$.
We define the dependent sum $\iSigma^*((A, \angles{A', \fib_{A'}}), (B, \angles{B', \fib_{B'}})) = (\iSigma(A, B), \angles{\iSigma(A, B)', \fib_{\iSigma(A, B)'}})$ where

\[
\iSigma(A, B)'\,\rho\,\rho'\,(\ipair(a, b)) = \Sigma(a' : A'\,\rho\,\rho'\,a). B'\,(\rho, a)\,(\rho', a')\,b
\]

and $\fib_{\iSigma(A, B)'}\,\rho\,\rho'\,(\ipair(a, b))$ is given by closure of $\CC$ under dependent sum applied to $\fib_{A'}\,\rho\,\rho'\,a$ and $\fib_{B'}\,(\rho, a)\,(\rho', a')\,b$.

Given elements $(a, a')$ of $(A, \angles{A', \fib_{A'}})$ and $(b, b')$ of $(B, \angles{B', \fib_{B'}})[(a, a')]$ in $\MM^*$, we define the pairing $\ipair^*((a, a'), (b, b')) = (\ipair(a, b), \angles{a', b'})$.

Given an element $(\ipair(a, b), \angles{a', b'})$ of $\iSigma^*((A, \angles{A', \fib_{A'}}), (B, \angles{B', \fib_{B'}}))$ in $\MM^*$, we define the projections $\ifst^*(\ipair(a, b), \angles{a', b'}) = (a, a')$ and $\isnd^*(\ipair(a, b), {\angles{a', b'}}) = (b, b')$.

§.§.§ Universes

We define the universe $\iU_n^* : \Type^*(\Gamma, \Gamma')$ as $\iU_n^* = (\iU_n, \angles{\iU_n', \fib_{\iU_n'}})$ where $\iU_n'\,\rho\,\rho'\,A = \verts{A}\,\rho \to \Ufib_n$ and $\fib_{\iU_n'}\,\rho\,\rho'\,A$ is given by $\CC(\Ufib_n)$ and closure of $\CC$ under exponentiation (note that fibrancy of $\verts{A}\,\rho$ is not used).
We have carefully chosen our definitions so that we get $\Elem^*((\Gamma, \Gamma'), \iU_n^*) = \Type_n^*(\Gamma, \Gamma')$ and see that this identity is compatible with the action in $\MM^*$ of substitution on both sides.

§.§.§ Natural numbers

As per <ref>, we have a fibrant indexed inductive set $\N' \co \verts{\iN} \to \Ufib_0$ (where $\iN : \Type_0(1)$, hence $\verts{\iN} : \U_0$) with constructors $\zero' : \N'\,\izero$ and $\succ' : \Pi(n : \verts{\iN}\,\rho). \N'\,n \to \N'\,(\isucc\,n)$.

In context $(\Gamma, \Gamma') : \Con^*$, we then define $\iN^* = (\iN, \lambda \rho\,\rho'. \N')$.
We have $\izero^* = (\izero, \lambda \rho\,\rho'. \zero')$ and $\isucc^*(n, n') = (\isucc(n), \lambda \rho\,\rho'. \succ'\,n \rho\,\ \!n')$ for $(n, n') : \Elem^*((\Gamma, \Gamma'), \iN^*)$.

Given $(P, P') : \Type((\Gamma, \Gamma').\iN^*)$ with

\begin{align*}
(z, z') &: \Elem^*((\Gamma, \Gamma')(P, P')[\izero^*])
(s, s') &: \Elem^*((\Gamma, \Gamma').\iN^*.(P, P'), (P, P') (\pp, S^*(\qq)) \pp)
\end{align*}

and $(n, n') : \Elem^*((\Gamma, \Gamma'), \iN^*)$, we define the elimination

\[
\inatrec^*((P, P'), (z, z'), (s, s'), (n, n')) = (\inatrec(P, z, s, n), \lambda \rho\,\rho'. h'\,n \rho\,(n'\,\rho\,\rho'))
\]

where $h' : \Pi(m : \verts{\iN})(m' : \N'\,m). P'\,(\rho, m)\,(\rho', m')\,(\inatrec(P \rho^+, z \rho, s \rho^{+++}, m))$ is given by induction on $\N'$ with defining equations

\begin{align*}
h'\,\izero\,\zero' &= z'\,\rho\,\rho'
, &
h'\,(\isucc(n))\,(\succ'\,n\,n') &= s'\,(\rho, n, \inatrec(P, z, s, n))\,(\rho', n', h'\,n\,n')

§.§.§ Dependent paths

Let $\angles{A, A'} : \II \to \Type^*(\Gamma, \Gamma')$ and $(a_b, a_b') : \Elem^*((\Gamma, \Gamma'), (A\,b, A'\,b))$ for $b \in \braces{0, 1}$.
We then define the dependent path type $\iPath^*(\angles{A, A'}, (a_0, a_0'), (a_1, a_1')) : \Type^*(\Gamma, \Gamma')$ as the tuple $(\iPath(A, a_0, a_1), \angles{\iPath(A, a_0, a_1)', \fib_{\iPath(A, a_0, a_1)'}})$ where

\[
\iPath(A, a_0, a_1)'\,\rho\,\rho'\,(\ipabs(u)) = \Path_{\lambda(i : \II).\,(A'\,i\,\rho\,\rho'\,(u\,i)).1} (a'_0\,\rho\,\rho') (a'_1\,\rho\, \rho')
\]

and $\fib_{\iPath(A, a_0, a_1)'}\,\rho\,\rho'\,(\ipabs(u))$ is closure of $\CC$ under $\Path$ applied to $(A'\,i\,\rho\,\rho'\,(u\,i)).2$ for $i : \II$.

Given $\angles{u, u'} : \Pi(i : \II). \Elem^*((\Gamma, \Gamma'), (A\,i, A'\,i))$, we define the path abstraction as $\ipabs^*(\angles{u, u'}) = (\ipabs(u), \lambda \rho\,\rho'\,i. u'\,i\,\rho\,\rho')$.

Given $(p, p') : \Elem^*((\Gamma, \Gamma'), \iPath^*(\angles{A, A'}, (a_0, a_0'), (a_1, a_1')))$ and $i : \II$, we define the path application $\ipapp^*(p, i) = (\ipapp(p, i), \lambda \rho\,\rho'. u'\,\rho\,\rho'\,i)$.

§.§.§ Filling operation

Given $\angles{A, A'} : \II \to \Type^*(\Gamma, \Gamma')$, $\phi : \FF$, $b \in \braces{0, 1}$, and $\angles{u, u'} : \Pi(i : \II). [\phi] \vee (i = b) \to \Elem^*((\Gamma, \Gamma'), (A\,i, A'\,i))$, we have to extend $u$ to

\[
\ifill^*(\angles{A, A'}, \phi, b, \angles{u, u'}) : \Pi(i : \II). \Elem^*((\Gamma, \Gamma'), (A\,i, A'\,i))

We define $\ifill^*(\angles{A, A'}, \phi, b, \angles{u, u'}) = \angles{\ifill(A, \phi, b, u), \ifill(A, \phi, b, u)'}$ where

\[
\ifill(A, \phi, b, u)'\,i\,\,\rho\,\rho' : A'\,i\,\rho\,\rho'\,(\ifill(A, \phi, b, u)\,i)\rho
\]

is defined using $\fillop$ from (<ref>) as

\[
\ifill(A, \phi, b, u)'\,i\,\,\rho\,\rho' = \fillop(\lambda i. A'\,i\,\rho\,\rho'\,(\ifill(A, \phi, b, u)\,i)\rho, \phi, b, \lambda i\, x. u'\,i\,x\,\rho\,\rho')

§.§.§ Glue types

Before defining the glueing operation in $\MM^*$, we will develop several lemmas relating notions such as contractibility and equivalences in $\MM$ with the corresponding notions of <ref>.
Given $f : \Elem(\Gamma, A \to B)$ in $\MM$, we write
\efun{f} : \Pi(\rho : \verts{\Gamma}). \verts{A}\,\rho \to \verts{B}\,\rho
for $\efun{f}\,\rho\,a = \iapp(f \rho, a)$.
This notation overlaps with the action of $\verts{-}$ on elements, but we will not use that one here.

Just in this subsection, we will use the alternative definition via given left and right homotopy inverses instead of contractible homotopy fibers of both equivalences $\iEquiv$ in the cubical cwf $\MM$ and equivalences $\Equiv$ in the (current) internal language.
In both settings, there are maps back and forth to the usual definition, which are furthermore natural in the context in the case of the cubical cwf $\MM$.
The statements we will prove are then also valid for the usual definition.

Given $f : \Elem(\Gamma, A \to B)$ in $\MM$ with $\Elem(\Gamma, \iisEquiv(f))$, we have $\Pi(\rho : \verts{\Gamma}). \isEquiv(\efun{f}\,\rho)$.
This is natural in $\Gamma$.

A (left or right) homotopy inverse $g : \Elem(\Gamma, B \to A)$ to $f$ in $\MM$ becomes a (left or right, respectively) homotopy inverse $\efun{g}\,\rho$ to $\efun{f}\,\rho$ for $\rho : \verts{\Gamma}$.

Given $(f, f') : \Elem((\Gamma, \Gamma'), (A, A') \to (B, B'))$ in $\MM^*$, the following statements are logically equivalent, naturally in $(\Gamma, \Gamma')$:

\begin{align}
\label{equiv-in-sconing:0}
&\Elem((\Gamma, \Gamma'), \iisEquiv^*(f, f'))
\label{equiv-in-sconing:1}
&\Elem(\Gamma, \iisEquiv(f)) \times \Pi(\rho : \verts{\Gamma})(\rho' : \Gamma'\,\rho). \isEquiv(\Sigma_{\efun{f}\,\rho} f'\,\rho\,\rho')
\label{equiv-in-sconing:2}
&\Elem(\Gamma, \iisEquiv(f)) \times \Pi(\rho : \verts{\Gamma})(\rho' : \Gamma'\,\rho)(a : \verts{A}\,\rho). \isEquiv(f'\,\rho\,\rho'\,a)
\end{align}

where $\Sigma_{\efun{f}\,\rho} f'\,\rho\,\rho' : \Sigma(a : \verts{A}\,\rho)\, A'\,\rho\,\rho'\,a \to \Sigma(b : \verts{B}\,\rho)\, B'\,\rho\,\rho'\,b$.

Let us only look at homotopy left inverses.

For $\eqref{equiv-in-sconing:0} \to \eqref{equiv-in-sconing:1}$, a homotopy left inverse $(g, g')$ to $(f, f')$ in $\MM^*$ gives a homotopy left inverse $\Sigma_{\efun{g}\,\rho} g'\,\rho\,\rho'$ to $\Sigma_{\efun{f}\,\rho} f'\,\rho\,\rho'$ for all $\rho, \rho'$.

For $\eqref{equiv-in-sconing:1} \to \eqref{equiv-in-sconing:2}$, we use <ref> and note that a fiberwise map over an equivalence is a fiberwise equivalence exactly if it is an equivalence on total spaces (the corresponding statement for identity types instead of paths is <cit.>).

For $\eqref{equiv-in-sconing:2} \to \eqref{equiv-in-sconing:0}$, given a homotopy left inverse $g$ to the equivalence $f$ in $\MM$ and a homotopy left inverse $\overline{g}'\,\rho\,\rho'\,a : B'\,\rho\,\rho'\,(\efun{f}\,a) \to A'\,\rho\,\rho'\,a$ to $f'\,\rho\,\rho'\,a$ for all $\rho, \rho', a$, we use <ref> to transpose $\overline{g}'$ to the second component $g'\,\rho\,\rho'\,b : B'\,\rho\,\rho'\,b \to A'\,\rho\,\rho'\,(\efun{g}\,b)$ for all $\rho, \rho', b$ of a homotopy left inverse $(g, g')$ to $(f, f')$ in $\MM^*$.

We can now define glue types in $\MM^*$.
Let $(A, A') : \Type(\Gamma, \Gamma')$, $\phi : \FF$, $b \in \braces{0, 1}$, $\angles{T, T'} : [\phi] \to \Type(\Gamma, \Gamma')$, and $\angles{e, e'} : [\phi] \to \Elem((\Gamma, \Gamma'), \iEquiv^*((T \TT, T' \TT), (A, A')))$.

We define $\iGlue^*((A, A'), \phi, b, \angles{T, T'}, \angles{e, e'}) = (\iGlue(A, \phi, b, T, e), \angles{G', \fib_{G'}})$ where

\[
G'\,\rho\,\rho'\,(\iglue(a, t)) = \Glue\,(A'\,\rho\,\rho'\,a).1\,[\phi \mapsto (T'\,\TT\,\rho\,\rho'\,(t\,\TT), ((e'\,\TT\,\rho\,\rho').1\, (t \,\TT), w\,\TT\,\rho\,\rho'))]
\]

using the witness $w\,\TT\,\rho\,\rho'$ that $(e'\,\TT\,\rho\,\rho').1 \,(t \,\TT)$ is an equivalence provided by the direction from (<ref>) to (<ref>) of <ref> and $\fib_{G'}\,\rho\,\rho'\,(\iglue(a, t))$ is given by closure of $\CC$ under $\Glue$ applied to $(A'\,\rho\,\rho'\,a).2$ and $T'\,\TT\,\rho\,\rho'\,(t\,\TT)$ on $[\phi]$.

We define $\iunglue^* = (\iunglue, \iunglue')$ where $\iunglue'\,\rho\,\rho'\,(\iglue(a, t)) = \unglue$.

Given $(a, a') : \Elem((\Gamma. \Gamma'), (A, A'))$ and $(t, t') :
[\phi] \to \Elem((\Gamma, \Gamma'), (T\,\TT, T'\,\TT))$ such that
$\iapp^*(\ifst^*(e, e')\,\TT, (t, t')\,\TT) = (a, a')$ on $[\phi]$, we
define $\iglue^*((a, a'), (t, t'))$ as the pair $(\iglue(a, t), \iglue(a, t)')$ where $\iglue(a, t')\,\rho\,\rho' = \glue\,(a'\,\rho\,\rho')\,[\phi \mapsto t'\,\TT\,\rho\,\rho']$.

§.§ Main result

One checks in a mechanical fashion that the operations we have defined above satisfy the required laws, including stability under substitution in the context $(\Gamma, \Gamma')$.
We thus obtain the following statement.

Assume the parameters $\mathcal{C}, \II, \FF$ satisfy the assumptions of <ref>.
Then given any cubical cwf $\MM$ that is size-compatible in the sense of the beginning of <ref>, the sconing $\MM^*$ is a cubical cwf with operations defined as above.
We further have a morphism $\MM^* \to \MM$ of cubical cwfs given by the first projection.

§ HOMOTOPY CANONICITY

We fix parameters $\mathcal{C}, \II, \FF$ as before.
To make our homotopy canonicity result independent of <ref> concerning initiality of the term model, we phrase it directly using the initial model $\mathcal{I}$, initial in the category of cubical cwfs with respect to the parameters $\mathcal{C}, \II, \FF$.
Its existence can be justified generically following [28, 25].
It is size-compatible in the sense of <ref>: internally, $\Subst_{\mathcal{I}}(\Delta, \Gamma)$ and $\Elem_{\mathcal{I}}(\Gamma, A)$ live in the lowest universe $\U_0$ for all $\Gamma, \Delta, A$.

Assume the parameters $\mathcal{C}, \II, \FF$ satisfy the assumptions of <ref>.
In the internal language of presheaves over $\mathcal{C}$, given a closed natural $n : \Elem(1, \iN)$ in the
initial model $\mathcal{I}$, we have a numeral $k : \N$ with $p : \Elem(1, \iPath(\iN, n, \isucc^k(\izero)))$.

We start the arguing reasoning externally.
Using <ref>, we build the sconing $\mathcal{I}^*$ of $\mathcal{I}$.
Using initiality, we obtain a section $F$ of the cubical cwf morphism $\mathcal{I}^* \to \mathcal{I}$.

Let us now proceed in the internal language.
Recall the construction of <ref> of natural numbers in $\mathcal{I}^*$.
We observe that $\Sigma(n : \verts{\iN}). \N'\,n$ forms a fibrant natural number set (in the sense of <ref>).
It is thus homotopy equivalent to $\N$.
Under this equivalence, the first projection $\Sigma(n : \verts{\iN}). \N'\,n \to \verts{\iN}$ implements the map sending $k : \N$ to $\isucc^k(\izero).$

Inspecting the action of $F$ on $n : \Elem(1, \iN)$, we obtain $n' : \N'\,n$.
By the preceding paragraph, this corresponds to $k : \N$ with a path $p' : \II \to \verts{\iN}$ from $n$ to $\isucc^k(\izero)$.
Now $p = \ipabs(p')$ is the desired witness of homotopy canonicity.

§ EXTENSIONS

§.§ Identity types

Our treatment extends to the variation of cubical cwfs that includes identity types.

Identity types in a cubical cwf denoted as in <ref> consist of the following operations and laws (omitting stability under substitution), internal to presheaves over $\mathcal{C}$.
Fix $A$ in $\Type(\Gamma)$.
Given $x, y$ in $\Elem(\Gamma, A)$, we have $\iId(A, x, y)$ in $\Type(\Gamma)$, of level $n$ if $A$ is.
Given $a$ in $\Elem(\Gamma, A)$, we have $\irefl(a)$ in $\Elem(\Gamma, \iId(A, a, a))$.
Given $P$ in $\Type(\Gamma.A.A \pp.\iId(A \pp \pp, \qq \pp, \qq))$ and $d$ in $\Elem(\Gamma.A, P[\qq, \qq, \irefl(q)])$ and $x, y$ in $\Elem(\Gamma, A)$ and $p$ in $\Elem(\Gamma, \iId(A, x, y))$, we have $\iJ(P, d, x, y, p)$ in $\Elem(\Gamma, P[x, y, p])$.
We have $\iJ(P, d, a, a, \irefl(a)) = d[a]$.

We can interpret univalent type theory in any such cubical cwf as per <ref>.

The standard model of <ref> has identity type $\iId(\angles{A, \fib_A}, x, y) : \Type(\Gamma)$ given by $\Pi(\rho : \Gamma). \Id_{A\,\rho}\,(x\,\rho)\,(y\,\rho)$ using Andrew Swan's construction of $\Id$ referenced in <ref>.
We omit the evident description of the remaining operations.

To obtain homotopy canonicity in this setting, it suffices to extend the sconing construction $\MM^*$ of <ref> to identity types.
Given $A : \Type(1)$ and $A' : \verts{A} \to \Ufib_\omega$, we define $\Id'_{A, A'}$ as the fibrant indexed inductive set (as per <ref>) over $x, y : \verts{A}$, $p : \verts{\iId(A, x, y)}$, $x' : A'\,x$, $y' : A'\,y$ with constructor
\refl' : \Pi(a : \verts{A})(a' : A'\,a). \Id'_{A, A'}\,a\,a\,(\irefl(a))\,a'\,a'

Now fix $(A, A') : \Type^*(\Gamma, \Gamma')$.
Given $\rho : \verts{\Gamma}$, $\rho' : \Gamma'\,\rho$, and
elements $(x, x'), (y, y')$ of $(A, A')$ in $\MM^*$, we define

\[
\iId^*((A, A'), (x, x'), (y, y')) = (\iId(A, x, y), \lambda \rho\,\rho'\,p. \Id'_{A \rho, A'\,\rho\,\rho'}\,x \rho\ y \rho\ p\,(x'\,\rho\,\rho')\,(y'\,\rho\,\rho'))

Given an element $(a, a')$ of $(A, A')$ in $\MM^*$, we define $\irefl^*(a, a') = (\irefl(a), \irefl(a)')$ where $\irefl(a)'\,\rho\,\rho' = \refl'\,a \rho\ (a'\,\rho\,\rho')$.

For the eliminator, let

\begin{align*}
(C, C') &: \Type^*((\Gamma, \Gamma').(A, A').(A, A')p.\iId((A, A') \pp \pp, \qq \pp, \qq))
(d, d') &: \Elem^*((\Gamma, \Gamma').(A, A'), (C, C')[\qq, \qq])
\end{align*}

and $(x, x'), (y, y')$ in $\Elem^*((\Gamma, \Gamma'), (A, A'))$ and $(p, p')$ in $\Elem^*((\Gamma, \Gamma'), \iId((A, A'), (x, x'), (y, y'))$.
We define

The eliminator $\iJ((C, C'), (d, d'), (x, x'), (y, y'), (p, p'))$ is
defined as $(\iJ(C, d, x, y, p), \lambda \rho\,\rho'. h'\,x \rho\ y
\rho\ p \rho\
(x'\,\rho\,\rho')\,(y'\,\rho\,\rho')\,(p'\,\rho\,\rho'))$ where

\[
\begin{split}
h' : \Pi&(x\,y : \verts{A}\,\rho)(p : \verts{\iId(A, x, y)}\,\rho)(x' : A'\,\rho')(y' : A'\,\rho')(p' : \Id'_{A \rho, A'\,\rho\,\rho'}\,x\,y\,p\,x'\,y').
\\
& P'\,(\rho, x, y, p)\,(\rho', x', y, p')\,(\iJ(P \rho^{+++}, d \rho^+, x, y, p))
\end{split}
\]

is given by induction on $\Id'_{A \rho, A'\,\rho\,\rho'}$ via $h'\,a\,a\,(\irefl(a))\,a'\,a'\,(\refl'\,a\,a') = d'\,(\rho, a)\,(\rho', a')$.

§.§ Higher inductive types

Our treatment extends to higher inductive types [33], following the semantics presented in [6].
Crucially, we have fibrant indexed higher inductive sets in presheaves over $\mathcal{C}$ as we have what we would call fibrant uniformly indexed higher inductive sets in the same fashion as in [6] and fibrant identity sets [5, 23], mirroring the derivation of fibrant indexed inductive sets from fibrant uniformly indexed inductive sets and fibrant identity sets recollected in <ref>.
[We stress that the use of “set” in this context refers to the types of the language of presheaves over $\mathcal{C}$, not homotopy sets.]

Let us look at the case of the suspension operation in a cubical cwf, where $\isusp(A) : \Type(\Gamma)$ has constructors $\inorth, \isouth$ and $\imerid(a, i)$ for $a : A$ and $i : \II$ with $\imerid(a, 0) = \inorth$ and $\imerid(a, 1) = \isouth$.

For the sconing model of <ref>, we define for $A : \Type(1)$ and $A' : \verts{A} \to \Ufib_\omega$ the indexed higher inductive set $\susp'_{A, A'}$ over $\verts{\isusp(A)}$ with constructors

' : '_A, A'
' : '_A, A'
' a a' i :(A)'((a, i))[i=0↦',i=1↦']

for $a : \verts{a}$ and $a' : A'\,a$ and $i : \II$ (using the notation of [6]).
In the above translation to a uniformly indexed higher inductive set, the constructor $\north'$ will for example be replaced by $\north'' : \Id_{\verts{\isusp(A)}}\,u\,\inorth \to \isusp'_{A, A'}\,u$.

Given $(A, A') : \Type^*(\Gamma, \Gamma')$, we then define $\isusp^*(A, A') = (\isusp(A), \lambda \rho \rho'. \susp'_{A\rho, A'\,\rho\,\rho'})$, with constructors and eliminator treated as in <ref>.

§ STRICT CANONICITY

The goal of this section is to show “usual” or “strict” canonicity for
cubical type theory. It states that any closed term of type $N$ is strictly
equal to a numeral. This is a stronger result  than homotopy canonicity, but it
requires further computation rule for the filling operation.
We actually first modify the notion of cubical type theory by replacing
the filling by the composition operation (filling is then a derived operation
defined in term of composition), and we add computation rules
corresponding to the computation rules of [5].

We then expand on subsection <ref>, by making explicit the
interplay between internal and external reasoning that is used
here to simplify the presentation of the canonicity proof. (This interplay
was used implicitly in the justification of higher inductive types in
the work [6].) Using this interplay we explain how to build a
new “computability” model starting from any model, with a (strict) projection
map. The main point is how to define the right notion of computability structure,
and once this is done, we can essentially follow the argument in [7].
If we apply this to the initial (term) model, we get the canonicity
result: any closed natural number term is convertible to a numeral.
This result was already proved in [16], but
like for the proof in [7], our new argument completely avoids the
need to define a reduction relation, which is quite subtle for cubical
type theory in [16] since it is not closed under name substitution.

We assume in this section that the interval has a connection structure as in [23, 5, 6],
with operations written $r\wedge s$ and $~r\vee s$, and a reverse operation $1-r$.
We also assume the fact that the interval $\II$ is representable.
These assumptions are not all necessary (for instance, as in [5],
we can avoid the reverse operation at the cost of carrying around an external boolean
paramater) but they simplify the presentation.

§.§ Composition operations and computation rules

Given $A : \II \to \U_\omega$, we write $\hasComp(A)$ for the set of operations taking as
inputs $\phi$ in $\FF$ with a partial section $u$ in $\Pi (i : \II). [\phi] \vee (i = 0) \to A\,i$
and producing an element in $A\,1$ which is equal to $u\,1\,\TT$ on $\phi$.
Given a set $X$ and $Y : X \to \U_\omega$, we write $\Comp(X, Y)$ for
the set of composition  structures on $Y$, producing an element of $\hasComp(Y \cc x)$
for $x$ in $\II \to X$.
Given $s$ in $\Comp(X, Y)$ and $x, \phi, u$ as above, we write $s(x, \phi, u)$ for
the resulting element in $Y\,(x\,1)$.

We consider the constant presheaf $N$ of natural numbers. One important property
we use is that any function $\II\rightarrow N$ is constant. This follows from the fact
that $\II$ is representable and $N$ constant. In particular
$N$ has a composition operation, since we can define $\Comp(\psi,u) = u_0\TT$ for
any family $u_i : N$ over $\II$ defined on $(i = 0)\vee\psi$.

The filling operation is now a derived operation. We define

\[
\ifill(A,\phi,u)\,r = \icomp(A',\phi,u')
\]

where $A'\,i = A\,(i\wedge r)$ and $u'\,i = u\,(i\wedge r)$.

We change then the definition of cubical cwf in two ways.

We replace first the filling
operation by a composition operation.
We have $\icomp$ in $\Comp(\Type(\Gamma), \lambda A. \Elem(\Gamma, A))$ for $\Gamma$ in $\Con$
together with stability under substitution: given $A \co \II \to \Type(\Gamma)$, $\phi$ in $\FF$,
$u$ in $\Pi(i:\II).\, [\phi] \vee (i = 0) \to \Elem(\Gamma, A\,i)$, and $\sigma$ in $\Subst(\Delta, \Gamma)$ and $r : \II$, we have $\icomp(A, \phi, u) \sigma = \icomp(\lambda i.\, (A\, i) \sigma, \phi, \lambda i\,x.\, (u\,i\,x) \sigma)$.
We add next suitable computation rules for this composition operation, by case on the type, following
the computation rules in [5, 6]. We give here only two examples, for $\Sigma$-types and for
the type of natural numbers, and we comment the case of the “glue” type.
The other cases can be treated similarly.

* For dependent sums, we add the computation rule

\[
\icomp(\lambda_i.\,\iSigma(A\,i,B\,i),\psi,w) = \ipair(u,v)
\]

where $u = \tilde{u}\,1$ and $v = \icomp(\lambda_i.\,B\,i[\tilde{u}\,i],\psi,\lambda_i.\,\lambda_x.\,\isnd(w\,i\,x))$ using

\[
\tilde{u} = \ifill(\lambda_i.\,A\,i,\psi,\lambda._i\,\lambda_x.\,\ifst(w\,i\,x))

* For natural numbers, we add the computation rules

\[
\icomp(\lambda_i.\,\iN,\psi,b,\lambda_i\lambda_x.\izero) = \izero~~~~~~
\icomp(\lambda_i.\,\iN,\psi,b,\lambda_i\lambda_x.\isucc (v~i~x)) =
\isucc (\icomp(\lambda_i.\,\iN,\psi,b,v))
\]

§.§ Internal and external notions

In this section, we provide general comments expanding on <ref>
on how to simplify some
proofs about presheaf models by an interplay between eternal and
internal notions. This will then be used in the next section to build
a computability model associated to any model of cubical type theory.

We have defined internally $\Comp(T,A)$ for $T$ in $\Uw$
and $A$ in $T\rightarrow \Uw$.

We define next a dependent type $\CC$ over  $\Uw$. This is externally
a presheaf over the category of elements of $\Uw$ and this is
defined by taking the set  $\CC(X,A)$, for $A:X\rightarrow\Uw$ to be
$\Box \Comp(X,A)$. Note that we have defined $\Comp(T,A)$ for an arbitrary
$T$ in $\Uw$, but we only need it for $T$ representable.

For size reasons, this can be seen as a map $\CC:\Uw\rightarrow\Uw$.
A dependent version of Yoneda's Lemma shows that there is a bijection
between $\Box \Comp(X,A)$ and $\Box (\Pi_{x:X}C(Ax))$ for global $A:X\rightarrow\Uw$
where $X$ is a representable presheaf.
One can then show that we have a bijection between
$\Box \Comp(T,A)$ and
$\Box (\Pi (x:T)C(Ax))$ for any global presheaf $T$ and $A:T\rightarrow \Uw$.
This uses essentially that exponential with $\II$ preserves colimits.
In particular, for $T = \Sigma_{X:\Uw}C(X)$ this gives a global element
in $\Comp(T,\pi_1)$.

The type $\Sigma_{A:\Uw}C(A)$ is the type $\Ufib_\omega$.
It would be possible to unfold externally the definition of
$\CC(A)$ and prove directly properties of this operation using this definition,
but the use of the internal language allows for a significant simplification.

Let us illustrate on the example of the definition of the suspension map [6]
on $\Ufib_\omega$, using the interplay between
external and internal reasoning. One first defines $\susp:\Uw\rightarrow\Uw$ and
we want to build an element of $\Pi_{A:\Uw}C(A)\rightarrow C(\susp(A))$
so that we can see the suspension map as a map on $\Ufib_\omega$.
This means externally that we have to build a map $\CC(X,A)\rightarrow C(X,\susp A)$
for $A:X\rightarrow\Uw$ natural in $X$. This amounts to give a map

\Box (\Comp(X,A))\rightarrow \Box(\Comp(X,A))

natural in $X$. We solve this by building internally a map

\Comp(X,A)\rightarrow \Comp(X,\susp~A)

natural in $X$, and we define more generally

\Comp(T,A)\rightarrow \Comp(T,\susp~A)

for any $T$ and $A:T\rightarrow\Uw$ and showing that this map
is natural in $\Gamma$. (This is what is done implicitly in [6].)
Once more, we only need this map for $T$ representable, but it is more
natural to define it for arbitrary $T$.

The same method can be used to show that $\CC$ is closed by dependent product.
We need for this to build an element of

\Pi_{A:\Uw}\Pi_{B:A\rightarrow\Uw}(\CC(A)\rightarrow (\Pi_{a:A}\CC(Ba))\rightarrow \CC(\Pi~A~B))

and we reduce it to building internally a map

\Comp(\Gamma,A)\rightarrow\Comp(\Gamma.A,B)\rightarrow \Comp(\Gamma,\lambda_{\rho}\Pi~A\rho~B\rho)

for $A:\Gamma\rightarrow\Uw$ and $B:\Gamma.A\rightarrow\Uw$
which we show is natural in $\Gamma$.

We are going to use this method to build the computability model.

§.§ The computability model

Starting from any model $\MM$ of cubical type theory, we explain now
how to build a new model $\MM^*$, the associated computability model,
with a (strict) projection map $\MM^*\rightarrow\MM$.

We write $|\Gamma|$ for $1\rightarrow\Gamma$. This defines a family of types
over $\Con$.

If $A$ is in $\Type(1)$ we write $|A|$ for $\Elem(1,A)$
and we define $\Pred = \Sigma_{A:\Type(1)}|A|\rightarrow\Uw$.

We define externally a family $R(B,B')$ in $\Uw$
for $B,B'$ in $\Pred$. For this we use the general method described above
and define first an internal notion.
For $T$ a type and $\angles{A,A'}$ in $T\rightarrow\Pred$
we define $\Red(T,A,A')$ to be the type of operations $c$ taking as argument $\gamma$ in $F^{\II}$ and
$\psi$ in $\FF$ and a family $u_i,u'_i$ for $i=0\vee\psi$
with $u_i$ in $A\gamma(i)$ and $u'_i$ in $A'\gamma(i)u_i$
and producing an element $c(\gamma,\psi,u,u')$ in $A'\gamma(1)(c_A(\gamma,\psi,u))$.

We can see $A'$ as a computability structure on $A$, and an
element of $\Red(T,A,A')$ expresses that the composition structure
on $A$ is computable.

We define then a dependent type $R(A,A')$ for $A,A'$ in $\Pred$
by taking $R(X,A,A')$ for $\angles{A,A'}:X\rightarrow \Pred$
to be $\Box \Red(X,A,A')$.

We then have a natural bijection
between $\Box\Red(T,A,A')$ and $\Box (\Pi_{\rho:T}R(A\rho,A'\rho))$
for $\angles{A,A'}$ in $T\rightarrow\Pred$. In particular, for
$T = \Sigma_{A,A':\Pred}R(A,A')$ we get the following result.

There is an operation $c_A'$ which, given
a family $A_i,A_i',e_i$ and $\psi$ in $\FF$ and $u'_i$ in $A'_iu_i$
for $i=0\vee\psi$, produces an element $c_A'(\psi,u,u')$ in $A'_1(c_{\lambda_iA_i}(\psi,u))$.

Starting from an arbitrary model $\MM$ of cubical type theory, we build a new model $\MM^*$
using this family of types $R(A,A')$.

A context is a pair $\Gamma,\Gamma'$ where $\Gamma$ is a context of $\MM$ and
$\Gamma'$ is in $|\Gamma|\rightarrow \Uw$.

We define $\Type^*(\Gamma,\Gamma')$ to be the type of triples $A,A',e_A$
where $A$ is in $\Type(\Gamma)$ and $A'\rho\rho'$ is in $|A\rho|\rightarrow\Uw$
for $\rho$ in $|\Gamma|$ and $\rho'$ in $\Gamma'\rho$ and
$e_A\rho\rho'$ is in $R(A\rho,A\rho\rho')$.
We define then $(\Gamma,\Gamma').(A,A',e_A)$ to be
$\Gamma.A,(\Gamma.A')$ where
$(\Gamma.A)'(\rho,u)$ is $\Sigma_{\rho':\Gamma'\rho}A'\rho\rho'u$.

We define $\Elem^*((\Gamma,\Gamma'),(A,A',e_A))$ to be the type
of pairs $a,a'$ where $a$ is in $\Elem(\Gamma,A)$ and
$a'\rho\rho'$ is in $A'\rho\rho'(a\rho)$ for $\rho$ in $|\Gamma|$ and
$\rho'$ in $\Gamma'\rho$.

§.§.§ Example of sum type

Given $A,A'$ in $\Pred$ and $B:\Type(1.A)$
and $B':\Pi_{u:|A|}A'u\rightarrow |B[u]|\rightarrow \Uw$
we define $\iSigma(A',B')$ by

\iSigma(A',B')w = \Sigma (u':A' (\ifst(w)))B' (\ifst(w)) u' \isnd(w)

We want then to define an operation

R(A,A')\rightarrow (\Pi_{u:|A|,u':A'u} R(B[u],B'uu'))\rightarrow R(\iSigma(A,B),\iSigma(A',B'))\leqno{(1)}

We use then the method of reducing this to an internal operation.

Given $T$ and
$\angles{A,A'}$ in $T\rightarrow \Pred$
we write
$T.(A,A')$ for the type
of triples $\rho,u,u'$
with $\rho$ in $T$ and $u$ in $|A\rho|$ and $u'$ in $A'\rho u$.
Let $B:\Pi_{\rho:T}\Type(A\rho)$
and $B':\Pi_{\rho:T,u:|A\rho|}A'\rho\rightarrow |B\rho[u]|\rightarrow \Uw$
We define $B_1:T.(A,A')\rightarrow\Type(1)$ by $B_1(\rho,u,u') = B\rho[u]$
and $B_1':\Pi_{\rho,u,u':T.(A,A')}|B\rho[u]|\rightarrow\Uw$
by $B_1'(\rho,u,u') = B'\rho u u'.$

We can then define internally an operation

\Red(T,A,A')\rightarrow \Red(T.(A,A'),B_1,B_1')\rightarrow
\Red(T,\lambda_{\rho}\iSigma(A\rho,B\rho),\lambda_{\rho}\iSigma(A'\rho,B'\rho))\leqno{(2)}

and from this we get an element of $(1)$.

The definition of the operation satisfying $(2)$ uses in a crucial way
(as expected) the computation rules for composition and the following Lemma.

Given an element $e_A$ of $\Red(T,A,A')$ the filling operation on $A$ is “computable”:
if we have a family $\rho_i$ in $T$ and $\psi$ in $\FF$
and a partial family $u_i$ of elements in $|A\rho_i|$
together with $u_i'$ in $A'\rho_i u_i$
defined for $(i=0)\vee\psi$, then for any $r$ in $\II$ we can compute
$\ifill'(\rho,\psi,u,u')\,r$ in $A'\rho_r (\ifill(\rho,\psi,u))$.

We define $\ifill'(\rho,\psi,u,u')\,r = e_A(\lambda (i:\II) \rho_{i\wedge r},\psi,v,v')$
with $v~i~x = u~(i\wedge r)~x$ and $v'~i~x = u'~(i\wedge r)~x$.

We can use these results to interpret sum types in the model $\MM^*$.
Given $(A,A',e_A)$ in $\Type^*(\Gamma,\Gamma')$ and
$(B,B',e_B)$ in $\Type^*((\Gamma,\Gamma').(A,A',e_A))$
we define $T,T',e_T$ where $T = \iSigma(A,B)$ in $\Type^*(\Gamma,\Gamma')$.
We define $T'\rho\rho' w = \Sigma (u':A'\rho\rho'\ifst(w))B'(\rho,\ifst(w))(\rho',u')\isnd(w)$.
Given $\rho$ and $\rho'$ we have $A_1 = A\rho$ in $\Type(1)$ and
$A_1' = A'\rho\rho'$ in $|A_1|\rightarrow\Uw$. We also have $B_1 = B\rho^+$ in
$\Type(A_1)$ and $B_1 u u' = B'(\rho,\ifst(w))(\rho',u')$
$\Pi_{u:|A_1|}A_1'u\rightarrow |B_1[u]|\rightarrow \Uw$
since $B_1[u] = B\rho^+[u] = B(\rho,u)$. We can then define $T'\rho\rho'$
to be $\iSigma(A_1',B_1')$ and use $(1)$ to define $e_T\rho\rho'$.

§.§.§ Comment on the “glue” type

To simplify notation in this subsection, an element $a$ of a type
of the form $[\psi]\rightarrow A$ is desribed as a “partial”
element of $A$
“defined on $\psi$” and we write simply $a$ instead of $a\,\TT$.

We start by giving a simplified version of the external “glue” type,
$\Glue_s(C,\psi,D,v)$ where $v:D\rightarrow C$ is
defined on $\psi$, without requiring $v$ to be an equivalence. This type
is equal to $D$ on $\psi$ and we have a function
$\unglue$ of type $\Glue_s(C,\psi,D,v)\rightarrow D$ equal to the function $v$
on $\psi$.
This type does not need to be fibrant, but it can be described externally, in the
same (and actually simpler) way we build the $\Glue$ type.

Given $A,A'$ in $\Pred$ and $\psi$ in $\FF$ and a partial
$T,T'$ in $\Pred$ defined on $\psi$ with $u$ in $|T\rightarrow A|$
and $u'$ in $\Pi (t:|T|)T't\rightarrow A'(\iapp(u,t))$ defined on $\psi$
togther with an element $u_1$ in $\iisEquiv(T,A,u)$ we explain how
to define the computability structure $B'$ for $B = \iGlue(A,\psi,T,\ipair(u,u_1))$.

We define $B'b$ to be
$\Glue_s(A'(\iapp(\iunglue,b),\psi,T'b,u'b)$, since $u'b:T'b\rightarrow A'(\iapp(u,b))$
and $\iapp(u,b) = \iapp(\iunglue,b)$ on $\psi$.
Using the computation rule for the Glue type, it is then possible to build
an element of $R(B,B')$ given $e_A$ in $R(A,A')$ and $e_T$ in $R(T,T')$ defined on $\psi$
and given $u_1'$ in $\iisEquiv(u)'(u_1)$.
The way to build this element is similar to the case of the sum type.
by reducing this to describing internally an operation which expresses
that composition for the glue type is computable.

§.§.§ Natural numbers

We define $N$ to be the constant presheaf of natural numbers. We have
a canonical map $\QUOTE:N\rightarrow |\iN|$ sending $k$ to $\isucc^k(\izero)$
and this can be seen as a dependent type $\iN'$ over $|\iN|$. Using the fact that
any function $\II\rightarrow N$ is constant (since $\II$ is representable),
we have an element of $R(\iN,\iN')$
and this provides the interpretation of the type of natural numbers in the model

This is an important difference with the model used for proving homotopy canonicity:
the computability structure used in this case is not fibrant[Note that the family

$$\Sigma (k:N)\QUOTE(k)=_{|\iN|} x$$

for $x:|\iN|$ is fibrant
but would not work for showing homotopy canonicity since it would not satisfy the rules
for $\inatrec$.].

§.§ Proof of canonicity

Starting from any model $\MM$ of cubical type theory, we have
built a new model $\MM^*$, the associated computability model,
with a (strict) projection map $\MM^*\rightarrow\MM$. Like in [7],
if we apply this to the term model, we get that any closed term of type $N$
is “computable”, i.e. is strictly equal to a numeral.

§ CONCLUSION

We have given two proofs of canonicity for cubical type theory.
The first one proves homotopy canonicity and
proves only that a closed term of type $N$ is path equal to a numeral, but does
not need any computation rules for the composition operation of cubical
type theory. The second one proves a stronger form of canonicity: any
closed term of type $N$ is strictly equal to a numeral, relying on given
computation rules for the composition operation. This second argument relies
on an interplay between external reasoning (while the first can be formulated
internally) and hopefully can be refined to a proof of normalisation.

[1]
P. Aczel.
On Relating Type Theories and Set Theories.
In T. Altenkirch, B. Reus, and W. Naraschewski, editors, Types
for Proofs and Programs, volume 1657 of Lecture Notes in Computer
Science, pages 1–18. Springer Verlag, Berlin, Heidelberg, New York, 1999.

[2]
C. Angiuli, G. Brunerie, T. Coquand, K.-B. Hou (Favonia), B. Harper, and
D. Licata.
Cartesian cubical type theory.
preprint available from the home page of D. Licata, 2017.

[3]
Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson.
Parametricity and dependent types.
In ICFP '10, pages 345–356, 2010.

[4]
M. Bezem, T. Coquand, and S. Huber.
A Model of Type Theory in Cubical Sets.
In R. Matthes and A. Schubert, editors, 19th International
Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107–128.
Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2014.

[5]
C. Cohen, T. Coquand, S. Huber, and A. Mörtberg.
Cubical Type Theory: A Constructive Interpretation of the Univalence
In T. Uustalu, editor, 21st International Conference on Types
for Proofs and Programs (TYPES 2015), volume 69 of Leibniz
International Proceedings in Informatics (LIPIcs). Schloss
Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018.

[6]
T. Coquand, S. Huber, and A. Mörtberg.
On higher inductive types in cubical type theory.
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS '18, pages 255–264, New York, NY, USA, 2018. ACM.

[7]
Thierry Coquand.
Canonicity and normalization for dependent type theory.
Theoretical Computer Science, 2019.

[8]
P. Dybjer.
Internal Type Theory.
In Lecture Notes in Computer Science, pages 120–134. Springer
Verlag, Berlin, Heidelberg, New York, 1996.

[9]
Th. Ehrhard.
Une sémantique catégorique des types dépendants:
Application au Calcul des Constructions.
Phd thesis, University Paris VII, 1988.

[10]
S. Eilenberg.
On the relation between the fundamental group of a space and the
higher homotopy groups.
Fundamenta Mathematicae, 32(1):169–175, 1939.

[11]
P. Gabriel and M. Zisman.
Calculus of fractions and homotopy theory, volume 35 of Ergebnisse der Mathematik und ihrer Grenzgebiete.
Springer, 1967.

[12]
N. Gambino and J. Kock.
Polynomial functors and polynomial monads.
In Mathematical Proceedings of the Cambridge Philosophical
Society, volume 154, pages 153–192. Cambridge University Press, 2013.

[13]
N. Gambino and C. Sattler.
The frobenius condition, right properness, and uniform fibrations.
Journal of Pure and Applied Algebra, 221(12):3027–3068, 2017.

[14]
K. Gödel.
Über eine bisher noch nicht benützte Erweiterung des finiten
Dialectica, 12:280–287, 1958.

[15]
M. Hofmann.
Syntax and semantics of dependent types.
In A.M. Pitts and P. Dybjer, editors, Semantics and logics of
computation, volume 14 of Publ. Newton Inst., pages 79–130. Cambridge
University Press, Cambridge, 1997.

[16]
S. Huber.
Canonicity for cubical type theory.
Journal of Automated Reasoning, 2018.

[17]
A. Joyal.
Notes on clans and tribes, 2017.

[18]
C. Kapulkin and P. LeFanu Lumsdaine.
The simplicial model of univalent foundations (after Voevodsky).
arXiv preprint arXiv:1211.2851, 2012.

[19]
K. Kapulkin and V. Voevodsky.
Cubical approach to straightening.
preprint available from the home page of K. Kapulkin, 2018.

[20]
G.M. Kelly.
A unified treatment of transfinite constructions for free algebras,
free monoids, colimits, associated sheaves, and so on.
Bulletin of the Australian Mathematical Society, 22(1):1–83,

[21]
D. R. Licata, I. Orton, A. M. Pitts, and B. Spitters.
Internal Universes in Models of Homotopy Type Theory.
In Hélène Kirchner, editor, 3rd International Conference
on Formal Structures for Computation and Deduction (FSCD 2018), volume 108
of Leibniz International Proceedings in Informatics (LIPIcs), pages
22:1–22:17. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018.

[22]
P. LeFanu Lumsdaine and M. Shulman.
Semantics of higher inductive types.
arXiv preprint arXiv:1705.07088, 2017.

[23]
I. Orton and A. M. Pitts.
Axioms for modelling cubical type theory in a topos.
In 25th EACSL Annual Conference on Computer Science Logic (CSL
2016), volume 62 of Leibniz International Proceedings in Informatics
(LIPIcs), pages 24:1–24:19, Dagstuhl, Germany, 2016. Schloss
Dagstuhl–Leibniz-Zentrum für Informatik.

[24]
E. Palmgren and S.J. Vickers.
Partial horn logic and cartesian categories.
Annals of Pure and Applied Logic, 145(3):314 – 353, 2007.

[25]
Erik Palmgren and Steven J Vickers.
Partial horn logic and cartesian categories.
Annals of Pure and Applied Logic, 145(3):314–353, 2007.

[26]
E. Riehl and M. Shulman.
A type theory for synthetic $\infty$-categories.
Higher Structures, 1(1), 2018.

[27]
M. Shulman.
Univalence for inverse diagrams and homotopy canonicity.
Mathematical Structures in Computer Science, 25(5):1203–1277,

[28]
Jonathan Sterling.
Algebraic type theory and universe hierarchies.
arXiv preprint arXiv:1902.08848, 2019.

[29]
T. Streicher.
Semantics of Type Theory.
Progress in Theoretical Computer Science. Birkhäuser Basel, 1991.

[30]
A. Swan.
An algebraic weak factorisation system on 01-substitution sets: A
constructive proof.
Journal of Logic & Analysis, 8(1):1–35, 2016.

[31]
A. Swan.
Semantics of higher inductive types, 2017.
On the HoTT mailing list.

[32]
W. W. Tait.
Intensional interpretations of functionals of finite type I.
Journal of Symbolic Logic, 32(2):198–212, 1967.

[33]
The Univalent Foundations Program.
Homotopy Type Theory: Univalent Foundations of Mathematics.
<http://homotopytypetheory.org/book>, Institute for Advanced
Study, 2013.

[34]
V. Voevodsky.
The equivalence axiom and univalent models of type theory. (Talk at
CMU on February 4, 2010).
Preprint arXiv:1402.5556 [math.LO], 2014.

§ RULES OF THE TERM MODEL

We denote the objects of our base category $\mathcal{C}$ by $X,Y,Z$
and its morphisms by $f,g,h$.  In the term model $\Syn$ morphisms $f
\co Y \to X$ act on judgments at stage $X$ via an implicit
substitution, while for substitutions on object variables we will use
explicit substitutions.  For this to make sense we first define the
raw expressions as a presheaf: at stage $X$ this is given by

\[
\begin{array}{rcl}
\Gamma,\Delta &::=
& \emptyctx \mid \Gamma.A
\\
A,B,t,u,v & ::=
& \qq \mid t \sigma \mid
% univ
\iU_n \mid
% pi
\iPi (A,B) \mid \iabs (u) \mid \iapp (u,v)
\\
& \mid
% sigma
\iSigma (A,B) \mid \ipair (u,v) \mid \ifst(u)
\mid \isnd (u)
% path
\\
& \mid
\iPath (\bar A,u,v) \mid \ipabs \bar u \mid \ipapp (u,r)
\\
& \mid
& \iGlue (A, \phi, \bar B, \bar u)
\mid \iglue (v,\bar u) \mid \iunglue (u)
\\
& \mid
& \ifill (\bar A, \phi, b, \bar u, r)
\mid \dots
\\
\bar A, \bar B, \bar u, \bar v
&::=& (A_{f,r})_{f,r} \mid (A_f)_{f \in [\phi]}
\\
\sigma,\tau,\delta
&::=& \pp \mid \id \mid \sigma \tau \mid
(\sigma,u) \mid \emptysubst
% \\
% r & \in & \II (X)
% \\
% \phi & \in & \FF (X)
\end{array}
\]

where $b \in \braces{0,1}$, $\phi \in \FF (X)$, and we skipped the
constants for natural numbers.  Above, we have families of
expressions, say $\bar A = (A_{f,r})_{f,r}$, whose index set ranges
over certain $Y$, $f \co Y \to X$, and $r \in \II(Y)$, and $A_{f,r}$
is a raw expression at stage $Y$; likewise $(A_f)_{f \in [\phi](X)}$
consists of raw expressions $A_f$ at stage $Y$ for $f \co Y \to X$ in
the sieve $[\phi]$ on $X$.  (The exact index sets will be clear from
the typing rules below.)  All other occurrences of $r$ above have $r
\in \II(X)$.  The restrictions along $f \co Y \to X$ on the raw syntax
then leave all the usual cwf structure untouched, so we have $\qq f =
\qq$ and $(\iPi (A,B))f = \iPi (A f, Bf)$, and uses the restrictions
in $\II$ and $\FF$ accordingly, , $(\ipapp (u,r)) f = \ipapp (uf ,
r f)$, and we will re-index families according to ${\bar A} f =
(A_{gf,rf})$ for $\bar A = (A_{g,r})_{g,r}$.

To get the initial cubical cwf we in fact need more annotations
to the syntax in order to be able to define a partial interpretation
(cf. [29, 15]) on the raw syntax.  But to enhance
readability we suppress these annotations.

We will now describe a type system indexed by stages $X$.  The forms
of judgment are:

Γ_X A
Γ_X A = B
Γ_X t : A
Γ_X t = u : A
σΔ→_X Γ
where the involved expressions are at stage $X$.

In cubical type theory as described in [5] we did not index
judgments by objects $X$ but allowed extending context by interval
variables instead.  Loosely speaking, a judgment $\Gamma
\der_{\braces{i_1,\dots,i_n}} \JJ$ corresponds to $i_1 : \II, \dots,
i_n : \II, \Gamma \der \JJ$ given the setting of [5].

As mentioned above
we have the rule:

f Y →X Γf _Y f

At each stage we have all the usual rules valid in a cwf with
$\Pi$-types, $\Sigma$-types, universes, and natural numbers.  We will
present some of the rules, but skip all congruence rules.

Γ_X AΓ.A_X

Γ_X A
Δ_X Aσ

Γ_X t:A
Δ_X tσ:Aσ

Γ_X AΓ.A_X :A

Γ_X t : A
Γ_X A = B Γ_X t : B

Γ_X𝕀Γ→_X Γ

Γ_X AΓ.A→_XΓ

σΔ→_X Γ
τΘ→_X Δ
στΘ→_X Γ

Γ_X A

Δ_X u:Aσ

Γ.A_X BΓ_X(A,B)

Γ.A_X B
Γ.A_X b:B

Γ_X w:(A,B)
Γ_X u:A
Γ_X (w,u):B[u]

where we write $[u]$ for $(\id,u)$ and $\sigma^+$ for $(\sigma \pp,
\qq)$.  The judgmental equalities (skipping suitable premises, types,
and contexts) are:

𝕀  σ= σ  𝕀= σ
(στ)δ= σ(τδ)
(σ,u)δ= (σδ,uδ) (σ,u) =
σ(σ,u) = u (, ) = 𝕀A   𝕀= A (A σ) δ= A (σδ) u
𝕀= u (u σ) δ= u (σδ)

((A,B))σ= (Aσ,B σ^+) ((b)) σ= (b σ^+)
(w,u)δ= (wδ,uδ)((b),u)=
b[u]w = ((w , ))

We skip the rules for $\Sigma$-types and natural numbers as they are
standard, but simply indexed with an object $X$ as we did for
$\Pi$-types.  The rules for universes are:

Γ_X Γ_X _n

Γ_X Γ_X _n : _n+1

Γ_X A : _n Γ_X A : _n+1

Γ_X A : _n Γ_X A

and we skip the rules for equality and closure under the type formers
$\iPi$,$\iSigma$, natural numbers, $\iPath$, and $\iGlue$.

To state the rules for dependent path-types we introduce the following
abbreviations.  We write $\Gamma.\II \der_X \bar A$ if $\bar A =
(A_{f,r})$ is a family indexed by $Y$, $f\co Y \to X$, and $r \in
\II(Y)$ such that

\[
\Gamma f \der_Y A_{f,r} \text{ and } \Gamma f g\der_Z (A_{f,r})g =
\]

Given $\Gamma.\II \der_X \bar A$ we write $\Gamma.\II\der_X \bar u :
\bar A$ whenever $\bar u = (u_{f,r})$ is a family indexed by $Y$,
$f\co Y \to X$, and $r \in \II(Y)$ such that

\[
\Gamma f \der_Y u_{f,r} : A_{f,r} \text{ and } %
\Gamma f g \der_Z (u_{f,r})g = u_{fg,rg} : A_{fg,rg}.
\]

The rules for the dependent path type are:

Γ._X A̅

Γ_X u: A_𝕀_X,0

Γ_X u: A_𝕀_X,1

Γ_X (A̅,u,v)

Γ._X A̅

Γ._X u̅ : A̅

Γ_X (u̅) : (A̅, u_𝕀_X,0, u_𝕀_X,1)

Γ_X t : (A̅,u,v)
r ∈(X)
Γ_X (t,r) : A_𝕀_X,r

((u̅), r) = u_𝕀,r
t = ((t f, r)_f,r)
(A̅, u, v) σ= ((A_f,r σf)_f,r, u σ, v
((u̅)) σ= ((u_f,r σf)_f,r)
((t,r)) σ= (t σ, r)

Note that in general these rules might have infinitely many premises.
We get the non-dependent path type for $\Gamma \der_X A$ by using the
family $A_{f,r} := Af$.

Given $\Gamma.\II \der_X \bar A$ and $b \in \braces{0,1}$ we write
$\Gamma.\II \der_X^{\phi,b} \bar u : \bar A$ for $\bar u = (u_{f,r})$ a
family indexed over all $Y$, $f \co Y \to X$, and $r \in \II(Y)$ such
that either $f$ is in the sieve $[\phi]$ or $r = b$ and we have

\[
\Gamma f \der_Y u_{f,r} : A_{f,r} \text{ and } \Gamma f g \der_Z
(u_{f,r})g = u_{fg,rg} : A_{fg,rg}
\]

for all $g \co Z \to Y$.  The rule for the filling operation is given

Γ._X A̅

b ∈0,1

Γ._X^ϕ,b u̅ : A̅

r ∈(X)

Γ_Y (A̅,ϕ,b,u̅,r) : A_𝕀,r

with judgmental equality

(A̅,ϕ,b,u̅,r) = u_𝕀,r  whenever  [ϕ]
is the maximal sieve or  r= b.

For the glueing operation we only present the formation rule; the
other rules are similar as in [5] but adapted to our setting.
We write $\Gamma \der_X^\phi \bar B$ if $\bar B$ is a family of $B_f$
for $f \co Y \to X$ in $[\phi]$ with $\Gamma f \der_Y B_f$ which is
compatible, $\Gamma f g \der_Z B_{f}g = B_{fg}$.  In this case, we
write likewise $\Gamma \der_X \bar u : \bar B$ if $\bar u$ is a
compatible family of terms $\Gamma f \der_Y u_f : B_f$.

Γ_X A

Γ_X^ϕu̅ : (B̅,A)

Γ_X (A,ϕ,B̅, u̅)

and the judgmental equality $\iGlue (A,\phi,\bar B, \bar u) = B_\id$
in case $[\phi]$ is the maximal sieve, and an equation for

This formal system gives rise to a cubical cwf $\Syn$ as follows.
First, define judgmental equality for contexts and substitutions as
usual (we could also have those as primitive judgments).  Next, we
define presheaves $\Con$ and $\Subst$ on $\mathcal{C}$ by taking, say,
$\Con (X)$ equivalence classes $\eqcl \Gamma$ of $\Gamma$ with $\Gamma
\der_X$ modulo judgmental equality; restrictions are induced by the
(implicit) substitution: $\eqcl{\Gamma} f = \eqcl{\Gamma f}$.  Types
$\Type(X,\eqcl{\Gamma})$ are equivalence classes of $A$ with $\Gamma
\der_X A$ modulo judgmental equality, and elements are defined
similarly as equivalence classes.

For type formers in $\Syn$ let us look at path types: we have to give
an element of $\Type(\Gamma)$ in a context (w.r.t. the internal
language) $\Gamma : \Con, A : \II \to \Type(\Gamma), u :
\Elem(\Gamma,A\,0), v : \Elem(\Gamma, A\,1)$.  Unfolding the use of
internal language, given $\eqcl{\Gamma} \in \Con(X)$, a compatible
family $\eqcl{A_{f,r}} \in \Type(Y,\eqcl{\Gamma} f)$ (for $f \co Y \to
X$ and $r \in \II(Y)$) and elements $\eqcl{u} \in
\Elem(\eqcl{\Gamma},\eqcl{A_{\id,0}})$ and $\eqcl{v} \in
(\eqcl{\Gamma},\eqcl{A_{\id,1}})$, we have to give an element of
$\Type (X,\eqcl{\Gamma})$, which we do by the formation rule for

The remainder of the cubical cwf structure for $\Syn$ is defined in a
similar manner, in fact the rules are designed to reflect the laws of
cubical cwfs. We conjecture that we can follow a similar argument as in
[29] to show that $\Syn$ is the initial cubical
cwf.  Given a cubical cwf $\MM$ over $\mathcal{C},\II,\FF$ we first
have to define partial interpretations of the raw syntax and
then show that each derivable judgment has a defined interpretation in
$\MM$, and for equality judgments both sides of the equation have a
defined interpretation in $\MM$ and are equal.  In an intuitionistic framework,
this partial interpretation should be described as an inductively defined relation,
which is shown to be functional. The partial
interpretation $\brackss{ - }$ assigns meanings to raw judgments with
the following signature:

\begin{equation*}
\begin{array}{lll}
\brackss{\Gamma \der_X}
& \in \Con_\MM (X)
\\
\brackss{\sigma : \Delta \to \Gamma}
& \in \Subst_\MM (X,\brackss{\Delta \der_X},\brackss{\Gamma \der_X})
\\
\brackss{\Gamma \der_X A}
& \in \Type_\MM (X, \brackss{\Gamma \der_X})
\\
\brackss{\Gamma \der_X u : A}
& \in \Elem_\MM (X,  \brackss{\Gamma \der_X}, \brackss{\Gamma \der_X A})
\end{array}
\end{equation*}

where among the conditions for the interpretation on the left-hand
side to be defined is that all references to the interpretation on the
right-hand side are defined.  This proceeds by structural induction on
the raw syntax and for $\brackss{\Gamma \der_X \JJ}$ to be defined we
assume all the ingredients needed are already defined.  for the
path type $\brackss{\Gamma \der_X \iPath (\bar A,u,v)}$ we in
particular have to assume that the assignment $f, r \mapsto
\brackss{\Gamma f \der_Y A_{f,r}}$ is defined and gives rise to a
suitable input of $\iPath_\MM$.

§ INDEXED INDUCTIVE SETS IN PRESHEAVES OVER $\MATHCAL{C}$

We work in the setting of <ref> given by presheaves over $\mathcal{C}$.

Given a set $I$, a family $A$ over $I$, a family $B$ over $i : I$ and $a : A\,i$, and a map

\[
s : \Pi(i : I)(a : A\,i). B\,i\,a \to I

the indexed inductive set $\W_{I, A, B, s}$ is the initial algebra of the polynomial endofunctor [12] on the (internal) category of families over $I$ sending a family $X$ to the family

\[
\brackss{I, A, B, s}\,i = \Sigma(a : A\,i). \Pi(b : B\,i\,a). X(s\,i\,a\,b)

Its constructive justification as an operation in the internal language of the presheaf topos using inductive constructions of the metatheory is folklore (in a classical setting, one would use transfinite colimits [20]).

If $I, A, B$ are small with respect to a universe $\U_i$ with $i \in \braces{0, 1, \ldots, \omega}$, then $\W_{I, A, B, s} : I \to \U_i$.

Let $I, A, B$ now be small with respect to $\U_\omega$.
Given elements of $\Fill(I, A)$ and $\Fill(\Sigma(i : I). A\,i, \lambda{(i, a)}. B\,i\,a)$, we may use induction (the universal property of $W_{I, A, B, s}$) to derive an element of $\Fill(I, \W_{I, A, B, s})$.
As in <ref> for dependent products, this implies (using external reasoning) the internal statement $\CC(\W_{I, A, B, s}\,i)$ for $i : I$ given $\CC(A\,i)$ for all $i$ and $\CC(B\,i\,a)$ for all $i, a$.
We then call $W_{I, A, B, s}$ a fibrant uniformly indexed inductive set.
The qualifier uniformly indexed indicates that $A$ is a fibrant family over $I$ rather than a fibrant set with a “target” map to $I$ that indicates the target sort of the constructor $\sup$.

Given $A : \U_\omega$ with $\Fill(1, A)$, we may use the technique of Andew Swan [30, 23] to construct a (level preserving) identity set $\Id_A\,a_0\,a_1$ for $a_0, a_1 : A$ (different from the equality set $a_0 = a_1$) with $\Fill(A \times A, \lambda(a_0, a_1). \Id_A\,a_0\,a_1))$ and constructor $\refl_a : \Id_A\,a\,a$ for $a : A$ that has the usual elimination with respect to families $P : \Pi(a_0\,a_1 : A). \Id_A\,a_0\,a_1 \to \U_\omega$ that satisfy $\Fill(\Sigma(a_0\,a_1 : A). \Id_A\,a_0\,a_1, P)$.
Using external reasoning as before, one has $\CC(\Id_A\,a_0\,a_1)$ given $\CC(A)$, justifying calling $\Id_A\,a_0\,a_1$ a fibrant identity set; using (<ref>) one has elimination with respect to families $P$ of the previous signature with $\CC(C\,a_0\,a_1\,p)$ for all $a_0, a_1, p$.

Using a folklore technique, we may use fibrant identity sets to derive fibrant indexed inductive sets from fibrant uniformly indexed inductive sets, by which we mean the following.
Given $(I, \fib_I) : \Ufib_\omega$, $(A, \fib_A) : \Ufib_\omega$, $\angles{B, \fib_B} : A \to \Ufib_\omega$ with maps $t : A \to I$ and $s : \Pi(a : A). B\,a \to I$, we have $\angles{W_{I, A, B, s, t}, \fib_W} : I \to \Ufib_\omega$ (we omit the subscripts to $W$ for readability), $W$ living in $\U_i$ if $I, A, B$ do,  with

\[
\sup : \Pi(a : A)(f : \Pi(b : B\,a). W\,(s\,a\,b)). W\,(t\,a)

Given $\angles{P, \fib_P} : \Pi(i : I). W \to \Ufib_\omega$ with

\[
h : \Pi(a : A)(f : \Pi(b : B\,a). W\,(s\,a\,b)). (\Pi(b : B\,a). P\,(s\,a\,b)\,(f\,b)) \to P\,(t\,a)\,(\sup\,a\,f)

we have $v : \Pi(i : I)(w : W\,i). P\,i\,w$ such that

\[
v\,(t\,a)\,(\sup\,a\,f) = h\,a\,f\,(\lambda{b}. v\,(s\,a\,b)\,(f\,b)

Fibrant indexed inductive sets are used for the interpretation in the sconing model of natural numbers in <ref>, higher inductive types in <ref>, and identity types in <ref>.
In practise, we will usually not bother to bring the fibrant indexed inductive set needed in into the above form and instead work explicitly with the more usual specification in terms of a list of constructors, each taking a certain number non-recursive and recursive arguments.
Note that the latter is really an instance of the former since our dependent sums, dependent products, and finite coproducts are extensional (satisfy universal properties).
Conversely, the former is an instance of the latter with a single constructor taking a non-recursive and a recursive argument.
For convenience, we explain concretely the example needed in <ref> of the fibrant indexed inductive set $\N'$ over

As an example, we construct the fibrant indexed inductive set $\N'$ needed in <ref>.
There, we have a fibrant set $\verts{\iN} : \U_0$ (satisfying $\CC(\verts{\iN})$) with an element $\izero : \verts{\iN}$ and an endofunction $\isucc : \verts{\iN} \to \verts{\iN}$.
We wish to define the fibrant indexed inductive set $\N' : \verts{\iN} \to \U_0$ with constructors $\zero' : \N'\,\izero$ and $\succ' : \Pi(n : \verts{\iN}\,\rho). \N'\,n \to \N'\,(\isucc\,n)$.
We let $\N'$ be the uniformly indexed inductive set over $m : \verts{\iN}$ with constructors

\begin{align*}
\zero'' &: \Id_{\verts{\iN}}\,m\,\izero \to \N'\,m
\succ'' &: \Pi_{n : \verts{\iN}}. \Id_{\verts{\iN}}\,m\,(\isucc\,n) \to \N'\,n \to \N'\,m

and define $\zero' = \zero''\,\refl_\izero$ and $\succ'\,n\,n' = \succ''\,n\,\refl_{\isucc(n)}\,n'$.
Fibrancy of $\Id$ ensures fibrancy of $\N'$ ($\CC(\N'\,n)$ for $n : \verts{\iN}$).
For elimination, we are given a fibrant family $P\,n\,n'$ for $n : \verts{\iN}$ and $n' : \N'\,n$ with $z' : P\,\izero\,\izero'$ and $s'\,n\,n'\,x : P\,(\isucc\,n)\,(\isucc'\,n\,n')$ for all $n, n'$ and $x : P\,n\,n'$.
We have to define $h'\,n\,n' : P\,n\,n'$ for all $n, n'$ such that $h'\,\izero\,\izero' = z'$ and $h'\,(\isucc\,n)\,(\isucc'\,n\,n') = s'\,n\,n'\,(h'\,n\,n')$.
We define $h'$ by induction on the uniformly indexed inductive set $\N'$ and fibrant identity sets (using fibrancy of $P$) via defining equations

\begin{align*}
h'\,\zero''\,\refl_\izero &= z
h'\,(\isucc n)\,(\succ''\,n\,\refl_{\isucc\,n}\,n') &= s'\,n\,n'\,(h'\,n\,n')

§ VARIATIONS

§.§ Univalence as an axiom

Our treatment extends to the case where the glue types in a cubical cwf as in <ref> are replaced by an operation $\Elem(\Gamma, \iUnivalence_n)$ for $\Gamma : \Con$ and $n \geq 0$, with $\iUnivalence_n$ defined in <ref>.

To define this operation in the sconing model of <ref>, one first shows analogously to <ref> that $\verts{-}$ preserves contractible types and that $(A, A') : \Type^*(\Gamma, \Gamma')$ is contractible exactly if $A$ is contractible and $A'\,\rho\,\rho'\,a$ for $\rho : \verts{\Gamma}$ and $\rho' : \Gamma'\,\rho$ where $a : \verts{A}$ is the induced center of contraction.
We have analogous statements for types of homotopy level $n \geq 0$i in $\MM$, in which case we instead have to quantify over all $a : \verts{A}$.

Given $(A, A') : \Type_n^*(\Gamma, \Gamma')$, we have show that the type $(S, S') = \iSigma^*(\iU_n, \Equiv^*(\qq, A))$ over $(\Gamma, \Gamma')$ is contractible in $\MM^*$.
Without loss of generality, we may assume the center of contraction of univalence in $\MM$ is given by the identity equivalence.
Using the observations of the preceding paragraph, it suffices to show that $V' = S'\,\rho\,\rho'\,(\ipair(A \rho, (\iabs(\qq), w)))$ is contractible for $\rho : \verts{\Gamma}$ and $\rho' : \Gamma'\,\rho$ where $w$ denotes the canonical witness that the identity map $\iabs(\qq)$ on $A \rho$ is an equivalence in $\MM$.
Inhabitation is evident, and so it remains to show propositionality.
By the case of the preceding paragraph for propositions, the second component of $V'$ is a proposition, and thus we can ignore it for the current goal, which then becomes

\[
\isProp \parens[\big]{\Sigma(T' : \verts{A} \to \U_n). \Pi(a : \verts{A}). \Equiv(T'\,a, A'\,\rho\,\rho'\,a)}
\]

and follows from univalence in the standard model, justified by glueing.

§ SIMPLICIAL SET MODEL

Choosing for $\mathcal{C}$ the simplex category $\Delta$, for $\II$ the usual interval $\Delta^1$ in simplicial sets, and for $\FF$ a small copy $\Omega_{0,\dec}$ of the sublattice of $\Omega_0$ of decidable sieves, we obtain a notion of cubical cwf with a simplicial notion of shape.

Assume now the law of excluded middle.
The above choice of $\mathcal{C}, \II, \FF$ satisfies all of the assumptions of <ref> but one: the existence of a right adjoint to exponentiation with $\II$.
However, the only place our development makes use of this assumption is in establishing (<ref>).
We will instead give a different definition of $\CC$ that still satisfies (<ref>).
Then the rest of our development still applies to simplicial sets.

A Kan fibration structure on a family $Y \co X \to \U_\omega$ in simplicial sets consists of a choice of diagonal fillers in all commuting squares of the form

Σ(x:X). Y x

with left map a horn inclusion.
Note that the codomains of horn inclusions are representable.
It follows that the presheaf of Kan fibration structures indexed over the slice of simplicial sets over $\U_\omega$ is representable.
Given $[n] \in \Delta$ and $A \in (\U_\omega)_n$ (an $\omega$-small presheaf on $\Delta/[n]$), we define $\CC([n], A)$ as the set of Kan fibration structures on $A \co \Delta^n \to \U_\omega$.
This defines a level preserving map $\CC \co \U_\omega \to \U_\omega$.
Then the representing object of the above presheaf is given by the first projection $\Ufib_\omega \to \U_\omega$ where $\Ufib_\omega = \Sigma(X:\U_\omega). \CC(X)$ is defined as before.

Let us now verify (<ref>).
Given a simplicial set $X$ with $Y \co X \to \U_\omega$, a global element of $\Fill(X, Y)$ corresponds to a uniform Kan fibration structure on $\Sigma(x:X)\,(Y\,x) \to X$ in the sense of [13].
A uniform Kan fibration structure induces a Kan fibration structure naturally in $X$, giving the forward direction of (<ref>).
For the reverse direction, it suffices to give a uniform Kan fibration structure in the generic case, a global element of $\Fill(\Ufib_\omega, \lambda (A, c). A)$.
This is <cit.> together with the fact proved in <cit.> that Kan fibrations lift against pushout products of interval endpoint inclusions with (levelwise decidable) monomorphisms.
[This is the only place where excluded middle is used, to produce a cellular decomposition in terms of simplex boundary inclusions of such a monomorphism.]

Having verified (<ref>), the rest of our development applies just as well to the case of simplicial sets.
In particular, we obtain in the standard model $\Std$ of <ref> a version of the simplicial set model [18] of univalent type theory (using <ref> for identity types).
[Instead of Kan fibration structures, we can also work with the property of being a Kan fibration.
Then $\CC$ is valued in propositions and we would obtain in $\Std$ a version of the simplicial set model in which being a type is truly just a property.
However, choice would be needed to obtain (<ref>).]
As per <ref>, we furthermore obtain higher inductive types in the simplicial set model in a way that avoids (as suggested by Andrew Swan [31]) the pitfall of fibrant replacement failing to preserve size encountered in [22].

Seeing simplicial sets as a full subtopos of distributive lattice cubical sets as observed in [19], there is a functor from cubical cwfs with $(\mathcal{C}, \II, \FF) = (\Delta, \Delta^1, \Omega_{0,\dec})$ to cubical cwfs where $\mathcal{C}$ is the Lawvere theory of distributive lattices, $\II$ is represented by the generic object, and $\FF$ is the (small) sublattice of $\Omega_0$ generated by distributive lattice equations.
The cubical cwfs in the image of this functor satisfy a sheaf condition, which can be represented syntactically as an operation allowing one to uniquely glue together to a type $\Gamma \vdash_{\braces{i, j}} A$ coherent families of types $\Gamma f \vdash_X A_f$ for $f$ a map to $X$ from the free distributive lattice on symbols $\braces{i, j}$ such that $f\,i \leq f\,j$ or $f\,j \leq f\,i$ (compare also the tope logic of [26]).

Applying this functor to the simplicial set model $\Std$ discussed above, we obtain an interpretation of distributive lattice cubical type theory (with $\II$ and $\FF$ as above) in the sense of the current paper (crucially, without computation rules for filling at type formers) in simplicial sets.
Thus, this cubical type theory is homotopically sound: can only derive statements which hold for standard homotopy types.