Guarded Cubical Type Theory

Abstract

This paper improves the treatment of equality in guarded dependent type theory ($\mathsf {GDTT}$), by combining it with cubical type theory ($\mathsf {CTT}$). $\mathsf {GDTT}$ is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement $\mathsf {GDTT}$ with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. $\mathsf {CTT}$ is a variation of Martin–Löf type theory in which the identity type is replaced by abstract paths between terms. $\mathsf {CTT}$ provides a computational interpretation of functional extensionality, enjoys canonicity for the natural numbers type, and is conjectured to support decidable type-checking. Our new type theory, guarded cubical type theory ($\mathsf {GCTT}$), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of $\mathsf {CTT}$ as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation. We show that $\mathsf {CTT}$ can be given semantics in presheaves on $\mathcal {C}\times \mathbb {D}$, where $\mathcal {C}$ is the cube category, and $\mathbb {D}$ is any small category with an initial object. We then show that the category of presheaves on $\mathcal {C}\times \omega$ provides semantics for $\mathsf {GCTT}$.

1 Introduction

Guarded recursion is a technique for defining and reasoning about infinite objects. Its applications include the definition of productive operations on data structures more commonly defined via coinduction, such as streams, and the construction of models of program logics for modern programming languages with features such as higher-order store and concurrency [5]. This is done via the type-former , called ‘later’, which distinguishes data which is available immediately from data only available after some computation, such as the unfolding of a fixed-point. For example, guarded recursive streams are defined by the equation

rather than the more standard , to specify that the head is available now but the tail only later. The type for guarded fixed-point combinators is then , rather than the logically inconsistent $(A\rightarrow A)\rightarrow A$, disallowing unproductive definitions such as taking the fixed-point of the identity function.

Clouston et al. [11] developed guarded recursive types in a simply-typed setting, following earlier work [1, 3, 27], with semantics in the presheaf category $\widehat{\omega }$ known as the topos of trees, and also presented a logic for reasoning about programs with guarded recursion. For large examples, such as models of program logics, we would like to be able to formalise such reasoning. A major approach to formalisation is via dependent types, used for example in the proof assistants Coq [24] and Agda [28]. Bizjak et al. [10], following earlier work [6, 26], introduced guarded dependent type theory ($\mathsf {GDTT}$), integrating the type-former into a dependently typed calculus, and supporting the definition of guarded recursive types as fixed-points of functions on universes, and guarded recursive operations on these types.

We wish to formalise non-trivial theorems about equality between guarded recursive constructions, but such arguments often cannot be accommodated within intensional Martin–Löf type theory. For example, we may need to be able to reason about the extensions of streams in order to prove the equality of different stream functions. Hence $\mathsf {GDTT}$ includes an equality reflection rule, which is well known to make type checking undecidable. This problem is close to well-known problems with functional extensionality [16, Section 3.1.3], and indeed this analogy can be developed. Just as functional extensionality involves mapping terms of type $(x:A)\rightarrow {\mathsf {Id\,}}B\, (fx)\, (gx)$ to proofs of ${\mathsf {Id\,}}\,(A\rightarrow B)\, f\, g$, extensionality for guarded recursion requires an extensionality principle for later types, namely the ability to map terms of type to proofs of , where is the constructor for . These types are isomorphic in the topos of trees, and so in $\mathsf {GDTT}$ their equality was asserted as an axiom. But in a calculus without equality reflection we cannot merely assert such axioms without losing canonicity.

Cubical type theory ($\mathsf {CTT}$) [12], for which we give a brief introduction in Sect. 2, is a new type theory with a computational interpretation of functional extensionality but without equality reflection, and hence is a candidate for extension with guarded recursion, so that we may formalise our arguments without incurring the disadvantages of fully extensional identity types. $\mathsf {CTT}$ was developed primarily to provide a computational interpretation of Voevodsky’s univalence axiom in homotopy type theory [33]. The most important novelty of $\mathsf {CTT}$ is the replacement of inductively defined identity types by paths, which can be seen as maps from an abstract interval, and are introduced and eliminated much like functions. $\mathsf {CTT}$ can be extended with identity types which model all rules of intensional equality in Martin–Löf type theory [12, Sect. 9.1], but these are logically equivalent to path types, and in our paper it suffices to work with path types only. $\mathsf {CTT}$ has sound denotational semantics in (fibrations in) cubical sets, a presheaf category that is used to model homotopy types. $\mathsf {CTT}$ enjoys canonicity for terms of natural number type [18] and is conjectured to have decidability of type-checking. Moreover, a type-checker has been implemented.¹

In Sect. 3 of this paper we propose guarded cubical type theory ($\mathsf {GCTT}$), a combination of the two type theories² which supports non-trivial proofs about guarded recursive types via path equality, while retaining the potential for good syntactic properties such as canonicity for base types and decidable type-checking. In particular, just as a term can be defined in $\mathsf {CTT}$ to witness functional extensionality, a term can be defined in $\mathsf {GCTT}$ to witness extensionality for later types. Further, we use elements of the interval of $\mathsf {CTT}$ to annotate fixed-points, and hence control their unfoldings. This ensures that fixed-points are path equal, but not judgementally equal, to their unfoldings, and hence prevents infinite unfoldings, an obvious source of non-termination in any calculus with infinite constructions. The resulting calculus is shown via examples to be useful for reasoning about guarded recursive operations; we also view it as potentially significant from the point of view of $\mathsf {CTT}$, extending its expressivity as a basis for formalisation.

In Sect. 4 we give semantics to this type theory via the presheaf category over the product of the categories used to define semantics for $\mathsf {GDTT}$ and $\mathsf {CTT}$. Defining semantics in this new category is non-trivial because we must check that all novel features of the two type theories can still be soundly interpreted. To achieve this we first define, in Sect. 4.1, an extension of dependent predicate logic in which the constructs of $\mathsf {CTT}$ may be interpreted, then show that this logic may be interpreted in a certain class of presheaf categories, including our intended category. We then show that this category also interprets the constructs of $\mathsf {GDTT}$. In particular we must ensure that the ‘later’ functor , which models the type-former of the same name, preserves the (Kan) composition operations which are central to the cubical model. In the conference version of this paper [7] the development of the semantics was presented only very briefly for space reasons; the technical appendix of that paper is integrated into the text of this paper, and forms the bulk of this paper’s contribution.

Moreover, we have implemented a prototype type-checker for this extended type theory,³ extending the implemented type-checker for $\mathsf {CTT}$, which provides confidence in our type theory’s syntactic properties. All constructions using the type theory $\mathsf {GCTT}$ presented in this paper, and many others, have been formalised in this type-checker.

2 Cubical Type Theory

This section gives a brief overview of cubical type theory ($\mathsf {CTT}$)⁴; for full details we refer to Cohen et al. [12].

We start with a standard dependent type theory with $\varPi , \varSigma$, natural numbers, and a Russell-style universe, but without identity types:

We adhere to the usual conventions of considering terms and types up to $\alpha$-equality, and writing $A \rightarrow B$, respectively $A \times B$, for non-dependent $\varPi$- and $\varSigma$-types. We use the symbol ‘$=$’ for judgemental equality.

$\mathsf {CTT}$ extends this basic type theory with the constructs below:

We now briefly discuss these constructs.

The central novelty of $\mathsf {CTT}$ is its treatment of equality. Instead of the inductively defined identity types of intensional Martin–Löf type theory [23], $\mathsf {CTT}$ has paths. The paths between two terms t, u of type A form a sort of function space, intuitively that of continuous maps from some interval $\mathbbm {I}$ to A, with endpoints t and u. Rather than defining the interval $\mathbbm {I}$ concretely as the unit interval $[0,1] \subseteq \mathbb {R}$, it is defined as the free De Morgan algebra on a discrete infinite set of names $\{i, j, k, \ldots \}$ with endpoints 0 and 1. A De Morgan algebra is a bounded distributive lattice with an involution $1-\cdot$ satisfying the De Morgan laws

$$\begin{aligned} 1-(i\wedge j)&= (1-i) \vee (1-j),&1-(i\vee j)&= (1-i) \wedge (1-j). \end{aligned}$$

The interval $[0,1] \subseteq \mathbb {R}$, with ${\mathsf {min}}, {\mathsf {max}}$ and $1-\cdot$, is an example of a De Morgan algebra.

The judgement $\varGamma \vdash r : \mathbbm {I}$ means that r draws its names from $\varGamma$. Despite this notation, $\mathbbm {I}$ is not a first-class type.

Path types and their elements are defined by the rules in Fig. 1. Path abstraction, $\langle i \rangle t$, and path application, $t \, r$, are analogous to $\lambda$-abstraction and function application, and support the familiar $\beta$-equality $(\langle i \rangle t)\, r = t\left\{ r/i\right\}$ and $\eta$-equality $\langle i \rangle t\, i = t$. There are two additional judgemental equalities for paths, regarding their endpoints: given $p : {\mathsf {Path\,}}A ~ t ~ u$ we have $p\, 0 = t$ and $p\, 1 = u$.

Fig. 1

Typing rules for path types

Paths provide a notion of identity which is more extensional than that of intensional Martin–Löf identity types, as exemplified by the proof term for functional extensionality:

$$\begin{aligned} {\mathsf {funext}} \, f\, g \triangleq \lambda p. \langle i \rangle \lambda x .\, p \, x \, i ~ : ~ \left( (x : A) \rightarrow {\mathsf {Path\,}}B ~ (f\, x) ~ (g\, x)\right) \rightarrow {\mathsf {Path\,}}~ (A\rightarrow B) ~ f ~ g. \end{aligned}$$

The rules above suffice to ensure that path equality is reflexive, symmetric, and a congruence, but we also need it to be transitive and, where the underlying type is the universe, to support a notion of transport. This is done via (Kan) composition operations.

To define these we need the face lattice, $\mathbbm {F}$, defined as the distributive lattice generated by the symbols $(i=0)$ and $(i=1)$ for all names i, quotiented by the relation $(i=0) \wedge (i=1) = 0_{\mathbbm {F}}$. As with the interval, $\mathbbm {F}$ is not a first-class type, but the judgement $\varGamma \vdash \varphi : \mathbbm {F}$ asserts that $\varphi$ draws its names from $\varGamma$. We also have the judgement which asserts the equality of $\varphi$ and $\psi$ in the face lattice. Contexts can be restricted by elements of $\mathbbm {F}$. Such a restriction affects equality judgements so that, for example, is equivalent to

We write $\varGamma \vdash t : A[\varphi \mapsto u]$ as an abbreviation for the two judgements $\varGamma \vdash t : A$ and , noting the restriction with $\varphi$ in the equality judgement. Now the composition operator is defined by the typing and equality rule

There are further equations for composition that depend on the type A they are applied to; we omit these from this short overview.

A simple use of composition is to implement the transport operation for ${\mathsf {Path\,}}$ types

where a has type $A\left\{ 0/i\right\}$. The notation [] stands for the empty system. In general a system is a list of pairs of faces and terms, and it defines an element of a type by giving the individual components at each face. Below we present two of the rules for systems; in particular the first rule ensures that for a system to be well-typed, all cases must be covered, and the components must agree where the faces overlap:

We will write $[ \varphi _1\mapsto t_1,\ldots ,\varphi _n\mapsto t_n ]$ as an abbreviation for $[\varphi _1\vee \ldots \vee \varphi _n \mapsto [ \varphi _1~t_1,\ldots ,\varphi _n~t_n ]]$.

A non-trivial example of the use of systems is the proof that ${\mathsf {Path\,}}$ is transitive; given $p\,:\,{\mathsf {Path\,}}A~a~b$ and $q\,:\,{\mathsf {Path\,}}A~b~c$ we can define

This builds a path between the appropriate endpoints because we have the equalities and .

The glueing construction [12, Sec. 6] is necessary to define the interaction of the universe with compositions, and hence to provide a computational interpretation of univalence. It has the following type-formation and typing rules:

where ${\mathsf {Equiv}}\,T\,A$ is the type of equivalence between types T and A, whose formal definition we omit. We also have the following equations:

$$\begin{aligned}&{\text {Glue}}\, \left[ 1_{\mathbbm {F}} \mapsto (T,f)\right] \, A = T, \\&{\text {glue}}\, \left[ 1_{\mathbbm {F}} \mapsto t\right] \, a = t, \\&{\text {glue}}\, \left[ \varphi \mapsto b\right] \, ({\text {unglue}}b) = b, \\&{\text {unglue}}({\text {glue}}\, \left[ \varphi \mapsto t\right] \, a) = a. \end{aligned}$$

3 Guarded Cubical Type Theory

The section introduces constructs from guarded dependent type theory ($\mathsf {GDTT}$) to $\mathsf {CTT}$, to define guarded cubical type theory ($\mathsf {GCTT}$):

recalling that r is an element of the interval. This section will also present examples that show how $\mathsf {GCTT}$ can be used to prove properties of guarded recursive constructions.

3.1 Later Types

In Fig. 2 we present the ‘later’ types of guarded dependent type theory ($\mathsf {GDTT}$) [10], with judgemental equalities in Figs. 3 and 4. Note that we do not add any new equation for the interaction of compositions with : while is a valid term which allows us to transport at types, any extra equation for it would be necessary only if we were to add the ‘previous’ eliminator ${\text {prev}}$ for , but this extension (which involves clock quantifiers) is left to further work. We delay the presentation of the fixed-point construction until the next subsection.

Fig. 2

Typing rules for later types

Fig. 3

Type equality rules for later types (congruence and equivalence rules are omitted)

Fig. 4

Term equality rules for later types. We omit congruence and equivalence rules, and the rules for terms of type ${\mathsf {U}}$, which reflect the type equality rules of Fig. 3

The typing rules use the delayed substitutions of $\mathsf {GDTT}$, as defined in Fig. 5. The notation for the delayed substitution is suggestive for its intended semantics as . Delayed substitutions resemble Haskell-style do-notation, or a delayed form of let-binding. If we have a term , we cannot access its contents ‘now’, but if we are defining a type or term that itself has some part that is available ‘later’, then this part should be able to use the contents of t. Therefore delayed substitutions allow terms of type to be unwrapped by and . As observed by Bizjak et al. [10], these constructions generalise the applicative functor [25] structure of ‘later’ types, by the definitions , and , and also generalise the $\circledast$ operation from simple functions to $\varPi$-types. We here make the new observation that delayed substitutions can express the function , introduced by Birkedal and Møgelberg [4] to express guarded recursive types as fixed-points on universes, as ; see for example the definition of streams in Sect. 3.3.

Fig. 5

Formation rules for delayed substitutions

Example 3.1

In $\mathsf {GDTT}$ it is essential that we can convert terms of type into terms of type , so that we may perform Löb induction, the technique of proof by guarded recursion where we assume , deduce p, and hence may conclude p with no assumptions. This is achieved in $\mathsf {GDTT}$ by postulating as an axiom the following judgemental equality:

(1)

A term from left-to-right of (1) can be defined using the ${\mathsf {J}}$-eliminator for identity types, but the more useful direction is right-to-left, as proofs of equality by Löb induction involve assuming that we later have an equality, then converting this into an equality on later types. In fact with the paths of $\mathsf {GCTT}$ we can define a term with the desired type:

(2)

Note the similarity of this term and type with that of ${\mathsf {funext}}$, for functional extensionality, presented on p. 4. Indeed we claim that (2) provides a computational interpretation of extensionality for later types.

3.2 Fixed Points

In this section we complete the presentation of $\mathsf {GCTT}$ by addressing fixed points. In $\mathsf {GDTT}$ there are fixed-point constructions with the judgemental equality . In $\mathsf {GCTT}$ we want decidable type checking, including decidable judgemental equality, and so we cannot admit such an unrestricted unfolding rule. Our solution is that fixed points should not be judgementally equal to their unfoldings, but merely path equal. We achieve this by decorating the fixed-point combinator with an interval element which specifies the position on this path. The 0-endpoint of the path is the stuck fixed-point term, while the 1-endpoint is the same term unfolded once. However this threatens canonicity for base types: if we allow stuck fixed-points in our calculus, we could have stuck closed terms inhabiting ${\mathsf {N}}$. To avoid this, we introduce the delayed fixed-point combinator ${\mathsf {dfix}}$, inspired by Sacchini’s guarded unfolding operator [31], which produces a term ‘later’ instead of a term ‘now’. Its typing rule, and notion of equality, is given in Fig. 6. We will write for $,$ for , and for .

Fig. 6

Typing and equality rules for the delayed fixed-point

Lemma 3.2

(Canonical unfold lemma) For any term there is a path between and , given by the term .

Transitivity of paths (via compositions) ensures that is path equal to any number of fixed-point unfoldings of itself.

A term a of type A is said to be a guarded fixed point of a function if there is a path from a to .

Proposition 3.3

(Unique guarded fixed points) Any guarded fixed-point a of a term is path equal to .

Proof

Given , we proceed by Löb induction, i.e., by assuming

We define a path

which is well-typed because the type of the variable q ensures that $q\, 0$ is judgementally equal to a, resp. $q\,1$ and . Note that we here implicitly use the extensionality principle for later (2). We compose s with p, and then with the inverse of the canonical unfold lemma of Lemma 3.2, to obtain our path from a to . We can write out our full proof term, where $p^{-1}$ is the inverse path of p, as

$\square$

3.3 Programming and Proving with Guarded Recursive Types

In this section we show some simple examples of programming with guarded recursion, and prove properties of our programs using Löb induction and univalence.

Streams The type of guarded recursive streams in $\mathsf {GCTT}$, as with $\mathsf {GDTT}$, are defined as fixed points on the universe:

Note the use of a delayed substitution to transform a term of type to one of type ${\mathsf {U}}$, as discussed at the start of Sect. 3.1. Desugaring to restate this in terms of , we have

The head function is the first projection. The tail function, however, cannot be the second projection, since this yields a term of type

(3)

rather than the desired . However we are not far off; is judgementally equal to

which is the same term as (3), apart from endpoint 1 replacing 0. The canonical unfold lemma (Lemma 3.2) tells us that we can build a path in ${\mathsf {U}}$ from to ; call this path . Then we can transport between these types:

Note that the compositions of these two operations are path equal to identity functions, but not judgementally equal. We can now obtain the desired tail function by composing the second projection with ${\mathsf {unfold}}$, so ${\mathsf {tl}} \, s \triangleq ({\mathsf {unfold}} \, s).2$. Similarly we can define the stream constructor ${\mathsf {cons}}$ (usually written infix as  :  : ) by using ${\mathsf {fold}}$:

We now turn to higher order functions on streams. We define , the stream function which maps a binary function on two input streams to produce an output stream, as

Of course ${\mathsf {zipWith}}$ is definable even with simple types and , but in $\mathsf {GCTT}$ we can go further and prove properties about the function:

Proposition 3.4

$({\mathsf {zipWith}}$ preserves commutativity) If $f : A \rightarrow A \rightarrow B$ is commutative, then is commutative.

Proof

Let ${\mathsf {c}} : (a_1 : A) \rightarrow (a_2 : A) \rightarrow {\mathsf {Path\,}}B ~ (f\, a_1 \, a_2) ~ (f\, a_2 \, a_1)$ witness commutativity of f. We proceed by Löb induction, i.e., by assuming

Let $i:\mathbbm {I}$ be a fresh name, and . Our aim is to construct a stream which is ${\mathsf {zipWith}}\, f \, s_1 \, s_2$ when substituting 0 for i, and ${\mathsf {zipWith}}\, f \, s_2 \, s_1$ when substituting 1 for i. An initial attempt at this proof is the term

which is equal to

when substituting 0 for i, which is ${\mathsf {zipWith}}\, f\, s_1\, s_2$, but unfolded once. Similarly, $v\left\{ 1/i\right\}$ is ${\mathsf {zipWith}}\, f\, s_2\, s_1$ unfolded once. Let $\langle j \rangle {\mathsf {zipWith}}^j$ be the canonical unfold lemma associated with ${\mathsf {zipWith}}$ (see Lemma 3.2). We can now finish the proof by composing v with (the inverse of) the canonical unfold lemma. Diagrammatically, with i along the horizontal axis and j along the vertical:

The complete proof term, in the language of the implemented type-checker, can be found in “Appendix A”. $\square$

Bisimularity equals equality Two (guarded) streams are bisimilar when both their heads and tails are equal. In $\mathsf {GCTT}$ we can prove that bisimilar streams are equal, and moreover that the type of bisimilar streams is equal to the type of equal streams.

Proposition 3.5

For all , there is a term of type .

Proof

We may strengthen extensionality for later (refeq:laterspsext), to get that

This strengthening may be compared to the strong version of functional extensionality which states an equivalence of the equality type on function types and the type of pointwise equality [33, 2.9].

For , we have the following chain of equivalences:

The last equivalence is constructed from the ${\mathsf {fold\,}}$ and ${\mathsf {unfold\,}}$ functions for streams. The statement then follows from univalence. $\square$

Guarded recursive types with negative variance A key feature of guarded recursive types are that they support negative occurrences of recursion variables. This is important for applications to models of program logics [5]. Here we consider a simple example of a negative variance recursive type, namely , which is path equal to . As a simple demonstration of the expressiveness we gain from negative guarded recursive types, we define a guarded variant of Curry’s Y combinator:

where ${\mathsf {fold}}$ and ${\mathsf {unfold}}$ are the transports along the path between ${\mathsf {Rec}}_A$ and . As with ${\mathsf {zipWith}}, {\mathsf {Y}}$ can be defined with simple types and  [1]; what is new to $\mathsf {GCTT}$ is that we can also prove properties about it:

Proposition 3.6

(${\mathsf {Y}}$ is a guarded fixed-point combinator) ${\mathsf {Y}} f$ is path equal to , for any . Therefore, by Proposition 3.3, ${\mathsf {Y}}$ is path equal to .

Proof

simplifies to , and is path equal to $\varDelta$. A congruence over this path yields our path between and . $\square$

4 Semantics

In this section we provide sound semantics of $\mathsf {GCTT}$, and hence prove the consistency of $\mathsf {GCTT}$. The semantics is based on the category ${\widehat{\mathcal {C}\times \omega }}$ of presheaves on the category $\mathcal {C}\times \omega$, where $\mathcal {C}$ is the category of cubes [12] and $\omega$ is the poset of natural numbers.

Given a countably infinite set of names $i, j, k, \ldots$, the category $\mathcal {C}$ has as objects finite sets of names I, J, and as morphisms $I \rightarrow J$, functions $J \rightarrow \mathbf {DM}\left( I\right)$, where $\mathbf {DM}\left( I\right)$ is the free De Morgan algebra with generators I. Equivalently, the category of cubes is the opposite of the Kleisli category of the free De Morgan algebra monad on finite sets. Hence in particular it has products, which are given by disjoint union, a fact used extensively below.

As is standard, contexts of $\mathsf {GCTT}$ are interpreted as objects of ${\widehat{\mathcal {C}\times \omega }}$. Following the approach of Cohen et al. [12] types in context $\varGamma$ are interpreted as pairs $(A, c_A)$ of a presheaf A on the category of elements of $\varGamma$ and a chosen composition structure $c_A$. We call such a pair a fibrant type.

Semantics of type theory in presheaf categories is well-known. When interpreting type constructions, such as dependent products, the type part of the pair $(A,c_A)$ is interpreted as usual in presheaf models. What is new is the addition of composition structure, and much of the work we do in this section is to show that composition structure is preserved by the various type constructors. It is complex both to define composition structure, and to show that all types can be equipped with this structure. To aid with this we describe the composition structure in the internal language of the presheaf topos. More precisely, in Sect. 4.1 we use dependent predicate logic extended with four assumptions, of which the most important asserts the existence of an interval type, as the internal language. A formulation of compositions in this manner, along with similarly internal descriptions of fillings and faces, appeared (in slightly different form) in an unpublished note by Coquand [13]. We recall the precise definitions of these in the following sections, and provide details of some constructions which were omitted in op. cit. The advantage of this approach is that we can show entirely in the internal language that constructions such as dependent products and sums have compositions satisfying the necessary properties, provided their constituent types do.

Working at this level, the notion of a model of $\mathsf {CTT}$ can be generalised from the category $\widehat{\mathcal {C}}$ of cubical sets to any topos whose internal logic satisfies the four assumptions. In particular, these assumptions hold in the presheaf category $\widehat{\mathcal {C}\times \mathbb {D}}$ for any small category $\mathbb {D}$ with an initial object. The category ${\widehat{\mathcal {C}\times \omega }}$ is obviously such a category; we will show that it is one that also allows the constructions of guarded recursion introduced in Sect. 3 to be modelled.

The notion of a model of $\mathsf {GCTT}$ is then formulated as follows: a type of $\mathsf {GCTT}$ in context $\varGamma$ is interpreted as a pair of a type $\varGamma \vdash A$ in the internal language of ${\widehat{\mathcal {C}\times \omega }}$, and a composition structure $c_A$, where $c_A$ is a term in the internal language of a specific type $\varPhi (\varGamma ;A)$ which we define below after introducing the necessary constructs. A term of $\mathsf {GCTT}$ is then interpreted simply as a term of the internal language. We use categories with families [15] as our notion of a model.

This section is organised as follows: Sect. 4.1 presents the general intermediate language $\mathcal {L}$ which we use to interpret $\mathsf {GCTT}$ in. Section 4.2 models $\mathsf {CTT}$ in $\mathcal {L}$. Section 4.3 models $\mathcal {L}$ in the category of cubical sets. Section 4.4 considers more general models of $\mathcal {L}$. Section 4.5 models $\mathsf {GCTT}$ in an extension of $\mathcal {L}$. Section 4.6 gives a summary of the semantics.

4.1 The Dependent Predicate Logic $\mathcal {L}$

Instead of formulating our model directly using regular mathematics, we will specify a type-theoretic language $\mathcal {L}$, tailor-made for the purpose of our model, and inspired by the internal logic of the presheaf topos of cubical sets, $\widehat{\mathcal {C}}$.

Fig. 7

Judgements of the dependent predicate logic $\mathcal {L}$

$\mathcal {L}$ is Phoa’s dependent predicate logic [30, Appendix I] (see also Johnstone [19, D4.3,4.4]) extended with four assumptions, detailed in this section. Figure 7 contains an overview of the types of judgements. We write $\varOmega$ for the type of propositions, $\top$ for true and $\bot$ for false.

In addition to the equality proposition ${t = u} : A$, we also have the extensional identity type ${\text {Id}}_{A} (t, u )$ with equality reflection:

${\text {Id}}$ (the type) and $\cdot = \cdot$ (the proposition) are equally expressive, but for presentation purposes it is practical to have both: Using ${\text {Id}}$ we can easily express the type of partial elements (elements of a type B which are defined only when $t=u$ in A) as ${\text {Id}}_{A} (t, u )\rightarrow B$. Terms of this type, however, are unwieldy to work with since one needs to carry around an explicit equality proof (which will be equal to ${\text {refl}}$ anyway by the extensionality of the identity type). Therefore we will implicitly convert back and forth between the type theoretic and the logical representation, and will often elide proofs, for example writing the context $\varGamma ,p:{\text {Id}}_{\varOmega } (\varphi , \top )$ as $\varGamma ,\varphi$.

Following Cohen et al. [12], our syntax in Sect. 2 was à la Russell, i.e. it did not contain explicit codes. The interpretation in op. cit. however contains a special form of Tarski-style universes with an explicit coding function which commutes with the decoding function ${\text {El}}$. These universes can be interpreted in presheaf models. To facilitate the interpretation of the fibrant universe (in Sect. 4.4.3) we assume that our intermediate language $\mathcal {L}$ contains an explicit “elements-of” operation ${\text {El}}$ for a universe $\mathcal {U}$ of small types.

We now turn to the first of our four assumptions necessary for modelling $\mathsf {CTT}$.

Assumption 1

(Interval type) In $\mathcal {L}$ we have a type $\mathbbm {I}$ with

which is a De Morgan algebra which enjoys the (finitary) disjunction property:

4.1.1 Constructions Definable from the Interval Type

This section will show that the interval type assumption above is sufficient for modelling all of $\mathsf {CTT}$ except for glueing and the universe, as we can use the interval type to define the face lattice, and hence systems, compositions, fillings, and paths. While some of the constructions of this section are complex to state, they are mostly fairly obvious translations of the type-theoretic constructions sketched in Sect. 2 to the language $\mathcal {L}$.

We will see three further assumptions, for modelling glueing and the universe, in Sect. 4.1.2.

Faces

Using the interval we define the type $\mathbbm {F}$ as the image of the function $\cdot = 1 : \mathbbm {I}\rightarrow \varOmega$. More precisely, $\mathbbm {F}$ is the subset type

$$\begin{aligned} \mathbbm {F}\triangleq \left\{ p : \varOmega \;|\;\exists (i : \mathbbm {I}), p = (i = 1) \right\} \end{aligned}$$

We will implicitly use the inclusion $\mathbbm {F}\rightarrow \varOmega$. The following lemma in particular states that the inclusion is compatible with all the lattice operations, hence omitting it is unambiguous.

Lemma 4.1

• $\mathbbm {F}$ is a lattice for operations inherited from $\varOmega$.

• The corestriction $\cdot = 1 : \mathbbm {I}\rightarrow \mathbbm {F}$ is a lattice homomorphism.

• $\mathbbm {F}$ inherits the disjunction property from $\mathbbm {I}$.

To define partial elements we first define, given a proposition $\varGamma \vdash \varphi : \mathbbm {F}$, the subsingleton $\left[ \varphi \right]$ as

$$\begin{aligned} \left[ \varphi \right] \triangleq {\text {Id}}_{\mathbbm {F}} (\varphi , \top ). \end{aligned}$$

For this type we have the logical equivalence $\left( \exists ! p : [\varphi ], \top \right) \Leftrightarrow \varphi$ which we use below when passing between type-theoretic and logical views in constructions of compositions.

Partial elements Given $\varGamma \vdash A$ and $\varGamma \vdash \varphi : \mathbbm {F}$ we say that a term t is a partial element of A of extent$\varphi$, if $\varGamma \vdash t : \varPi (p : \left[ \varphi \right] ).A$. If we are in a context with $p : \left[ \varphi \right]$, then we treat such a partial element t as a term of type A, leaving implicit the application to the proof p, i.e., we write t for $t\,p$. We similarly will often write $\varGamma , \left[ \varphi \right]$ for $\varGamma , p : \left[ \varphi \right]$, and $\left[ \varphi \right] \rightarrow B$ for the dependent function space $\varPi (p : \left[ \varphi \right] ).B$, leaving the proof variable p implicit.

If we have a term $\varGamma , p:\left[ \varphi \right] \vdash u : A$ (a partial element), then we define

$$\begin{aligned} A[\varphi \mapsto u] \triangleq \varSigma (a:A). \left[ \varphi \right] \rightarrow \left( {\text {Id}}_{A} (a, u )\right) \end{aligned}$$

(4)

as the type of elements of a which equal the partial element u on extent $\varphi$. Note that the second component of the pair is uniquely determined (up to judgemental equality) by equality reflection. Thus often to construct terms of this type we construct a term of type A and show, in the logic, that it is equal to the partial element u on extent $\varphi$. We do not construct the second component explicitly.

Systems Given $\varGamma \vdash A$, assume we have the following:

In other words: We have n partial elements of A which agree with each other on the intersection of their extents. We can use the axiom of definite description to define the term

$$\begin{aligned}{}[\varphi _1t_1,\ldots ,\varphi _nt_n] \triangleq \text {the }x^A \text {such that }\chi (x) \end{aligned}$$

where

$$\begin{aligned} \chi (x) \triangleq (\varphi _1 \wedge (x = t_1)) \vee \cdots \vee (\varphi _n \wedge (x = t_n)). \end{aligned}$$

We call this term a system. The condition for using definite description is a proof (in the logic) of the unique existence of such a term. Given the assumptions above, unique existence of the term follows easily.

Using systems, we generalise the earlier definition (4): We define

$$\begin{aligned} A[\varphi _1 \mapsto t_1, \ldots , \varphi _n \mapsto t_n] \triangleq A[\varphi _1\vee \cdots \vee \varphi _n \mapsto [\varphi _1t_1,\ldots ,\varphi _nt_n]], \end{aligned}$$

where the type on the right hand side is using the definition (4). Note that $A[\varphi \mapsto t]$ is unambiguous, as we have $\varGamma , [\varphi ] \vdash [\varphi t] = t : A$.

Compositions Given $\varGamma \vdash A$, we can define the type of compositions:

$$\begin{aligned} \varPhi (\varGamma ;A) \triangleq&\varPi (\gamma : \mathbbm {I}\rightarrow \varGamma )\\&(\varphi : \mathbbm {F})\\&(u : \varPi (i:\mathbbm {I}). \left[ \varphi \right] \rightarrow A(\gamma (i))) . \\&A(\gamma (0))[ \varphi \mapsto u(0) ] \rightarrow A(\gamma (1))[ \varphi \mapsto u(1) ]. \end{aligned}$$

Here we treat the context $\varGamma$ as a closed type. This is justified because there is a canonical bijection between contexts and closed types of the internal language. The notation $A(\gamma (i))$ means substitution along the (uncurried) $\gamma$, by which we mean the following. Given some term $\gamma$ of type $\mathbbm {I}\rightarrow \varGamma$ in some context $\varGamma '$, there is the “uncurried” term $\varGamma ', i : \mathbbm {I} \vdash \gamma (i) : \varGamma$ which arises by application of $\gamma$ to i. Finally, we assume the variable i appearing in the type of u is fresh for $\varphi , \gamma$ and A.

Note that there is an important difference between the type of compositions in $\mathcal {L}$ as defined above and the form of the rule for compositions in $\mathsf {CTT}$. In the latter the type A depends on $\mathbbm {I}$, whereas it seemingly does not in the type of compositions. This difference however is only superficial since the first argument in the type of compositions is a path in $\varGamma$, which gives a dependence of A on $\mathbbm {I}$.

Recall that we call a pair of a type $\varGamma \vdash A$ in $\mathcal {L}$ together with a term $\vdash \mathbf {c}: \varPhi (\varGamma ;A)$ a fibrant type.

Fillings Given $\varGamma \vdash A$, we can define the type of (Kan) fillings:

$$\begin{aligned} \varPsi (\varGamma ,A) \triangleq \varPi&(\gamma : \mathbbm {I}\rightarrow \varGamma ) \\&(\varphi : \mathbbm {F}) \\&(u : \varPi (i: \mathbbm {I}) . \left[ \varphi \right] \rightarrow A (\gamma (i))) \\&(a_0 : A(\gamma (0))[\varphi \mapsto {} u(0)]) \\&(i : \mathbbm {I}) . \\&A(\gamma (i))[\varphi \mapsto u(i), (1-i) \mapsto \pi _1 a_0]. \end{aligned}$$

If we have a filling operation $\mathbf {f}: \varPsi (\varGamma ,A)$ then we can get a path lifting operation which states that given a path $\gamma$ and an element $a_0$ in Aover$\gamma (0)$ we get a path in A which starts at $a_0$. Concretely, path lifting is the term $\varvec{\ell }$ of the following type

$$\begin{aligned} \varvec{\ell }: \varPi&(\gamma : \mathbbm {I}\rightarrow \varGamma ) \\&(a_0 : A(\gamma (0))) \\&(i:\mathbbm {I}). \\&A(\gamma (i))[(1-i) \mapsto a_0]. \end{aligned}$$

It is defined as a degenerate case of $\mathbf {f}$ where $\varphi$ is $\bot$, and u therefore is uniquely determined (since it is a partial function defined where $\bot$ holds). Path lifting is used when constructing compositions for dependent products and sums.

Lemma 4.2

(Fillings from compositions) If we have a fibrant type $\varGamma \vdash A$ with $\mathbf {c}_A : \varPhi (\varGamma ;A)$, then we have a filling operation $\vdash \mathbf {f}: \varPsi (\varGamma ,A)$.

Proof

We introduce the variables of appropriate types:

$$\begin{aligned}&\gamma : \mathbbm {I}\rightarrow \varGamma , \\&\varphi : \mathbbm {F}, \\&u : \varPi (i: \mathbbm {I}). [\varphi ] \rightarrow A (\gamma (i)), \\&a_0 : A(\gamma (0))[\varphi \mapsto u(0)], \\&i : \mathbbm {I}. \end{aligned}$$

We need to find a term of type

$$\begin{aligned} A(\gamma (i))[\varphi \mapsto u(i), (i=0) \mapsto \pi _1a_o]. \end{aligned}$$

We check that the following system is well-defined (in a context with $\varphi \vee (i=0)$):

$$\begin{aligned}{}[\varphi u(i\wedge j), (i=0)\pi _1 a_0]. \end{aligned}$$

• If $\varphi$, then $u(i\wedge j) : A(\gamma (i\wedge j))$.

• If $i=0$, then $\pi _1a_0 : A(\gamma (0)) = A(\gamma (i\wedge j))$.

• If $\varphi$ and $i=0$, then $\pi _1a_0 = u(0) = u(i\wedge j)$.

Note also that this means that

$$\begin{aligned} A(\gamma (0))[\varphi \mapsto u(0)] = A(\gamma (0))[\varphi \mapsto u(0),(i=0) \mapsto \pi _1a_0], \end{aligned}$$

and therefore we can write the following term:

$$\begin{aligned} \mathbf {c}_A ~ (\lambda j.\gamma (i\wedge j)) ~ (\varphi \vee (i=0)) ~ (\lambda j. [\varphi u(i\wedge j), (i=0)\pi _1 a_0]) ~ a_0 \end{aligned}$$

which has the type

$$\begin{aligned} A(\gamma (i))[\varphi \mapsto u(i), (i=0) \mapsto \pi _1a_o], \end{aligned}$$

as was needed. $\square$

Path types Given $\varGamma \vdash A$ and terms $\varGamma \vdash t,u : A$, we can define the Path type

$$\begin{aligned} {\text {Path}}_{A} \, t ~ u \triangleq \varPi (i:\mathbbm {I}).A[(1-i)\mapsto t, i \mapsto u] \end{aligned}$$

as the type of paths in A, i.e., terms of type $\mathbbm {I}\rightarrow A$, which start at t and end at u.

4.1.2 Assumptions for Glueing and the Universe

Assumption 2

(Glueing) There is a type for glueing with the following type formation and typing rules

Satisfying the following judgemental equalities:

The assumption above is essentially the same as the rules for the glueing type in $\mathsf {CTT}$. One difference is that in the formation rule for ${\text {Glue}}$ we do not require f to be an equivalence. We need only additionally assume that f is an equivalence, which is stated in terms of the ${\mathsf {Path\,}}$ type, when proving that glueing is fibrant in Lemma 4.6.

Assumption 3

(Fibrant universe) There is a fibrant universe$\mathcal {U}_{f}$ which contains pairs of a code in $\mathcal {U}$ with an associated composition operator:

satisfying

Assumption 4

($\forall$) We assume that the map $\varphi \mapsto \lambda \_.\varphi : \mathbbm {F}\rightarrow (\mathbbm {I}\rightarrow \mathbbm {F})$ between posets has an internal right adjoint $\forall$. Concretely this means that for any $\varphi : \mathbbm {F}$ and any $f : \mathbbm {I}\rightarrow \mathbbm {F}$ we assume

Moreover we assume that this right adjoint preserves joins in the following sense. Let $\varphi$ and $\psi$ be elements of $\mathbbm {I}\rightarrow \mathbbm {F}$. We assume

$$\begin{aligned} \forall i : \mathbbm {I}, \varphi (i) \vee \psi (i) = \top \vdash \forall (\varphi ) \vee \forall (\psi ) = \top . \end{aligned}$$

4.2 A Model of $\mathsf {CTT}$ in Fibrant Types in $\mathcal {L}$

In this section we show how to use the assumptions from the preceding section to interpret $\mathsf {CTT}$. In the following sections we show how to extend the interpretation to $\mathsf {GCTT}$. We fix a presheaf category which models $\mathcal {L}$ and define a category with families [15] by specifying the type and term functors ${\text {Ty}}$ and ${\text {Tm}}$. The base category of the category with families, the category of contexts, is the chosen presheaf category. We use the language $\mathcal {L}$ as the internal language of the presheaf category to describe the objects and morphisms. Thus to construct the model of $\mathsf {CTT}$ we reuse the types and terms of the language $\mathcal {L}$, but we only take the fibrant types, i.e., the ones with associated composition operators. The type and term functors are as defined as

where we use [A] and [t] respectively for the equivalence classes of A and t modulo judgemental equality of $\mathcal {L}$. Note that if A and B are equivalent types then $\varPhi (\varGamma ;A)$ and $\varPhi (\varGamma ;B)$ are also equivalent, hence the type functor is well-defined. In constructions and proofs we will omit the mention of equivalence classes and work with representatives. This is justified since all operations in $\mathcal {L}$ respect judgemental equality.

Note that the context $\varGamma$ need not correspond to a type, i.e. it need not be fibrant. Context extension and projections can be taken directly from the internal language: $\varGamma .A \triangleq \varSigma \varGamma A, \mathsf {p} \triangleq \pi _1$, and $\mathsf {q} \triangleq \pi _2$.

The main challenge addressed in this section is showing that the category with families supports dependent sums, dependent products and universes. This involves showing that these types of the internal language can be equipped with compositions. Additionally compositions need to satisfy certain judgemental equalities [12, Section 4.5]. Checking these equalities is routine from construction of compositions at different types. Thus we only construct compositions and leave showing judgemental equalities to the reader.

4.2.1 Interpreting Composition

The following composition term is interpreted in terms of the composition in $\mathcal {L}$.

By assumption we have $c_A$ of type $\varPhi (\varGamma , i : \mathbbm {I};A)$ and u and $a_0$ are interpreted as terms in the internal language of the corresponding types. The interpretation of composition is then the term

$$\begin{aligned} \gamma : \varGamma \vdash c_A \left( \lambda (i : \mathbbm {I}). (\gamma , i)\right) \varphi \left( \lambda (i : \mathbbm {I}) (p : \left[ \varphi \right] ). u\right) a_0 : A(\gamma (1))[ \varphi \mapsto u(1)] \end{aligned}$$

where we have omitted writing the proof $u(0) = a_0$ on $\left[ \varphi \right]$. This proof is constructed from the third premise of the rule.

4.2.2 Interpreting Dependent Function Types

Assume that $\llbracket \varGamma \vdash A' \rrbracket = (A, \mathbf {c}_A)$ and $\llbracket \varGamma , x: A' \vdash B' \rrbracket = (B, \mathbf {c}_B)$. We define

$$\begin{aligned} \llbracket \varGamma \vdash (x:A')\rightarrow B' \rrbracket \triangleq (\varPi (x:A). B, \mathbf {c}_{\varPi (x:A). B}) \end{aligned}$$

where $\mathbf {c}_{\varPi (x:A). B} : \varPhi (\varGamma ;\varPi (x:A). B)$ comes from the following lemma.

Lemma 4.3

(cf. [13, Proposition 0.3]) $\varPi$-types preserve compositions: if we have composition terms $\mathbf {c}_A : \varPhi (\varGamma ;A)$ and $\mathbf {c}_B : \varPhi (\varGamma .A;B)$, then we can form a new composition $\mathbf {c}_{\varPi (x:A).B} : \varPhi (\varGamma , \varPi (x:A).B)$.

Proof

Recall that $\varPi$-types commutes with substitution:

$$\begin{aligned} (\varPi (x:A).B)(\gamma ) = \varPi (x:A(\gamma )).B(\gamma ), \end{aligned}$$

where $B(\gamma )$ is a type in the context with A. We introduce the variables:

$$\begin{aligned}&\gamma : \mathbbm {I}\rightarrow \varGamma , \\&\varphi : \mathbbm {F}, \\&u : \varPi (i : \mathbbm {I}). [\varphi ] \rightarrow \varPi (a:A(\gamma (i))). B(\gamma (i)), \\&c_0 : (\varPi (a : A(\gamma (0))). B(\gamma (0)))[\varphi \mapsto u(0)]. \end{aligned}$$

We need to find an element in

$$\begin{aligned} \varPi (a:A(\gamma (1))). B(\gamma (1)), \end{aligned}$$

along with a proof that it is u(1) when $\varphi =1$.

Let $a_1 : A(\gamma (1))$ be given. We define $a(i) : A(\gamma (i))[i \mapsto a_1]$ by using path lifting on $a_1$, i.e.,

$$\begin{aligned} a(i) \triangleq \varvec{\ell }~ (\lambda i. \gamma (1-i)) ~ a_1 ~ (1-i); \end{aligned}$$

where $\varvec{\ell }$ is the filling operation defined earlier. Then

$$\begin{aligned} b_1 \triangleq \mathbf {c}_B ~(\lambda i. \langle \gamma (i), a(i) \rangle ) ~ \varphi ~ (\lambda i. u(i)(a(i))) \end{aligned}$$

will have the type $B(\gamma (1))[\varphi \mapsto u(1)a_1]$. So $\lambda a_1. \pi _1 b_1$ has the type we are looking for. Now assume $\varphi = \top$; then $\lambda a_1. b_1 = \lambda a_1. u(i)a_1 = u(i)$, which is what we needed. $\square$

4.2.3 Interpreting Dependent Sum Types

Dependent sum types $(x : A) \times B$ are interpreted by $\varSigma$-types from $\mathcal {L}$, along with the composition operation that comes from the following lemma:

Lemma 4.4

$\varSigma$-types preserve compositions: if we have composition terms $\mathbf {c}_A : \varPhi (\varGamma ;A)$ and $\mathbf {c}_B : \varPhi (\varGamma . A;B)$, then we can form a new composition $\mathbf {c}_{\varSigma (x:A). B} : \varPhi (\varGamma , \varSigma (x:A). B)$.

The proof proceeds similarly to the previous proof that dependent products have compositions.

4.2.4 Interpreting Systems

We interpret the systems of $\mathsf {CTT}$ by using the systems of $\mathcal {L}$, and by using the fact that systems preserve compositions. Indeed, assume we have a system $\varGamma \vdash [\varphi _1 A_1, \ldots , \varphi _n A_n]$, together with compositions $\mathbf {c}_{A_k} : \varPhi (\varGamma , \left[ \varphi _k\right] ;A_k)$ such that

$$\begin{aligned}&\forall \left( \gamma : \left( \mathbbm {I}\rightarrow (\varGamma , \left[ \varphi _k \wedge \varphi _j\right] )\right) \right) ,\\&\forall \left( \psi : \mathbbm {F}{}\right) ,\\&\forall \left( u : \varPi (i:\mathbbm {I}). \left[ \psi \right] \rightarrow A_k(\gamma ^k(i))\right) ,\\&\forall \left( a_0 : A(\gamma ^k(0))[ \psi \mapsto u(0) ]\right) ,\\&\mathbf {c}_{A_k} \gamma ^k\,\psi \, u\, a_0 = \mathbf {c}_{A_j} \gamma ^j\,\psi \, u\, a_0 : A_k(\gamma ^k(1))[ \psi \mapsto u(1) ]. \end{aligned}$$

where $\gamma ^k$ and $\gamma ^j$ are $\gamma$ composed with inclusions from $\varGamma , \left[ \varphi _k \wedge \varphi _j\right]$ to $\varGamma , \left[ \varphi _k\right]$ and $\varGamma , \left[ \varphi _k\right]$, respectively. Note that this judgement is well-formed because we assume

$$\begin{aligned} \varGamma , \left[ \varphi _k \wedge \varphi _j\right] \vdash A_k = A_j \end{aligned}$$

and thus

$$\begin{aligned} A_k(\gamma ^k(i)) = A_j(\gamma ^j(i)) \end{aligned}$$

for all i. Composition structures satisfying these equalities come from the assumptions of the systems formation rule in guarded cubical type theory.

Under these assumptions we can define a new composition using a system consisting of the compositions of all the components, and combining them using the $\forall$ operation on the lattice of faces.

$$\begin{aligned}&\mathbf {c}\triangleq \lambda \gamma , \psi , u, a_0. [\left( \forall \left( \varphi _1 \circ \gamma \right) \right) (\mathbf {c}_{A_1} \, \gamma _1 \, \psi \, u \, a_0), \ldots , \\&\quad \left( \forall \left( \varphi _n \circ \gamma \right) \right) (\mathbf {c}_{A_n} \, \gamma _n \, \psi \, u \, a_0)] : \varPhi (\varGamma ;[\varphi _1 A_1, \ldots , \varphi _n A_n]). \end{aligned}$$

Here $\gamma _m : \mathbbm {I}\rightarrow \varGamma , [\varphi _m]$ is the context map $\gamma$ extended with the witness of $[\varphi _m]$, i.e., it is the map $\lambda i. (\gamma (i), \star )$ which is well-typed in context $\left[ \forall \left( \varphi _k \circ \gamma \right) \right]$. Indeed, if $\forall \left( \varphi _k \circ \gamma \right) = \top$ then $(\varphi _k \circ \gamma )(i) = \top$ for all i, giving the witness $\star$.

This system is well-defined. The fact that $\forall \left( \varphi _1 \circ \gamma \right) \vee \cdots \vee \forall \left( \varphi _n \circ \gamma \right) = \top$ follows directly from the fact that $\forall (i : \mathbbm {I}) \varphi _1(\gamma (i)) \vee \cdots \vee \varphi _n(\gamma (i)) = \top$ and the second property of $\forall$. Next, the terms $\mathbf {c}_{A_k} \, \gamma _k \, \psi \, u \, a_0$ are well-typed in the relevant context. Indeed, in context with $\left[ \forall \left( \varphi _k \circ \gamma \right) \right]$ we also have $\varphi _k(\gamma (0)) = \top$ and thus $a_0$ has type $A_k\gamma (0)$. For the same reason the whole term $\mathbf {c}_{A_k} \, \gamma _k \, \psi \, u \, a_0$ has the correct type $A_k\gamma (1)$.

Finally, the assumption on the composition structures ensures that the terms $\mathbf {c}_{A_k} \, \gamma _k \, \psi \, u \, a_0$ agree where they overlap (on extents $\left[ \varphi _k \wedge \varphi _j\right]$), which makes the system well-defined.

4.2.5 Interpreting Path Types

We interpret the path types:

$$\begin{aligned} \llbracket \varGamma \vdash {\mathsf {Path\,}}A ~ t~s \rrbracket \triangleq ({\text {Path}}_{A'} \, \llbracket t \rrbracket ~ \llbracket s \rrbracket , \mathbf {c}), \end{aligned}$$

where $\llbracket A \rrbracket = (A', \mathbf {c}_A)$ and $\mathbf {c}: \varPhi (\varGamma ;{\text {Path}}_{A'} \, \llbracket t \rrbracket ~ \llbracket s \rrbracket )$ comes from Lemma 4.5.

Lemma 4.5

Path-types preserve composition: if $\varGamma \vdash A$ is fibrant, then for any $\varGamma \vdash t,s : A$, we have a composition operator $\mathbf {c}: \varPhi (\varGamma ;{\text {Path}}_{A} \, t ~ s)$.

Proof

First note that if we have $\varGamma \vdash {\text {Path}}_{A} \, t ~ s :$ and $\vdash \gamma : \varGamma$, then

$$\begin{aligned} ({\text {Path}}_{A} \, t ~ s)(\gamma ) = {\text {Path}}_{A(\gamma )} \, t(\gamma ) ~ s(\gamma ) = \varPi (i:\mathbbm {I}). A(\gamma )\left[ \begin{array}{l@{ }l} i=0~&{}\mapsto t(\gamma ) \\ i=1 &{}\mapsto s(\gamma ) \end{array} \right] . \end{aligned}$$

Now let

$$\begin{aligned}&\gamma : \mathbbm {I}\rightarrow \varGamma \\&\varphi : \mathbbm {F}\\&u : \varPi (j:\mathbbm {I}). [\varphi ] \rightarrow {\text {Path}}_{A(\gamma \, j)} \, t(\gamma \, j) ~ s(\gamma \, j) \\&p_0 : ({\text {Path}}_{A(\gamma \, 0)} \, t(\gamma \, 0) ~ s(\gamma \, 0))[\varphi \mapsto u0] \end{aligned}$$

be given. Our goal is to find a term $p_1$ such that

$$\begin{aligned} p_1 : ({\text {Path}}_{A(\gamma \, 1)} \, t(\gamma \, 1) ~ s(\gamma \, 1))[\varphi \mapsto u1]. \end{aligned}$$

We will do this by finding a term $q : \varPi (i : \mathbbm {I}). A(\gamma \, 1)[\varphi \mapsto u\, 1\, i]$, for which we verify that $q\, 0 = t(\gamma \, 1)$ and $q1 = s(\gamma \, 1)$, in other words,

$$\begin{aligned} q : \varPi (i: \mathbbm {I}). A(\gamma \, 1)[\varphi \mapsto u\, 1\, i, (1-i) \mapsto t(\gamma \, 1), i \mapsto s(\gamma \, 1)] \end{aligned}$$

as this will be equivalent to having such a $p_1$.

Let $i:\mathbbm {I}$. By leaving some equality proofs implicit we can define the system

$$\begin{aligned} r(j) \triangleq [\varphi u\, j\, i, (1-i)t(\gamma \, j), i s(\gamma \, j)] : \varPi (j:\mathbbm {I}).[\varphi \vee (1-i) \vee i] \rightarrow A(\gamma \, j), \end{aligned}$$

which is well-defined because $u\, j\, 0=t(\gamma \, j)$ and $u\, j\, 1 = s(\gamma \, j)$. We also have that $p_0\, i : A(\gamma \, 0)[\varphi \mapsto u\, 0\, i ]$, and since $p_0\, 0 = t(\gamma \, 0)$ and $p_0 1 = s(\gamma \, 0)$, we can say that

$$\begin{aligned} p_0\, i : A(\gamma \, 0)[\varphi \mapsto u\, 0\, i, (1-i)\mapsto t(\gamma \, 0), i \mapsto s(\gamma \, 0)] \end{aligned}$$

so we can use the fibrancy of A to define the term

$$\begin{aligned} q(i) \triangleq \mathbf {c}_A \gamma ~ (\varphi \vee (1-i) \vee i) ~ r ~ (p_0\, i) : \varPi (i: \mathbbm {I}). A(\gamma \, 1)[\varphi \mapsto u\, 1\, i, (1-i) \mapsto t(\gamma \, 1), i \mapsto s(\gamma \, 1)], \end{aligned}$$

which is what we wanted. $\square$

4.2.6 Interpreting Glue Types

We interpret ${\mathsf {Glue}}$ from $\mathsf {CTT}$ using ${\text {Glue}}$ from $\mathcal {L}$ along with a composition operator, which we have by the following lemma:

Lemma 4.6

Glueing is fibrant, i.e., if we have

$$\begin{aligned} \varGamma&\vdash A \\ \varGamma&\vdash \varphi : \mathbbm {F}\\ \varGamma , [\varphi ]&\vdash T \\ \varGamma&\vdash w: [\varphi ] \rightarrow T \rightarrow A \\ \varGamma&\vdash p : {\text {isEquiv}} w \end{aligned}$$

then there is a term $\mathbf {c}: \varPhi (\varGamma ;{\text {Glue}}\, \left[ \varphi \mapsto (T,w)\right] \, A)$.

The construction of $\mathbf {c}$ in the proof of the above lemma is analogous to the construction of the composition operation for glueing in $\mathsf {CTT}$ [12], but formulated in $\mathcal {L}$. A crucial part of the construction is the face $\delta \triangleq \forall (\varphi \circ \gamma )$, where $\gamma : \mathbbm {I}\rightarrow \varGamma$, which satisfies that $[\delta ]$ implies $[\varphi (\gamma \, i)]$ for all $i: \mathbbm {I}$.

4.2.7 Interpreting the Universe

The universe of $\mathsf {CTT}$ is interpreted using the universe of fibrant types $\mathcal {U}_{f}$. To define the composition for the universe we follow the construction of Cohen et al. [12] in the language $\mathcal {L}$.

4.3 A Model of $\mathcal {L}$ in Cubical Sets

In this section we construct a model of $\mathcal {L}$ in the category of cubical sets. Recall that the category of cubes $\mathcal {C}$ has as objects finite sets of names $i,j,k,\ldots$ and as morphism the functions $J \rightarrow \mathbf {DM}\left( I\right)$ where $\mathbf {DM}\left( I\right)$ is the free De Morgan algebra on I. Alternatively, $\mathcal {C}$ can be described as the opposite of the Kleisli category of the free De Morgan algebra monad on ${\text {Fin}}$. The category of cubical sets is then the category $\widehat{\mathcal {C}}$ of presheaves on $\mathcal {C}$.

In the previous section we showed how to construct a model of $\mathsf {CTT}$ using $\mathcal {L}$. Constructing a model of $\mathcal {L}$ in cubical sets then shows we can give a model of $\mathsf {CTT}$ in cubical sets. This was shown already by Cohen et al. [12], however we will use results in this section to construct additional models of $\mathsf {CTT}$ in the subsequent section. In particular, we shall use presheaves over $\mathcal {C}\times \omega$ to model the full $\mathsf {GCTT}$ type theory.

The references in Sect. 4.1 show how to model dependent predicate logic in any presheaf topos [30], so we omit the verification of this part. We do however note how the judgements are interpreted since this will be used later in concrete calculations where working in the internal language no longer suffices, e.g., in the definition of the fibrant universe.

• A context $\varGamma \vdash$ is interpreted as a presheaf.

• The judgement $\varGamma \vdash A$ gives a pair of a presheaf $\varGamma$ on $\mathcal {C}$ and a presheaf A on the category of elements of $\varGamma$.

• The judgement $\varGamma \vdash t : A$ in addition gives a global element of the presheaf A. Thus for each $I \in \mathcal {C}$ and $\gamma \in \varGamma (I)$ we have $t_{I,\gamma } \in A(I,\gamma )$ satisfying naturality conditions.

Moreover, there is a canonical bijective correspondence between presheaves $\varGamma$ on $\mathcal {C}$ and interpretations of types . This justifies treating contexts as types in $\mathcal {L}$ when it is convenient to do so.

4.3.1 The Interval Type Assumption is Satisfied

Take $\mathbbm {I}$ to be the functor $y_1$ mapping $I \mapsto \mathbf {Hom}_{\mathcal {C}}\left( I,1\right) =\mathbf {DM}\left( I\right)$, where 1 is the (globally) chosen singleton set. Since the theory of De Morgan algebras is geometric and for each I we have a De Morgan algebra, together with the fact that the morphisms are De Morgan algebra morphisms, we have that $\mathbbm {I}$ is an internal De Morgan algebra, as needed.

Moreover the finitary disjunction property axiom is also geometric, and since it is satisfied by each free De Morgan algebra $\mathbf {DM}\left( I\right)$, it also holds internally.

4.3.2 The Glueing Assumption is Satisfied

We will define glueing internally, apart from a “strictness” fix, for which we use the following lemma, which we will also require in Sect. 4.5:

Lemma 4.7

(Strictification) Let C be a small category and $\top$ a global element⁵ of an object $\mathbb {K}$ in $\widehat{C}$. Denote by $[\varphi ]$ the identity type $\varphi =\top$.

Let $\varGamma \vdash \varphi : \mathbb {K}$. Suppose $\varGamma \vdash T, \varGamma , [\varphi ] \vdash A$ and $\varGamma , [\varphi ] \vdash T \cong A$ as witnessed by the terms $\alpha , \beta$ satisfying

$$\begin{aligned}&\varGamma , [\varphi ], x : A \vdash \alpha : T\\&\varGamma , [\varphi ], x : T \vdash \beta : A \end{aligned}$$

plus the equations stating that they are inverses.

Then there exists a type $\varGamma \vdash \mathcal {T}(A,T,\varphi )$ such that

• 1. $\varGamma , [\varphi ] \vdash \mathcal {T}(A,T,\varphi ) = A$

• 2. $\varGamma \vdash T \cong \mathcal {T}(A,T,\varphi )$ by an isomorphism $\alpha ', \beta '$ extending $\alpha$ and $\beta$. This means that the following two judgements hold.

  $$\begin{aligned}&\varGamma , [\varphi ], x : A \vdash \alpha = \alpha ' : T\\&\varGamma , [\varphi ], x : T \vdash \beta = \beta ' : A. \end{aligned}$$

  The judgements are well-formed because in context $\varGamma , [\varphi ]$ the types $\mathcal {T}(A, T,\varphi )$ and A are equal by the first item of this lemma.

• 3. Let $\rho : \varDelta \rightarrow \varGamma$ be a context morphism. Consider its extension $\varDelta , [\varphi \rho ] \rightarrow \varGamma , [\varphi ]$. Then $\mathcal {T}(A,T,\varphi )\rho = \mathcal {T}(A\rho ,T\rho ,\varphi \rho )$.

Proof

We write $T'$ for $\mathcal {T}(A,T,\varphi )$ and define it as follows.

$$\begin{aligned} T'(c,\gamma ) = {\left\{ \begin{array}{ll} A(c,(\gamma , \star )) &{} \text { if } \varphi _{c,\gamma } = \top _c\\ T(c, \gamma ) &{} \text { otherwise} \end{array}\right. } \end{aligned}$$

Here $\star$ is the unique proof of $[\varphi ]$. The restrictions are important. Given $f : (c, \varGamma (f)(\gamma )) \rightarrow \left( d, \gamma \right)$ define $T'(f)$ by cases

$$\begin{aligned} T'(f)(x)&= {\left\{ \begin{array}{ll} A(f)(x) &{} \text { if } \varphi _d(\gamma ) = \top _d(\star )\\ \beta _{c,\varGamma (f)(\gamma ), \star , T(f)(x)} &{} \text { if } \varphi _{c,\varGamma (f)(\gamma )} = \top _c\\ T(f)(x) &{} \text { otherwise } \end{array}\right. } \end{aligned}$$

We need to check that this definition is functorial. The fact that $T'(id) = id$ is trivial. Given $f : (d, \varGamma (f)(\gamma )) \rightarrow \left( c, \gamma \right)$ and $g : \left( e, \varGamma (f\circ g)(\gamma )\right) \rightarrow (d, \varGamma (f)(\gamma ))$ we have

$$\begin{aligned} T'(f \circ g)(x)&= {\left\{ \begin{array}{ll} A(f \circ g)(x) &{} \text { if } \varphi _{c,\gamma } = \top _c\\ \beta _{e,\varGamma (f \circ g)(\gamma ), \star , T(f \circ g)(x)} &{} \text { if } \varphi _{e,\varGamma (f \circ g)(\gamma )} = \top _e\\ T(f \circ g)(x) &{} \text { otherwise } \end{array}\right. } \end{aligned}$$

In the first and third cases this is easily seen to be the same as $T'(g)(T'(f)(x))$, since if $\varphi _{e,\varGamma (f \circ g)(\gamma )} \ne \top _e$ then also $\varphi _{d,\varGamma (f)(\gamma )} \ne \top _d$ by naturality of $\varphi$ and the fact that $\top$ is a global element and the terminal object is a constant presheaf.

So assume the remaining option is the case, that is, $\varphi _{e,\varGamma (f \circ g)(\gamma )} = \top _e$ but $\varphi _{c,\gamma } \ne \top _c$.

We split into two further cases.

• Case $\varphi _{d,\varGamma (f)(\gamma )} = \top _d$. Then $T'(f)(x) = \beta _{d,\varGamma (f)(\gamma ), \star , T(f)(x)}$ and so

  $$\begin{aligned} T'(g)(T'(f)(x)) = T'(g)\left( \beta _{d, (\varGamma (f)(\gamma ), \star , T(f)(x))}\right) \end{aligned}$$

  By naturality of $\beta$ the right-hand side is the same as

  $$\begin{aligned} \beta _{e,\varGamma (f\circ g)(\gamma ), \star , T(f \circ g)(x)} \end{aligned}$$

  which is what is needed.

• Case $\varphi _{d,\varGamma (f)(\gamma )} \ne \top _d$. In this case we have

  $$\begin{aligned} T'(f)(x) = T(f)(x) \end{aligned}$$

  and

  $$\begin{aligned} T'(g)(T'(f)(x)) = \beta _{e,\varGamma (f \circ g)(\gamma ), \star , T(g)(T(f)(x))} \end{aligned}$$

  which is again, as needed by functoriality of T.

Now, directly from the definition we have the equality $\varGamma , [\varphi ] \vdash T' = A$.

It is similarly easy to check the last required property, the naturality of the construction.

$$\begin{aligned} T(A, T, \varphi )\rho = T(A\rho ,T\rho ,\varphi \rho ). \end{aligned}$$

Finally, we extend the isomorphisms $\alpha$ and $\beta$ to $\alpha '$ and $\beta '$.

Define $\beta '$ satisfying $\varGamma , x : T \vdash \beta ':T'$ as

$$\begin{aligned} \beta '_{c,\gamma , x}&= {\left\{ \begin{array}{ll} \beta _{c,\gamma , \star , x} &{}\text { if } \varphi _c(\gamma ) = \top _c(\star )\\ x &{} \text { otherwise } \end{array}\right. } \end{aligned}$$

And $\alpha '$ analogously. One needs to check that this is a natural transformation, i.e., a global element. Finally, $\beta '$ is the inverse to $\alpha '$ by construction. $\square$

Definition of glueing Given the following types and terms

$$\begin{aligned}&\varGamma \vdash \varphi : \mathbbm {F}\\&\varGamma ,\left[ \varphi \right] \vdash T\\&\varGamma \vdash A\\&\varGamma , \left[ \varphi \right] \vdash w : T \rightarrow A \end{aligned}$$

we define a new type $\varGamma \vdash {\text {Glue}}\, \left[ \varphi \mapsto (T,w)\right] \, A$ in two steps.

First we define the type⁶$Glue'_\varGamma (\varphi , T, A, w)$ in context $\varGamma$ as

$$\begin{aligned} Glue'_\varGamma (\varphi , T, A, w) = \sum _{a : A}\sum _{t : \left[ \varphi \right] \rightarrow T}\prod _{p : [\varphi ]} w (t p) = a. \end{aligned}$$

For this type we have the following property (we write $G'$ for $Glue'(\cdots )$)

$$\begin{aligned} \varGamma , [\varphi ] \vdash T \cong G' \end{aligned}$$

with the isomorphism consisting of the second projection from right to left and from left to right we use w to construct the pair.

Finally, we define ${\text {Glue}}\, \left[ \varphi \mapsto (T,w)\right] \, A$ using Lemma 4.7 applied to the type $Glue'$. Let

$$\begin{aligned} \beta : {\text {Glue}}\, \left[ \varphi \mapsto (T,w)\right] \, A \rightarrow Glue'(\varphi , T, A, w) \end{aligned}$$

be the extension of pairing and

$$\begin{aligned} \alpha : Glue'(\varphi , T, A, w) \rightarrow {\text {Glue}}\, \left[ \varphi \mapsto (T,w)\right] \, A \end{aligned}$$

the extension of the projection as per Lemma 4.7.

Define ${\text {unglue}}: {\text {Glue}}\, \left[ \varphi \mapsto (T,w)\right] \, A \rightarrow A$ be the composition of $\beta$ and the first projection $G' \rightarrow A$. Now if $\varphi = \top$ then $\beta$ is just pairing and in this case we also have ${\text {Glue}}\, \left[ \varphi \mapsto (T,w)\right] \, A = T$. So by definition of $G'$ we have ${\text {unglue}}(t) = w t$, validating one of the equalities.

Given $\varGamma , [\varphi ] \vdash t : T$ and $\varGamma \vdash a : A$ satisfying $a = w t$ on $[\varphi ]$ define $\varGamma \vdash {\text {glue}}\, \left[ \varphi \mapsto t\right] \, a : {\text {Glue}}\, \left[ \varphi \mapsto (T,w)\right] \, A$ to be pairing followed by $\alpha$. If $\varphi = \top$ we have, because $\alpha$ is just the projection in this case, that ${\text {glue}}\, \left[ 1 \mapsto t\right] \, a = t$.

To appreciate the technicalities in this section, we remark that $Glue'$ is a pullback. The difference between $Glue'$ and ${\mathsf {Glue}}$ is that the latter is strict when pulling back along the identity morphism. Such coherence issues have discussed at length for the simplicial model; see e.g. Kapulkin and Lumsdaine [20].

4.3.3 The Fibrant Universe Assumption is Satisfied

This will be proved in greater generality in Sect. 4.4.3.

4.3.4 The $\forall$ Assumption is Satisfied

Theorem 4.8

$\widehat{\mathcal {C}}$ models an operation $\forall :\mathbbm {F}^\mathbbm {I}\rightarrow \mathbbm {F}$ which is right-adjoint to the constant map of posets $\mathbbm {F}\rightarrow \mathbbm {F}^\mathbbm {I}$.

Proof

We will first give a concrete description of $\mathbbm {I}$ and $\mathbbm {F}$. We know that $\mathbbm {I}(I)=\mathbf {DM}\left( I\right)$. We use Birkhoff duality [8] between finite distributive lattices and finite posets. This duality is given by a functor $J=\mathbf {Hom}_{\mathrm {fDL}}\left( -,\mathbbm {2}\right)$ from finite distributive lattices to the opposite of the category of finite posets. This functor sends a distributive lattice to its join-irreducible elements. It’s inverse is the functor $\mathbf {Hom}_{\mathrm {poset}}\left( -,\mathbbm {2}\right)$ which sends a poset to its the distributive lattice of lower sets. This restricts to a duality between free distributive lattices and powers of $\mathbbm {2}$. A free De Morgan algebra on I is a free distributive lattice on 2I($=I+I$). We obtain a duality with the category of even powers of $\mathbbm {2}$ and maps preserving the De Morgan involution [14]. Moreover, this duality is poset enriched: If $\psi \le \varphi :\mathbf {DM}\left( I\right) \rightarrow \mathbf {DM}\left( J\right)$, then the corresponding maps on even powers of $\mathbbm {2}$, which are defined by pre-composition, are in the same order relation.

The dual of the inclusion map is the projection $p:\mathbbm {2}^{2(I+1)}\rightarrow \mathbbm {2}^{2I}$. This has a right adjoint: concatenation with 11: $p\alpha \le \beta$ iff $\alpha \le \beta \cdot 11$. Concatenation with 11 is natural:

By duality we obtain a natural right adjoint to the poset-inclusion of DM-algebras. Finally, we recall that in $\widehat{\mathcal {C}}$ we have $\mathbbm {I}^\mathbbm {I}(I)=\mathbbm {I}(I+1)$ and hence we have an internal map $\forall :\mathbbm {I}^\mathbbm {I}\rightarrow \mathbbm {I}$ which is right-adjoint to the constant map $\mathbbm {I}\rightarrow \mathbbm {I}^\mathbbm {I}$.

The lattice $\mathbbm {F}$ is the quotient of $\mathbbm {I}$ by the relation generated by $x\wedge (1-x)=0$ for all x; see [12, p. 7, p. 17]. Duality turns the quotients into inclusions. So, we have the inclusion $\{01,10,11\}^I\subset \mathbbm {2}^{2I}$ as the set of join irreducible elements. Here 00 presents $x\wedge -x$ which is now identified with $\bot$ and hence no longer join-irreducible. This presentation allows us to define $\forall :\mathbbm {F}^\mathbbm {I}\rightarrow \mathbbm {F}$. Since $\mathbbm {F}^\mathbbm {I}(I)=\mathbbm {F}(I+1)$, the right adjoint is again given by concatenation by 11. We just replace $\mathbbm {2}^2$ by $\{01,10,11\}$ in the diagram above. $\square$

4.3.5 Interpreting Base Types

In Sect. 4.1 we did not provide any means of interpreting base types such as ${\mathsf {N}}$. In this section we show that the concrete models we are interested in do support that, but we show this (mostly) externally.

A cubical set A is discrete if $A \cong \varDelta (a)$ for some $a \in {\text {Set}}$, where $\varDelta : {\text {Set}}\rightarrow \widehat{\mathcal {C}}$ is the constant presheaf functor. Equivalently we can characterise discrete types internally, as in Proposition 4.12 below. This characterisation is useful to define composition for discrete types internally.

Lemma 4.9

For any cubical set A and any $I \in \mathcal {C}$ and $i \not \in I$ the function $\beta _I^i : A^\mathbbm {I}(I) \rightarrow A(I,i)$ defined as

$$\begin{aligned} \beta _I^i(f) = f_{\iota }(i), \end{aligned}$$

where $\iota : I \rightarrow I,i$ is the inclusion, is an isomorphism. Moreover the family $\beta$ is natural in I and i in the following sense. For any $J \in \mathcal {C}$ and $j \not \in J$ and any $g : I \rightarrow J$ we have

$$\begin{aligned} A(g + (i \mapsto j)) \circ \beta ^i_{I} = \beta _J^j \circ A^\mathbbm {I}(g). \end{aligned}$$

Corollary 4.10

If the constant map $a \mapsto \lambda \_.a$ of type $A \rightarrow A^\mathbbm {I}$ is an isomorphism, then A is isomorphic to an object of the form $\varDelta (a)$ for some $a \in {\text {Set}}$.

Proof

Using Lemma 4.9 we have that for each I and $i\not \in I, A(\iota ) : A(I) \rightarrow A(I,i)$ is an isomorphism, where, again, $\iota$ is the inclusion. From this we have that for all I, the inclusion $A(\iota _I) : A(\emptyset ) \rightarrow A(I)$ is an isomorphism.

Define $a = A(\emptyset )$ and $\alpha : \varDelta (a) \rightarrow A$ as

$$\begin{aligned} \alpha _I = A(\iota _I). \end{aligned}$$

We then have for any $f : I \rightarrow J$ the following

$$\begin{aligned} A(f) \circ \alpha _I = A(f \circ \iota _I) = A(\iota _J). \end{aligned}$$

The latter because $f \circ \iota _I$ and $\iota _J$ are both maps from the empty set, hence they are equal.

By the previous lemma each $\alpha _I$ is an isomorphism and by the preceding calculation $\alpha$ is a natural transformation. Hence $\alpha$ is a natural isomorphism. $\square$

Lemma 4.11

If A is isomorphic to $\varDelta (a)$ for some $a \in {\text {Set}}$ then the obvious morphism $A \rightarrow A^\mathbbm {I}$ is an isomorphism.

Proof

The inverse to the isomorphism $\beta$ in Lemma 4.9 is the morphism $\alpha _I^i$

$$\begin{aligned} \alpha _I^i(a)_f(j) = A([f,(i\mapsto j)])(a). \end{aligned}$$

By assumption $A(\iota )$ for any inclusion $\iota : I \rightarrow I,i$ is an isomorphism. It is easy to compute that the canonical morphism $A \rightarrow A^\mathbbm {I}$ arises as the composition of $A(\iota )$ and $\alpha _I^i$. $\square$

Proposition 4.12

Let A be a cubical set. The formula

$$\begin{aligned} i : \mathbbm {I}, j : \mathbbm {I}, f : (\mathbbm {I}\rightarrow A) \mid \cdot \vdash f(i) = f(j) \end{aligned}$$

holds in the internal language if and only if A is isomorphic to $\varDelta (a)$ for some $a \in {\text {Set}}$.

Proof

Suppose the formula holds. Then it is easy to see that the constant map from A to $A^\mathbbm {I}$ is an isomorphism (the inverse is given, for instance, by evaluation at 0). Corollary 4.10 implies the result.

Conversely assume $A \cong \varDelta (a)$ for some $a \in {\text {Set}}$. Then by Lemma 4.11 the canonical map ${\text {const}} : A \rightarrow A^\mathbbm {I}$ is an isomorphism. Hence it is internally surjective. Thus for any $f : \mathbbm {I}\rightarrow A$ there is an a in A, such that ${\text {const}} a = f$. From this we immediately have $f(i) = f(j)$ for any i and j in $\mathbbm {I}$. $\square$

Lemma 4.13

Every discrete type $\vdash A$ is fibrant, i.e., it has a composition operator $\mathbf {c}_A : \varPhi (\cdot ;A)$.

Proof

Since A is discrete, we have that $u(0) = u(1)$ for any $u: \varPi (i:\mathbbm {I}).[\varphi ] \rightarrow A$. Therefore $A[\varphi \mapsto u(0)] = A[\varphi \mapsto u(1)]$, so we can choose the constant function $\lambda \gamma , \varphi , u, a. a$ to be $\mathbf {c}_A$, since this will be of type $\varPhi (\cdot , A)$. $\square$

If we have a composition operator $\mathbf {c}_A : \varPhi (\cdot ;A)$ then we can always construct a weakened version $\mathbf {c}_A' : \varPhi (\varGamma ;A)$ for any $\varGamma$, since A does not depend on $\varGamma$.

Therefore we can interpret the natural number type:

$$\begin{aligned} \llbracket \varGamma \vdash {\mathsf {N}} \rrbracket \triangleq (\mathbb {N}, \mathbf {c}_{\mathbb {N}}), \end{aligned}$$

where $\mathbf {c}_{\mathbb {N}}$ is the composition that we get from Lemma 4.13.

4.4 More General Models of $\mathcal {L}$

The type theory $\mathsf {GCTT}$ is an extension of $\mathsf {CTT}$, and we intend to model it in the category of presheaves over $\mathcal {C}\times \omega$. We first need to establish that we can model $\mathsf {CTT}$ in this category. This section shows how to do this by demonstrating that we can lift all constructions of $\mathsf {CTT}$ from the category of cubical sets to $\mathcal {C}\times \mathbb {D}$, for any small category $\mathbb {D}$ with an initial object.

We first prove some general lemmas.

Lemma 4.14

Let $\mathbb {C},\mathbb {D}$ be small categories and let $\pi : \mathbb {C}\times \mathbb {D}\rightarrow \mathbb {C}$ be the projection functor. Then the geometric morphism $\pi ^* \dashv \pi _*$ is open. If $\mathbb {D}$ is inhabited then it is also surjective.

Proof

By Theorem C.3.1.7 of Johnstone [19] it suffices to show that $\pi ^*$ is sub-logical. To show this we use Lemma C.3.1.2 of op. cit (we use notation introduced in that lemma).

Let $b : \pi (I,n) \rightarrow J$ be a morphism in $\mathbb {C}$. Let $U' = (J,n), a = (b, id_n) : (I,n) \rightarrow (J,n), r = id_{J} : \pi U' \rightarrow J$ and $i = id_J : J \rightarrow \pi U'$. Then we have $r \circ i = id_J$ and $i \circ b = \pi a$ as required by Lemma C.3.1.2.

If $\mathbb {D}$ is inhabited the projection $\pi$ is surjective on objects, so the corresponding geometric morphism is surjective; see Johnstone [19, A4.2.7b] $\square$

The above lemma may be read as stating that $\widehat{\mathbb {C}\times \mathbb {D}}$ is a conservative extension of $\hat{\mathbb {C}}$, provided that $\mathbb {D}$ is inhabited.

Lemma 4.15

If $\mathbb {D}$ has an initial object 0, then $\pi ^*$ is full, faithful, and cartesian closed.

Proof

The functor $\pi$ has a left adjoint, which is the functor

$$\begin{aligned}&\iota : \mathbb {C}\rightarrow \mathbb {C}\times \mathbb {D}\\&\iota (I) = (I,0) \end{aligned}$$

Trivially we have $\pi \circ \iota = id_\mathbb {C}$. Thus we have that $\iota ^*$ is left adjoint to $\pi ^*$ and because $\pi \circ \iota = id_\mathbb {C}$ we also have $\iota ^* \circ \pi ^* = id$ and moreover the counit of the adjunction is the identity. Hence the functor $\pi ^*$ is full and faithful [21, Theorem IV.3.1] and by Johnstone [19, Corollary A.1.5.9], since $\iota ^*$ preserves all limits, we have that $\pi ^*$ cartesian closed. $\square$

Let $\varOmega ^\mathbb {D}$ be the subobject classifier of $\widehat{\mathbb {C}\times \mathbb {D}}$ and $\varOmega$ be the subobject classifier of $\widehat{\mathbb {C}}$.

Lemma 4.16

There is a monomorphism$\upsilon : \pi ^*\left( \varOmega \right) \rightarrow \varOmega ^\mathbb {D}$ which fits into the pullback

Proof

As an inverse image, $\pi ^*$ preserves monos. So, $\pi ^*({\top })$ is a mono. Its characteristic map is:

$$\begin{aligned} \upsilon _{I,c}(S) = \left\{ (f,g) \;|\;f \in S \right\} . \end{aligned}$$

This is clearly a mono. $\square$

Corollary 4.17

If $X = \pi ^*(Y)$ then the equality predicate factors uniquely through $\upsilon$ and the inclusion of the equality predicate of Y.

Proof

The equality predicate is by definition the characteristic map of the diagonal $\delta : X \rightarrow X \times X$. Let be the diagonal. Because $\pi ^*$ preserves finite limits the following square is a pullback.

And by uniqueness of characteristic maps we have . Uniqueness of the factorisation follows from the fact that $\upsilon$ is a mono. $\square$

Let $\mathbb {D}$ be a small category with an initial object. We show that .

4.4.1 The Interval Type Assumption is Satisfied

Let . Since $\pi ^*$ preserves products we can lift all the De Morgan algebra operations of $\mathbbm {I}$ to operations on $\mathbbm {I}^{\mathbb {D}}$. The theory of a De Morgan algebra with the finitary disjunction property is geometric [22, Section X.3]. Thus the geometric morphism preserves validity of all the axioms, which means that $\mathbbm {I}^{\mathbb {D}}$ is an internal De Morgan algebra with the finitary disjunction property.

Faces

Lemma 4.18

Let be defined as in Sect. 4.1.1 from $\mathbbm {I}^{\mathbb {D}}$ and $\mathbbm {I}$. Then .

Proof

Let $e : \mathbbm {I}^{\mathbb {D}}\rightarrow \varOmega ^\mathbb {D}$ be the composition where $\delta$ is the diagonal $\mathbbm {I}^{\mathbb {D}}\rightarrow \mathbbm {I}^{\mathbb {D}}\times \mathbbm {I}^{\mathbb {D}}$. By definition $\mathbbm {F}^{\mathbb {D}}$ is the image of e. By Corollary 4.17 and the way we have defined $\mathbbm {I}^{\mathbb {D}}$, and all the operations on it, we have that $e = \upsilon \circ \pi ^*(e')$ where $e' : \mathbbm {I}\rightarrow \varOmega$ is defined analogously to e above. By definition $\mathbbm {F}$ is the image of $e'$. Because inverse images of geometric morphisms preserve image factorisations [34, Remark 1.34], $\pi ^*(\mathbbm {F})$ is the image of $\pi ^*(e')$. So,

$$\begin{aligned} \pi ^*\mathbbm {I}\twoheadrightarrow \pi ^*\mathbbm {F}\rightarrowtail \pi ^*\varOmega {\mathop {\rightarrowtail }\limits ^{\upsilon }}\varOmega ^\mathbb {D}\end{aligned}$$

is the unique factorization of the map $[\cdot =1]:\mathbbm {I}^\mathbb {D}\rightarrow \varOmega ^\mathbb {D}$. $\square$

4.4.2 The Glueing Assumption is Satisfied

This proceeds exactly as in Sect. 4.3.2.

4.4.3 The Fibrant Universe Assumption is Satisfied

To define the fibrant universe it appears necessary to describe compositions externally. The following two lemmas aid in this description because they allow us to simplify the exponential $\varGamma ^\mathbbm {I}$, i.e., the denotation of paths.

Lemma 4.19

Let $\mathbb {C}$ and $\mathbb {D}$ be small categories and assume $\mathbb {C}$ has products. Let $k_1 : \mathbb {C}\rightarrow \widehat{\mathbb {C}}$ and $k_2 : \mathbb {D}\times \mathbb {C}\rightarrow \widehat{\mathbb {D}\times \mathbb {C}}$ be the Yoneda embeddings. Let $\pi ^* : \widehat{\mathbb {C}} \rightarrow \widehat{\mathbb {D}\times \mathbb {C}}$ be the constant presheaf functor.

For any $d, e \in \mathbb {C}$ and any $c \in \mathbb {D}$ there is an isomorphism

$$\begin{aligned} k_2(c, d) \times \pi ^*(k_1 e) \cong k_2(c, d \times e) \end{aligned}$$

in $\widehat{\mathbb {D}\times \mathbb {C}}$ which is natural in c, d and e.

Proof

For any $(c', d') \in \mathbb {D}\times \mathbb {C}$

as required. $\square$

Lemma 4.20

Let $\mathbb {D}$ be a small category. Let $\mathbbm {I}^{\mathbb {D}}\in \widehat{\mathbb {D}\times \mathcal {C}}$ be the inclusion $\pi ^*(\mathbbm {I})$ of $\mathbbm {I}\in \widehat{\mathcal {C}}$. Let $X \in \widehat{\mathcal {C}\times \mathbb {D}}$. Then for any $c \in \mathbb {D}$, any $I \in \mathcal {C}$ and any $i \not \in I$ we have

$$\begin{aligned} X^{\mathbbm {I}^{\mathbb {D}}}(I, c) \cong X(I \cup \{i\},c) \end{aligned}$$

naturally in c, I and i.

Proof

Using the Yoneda lemma and the defining property of exponents we have

recalling that disjoint union is the coproduct in the Kleisli category of the free De Morgan algebra monad, and so disjoint union defines the product in $\mathcal {C}$.

Concretely, the isomorphism $\alpha _{I,i}^c$ maps $\xi \in X^{\mathbbm {I}^{\mathbb {D}}}(I, c)$ to $\xi _{(\iota _{I,i},id_{c}, )}(i)$, where $\iota _{I,i} : I \rightarrow I,i$ (in $\mathcal {C}^{{\text {op}}}$) is the inclusion. Its inverse $\beta _{I,i}^c$ maps $x \in X(I \cup \{i\},c)$ to the family of functions $\xi _{(f,g)} : \mathbbm {I}(J) \rightarrow X(J,d)$ indexed by morphisms $(f,g) : (J,d) \rightarrow (I,c)$ (in $(\mathcal {C}\times \mathbb {D})$). This family is defined as

$$\begin{aligned} \xi _{(f,g)}(\varphi ) = X([g, i \mapsto \varphi ],g)(x) \end{aligned}$$

where $[g, i \mapsto \varphi ]$ is the map $I, i \rightarrow J$ (in $\mathcal {C}^{{\text {op}}}$) which maps i to $\varphi$ and otherwise acts as g. This map is well-defined because disjoint union is the coproduct in $\mathcal {C}^{{\text {op}}}$. $\square$

Definition of the universe We can now define the universe $\mathcal {U}_{f}^\mathbb {D}$. For this we assume a Grothendieck universe $\mathfrak {U}$ in our ambient set theory. First, recall that the Hofmann–Streicher universe $\mathcal {U}^\mathbb {D}$ in $\widehat{\mathcal {C}\times \mathbb {D}}$ maps (I, c) to the set of functors valued in $\mathfrak {U}$ on the category of elements of y(I, c). It acts on morphisms $(I,c) \rightarrow (J,d)$ by composition (in the same way as substitution in types is modelled).

The elements operation

$$\begin{aligned} \frac{\varGamma \vdash a : \mathcal {U}^\mathbb {D}}{\varGamma \vdash {\mathsf {El}}(a)} \end{aligned}$$

is interpreted as

$$\begin{aligned} {\mathsf {El}}(a)((I,c),\gamma ) = a_{(I,c),\gamma }(\star )\left( id_{I,c}\right) , \end{aligned}$$

recalling that terms are interpreted as global elements, and $\star$ is the unique inhabitant of the chosen singleton set.

We define $\mathcal {U}_{f}^\mathbb {D}$ analogously to the way it is defined in Sect. 4.3, that is

$$\begin{aligned} \mathcal {U}_{f}^\mathbb {D}(I,c) = {\text {Ty}}(y(I,c)). \end{aligned}$$

We first look at the following rule.

Let us write . We need to give for each $I \in \mathcal {C}, c \in \mathbb {D}$ and $\gamma \in \varGamma (I,c)$ a pair $(b_0, b_1)$ where

$$\begin{aligned}&y(I,c) \vdash b_0 : \mathcal {U}^\mathbb {D}\\&\cdot \vdash b_1 : \varPhi (y(I,c);{\text {El}}(b_0)) \end{aligned}$$

Now $b_0$ is easy. It is simply $a_{(I,c),\gamma }$. Composition is also conceptually simple, but somewhat difficult to write down precisely. Elements $\gamma \in \varGamma (I,c)$ are in bijective correspondence (by Yoneda and exponential transpose) to terms $\overline{\gamma }$

$$\begin{aligned} \cdot \vdash \overline{\gamma } : {y(I,c)} \rightarrow \varGamma . \end{aligned}$$

Thus we define

$$\begin{aligned} b_1 = \lambda \rho . \mathbf {c}\left( \overline{\gamma } \circ \rho \right) . \end{aligned}$$

One checks that this is well-defined and natural by a tedious computation, which we omit here.

We now look at the converse rule in $\mathcal {L}$

To interpret this rule with $\mathcal {U}_{f}^\mathbb {D}$, we interpret for any a and $\mathbf {c},$ by ${\text {El}}(a)$, where the latter is ${\mathsf {El}}$ map of the Hofmann–Streicher universe.

We need to define ${\text {Comp}}(a)$ which we abbreviate to c. We need to give for each $I \in \mathcal {C}$ and $c \in \mathbb {D}$ an element $c_{I,c} \in \varPhi (\varGamma ;{\text {El}}(a))(I,c)$, and this family needs to be natural in I and c. Given $\gamma \in (\varGamma ^{\mathbbm {I}^{\mathbb {D}}})(I,c)$ and a fresh $i\not \in I$ we get by Lemma 4.20 an element $\gamma ' \in \varGamma \left( (I, i), c\right)$. Let $\overline{\gamma '} : y((I,i),c) \rightarrow \varGamma$ be the morphism corresponding to $\gamma '$ by the Yoneda lemma. Thus we get from a the term $c'_{I,i,c,\gamma }$

$$\begin{aligned} \cdot \vdash c'_{I,i,c,\gamma } : \varPhi (y((I,i),c);{\text {El}}(a) \overline{\gamma '}) \end{aligned}$$

and hence by weakening a term

$$\begin{aligned} y(I,c) \vdash c'_{I,i,c,\gamma } : \varPhi (y((I,i),c);{\text {El}}(a) \overline{\gamma '}) \end{aligned}$$

By Lemma 4.19 and the way $\mathbbm {I}^{\mathbb {D}}$ is defined we have a canonical isomorphism $y((I,i),c) \cong y(I,c) \times \mathbbm {I}^{\mathbb {D}}$. We now apply $c'_{I,i,c,\gamma }$ to the path $\delta = \lambda (i : \mathbbm {I}^{\mathbb {D}}).(\rho , i)$ to get the element

$$\begin{aligned}&\rho : y(I,c) \vdash c'_{I,i,c,\gamma }\delta : \varPi (\varphi : \mathbbm {F})(u : \varPi (i:\mathbbm {I}). \left[ \varphi \right] \rightarrow B(\delta (i))).B(\delta (0))[ \varphi \mapsto u(0) ] \\&\quad \rightarrow B(\delta (1))[ \varphi \mapsto u(1) ] \end{aligned}$$

Where $B = {\text {El}}(a)\overline{\gamma '}$.

From this element we can define $c_{I,c}$ by using the Yoneda lemma again to get the element $\overline{c'_{I,i,c,\gamma }}$ of type

$$\begin{aligned} \varPi (\varphi : \mathbbm {F})(u : \varPi (i:\mathbbm {I}). \left[ \varphi \right] \rightarrow B(\delta (i))).B(\delta (0))[ \varphi \mapsto u(0) ] \rightarrow B(\delta (1))[ \varphi \mapsto u(1) ], \end{aligned}$$

which is a type in context y(I, c), at $(I, c), id_{I,c}$. To recap, the composition c will map $\gamma \in (\varGamma ^{\mathbbm {I}^{\mathbb {D}}})(I,c)$ to the element $\overline{c'_{I,i,c,\gamma }}$.

Lemma 4.21

For any a and $\mathbf {c}$ of correct types we have

4.4.4 The $\forall$ Assumption is Satisfied

Using Lemmas 4.15 and 4.18 we can define $\forall$ in $\widehat{\mathcal {C}\times \mathbb {D}}$ as the inclusion of the $\forall$ from $\widehat{\mathcal {C}}$. Lemma 4.14 can then be used to show that the new $\forall$ is the right adjoint to the map $\varphi \mapsto \lambda \_.\varphi$, and that it preserves joins in the relevant way 4.

4.5 A Model of $\mathsf {GCTT}$

Our construction of a model for $\mathsf {GCTT}$ again proceeds via a dependent predicate logic, extending the language $\mathcal {L}$ used above with counterparts of the later, delayed substitutions, and fixed-point constructs introduced in Sects. 3.1 and 3.2. We call this new language . One difference between $\mathsf {GCTT}$ and is that in the latter our fixed-point combinator has a judgemental equality

The $\mathsf {GCTT}$ term is interpreted as , forgetting r. This is consistent with the motivation for annotating with an interval element r: it is needed to ensure termination of fixed-point unfolding, but it is semantically irrelevant.

Since is an extension of $\mathcal {L}$ we can use it to construct a model of $\mathsf {CTT}$. The interpretation of delayed fixed point combinator and delayed substitutions of $\mathsf {GCTT}$ is straightforward in terms of corresponding constructs of . The most difficult part is showing that the type-former, with delayed substitutions, has compositions, which we do in Sect. 4.5.3. The rest of the section is devoted to providing a model of in the presheaf category $\widehat{\mathcal {C}\times \omega }$. Because of the results of the previous subsection this is immediately a model of $\mathcal {L}$; we need only show that the category $\widehat{\mathcal {C}\times \omega }$ also models the constructs of guarded recursive types. The constructions are straightforward modifications of constructions used to model guarded recursive types in the topos of trees [6, 10], which is the category $\widehat{\omega }$.

4.5.1 The Functor ${\triangleright }$

In this section we sketch how to model the later type, delayed substitutions, and the fixed-point operator of . Since the constructions are straightforward modifications of constructions explained in previous work we omit most proofs. They are, mutatis mutandis, as in previous work.

The ${\triangleright }$ functor on the topos of trees $\widehat{\omega }$ was defined by Birkedal et al. [6]. It is straightforward to extend this to the category $\widehat{\mathcal {C}\times \omega }$, simply ignoring the cube component: given $X \in \widehat{\mathcal {C}\times \omega }$ define

$$\begin{aligned} {\triangleright }{X}(I,n) = {\left\{ \begin{array}{ll} \{\star \} &{} \text { if } n = 0\\ X(I,m) &{} \text { if } n = m + 1 \end{array}\right. } \end{aligned}$$

with restrictions inherited from X; i.e. if $(f, n \le m) : (I,n) \rightarrow (J,m)$ then

$$\begin{aligned} {\triangleright }{X}(f,n \le m)&: X(J,m) \rightarrow X(I,n)\\ {\triangleright }{X}(f,n \le m)&= {\left\{ \begin{array}{ll} ! &{} \text { if } n = 1\\ X(f, k \le m - 1) &{} \text { if } n = k + 1 \end{array}\right. } \end{aligned}$$

where $n \le m$ is the unique morphism $n \rightarrow m$ (and similarly $k \le m - 1$), and ! is the unique morphism into $\{\star \}$, the chosen singleton set.

Less concretely, the functor on $\widehat{\omega }$ arises via a geometric morphism induced by the successor functor on $\omega$ [6, Section 2.2]; the functor above arises similarly from the successor functor on $\mathcal {C}\times \omega$ which is the identity on the cube component.

There is a natural transformation

$$\begin{aligned}&{\text {next}}: id_{\widehat{\mathcal {C}\times \omega }} \rightarrow {\triangleright }\\&\left( {\text {next}}_X\right) _{I,0} =~!\\&\left( {\text {next}}_X\right) _{I,n+1} = X\left( id_I,(n \le n+1)\right) \end{aligned}$$

and a natural family of morphisms making the triple an applicative functor [25].

Lemma 4.22

For any X and any morphism $\alpha : {\triangleright }X \rightarrow X$ there exists a unique global element $\beta : 1 \rightarrow X$ such that

$$\begin{aligned} \alpha \circ {\text {next}}\circ \beta = \beta . \end{aligned}$$

Hence the triple $(\widehat{\mathcal {C}\times \omega },{\triangleright }, {\text {next}})$ is a model of guarded recursive terms [6, Definition 6.1].

Proof

Any global element $\beta$ satisfying the fixed-point equation must satisfy the following two equations

$$\begin{aligned} \beta _{I,0}(\star )&= \alpha _{I,0}(\star )\\ \beta _{I,n+1}(\star )&= \alpha _{I,n+1}\left( \beta _{I,n}(\star )\right) . \end{aligned}$$

Hence define $\beta$ recursively on n. It is then easy to see that $\beta$ is a global element and that it satisfies the fixed-point equation and that it is unique such. $\square$

By Lemma 4.22 and Birkedal et al. [6, Theorem 6.3], ${\triangleright }$ extends to all slices of $\widehat{\mathcal {C}\times \omega }$, and contractive morphisms on slices have unique fixed-points.

The above translations from $\widehat{\omega }$ to $\widehat{\mathcal {C}\times \omega }$ are straightforward, but are not sufficient. First, we need to consider coherence issues, which are ignored by Birkedal et al. [6]. Second, we need to consider delayed substitutions, which we do below, following the development for $\mathsf {GDTT}$ [10]. Third, we need to show that the later types are fibrant, i.e. support the notion of composition, which we do in Sect. 4.5.3.

Delayed substitutions Semantically a delayed substitution of

will be interpreted [10] as a morphism making the following diagram commute

Here is the composition of projections of the form .

In particular, if $\varGamma '$ is the empty context then and so , where $\cdot$ is the empty delayed substitution.

Thus given a delayed substitution and a type

$$\begin{aligned} \varGamma ,\varGamma ' \vdash A \end{aligned}$$

define

to be

Note that this is exactly like substitution $A\xi$, except in the case where $n = 0$.

In turn, we interpret the rules

as follows. First, the empty delayed substitution is interpreted as ${\text {next}}$, as we already remarked above. Given and define

Next The term-level counterpart is interpreted similarly. To interpret the rule

we proceed as follows. Given a term t and a delayed substitution $\xi$ we define the interpretation of

The type and term equalities for delayed substitutions then follow as in previous work.

4.5.2 Dependent Products, Later, and “Constant” Types

To define composition for the ${\triangleright }$ type we will need type isomorphisms commuting ${\triangleright }$ and dependent products in certain cases. We start with a definition.

Definition 4.23

A type $\varGamma \vdash A$ is constant with respect to$\omega$ if for all $I \in \mathcal {C}, n \in \omega , \gamma \in \varGamma (I,n)$ and for all $m \le n$ the restriction

$$\begin{aligned} A(I,n,\gamma ) \rightarrow A\left( I,m,\varGamma (id_I,m \le n)(\gamma )\right) \end{aligned}$$

is the identity function⁷ (in particular, the two sets are equal).

Note that this is a direct generalisation of “being constant” (being in the image of $\pi ^*$) for presheaves (i.e., closed types). Below we will use the shorter notation for $\varGamma (id_I, m\le n)(\gamma )$. We have the following easy, but important, lemma.

Lemma 4.24

Being constant with respect to $\omega$ is closed under substitution. If $\varGamma \vdash A$ is constant and $\rho : \varGamma ' \rightarrow \varGamma$ is a context morphism then $\varGamma ' \vdash A\rho$ is constant.

Lemma 4.25

Let X be a presheaf in the essential image of $\pi ^*$. The identity type $x : X, y : X \vdash {\text {Id}}_{X} (x, y )$ is constant with respect to $\omega$.

Proof

Recall that we have for $\gamma , \gamma ' \in X(I,n)$.

$$\begin{aligned} ({\text {Id}}_{X} (x, y ))(I,n,\gamma ,\gamma ')&= {\left\{ \begin{array}{ll} \{\star \} &{} \text { if } \gamma = \gamma '\\ \emptyset &{} \text { otherwise } \end{array}\right. } \end{aligned}$$

Thus for any $m \le n$

But since is an isomorphism we have if and only if $\gamma = \gamma '$, which concludes the proof. Since all the sets are chosen singletons or the empty set the relevant restrictions are then trivially identity functions. $\square$

Using the assumptions stated above we have the following proposition.

Proposition 4.26

Assume

and further that A is constant with respect to $\omega$.

The canonical morphism from left to right in

(5)

is an isomorphism. The canonical morphism is derived from the term .

Proof

We need to establish an isomorphism of two presheaves on the category of elements of $\varGamma$. Since we already have one of the directions we will first define the other direction explicitly. We define

Let $I \in \mathcal {C}, n \in \omega$ and $\gamma \in \varGamma (I,n)$. Take . If $n = 0$ then we have only one choice.

$$\begin{aligned} F_{I,0,\gamma }(\alpha ) = \star \end{aligned}$$

So assume that $n = m + 1$. Then we need to provide an element of

$$\begin{aligned} F_{I,n,\gamma }(\alpha ) \in \left( \varPi (x : A).B\right) \left( I,m,\xi _{I,n}(\gamma )\right) . \end{aligned}$$

Which means that for each $f : J \rightarrow I$ and each $k \le m$ we need to give a dependent function

$$\begin{aligned}&\beta _{f,k} : (a \in A\left( J,k,(\varGamma ,\varGamma ')(f,k\le m)\left( \xi _{I,n}(\gamma )\right) \right) ) \\&\quad \rightarrow B\left( J,k,(\varGamma ,\varGamma ')(f,k\le m)\left( \xi _{I,n}(\gamma )\right) , a\right) \end{aligned}$$

Because $\varGamma \vdash A$ we have

$$\begin{aligned} A\left( J,k,(\varGamma ,\varGamma ')(f,k\le m)\left( \xi _{I,n}(\gamma )\right) \right) = A\left( J,k,\pi _{J,k}\left( (\varGamma ,\varGamma ')(f,k\le m)\left( \xi _{I,n}(\gamma )\right) \right) \right) \end{aligned}$$

where $\pi : \varGamma ,\varGamma ' \rightarrow \varGamma$ is the composition of projections. By naturality we have

$$\begin{aligned} \pi _{J,k}\left( (\varGamma ,\varGamma ')(f,k\le m)\left( \xi _{I,n}(\gamma )\right) \right) = \varGamma (f,k\le m)\left( \pi _{I,m}\left( \xi _{I,n}(\gamma )\right) \right) . \end{aligned}$$

Now $\pi _{I,m} = {\triangleright }(\pi )_{I,n}$ and so we have (because $\xi$ is a delayed substitution)

$$\begin{aligned} \pi _{I,m}\left( \xi _{I,n}(\gamma )\right) = {\text {next}}(\gamma )_{I,n} = \varGamma (id_I,m \le n)(\gamma ). \end{aligned}$$

Hence we have

$$\begin{aligned} A\left( J,k,(\varGamma ,\varGamma ')(f,k\le m)\left( \xi _{I,n}(\gamma )\right) \right) = A\left( J,k,\varGamma (f, k \le n)(\gamma )\right) . \end{aligned}$$

And because A is constant we further have

$$\begin{aligned} A\left( J,k,\varGamma (f, k \le n)(\gamma )\right) = A(J,k+1,\varGamma (f,k+1 \le n)(\gamma )) \end{aligned}$$

(by assumption $k \le m$ and $n = m + 1$.

Now $\alpha _{f,k+1}$ is a dependent function

And we have

(because the relevant restriction of A is the identity). Now

$$\begin{aligned} \xi _{J,k+1}(\varGamma (f,k+1\le n))&= ({\triangleright }(\varGamma ,\varGamma '))(f,k+1\le n)(\xi _{I,n}(\gamma ))\\&= (\varGamma ,\varGamma ')(f,k\le m)(\xi _{I,n}(\gamma )). \end{aligned}$$

Thus, we can define

$$\begin{aligned} \beta _{f,k} = \alpha _{f,k+1}. \end{aligned}$$

The fact that $\beta$ is a natural family follows from the fact that $\alpha$ is a natural family. Naturality of F follows easily by the fact that restrictions for $\varPi$ types are defined by precomposition.

The fact that it is the inverse to the canonical morphism follows by a tedious computation. $\square$

Corollary 4.27

If $\varGamma \vdash \varphi : \mathbbm {F}$ then we have an isomorphism of types

(6)

Proof

Using Proposition 4.26 it suffices to show that $\varGamma \vdash \left[ \varphi \right]$ is constant with respect to $\omega$. Using Lemmas 4.24 and 4.25 it further suffices to show that the presheaf $\mathbbm {F}$ is in the essential image of $\pi ^*$, which is exactly what Lemma 4.18 states. $\square$

Finally we need the following technical construction, allowing us to view delayed substitutions as terms in a certain way. This is needed in showing that later types have compositions in the following section. Delayed substitutions and later As we mentioned above a delayed substitution $\xi$ is a morphism

$$\begin{aligned} \varGamma \rightarrow {\triangleright }(\varGamma ,\varGamma '). \end{aligned}$$

Hence we can treat it as a term of type ${\triangleright }(\varGamma ,\varGamma ')$ in context $\varGamma$. Further given a morphism $\gamma : \mathbbm {I}^{\omega }\rightarrow \varGamma$ we can form the morphism

$$\begin{aligned} \xi \circ \gamma : \mathbbm {I}^{\omega }\rightarrow {\triangleright }(\varGamma ,\varGamma '). \end{aligned}$$

Finally by using Proposition 4.26 we can transport $\xi \circ \gamma : \mathbbm {I}^{\omega }\rightarrow {\triangleright }(\varGamma ,\varGamma ')$ to a term

$$\begin{aligned} \overline{\xi \circ \gamma } : {\triangleright }(\mathbbm {I}^{\omega }\rightarrow \varGamma ,\varGamma ') \end{aligned}$$

in the empty context. For this term we have the following equality.

Lemma 4.28

Given $\gamma$ and $\xi$ as above then for any type $\varGamma ,\varGamma ' \vdash A$ we have the equality of types

Here $\xi \gamma (i)$ is the delayed substitution obtained by substitution in terms of $\xi$.

Proof

Proof by computation; we require the unfolding of the definition of the isomorphism in Proposition 4.26. $\square$

4.5.3 Interpreting Later Types

The type part of the delayed substitution type is interpreted using delayed substitutions in the language . In this section we show that we can also construct a composition term for this type.

Lemma 4.29

Formation of -types preserves compositions. More precisely, if is a well-formed type in context $\varGamma$ and we have a composition term $\mathbf {c}_A : \varPhi (\varGamma ,\varGamma ';A)$, then there is a composition term .

Proof

We introduce the following variables:

Using Lemma 4.28 we can rewrite the types of u and $a_0$:

Furthermore, we have the following type isomorphisms:

which means that we have a term

We can now—almost—form the term

In order for the composition sub-term to be well-typed, we need that $a_0' = u\, 0$ under the assumption $\varphi$. This is equivalent to saying that the type

is inhabited. We transform the type as follows:

where the last equality uses that $\tilde{u}$ is defined using the inverse of (Proposition 4.26). By assumption it is the case that $\left( {\text {Id}}_{} (a_0, u\, 0 )\right) ^{\varphi }$ is inhabited, and therefore (*) is well-defined. This concludes the existence part of the proof, as

by Lemma 4.28.

We now have to show that the term (*) is equal to $u\, 1$ under the assumption of $\varphi$. Assuming $\varphi$, we get by the properties of $\mathbf {c}_A$ that

and by the definition of $\tilde{u}$ (Proposition 4.26) we have that

as desired. $\square$

Note that in the lemma above we do not require that the types in $\varGamma '$ are fibrant.

4.6 Summary of the Semantics of $\mathsf {GCTT}$

The interpretation of the syntax of $\mathsf {GCTT}$ follows the pattern for interpreting cubical type theory outlined in Cohen et al. [12, Sects. 8.2–8.3], following standard techniques for interpreting dependent type theory in a presheaf category. In summary, the following judgements need to be interpreted.

• 
• 
• 
• 
• 

where the last one is a context morphism. These judgements are interpreted via a partial map from raw (not necessarily well-formed) syntax to objects and arrows of the category. This function merely consists of mapping syntactic constructions to their semantical analogues developed in the previous sections, and so we omit the details. A proof that well-formed syntax has a well-defined intepretation follows from a series of lemmas (c.f. Cohen et al. [12, Lemmas 19–22]) establishing that basic properties such as weakening hold.

Because of the way we developed the results of this section, the interpretations of the judgements in presheaf categories may be separated into three stages.

• 1. Every presheaf topos with a non-trivial internal De Morgan algebra $\mathbbm {I}$ satisfying the disjunction property can be used to give semantics to the subset of the cubical type theory $\mathsf {CTT}$ without glueing and the universe. Further, for any category $\mathbb {D}$, the category of presheaves on $\mathcal {C}\times \mathbb {D}$ has an interval $\mathbbm {I}$, which is the inclusion of the interval in presheaves over the category of cubes $\mathcal {C}$. This was done in Sects. 4.4.1 and 4.4.2.

• 2. The topos of presheaves $\mathcal {C}\times \mathbb {D}$ for any small category $\mathbb {D}$ with an initial object gives a semantics of the entire $\mathsf {CTT}$. This was done in Sects. 4.4.3 and 4.4.4.

• 3. In Sect. 4.5, we showed that the category of presheaves on $\mathcal {C}\times \omega$ gives semantics for $\mathsf {GCTT}$.

For all these three cases we have:

Theorem 4.30

(Soundness and consistency) The interpretation in particular satisfies the following properties. If

is derivable then the types and are interpreted as the same object.

If

is derivable then the terms and are interpreted as equal.

As a consequence, the judgement $\vdash t : {\mathsf {Path\,}}~{\mathsf {N}}~0~1$ is not derivable for any closed term t.

This completes the construction of a model of $\mathsf {GCTT}$, as outlined in the beginning of Sect. 4.

5 Conclusion

In this paper we have made the following contributions:

• We introduce guarded cubical type theory ($\mathsf {GCTT}$), which combines features of cubical type theory ($\mathsf {CTT}$) and guarded dependent type theory ($\mathsf {GDTT}$). The path equality of $\mathsf {CTT}$ is shown to support reasoning about extensional properties of guarded recursive operations, and we use the interval of $\mathsf {CTT}$ to constrain the unfolding of fixed-points.

• We show that $\mathsf {CTT}$ can be modelled in any presheaf topos with an internal non-trivial De Morgan algebra with the disjunction property, glueing, a universe of fibrant types, and an operator $\forall$. Most of these constructions are done via the internal logic. We then show that a class of presheaf models of the form $\widehat{\mathcal {C}\times \mathbb {D}}$, for any small category $\mathbb {D}$ with an initial object, satisfy the above axioms and hence gives rise to a model of $\mathsf {CTT}$.

• We give semantics to $\mathsf {GCTT}$ in the topos of presheaves over $\mathcal {C}\times \omega$.

Further work We wish to establish key syntactic properties of $\mathsf {GCTT}$, namely decidable type-checking and canonicity for base types. Our prototype implementation establishes some confidence in these properties.

We wish to further extend $\mathsf {GCTT}$ with clock quantification [3], such as is present in $\mathsf {GDTT}$. Clock quantification allows for the controlled elimination of the later type-former, and hence the encoding of first-class coinductive types via guarded recursive types. The generality of our approach to semantics in this paper should allow us to build a model by combining cubical sets with the presheaf model of $\mathsf {GDTT}$ with multiple clocks [9]. The main challenges lie in ensuring decidable type checking ($\mathsf {GDTT}$ relies on certain rules involving clock quantifiers which seem difficult to implement), and solving the coherence problem for clock substitution.

The cubical model is constructive, as indicated, for example, by the forthcoming formalization in NuPrl,⁸ so it is tempting to consider our construction as the interpretation of this model in the internal logic of the topos of trees. One technical obstacle to this is the absence of a constructive development of universes in presheaf toposes. Hofmann and Streicher [17] started from a Grothendieck universe in a classical set theory, instead of working in the internal logic of an ambient topos. Moreover, if $\mathbb {D}$ is an internal category in ${\hat{\mathbb {C}}}$, then ${\hat{\mathbb {C}}}^\mathbb {D}\equiv \widehat{\mathbb {C}\times \mathbb {D}}$; c.f. Johnstone [19, Lem. 2.5.3]. However, this is not an isomorphism of categories, so we need to deal with the usual coherence issues when interpreting type theory. Such obstacles are part of active research. For example, see work by Voevodsky on building a new theory of models of type theory [35]. Our present theory centers around the geometric morphism $\hat{\pi _1}:\widehat{\mathcal {C}\times \omega }\rightarrow {\hat{\mathcal {C}}}$. This suggests interpreting the topos of trees in the topos of cubical sets. However, this would not complete the construction of the model, as we would still need to add the compositions operations.

A related question is how $\mathsf {GCTT}$ relates to the model of simplicial presheaves over $\omega$ in Birkedal et al. [4]. However to answer this, one would probably first need to understand the precise relation between the (non-guarded) cubical model and the simplicial model.

Finally, some higher inductive types, like the truncation, can be added to $\mathsf {CTT}$. We would like to understand how these interact with .

Related work Another type theory with a computational interpretation of functional extensionality, but without equality reflection, is observational type theory ($\mathsf {OTT}$) [2]. We found $\mathsf {CTT}$’s prototype implementation, its presheaf semantics, and its interval as a tool for controlling unfoldings, most convenient for developing our combination with $\mathsf {GDTT}$, but extending $\mathsf {OTT}$ similarly would provide an interesting comparison.

Spitters [32] used the interval of the internal logic of cubical sets to model identity types. Coquand [13] defined the composition operation internally to obtain a model of type theory. We have extended both these ideas to a full model of $\mathsf {CTT}$. Recent independent work by Orton and Pitts [29] axiomatises a model for $\mathsf {CTT}$ without a universe, again building on Coquand [13]. With the exception of the absence of the universe, their development is more general than ours. Our semantic developments are sufficiently general to support the sound addition of guarded recursive types to $\mathsf {CTT}$.

A Preserves Commutativity

We provide a formalisation of Sect. 3.3 which can be verified by our type-checker. This file, among other examples, is available in the gctt-examples folder in the type-checker repository.