1611.09263

Model: nemotron-free

## Guarded Cubical Type Theory Lars Birkedal 1 , Aleš Bizjak 1 , Ranald Clouston 1 , Hans Bugge Grathwohl 1 Bas Spitters , and Andrea Vezzosi , 1 2 1 Department of Computer Science, Aarhus University, Denmark 2 Department of Computer Science and Engineering, Chalmers University of Technology, Sweden ## October 9, 2017 ## Abstract This paper improves the treatment of equality in guarded dependent type theory ( GDTT ), by combining it with cubical type theory ( CTT ). 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 GDTT with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-Löf type theory in which the identity type is replaced by abstract paths between terms. 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 ( GCTT ), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of 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 CTT can be given semantics in presheaves on C × D , where C is the cube category, and D is any small category with an initial object. We then show that the category of presheaves on C × ω provides semantics for 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 [7]. 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 Str A = A × Str A , to specify that the head is available now but the tail only later. The type for guarded fixed-point combinators is then ( A → A ) → A , rather than the logically inconsistent ( A → A ) → 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 [27, 3, 1], with semantics in the presheaf category ̂ ω 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 ( 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 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 ) → Id B ( fx ) ( gx ) to proofs of Id ( A → B ) f g , extensionality for guarded recursion requires an extensionality principle for later types, namely the ability to map terms of type Id Atu to proofs of Id ( A ) ( next t ) ( next u ) , where next is the constructor for . These types are isomorphic in the topos of trees, and so in 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 ( CTT ) [12], for which we give a brief introduction in Section 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. CTT was developed primarily to provide a computational interpretation of Voevodsky's univalence axiom in Homotopy Type Theory [33]. The most important novelty of 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. CTT can be extended with identity types which model all rules of intensional equality in Martin-Löf type theory [12, Sec. 9.1], but these are logically equivalent to path types, and in our paper it suffices to work with path types only. CTT has sound denotational semantics in (fibrations in) cubical sets , a presheaf category that is used to model homotopy types. 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 1 . In Section 3 of this paper we propose guarded cubical type theory ( GCTT ), a combination of the two type theories 2 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 CTT to witness functional extensionality, a term can be defined in GCTT to witness extensionality for later types. Further, we use elements of the interval of 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 CTT , extending its expressivity as a basis for formalisation. In Section 4 we give semantics to this type theory via the presheaf category over the product 1 https://github.com/mortberg/cubicaltt 2 with the exception of the clock quantification of GDTT , which we leave to future work. of the categories used to define semantics for GDTT and 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 Section 4.1, an extension of dependent predicate logic in which the constructs of 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 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 [4] 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 3 , extending the implemented type-checker for CTT , which provides confidence in our type theory's syntactic properties. All constructions using the type theory 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 ( CTT ) 4 ; for full details we refer to Cohen et al. [12]. We start with a standard dependent type theory with Π , Σ , natural numbers, and a Russellstyle universe, but without identity types: | Γ , ∆ | ::= | () | Γ ,x : A | Contexts | |---------|---------------------------------|---------------------------------------------------------------------------------------------------------------------------------------|------------------------------------------------------| | t,u,A,B | ::= | | | | | x λx : A.t | tu | ( x : A ) → B ( t,u ) | t. 1 | t. 2 | ( x : A ) × 0 | s t | natrec tu | N U | Variables Π -types Σ -types Natural numbers Universe | We adhere to the usual conventions of considering terms and types up to α -equality, and writing A → B , respectively A × B , for non-dependent Π - and Σ -types. We use the symbol ' = ' for judgemental equality. CTT extends this basic type theory with the constructs below: | r, s | ::= | 0 | 1 | i | 1 - r | r ∧ s | r ∨ s | The interval, | |---------|--------|------------------------------------------------------------------------|-----------------------| | ϕ,ψ | ::= | 0 ❋ | 1 | ( i = 0) | ( i = 1) | ϕ ∧ ψ | ϕ ∨ ψ | ■ The face lattice, ❋ | | Γ , ∆ | ::= | ❋ · · · | Γ , i : | Γ ,ϕ | Contexts | | t,u,A,B | ::= | · · · | | | | | | ■ 〈 i 〉 t | t r | Path A t u | Path types | | | | | [ ϕ 1 t 1 , . ..,ϕ n t n ] | Systems | | | | | comp i A [ ϕ ↦→ u ] t | Compositions | | | | | glue [ ϕ ↦→ t ] u | unglue t | Glue [ ϕ ↦→ ( B,t )] A | Glueing | We now briefly discuss these constructs. 3 http://github.com/hansbugge/cubicaltt/tree/gcubical 4 http://www.cse.chalmers.se/~coquand/selfcontained.pdf provides a concise presentation of CTT .    Figure 1: Typing rules for path types. The central novelty of CTT is its treatment of equality. Instead of the inductively defined identity types of intensional Martin-Löf type theory [23], 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 ■ to A , with endpoints t and u . Rather than defining the interval ■ concretely as the unit interval [0 , 1] ⊆ R , it is defined as the free De Morgan algebra on a discrete infinite set of names { i, j, k, . . . } with endpoints 0 and 1 . A De Morgan algebra is a bounded distributive lattice with an involution 1 -· satisfying the De Morgan laws  The interval [0 , 1] ⊆ R , with min , max and 1 -· , is an example of a De Morgan algebra. The judgement Γ r : ■ means that r draws its names from Γ . Despite this notation, ■ is not a first-class type. Path types and their elements are defined by the rules in Figure 1. Path abstraction , 〈 i 〉 t , and path application , t r , are analogous to λ -abstraction and function application, and support the familiar β -equality ( 〈 i 〉 t ) r = t [ r/i ] and η -equality 〈 i 〉 t i = t . There are two additional judgemental equalities for paths, regarding their endpoints: given p : Path A t u we have p 0 = t and p 1 = u . 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:  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 , ❋ , defined as the free distributive lattice on the symbols ( i = 0) and ( i = 1) for all names i , quotiented by the relation ( i = 0) ∧ ( i = 1) = 0 ❋ . As with the interval, ❋ is not a first-class type, but the judgement Γ ϕ : ❋ asserts that ϕ draws its names from Γ . We also have the judgement Γ ϕ = ψ : ❋ which asserts the equality of ϕ and ψ in the face lattice. Contexts can be restricted by elements of ❋ . Such a restriction affects equality judgements so that, for example, Γ , ϕ ψ 1 = ψ 2 : is equivalent to Γ ϕ ∧ ψ 1 = ϕ ∧ ψ 2 : ❋ ❋ We write Γ t : A [ ϕ ↦→ u ] as an abbreviation for the two judgements Γ t : A and Γ , ϕ t = u : A , noting the restriction with ϕ 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 Path types  ❋ where a has type A [0 /i ] . 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 [ ϕ 1 ↦→ t 1 , . . . , ϕ n ↦→ t n ] as an abbreviation for [ ϕ 1 ∨ . . . ∨ ϕ n ↦→ [ ϕ 1 t 1 , . . . , ϕ n t n ]] . A non-trivial example of the use of systems is the proof that Path is transitive; given p : Path A a b and q : Path A b c we can define   This builds a path between the appropriate endpoints because we have the equalities comp j A [1 ❋ ↦→ a ] ( p 0) = a and comp j A [1 ↦→ q j ] ( p 1) = q 1 = c . ❋ 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 Equiv T A is the type of equivalence between types T and A , whose formal definition we omit. We also have the following equations:  ## 3 Guarded Cubical Type Theory The section introduces constructs from guarded dependent type theory ( GDTT ) to CTT , to define guarded cubical type theory ( GCTT ): Delayed substitutions   Figure 2: Formation rules for delayed substitutions.  Figure 3: Typing rules for later types. recalling that r is an element of the interval. This section will also present examples that show how GCTT can be used to prove properties of guarded recursive constructions. ## 3.1 Later Types In Figure 3 we present the 'later' types of guarded dependent type theory ( GDTT ) [10], with judgemental equalities in Figures 4 and 5. Note that we do not add any new equation for the interaction of compositions with : while comp i ξ.A [ ϕ ↦→ u ] t 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 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. The typing rules use the delayed substitutions of GDTT , as defined in Figure 2. 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 t : A , 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 A to be unwrapped by and next . As observed by Bizjak et al. [10], these constructions generalise the applicative functor [25] structure of 'later' types, by the definitions pure t next t , and f t next [ f ′ ← f, t ′ ← t ] . f ′ t ′ , and also generalise the operation from simple functions to Π -types. We here make the new observation that delayed substitutions can express the function ̂ : U → U , introduced by Birkedal and Møgelberg [5] to express guarded recursive types as fixed-points on universes, as λu. [ u ′ ← u ] .u ′ ; see for example the definition of streams in Section 3.3. Example 3.1. In GDTT it is essential that we can convert terms of type ξ. Id A t u into terms of type Id ξ .A ( next ξ. t ) ( next ξ. u ) , so that we may perform Löb induction , the technique of proof by guarded recursion where we assume p , deduce p , and hence may conclude p with no assumptions. This is achieved in GDTT by postulating as an axiom the following judgemental equality:  A term from left-to-right of (1) can be defined using the 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 GCTT we can define a term with the desired type:    Figure 4: Type equality rules for later types (congruence and equivalence rules are omitted).  Figure 5: Term equality rules for later types. We omit congruence and equivalence rules, and the rules for terms of type U , which reflect the type equality rules of Figure 4.   Figure 6: Typing and equality rules for the delayed fixed-point Note the similarity of this term and type with that of funext , for functional extensionality, presented on page 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 GCTT by addressing fixed points. In GDTT there are fixed-point constructions fix x.t with the judgemental equality fix x.t = t [ next fix x.t/x ] . In 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 fix i x.t inhabiting N . To avoid this, we introduce the delayed fixed-point combinator 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 Figure 6. We will write fix r x.t for t [ dfix r x.t/x ] , fix x.t for fix 0 x.t , and dfix x.t for dfix 0 x.t . Lemma 3.2 (Canonical unfold lemma) . For any term Γ , x : A t : A there is a path between fix x.t and t [ next fix x.t/x ] , given by the term 〈 i 〉 fix i x.t . Transitivity of paths (via compositions) ensures that fix x.t 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 f : A → A if there is a path from a to f ( next a ) . Proposition 3.3 (Unique guarded fixed points) . Any guarded fixed-point a of a term f : A → A is path equal to fix x.f x . Proof. Given p : Path A a ( f ( next a )) , 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 fix x.f x . 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 fix x.f x . We can write out our full proof term, where p -1 is the inverse path of p , as  ## 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 GCTT , as with GDTT , are defined as fixed points on the universe:  Note the use of a delayed substitution to transform a term of type U to one of type U , as discussed at the start of Section 3.1. Desugaring to restate this in terms of dfix , we have  The head function hd : Str A → A is the first projection. The tail function, however, cannot be the second projection, since this yields a term of type  rather than the desired Str A . However we are not far off; Str A 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 U from Str A to A × Str A ; call this path 〈 i 〉 Str i A . 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 tl : Str A → Str A by composing the second projection with unfold , so tl s ( unfold s ) . 2 . Similarly we can define the stream constructor cons (usually written infix as :: ) by using fold :  We now turn to higher order functions on streams. We define zipWith : ( A → B → C ) → Str A → Str B → Str C , the stream function which maps a binary function on two input streams to produce an output stream, as  Of course zipWith is definable even with simple types and , but in GCTT we can go further and prove properties about the function: Proposition 3.4 ( zipWith preserves commutativity) . If f : A → A → B is commutative, then zipWith f : Str A → Str A → Str B is commutative. Proof. Let c : ( a 1 : A ) → ( a 2 : A ) → 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 : ■ be a fresh name, and s 1 , s 2 : Str A . Our aim is to construct a stream which is zipWith f s 1 s 2 when substituting 0 for i , and 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 zipWith f s 1 s 2 , but unfolded once . Similarly, v [1 /i ] is zipWith f s 2 s 1 unfolded once. Let 〈 j 〉 zipWith j be the canonical unfold lemma associated with 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. Bisimularity equals equality Two (guarded) streams are bisimilar when both their heads and tails are equal. In 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 s, t : Str A , there is a term of type Path U ( bisim A s t )( Path Str A s t ) . Proof. We may strengthen extensionality for later (Equation 2), 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 s, t : Str A , we have the following chain of equivalences:  The last equivalence is constructed from the fold and unfold functions for streams. The statement then follows from univalence. 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 [7]. Here we consider a simple example of a negative variance recursive type, namely Rec A fix x. ( [ x ′ ← x ] .x ′ ) → A , which is path equal to Rec A → A . 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 fold and unfold are the transports along the path between Rec A and Rec A → A . As with zipWith , Y can be defined with simple types and [1]; what is new to GCTT is that we can also prove properties about it: Proposition 3.6 ( Y is a guarded fixed-point combinator) . Y f is path equal to f ( next ( Y f )) , for any f : A → A . Therefore, by Proposition 3.3, Y is path equal to fix . Proof. Y f simplifies to f ( next ( unfold ( fold ∆)( next fold ∆))) , and unfold ( fold ∆) is path equal to ∆ . A congruence over this path yields our path between Y f and f ( next ( Y f )) . ## 4 Semantics In this section we provide sound semantics of GCTT , and hence prove the consistency of GCTT . The semantics is based on the category ̂ C × ω of presheaves on the category C × ω , where C is the category of cubes [12] and ω is the poset of natural numbers. Given a countably infinite set of names i, j, k, . . . , the category C has as objects finite sets of names I, J , and as morphisms I → J , functions J → DM ( I ) , where DM ( I ) 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 GCTT are interpreted as objects of ̂ C × ω . Following the approach of Cohen et al. [12] types in context Γ are interpreted as pairs ( A,c A ) of a presheaf A on the category of elements of Γ 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 Section 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. Figure 7: Judgements of the dependent predicate logic L . | Γ | well-formed context | |----------------------------------|-----------------------| | Γ A | well-formed type | | Γ t : A | typing judgement | | Γ A = B | type equality | | Γ t = u : A | term equality | Working at this level, the notion of a model of CTT can be generalised from the category ̂ C of cubical sets to any topos whose internal logic satisfies the four assumptions. In particular, these assumptions hold in the presheaf category ̂ C × D for any small category D with an initial object. The category ̂ C × ω is obviously such a category; we will show that it is one that also allows the constructions of guarded recursion introduced in Section 3 to be modelled. The notion of a model of GCTT is then formulated as follows: a type of GCTT in context Γ is interpreted as a pair of a type Γ A in the internal language of ̂ C × ω , and a composition structure c A , where c A is a term in the internal language of a specific type Φ(Γ; A ) which we define below after introducing the necessary constructs. A term of 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: Section 4.1 presents the general intermediate language L which we use to interpret GCTT in. Section 4.2 models CTT in L . Section 4.3 models L in the category of cubical sets. Section 4.4 considers more general models of L . Section 4.5 models GCTT in an extension of L . Section 4.6 gives a summary of the semantics. ## 4.1 The Dependent Predicate Logic L Instead of formulating our model directly using regular mathematics, we will specify a typetheoretic language L , tailor-made for the purpose of our model, and inspired by the internal logic of the presheaf topos of cubical sets, ̂ C . 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 Ω for the type of propositions, for true and ⊥ for false. In addition to the equality proposition t = u : A , we also have the extensional identity type Id A ( t, u ) with equality reflection:  Id (the type) and · = · (the proposition) are equally expressive, but for presentation purposes it is practical to have both: Using 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 Id A ( t, u ) → 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 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 Γ , p : Id Ω ( ϕ, ) as Γ , ϕ . Following Cohen et al. [12], our syntax in Section 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 El . These universes can be interpreted in presheaf models. To facilitate the interpretation of the fibrant universe (in Section 4.4.3) we assume that our intermediate language L contains an explicit 'elements-of' operation El for a universe U of small types. We now turn to the first of our four assumptions necessary for modelling CTT . Assumption 1 (Interval type) . In L we have a type 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 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 Section 2 to the language L . We will see three further assumptions, for modelling glueing and the universe, in Section 4.1.2. Faces. Using the interval we define the type ❋ as the image of the function · = 1 : ■ → Ω . More precisely, ❋ is the subset type ❋ { p : Ω | ∃ ( i : ■ ) , p = ( i = 1) } We will implicitly use the inclusion ❋ → Ω . The following lemma in particular states that the inclusion is compatible with all the lattice operations, hence omitting it is unambiguous. ## Lemma 4.1. - ❋ is a lattice for operations inherited from Ω . · The corestriction · = 1 : → is a lattice homomorphism.  - ■ ❋ · inherits the disjunction property from . ] ❋ For this type we have the logical equivalence ( ∃ ! p : [ ϕ ] , ) ⇔ ϕ which we use below when passing between type-theoretic and logical views in constructions of compositions. Partial elements. Given Γ A and Γ ϕ : ❋ we say that a term t is a partial element of A of extent ϕ , if Γ t : Π( p : [ ϕ ]) .A . If we are in a context with p : [ ϕ ] , 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 Γ , [ ϕ ] for Γ , p : [ ϕ ] , and [ ϕ ] → B for the dependent function space Π( p : [ ϕ ]) .B , leaving the proof variable p implicit. If we have a term Γ , p : [ ϕ ] u : A (a partial element), then we define  as the type of elements of a which equal the partial element u on extent ϕ . 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 ϕ . We do not construct the second component explicitly. Systems. Given Γ 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    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  where the type on the right hand side is using the definition (4). Note that A [ ϕ ↦→ t ] is unambiguous, as we have Γ , [ ϕ ] [ ϕt ] = t : A . Compositions. Given Γ A , we can define the type of compositions :  where Here we treat the context Γ 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 ( γ ( i )) means substitution along the (uncurried) γ , by which we mean the following. Given some term γ of type ■ → Γ in some context Γ ′ , there is the 'uncurried' term Γ ′ , i : ■ γ ( i ) : Γ which arises by application of γ to i . Finally, we assume the variable i appearing in the type of u is fresh for ϕ , γ and A . ■ Recall that we call a pair of a type Γ A in L together with a term c : Φ(Γ; A ) a fibrant type . Note that there is an important difference between the type of compositions in L as defined above and the form of the rule for compositions in CTT . In the latter the type A depends on ■ , 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 Γ , which gives a dependence of A on . Fillings. Given Γ A , we can define the type of (Kan) fillings : ``` ``` If we have a filling operation f : Ψ(Γ , A ) then we can get a path lifting operation which states that given a path γ and an element a 0 in A over γ (0) we get a path in A which starts at a 0 . Concretely, path lifting is the term of the following type ``` ``` It is defined as a degenerate case of f where ϕ is ⊥ , and u therefore is uniquely determined (since it is a partial function defined where ⊥ 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 Γ A with c A : Φ(Γ; A ) , then we have a filling operation f : Ψ(Γ , A ) . Proof. We introduce the variables of appropriate types: We need to find a term of type ``` ```  We check that the following system is well-defined (in a context with ϕ ∨ ( i = 0) ):  - If ϕ , then u ( i ∧ j ) : A ( γ ( i ∧ j )) . - If i = 0 , then π 1 a 0 : A ( γ (0)) = A ( γ ( i ∧ j )) . - If ϕ and i = 0 , then π 1 a 0 = u (0) = u ( i ∧ j ) . Note also that this means that  and therefore we can write the following term:  which has the type as was needed. Path types. Given Γ A and terms Γ t, u : A , we can define the Path type Path A t u Π( i : ■ ) .A [(1 -i ) ↦→ t, i ↦→ u ] as the type of paths in A , i.e., terms of type → 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 CTT . One difference is that in the formation rule for 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 Path type, when proving that glueing is fibrant in Lemma 4.6.  Assumption 3 (Fibrant universe) . There is a fibrant universe U f which contains pairs of a code in U with an associated composition operator:  satisfying  Assumption 4 ( ∀ ) . We assume that the map ϕ ↦→ λ \_ .ϕ : ❋ → ( ■ → ❋ ) between posets has an internal right adjoint ∀ . Concretely this means that for any ϕ : and any f : → we assume  ## ■ 4.2 A Model of CTT in fibrant types in L In this section we show how to use the assumptions from the preceding section to interpret CTT . In the following sections we show how to extend the interpretation to GCTT . We fix a presheaf category which models L and define a category with families [15] by specifying the type and term functors Ty and Tm . The base category of the category with families, the category of contexts, is the chosen presheaf category. We use the language L as the internal language of the presheaf category to describe the objects and morphisms. Thus to construct the model of CTT we reuse the types and terms of the language 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 L . Note that if A and B are equivalent types then Φ(Γ; A ) and Φ(Γ; 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 L respect judgemental equality. Note that the context Γ 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: Γ .A ΣΓ A , p π 1 , and q π 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 L .  By assumption we have c A of type Φ(Γ , 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 γ : Γ c A ( λ ( i : ■ ) . ( γ, i )) ϕ ( λ ( i : ■ )( p : [ ϕ ]) .u ) a 0 : A ( γ (1))[ ϕ ↦→ u (1)] where we have omitted writing the proof u (0) = a 0 on [ ϕ ] . This proof is constructed from the third premise of the rule. ## 4.2.2 Interpreting dependent function types Assume that J Γ A ′ K = ( A, c A ) and J Γ , x : A ′ B ′ K = ( B, c B ) . We define  where c Π( x : A ) .B : Φ(Γ;Π( x : A ) .B ) comes from the following lemma. Lemma 4.3 ( cf. [13, Proposition 0 . 3 ]) . Π -types preserve compositions: if we have composition terms c A : Φ(Γ; A ) and c B : Φ(Γ .A ; B ) , then we can form a new composition c Π( x : A ) .B : Φ(Γ , Π( x : A ) .B ) . Proof. Recall that Π -types commutes with substitution:  where B ( γ ) is a type in the context with A . We introduce the variables:  We need to find an element in  along with a proof that it is u (1) when ϕ = 1 . Let a 1 : A ( γ (1)) be given. We define a ( i ) : A ( γ ( i ))[ i ↦→ a 1 ] by using path lifting on a 1 , i.e.,  where is the filling operation defined earlier. Then  will have the type B ( γ (1))[ ϕ ↦→ u (1) a 1 ] . So λa 1 .π 1 b 1 has the type we are looking for. Now assume ϕ = ; then λa 1 .b 1 = λa 1 .u ( i ) a 1 = u ( i ) , which is what we needed. ## 4.2.3 Interpreting dependent sum types Dependent sum types ( x : A ) × B are interpreted by Σ -types from L , along with the composition operation that comes from the following lemma: Lemma 4.4. Σ -types preserve compositions: if we have composition terms c A : Φ(Γ; A ) and c B : Φ(Γ .A ; B ) , then we can form a new composition c Σ( x : A ) .B : Φ(Γ , Σ( 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 CTT by using the systems of L , and by using the fact that systems preserve compositions: If we have a system Γ [ ϕ 1 A 1 , . . . , ϕ n A n ] , then we can define a new composition using a system consisting of the compositions of all the components:  where γ m : → Γ , [ ϕ m ] is the context map γ extended with the witness of [ ϕ m ] . ## ■ 4.2.5 Interpreting path types We interpret the path types:  where J A K = ( A ′ , c A ) and c : Φ(Γ;Path A ′ J t K J s K ) comes from Lemma 4.5. Lemma 4.5. Path-types preserve composition: if Γ A is fibrant, then for any Γ t, s : A , we have a composition operator c : Φ(Γ;Path A t s ) . Proof. First note that if we have Γ Path A t s : and γ : Γ , then Now let   be given. Our goal is to find a term p 1 such that  We will do this by finding a term q : Π( i : ■ ) .A ( γ 1)[ ϕ ↦→ u 1 i ] , for which we verify that q 0 = t ( γ 1) and q 1 = s ( γ 1) , in other words,  ■ as this will be equivalent to having such a p 1 . Let i : ■ . By leaving some equality proofs implicit we can define the system r ( j ) [ ϕuj i, (1 -i ) t ( γ j ) , is ( γ j )] : Π( j : ■ ) . [ ϕ ∨ (1 -i ) ∨ i ] → A ( γ j ) , which is well-defined because uj 0 = t ( γ j ) and uj 1 = s ( γ j ) . We also have that p 0 i : A ( γ 0)[ ϕ ↦→ u 0 i ] , and since p 0 0 = t ( γ 0) and p 0 1 = s ( γ 0) , we can say that  so we can use the fibrancy of A to define the term  which is what we wanted. ## 4.2.6 Interpreting glue types We interpret Glue from CTT using Glue from L along with a composition operator, which we have by the following lemma: Lemma 4.6. Glueing is fibrant, i.e., if we have  then there is a term c : Φ(Γ;Glue [ ϕ ↦→ ( T, w )] A ) . The construction of c in the proof of the above lemma is analogous to the construction of the composition operation for glueing in CTT [12], but formulated in L . A crucial part of the construction is the face δ ∀ ( ϕ ◦ γ ) , where γ : ■ → Γ , which satisfies that [ δ ] implies [ ϕ ( γ i )] for all i : . ## ■ 4.2.7 Interpreting the universe The universe of CTT is interpreted using the universe of fibrant types U f . To define the composition for the universe we follow the construction of Cohen et al. [12] in the language L . ## 4.3 A Model of L in Cubical Sets In this section we construct a model of L in the category of cubical sets. Recall that the category of cubes C has as objects finite sets of names i, j, k, . . . and as morphism the functions J → DM ( I ) where DM ( I ) is the free De Morgan algebra on I . Alternatively, C can be described as the opposite of the Kleisli category of the free De Morgan algebra monad on Fin . The category of cubical sets is then the category ̂ C of presheaves on C . In the previous section we showed how to construct a model of CTT using L . Constructing a model of L in cubical sets then shows we can give a model of 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 CTT in the subsequent section. In particular, we shall use presheaves over C × ω to model the full GCTT type theory.  The references in Section 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 Γ is interpreted as a presheaf. - The judgement Γ A gives a pair of a presheaf Γ on C and a presheaf A on the category of elements of Γ . - The judgement Γ t : A in addition gives a global element of the presheaf A . Thus for each I ∈ C and γ ∈ Γ( I ) we have t I,γ ∈ A ( I, γ ) satisfying naturality conditions. Moreover, there is a canonical bijective correspondence between presheaves Γ on C and interpretations of types · Γ . This justifies treating contexts as types in L when it is convenient to do so. ## 4.3.1 The interval type assumption is satisfied Take ■ to be the functor y 1 mapping I ↦→ Hom C ( I, 1) = DM ( I ) , 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 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 DM ( I ) , 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 Section 4.5: Lemma 4.7 (Strictification) . Let C be a small category and a global element 5 of an object K in ̂ C . Denote by [ ϕ ] the identity type ϕ = . Let Γ ϕ : K . Suppose Γ T , Γ , [ ϕ ] A and Γ , [ ϕ ] T ∼ = A as witnessed by the terms α, β satisfying  plus the equations stating that they are inverses. Then there exists a type Γ T ( A,T,ϕ ) such that 1. Γ , [ ϕ ] T ( A,T,ϕ ) = A 2. Γ T ∼ = T ( A,T,ϕ ) by an isomorphism α ′ , β ′ extending α and β . This means that the following two judgements hold.    The judgements are well-formed because in context Γ , [ ϕ ] the types T ( A,T,ϕ ) and A are equal by the first item of this lemma. 5 For a constructive meta-theory we add that, for each c , equality with c is decidable. 3. Let ρ : ∆ → Γ be a context morphism. Consider its extension ∆ , [ ϕρ ] → Γ , [ ϕ ] . Then T ( A,T,ϕ ) ρ = T ( Aρ,Tρ,ϕρ ) . Proof. We write T ′ for T ( A,T,ϕ ) and define it as follows.  Here is the unique proof of [ ϕ ] . The restrictions are important. Given f : ( c, Γ( f )( γ )) → ( d, γ ) define T ′ ( f ) by cases  We need to check that this definition is functorial. The fact that T ′ ( id ) = id is trivial. Given f : ( d, Γ( f )( γ )) → ( c, γ ) and g : ( e, Γ( f ◦ g )( γ )) → ( d, Γ( f )( γ )) we have  In the first and third cases this is easily seen to be the same as T ′ ( g )( T ′ ( f )( x )) , since if ϕ e, Γ( f ◦ g )( γ ) = e then also ϕ d, Γ( f )( γ ) = d by naturality of ϕ and the fact that is a global element and the terminal object is a constant presheaf. So assume the remaining option is the case, that is, ϕ e, Γ( f ◦ g )( γ ) = e but ϕ c,γ = c . We split into two further cases. - Case ϕ d, Γ( f )( γ ) = d . Then T ′ ( f )( x ) = β d, Γ( f )( γ ) ,,T ( f )( x ) and so  By naturality of β the right-hand side is the same as  which is what is needed. and - Case ϕ d, Γ( f )( γ ) = d . In this case we have   which is again, as needed by functoriality of T . Now, directly from the definition we have the equality Γ , [ ϕ ] T ′ = A . It is similarly easy to check the last required property, the naturality of the construction.  Finally, we extend the isomorphisms α and β to α ′ and β ′ . Define β ′ satisfying Γ , x : T β ′ : T ′ as  And α ′ analogously. One needs to check that this is a natural transformation, i.e., a global element. Finally, β ′ is the inverse to α ′ by construction. Definition of glueing. Given the following types and terms     we define a new type Γ Glue [ ϕ ↦→ ( T, w )] A in two steps. 6 ′ First we define the type Glue Γ ( ϕ, T, A, w ) in context Γ as  For this type we have the following property (we write G ′ for Glue ′ ( · · · ) )  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 Glue [ ϕ ↦→ ( T, w )] A using Lemma 4.7 applied to the type Glue ′ . Let  be the extension of pairing and  the extension of the projection as per Lemma 4.7. Define unglue : Glue [ ϕ ↦→ ( T, w )] A → A be the composition of β and the first projection G ′ → A . Now if ϕ = then β is just pairing and in this case we also have Glue [ ϕ ↦→ ( T, w )] A = T . So by definition of G ′ we have unglue( t ) = wt , validating one of the equalities. Given Γ , [ ϕ ] t : T and Γ a : A satisfying a = wt on [ ϕ ] define Γ glue [ ϕ ↦→ t ] a : Glue [ ϕ ↦→ ( T, w )] A to be pairing followed by α . If ϕ = we have, because α is just the projection in this case, that glue [1 ↦→ t ] a = t . To appreciate the technicalities in this section, we remark that Glue ′ is a pullback. The difference between Glue ′ and 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]. 6 This type is already present in Kapulkin and Lumsdaine [20, Theorem 3.4.1]. ## 4.3.3 The fibrant universe assumption is satisfied This will be proved in greater generality in Section 4.4.3. ## 4.3.4 The ∀ assumption is satisfied Theorem 4.8. ̂ C models an operation ∀ : ❋ ■ → ❋ which is right-adjoint to the constant map of posets → . ✷ The dual of the inclusion map is the projection p : ✷ 2( I +1) → ✷ 2 I . This has a right adjoint: concatenation with 11: pα ≤ β iff α ≤ β · 11 . Concatenation with 11 is natural: ❋ ❋ ■ Proof. We will first give a concrete description of ■ and ❋ . We know that ■ ( I ) = DM ( I ) . We use Birkhoff duality [8] between finite distributive lattices and finite posets. This duality is given by a functor J = Hom fDL ( -, ✷ ) 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 Hom poset ( -, ✷ ) which sends a poset to its the distributive lattice of lower sets. This restricts to a duality between free distributive lattices and powers of ✷ . A free De Morgan algebra on I is a free distributive lattice on 2 I ( = I + I ). We obtain a duality with the category of even powers of ✷ and maps preserving the De Morgan involution [14]. Moreover, this duality is poset enriched: If ψ ≤ ϕ : DM ( I ) → DM ( J ) , then the corresponding maps on even powers of , which are defined by pre-composition, are in the same order relation.  ■ ■ ■ The lattice ❋ is the quotient of ■ by the relation generated by x ∧ (1 -x ) = 0 for all x ; see [12, p7,p17]. Duality turns the quotients into inclusions. So, we have the inclusion { 01 , 10 , 11 } I ⊂ ✷ 2 I as the set of join irreducible elements. Here 00 presents x ∧ -x which is now identified with ⊥ and hence no longer join-irreducible. This presentation allows us to define ∀ : ❋ ■ → ❋ . Since ❋ ■ ( I ) = ❋ ( I +1) , the right adjoint is again given by concatenation by 11 . We just replace ✷ 2 by { 01 , 10 , 11 } in the diagram above. ✷ ✷ By duality we obtain a natural right adjoint to the poset-inclusion of DM-algebras. Finally, we recall that in ̂ C we have ■ ■ ( I ) = ■ ( I +1) and hence we have an internal map ∀ : ■ ■ → ■ which is right-adjoint to the constant map → . ## 4.3.5 Interpreting base types In Section 4.1 we did not provide any means of interpreting base types such as 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 ∼ = ∆( a ) for some a ∈ Set , where ∆: Set → ̂ 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 ∈ C and i ∈ I the function β i I : A ■ ( I ) → A ( I, i ) defined as  where ι : I → I, i is the inclusion, is an isomorphism. Moreover the family β is natural in I and i in the following sense. For any J ∈ C and j ∈ J and any g : I → J we have A ( g +( i ↦→ j )) ◦ β i I = β j J ◦ A ■ ( g ) . Corollary 4.10. If the constant map a ↦→ λ \_ .a of type A → A ■ is an isomorphism, then A is isomorphic to an object of the form ∆( a ) for some a ∈ Set . Proof. Using Lemma 4.9 we have that for each I and i ∈ I , A ( ι ) : A ( I ) → A ( I, i ) is an isomorphism, where, again, ι is the inclusion. From this we have that for all I , the inclusion A ( ι I ) : A ( ∅ ) → A ( I ) is an isomorphism. Define a = A ( ∅ ) and α : ∆( a ) → A as  We then have for any f : I → J the following  The latter because f ◦ ι I and ι J are both maps from the empty set, hence they are equal. By the previous lemma each α I is an isomorphism and by the preceding calculation α is a natural transformation. Hence α is a natural isomorphism. Lemma 4.11. If A is isomorphic to ∆( a ) for some a ∈ Set then the obvious morphism A → A ■ is an isomorphism. Proof. The inverse to the isomorphism β in Lemma 4.9 is the morphism α i I  By assumption A ( ι ) for any inclusion ι : I → I, i is an isomorphism. It is easy to compute that the canonical morphism A → A ■ arises as the composition of A ( ι ) and α i I . Proposition 4.12. Let A be a cubical set. The formula i : ■ , j : ■ , f : ( ■ → A ) | · f ( i ) = f ( j ) holds in the internal language if and only if A is isomorphic to ∆( a ) for some a ∈ Set . Proof. Suppose the formula holds. Then it is easy to see that the constant map from A to A ■ is an isomorphism (the inverse is given, for instance, by evaluation at 0 ). Corollary 4.10 implies the result. Conversely assume A ∼ = ∆( a ) for some a ∈ Set . Then by Lemma 4.11 the canonical map const : A → A ■ is an isomorphism. Hence it is internally surjective. Thus for any f : ■ → A there is an a in A , such that const a = f . From this we immediately have f ( i ) = f ( j ) for any i and j in . Proof. Since A is discrete, we have that u (0) = u (1) for any u : Π( i : ■ ) . [ ϕ ] → A . Therefore A [ ϕ ↦→ u (0)] = A [ ϕ ↦→ u (1)] , so we can choose the constant function λγ, ϕ, u, a.a to be c A , since this will be of type Φ( · , A ) . ■ Lemma 4.13. Every discrete type A is fibrant, i.e., it has a composition operator c A : Φ( · ; A ) . If we have a composition operator c A : Φ( · ; A ) then we can always construct a weakened version c ′ A : Φ(Γ; A ) for any Γ , since A does not depend on Γ . Therefore we can interpret the natural number type:  where c N is the composition that we get from Lemma 4.13. ## 4.4 More General Models of L The type theory GCTT is an extension of CTT , and we intend to model it in the category of presheaves over C × ω . We first need to establish that we can model CTT in this category. This section shows how to do this by demonstrating that we can lift all constructions of CTT from the category of cubical sets to C × D , for any small category D with an initial object. We first prove some general lemmas. Lemma 4.14. Let C , D be small categories and let π : C × D → C be the projection functor. Then the geometric morphism π ∗ π ∗ is open. If D is inhabited then it is also surjective. Proof. By Theorem C. 3 . 1 . 7 of Johnstone [19] it suffices to show that π ∗ 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 : π ( I, n ) → J be a morphism in C . Let U ′ = ( J, n ) , a = ( b, id n ) : ( I, n ) → ( J, n ) , r = id J : πU ′ → J and i = id J : J → πU ′ . Then we have r ◦ i = id J and i ◦ b = πa as required by Lemma C. 3 . 1 . 2 . If D is inhabited the projection π is surjective on objects, so the corresponding geometric morphism is surjective; see Johnstone [19, A4.2.7b] The above lemma may be read as stating that Ĉ × D is a conservative extension of ˆ C , provided that D is inhabited. Lemma 4.15. If D has an initial object 0, then π ∗ is full, faithful, and cartesian closed. Proof. The functor π has a left adjoint, which is the functor  Trivially we have π ◦ ι = id C . Thus we have that ι ∗ is left adjoint to π ∗ and because π ◦ ι = id C we also have ι ∗ ◦ π ∗ = id and moreover the counit of the adjunction is the identity. Hence the functor π ∗ is full and faithful [21, Theorem IV. 3 . 1 ] and by Johnstone [19, Corollary A. 1 . 5 . 9 ], since ι ∗ preserves all limits, we have that π ∗ cartesian closed. Let Ω D be the subobject classifier of Ĉ × D and Ω be the subobject classifier of ̂ C . Lemma 4.16. There is a monomorphism υ : π ∗ (Ω) → Ω D which fits into the pullback  Proof. As an inverse image, π ∗ preserves monos. So, π ∗ ( ) is a mono. Its characteristic map is:  This is clearly a mono. Corollary 4.17. If X = π ∗ ( Y ) then the equality predicate χ δ : X × X → Ω D factors uniquely through υ and the inclusion of the equality predicate of Y . Proof. The equality predicate is by definition the characteristic map of the diagonal δ : X → X × X . Let δ ′ : Y → Y × Y be the diagonal. Because π ∗ 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 υ is a mono. Let D be a small category with an initial object. We show that ̂ C × D models L . ## 4.4.1 The interval type assumption is satisfied Let ■ D = π ∗ ( ■ ) . Since π ∗ preserves products we can lift all the De Morgan algebra operations of ■ to operations on ■ 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 ■ D is an internal De Morgan algebra with the finitary disjunction property. ## Faces Lemma 4.18. Let ❋ D ∈ ̂ C × D and ❋ ∈ ̂ C be defined as in Section 4.1.1 from ■ D and ■ . Then D ∼ = π ∗ ( ) .  ❋ ❋ Proof. Let e : ■ D → Ω D be the composition χ δ ◦ 〈 id, 1 〉 where δ is the diagonal ■ D → ■ D × ■ D . By definition ❋ D is the image of e . By Corollary 4.17 and the way we have defined ■ D , and all the operations on it, we have that e = υ ◦ π ∗ ( e ′ ) where e ′ : ■ → Ω is defined analogously to e above. By definition ❋ is the image of e ′ . Because inverse images of geometric morphisms preserve image factorisations [34, Remark 1.34], π ∗ ( ) is the image of π ∗ ( e ′ ) . So, ## ■ 4.4.2 The glueing assumption is satisfied ■ ❋ is the unique factorization of the map [ · = 1] : D → Ω D . This proceeds exactly as in Section 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 Γ ■ , i.e., the denotation of paths. Lemma 4.19. Let C and D be small categories and assume C has products. Let k 1 : C → ̂ C and k 2 : D × C → D̂ × C be the Yoneda embeddings. Let π ∗ : ̂ C → D̂ × C be the constant presheaf functor. For any d, e ∈ C and any c ∈ D there is an isomorphism  in D̂ × C which is natural in c , d and e . Proof. For any ( c ′ , d ′ ) ∈ D × C  and because the hom functor preserves products we have   as required. Lemma 4.20. Let D be a small category. Let ■ D ∈ D̂ ×C be the inclusion π ∗ ( ■ ) of ■ ∈ ̂ C . Let X ∈ ̂ C × D . Then for any c ∈ D , any I ∈ C and any i ∈ I we have naturally in c , I and i . Proof. Using the Yoneda lemma and the defining property of exponents we have which by Lemma 4.19, together with the fact that is isomorphic to y { i } , is isomorphic to   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 C . Concretely, the isomorphism α c I,i maps ξ ∈ X ■ D ( I, c ) to ξ ( ι I,i ,id c , ) ( i ) , where ι I,i : I → I, i (in C op ) is the inclusion. Its inverse β c I,i maps x ∈ X ( I ∪ { i } , c ) to the family of functions ξ ( f,g ) : ■ ( J ) → X ( J, d ) indexed by morphisms ( f, g ) : ( J, d ) → ( I, c ) (in ( C × D ) ). This family is defined as  where [ g, i ↦→ ϕ ] is the map I, i → J (in C op ) which maps i to ϕ and otherwise acts as g . This map is well-defined because disjoint union is the coproduct in C op . Definition of the universe. We can now define the universe U D f . For this we assume a Grothendieck universe U in our ambient set theory. First, recall that the Hofmann-Streicher universe U D in ̂ C × D maps ( I, c ) to the set of functors valued in U on the category of elements of y ( I, c ) . It acts on morphisms ( I, c ) → ( J, d ) by composition (in the same way as substitution in types is modelled). The elements operation is interpreted as We first look at the following rule.  Let us write b = L a, c M . We need to give for each I ∈ C , c ∈ D and γ ∈ Γ( I, c ) a pair ( b 0 , b 1 ) where  Now b 0 is easy. It is simply a ( I,c ) ,γ . Composition is also conceptually simple, but somewhat difficult to write down precisely. Elements γ ∈ Γ( I, c ) are in bijective correspondence (by Yoneda and exponential transpose) to terms γ   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 L  To interpret this rule with U D f , we interpret for any a and c , El( L a, c M ) by El( a ) , where the latter is El map of the Hofmann-Streicher universe. We need to define Comp( a ) which we abbreviate to c . We need to give for each I ∈ C and c ∈ D an element c I,c ∈ Φ(Γ;El( a ))( I, c ) , and this family needs to be natural in I and c . Given γ ∈ (Γ ■ D )( I, c ) and a fresh i ∈ I we get by Lemma 4.20 an element γ ′ ∈ Γ(( I, i ) , c ) . Let Thus we define   recalling that terms are interpreted as global elements, and is the unique inhabitant of the chosen singleton set. We define U D f analogously to the way it is defined in Section 4.3, that is  γ ′ : y (( I, i ) , c ) → Γ be the morphism corresponding to γ ′ by the Yoneda lemma. Thus we get from a the term c ′ I,i,c,γ  and hence by weakening a term  By Lemma 4.19 and the way ■ D is defined we have a canonical isomorphism y (( I, i ) , c ) ∼ = y ( I, c ) × ■ D . We now apply c ′ I,i,c,γ to the path δ = λ ( i : D ) . ( ρ, i ) to get the element From this element we can define c I,c by using the Yoneda lemma again to get the element c ′ I,i,c,γ of type  Π( ϕ : ❋ )( u : Π( i : ■ ) . [ ϕ ] → B ( δ ( i ))) .B ( δ (0))[ ϕ ↦→ u (0)] → B ( δ (1))[ ϕ ↦→ u (1)] , which is a type in context y ( I, c ) , at ( I, c ) , id I,c . To recap, the composition c will map γ ∈ (Γ ■ D )( I, c ) to the element c ′ I,i,c,γ . Lemma 4.21. For any a and c of correct types we have  ## 4.4.4 The ∀ assumption is satisfied Using Lemmas 4.15 and 4.18 we can define ∀ in ̂ C × D as the inclusion of the ∀ from ̂ C . Lemma 4.14 can then be used to show that the new ∀ is the right adjoint to the map ϕ ↦→ λ \_ .ϕ . ## 4.5 A model of GCTT Our construction of a model for GCTT again proceeds via a dependent predicate logic, extending the language L used above with counterparts of the later, delayed substitutions, and fixed-point constructs introduced in Sections 3.1 and 3.2. We call this new language L ′ . One difference between GCTT and L ′ is that in the latter our fixed-point combinator fix x.t has a judgemental equality  The GCTT term dfix r x.t is interpreted as next( fix x.t ) , forgetting r . This is consistent with the motivation for annotating dfix r x.t with an interval element r : it is needed to ensure termination of fixed-point unfolding, but it is semantically irrelevant. Since L ′ is an extension of L we can use it to construct a model of CTT . The interpretation of delayed fixed point combinator and delayed substitutions of GCTT is straightforward in terms of corresponding constructs of L ′ . The most difficult part is showing that the type-former, with delayed substitutions, has compositions, which we do in Section 4.5.3. The rest of the section is devoted to providing a model of L ′ in the presheaf category ̂ C × ω . Because of the results of the previous subsection this is immediately a model of L ; we need only show that the category ̂ C × ω 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 ̂ ω . ## 4.5.1 The functor In this section we sketch how to model the later type, delayed substitutions, and the fixedpoint operator of L ′ . 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 functor on the topos of trees ̂ ω was defined by Birkedal et al. [6]. It is straightforward to extend this to the category ̂ C × ω , simply ignoring the cube component: given X ∈ ̂ C × ω define  with restrictions inherited from X ; i.e. if ( f, n ≤ m ) : ( I, n ) → ( J, m ) then  where n ≤ m is the unique morphism n → m (and similarly k ≤ m -1 ), and ! is the unique morphism into { } , the chosen singleton set. Less concretely, the functor on ̂ ω arises via a geometric morphism induced by the successor functor on ω [6, Section 2.2]; the functor above arises similarly from the successor functor on C × ω which is the identity on the cube component. There is a natural transformation  and a natural family of morphisms : ( Y X ) × X → Y making the triple ( , next , ) an applicative functor [25]. Lemma 4.22. For any X and any morphism α : X → X there exists a unique global element β : 1 → X such that  Hence the triple ( ̂ C × ω, , next) is a model of guarded recursive terms [6, Definition 6 . 1 ]. Proof. Any global element β satisfying the fixed-point equation must satisfy the following two equations  Hence define β recursively on n . It is then easy to see that β is a global element and that it satisfies the fixed-point equation and that it is unique such. By Lemma 4.22 and Birkedal et al. [6, Theorem 6 . 3 ], extends to all slices of ̂ C × ω , and contractive morphisms on slices have unique fixed-points. The above translations from ̂ ω to ̂ C × ω 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 GDTT [10]. Third, we need to show that the later types are fibrant, i.e. support the notion of composition, which we do in Section 4.5.3. Delayed substitutions Semantically a delayed substitution of L ′  will be interpreted [10] as a morphism J ξ K : J Γ K → J Γ , Γ ′ K making the following diagram commute  Here π : Γ , Γ ′ → Γ is the composition of projections of the form Γ , Γ ′′ , x : A → Γ , Γ ′′ . J K J K J K J K In particular, if Γ ′ is the empty context then π = id J Γ K and so J · K = next , where · is the empty delayed substitution. Thus given a delayed substitution ξ : Γ \_ Γ ′ and a type    Note that this is exactly like substitution Aξ , except in the case where n = 0 . In turn, we interpret the rules  as follows. First, the empty delayed substitution is interpreted as next , as we already remarked above. Given ξ : Γ \_ Γ ′ and Γ t : ξ.A define  define to be Next The term-level counterpart is interpreted similarly. To interpret the rule  we proceed as follows. Given a term t and a delayed substitution ξ 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 type we will need type isomorphisms commuting and dependent products in certain cases. We start with a definition. Definition 4.23. A type Γ A is constant with respect to ω if for all I ∈ C , n ∈ ω, γ ∈ Γ( I, n ) and for all m ≤ n the restriction  is the identity function 7 (in particular, the two sets are equal). Note that this is a direct generalisation of 'being constant' (being in the image of π ∗ ) for presheaves (i.e., closed types). Below we will use the shorter notation γ m for Γ( id I , m ≤ n )( γ ) . We have the following easy, but important, lemma. Lemma 4.24. Being constant with respect to ω is closed under substitution. If Γ A is constant and ρ : Γ ′ → Γ is a context morphism then Γ ′ Aρ is constant. Lemma 4.25. Let X be a presheaf in the essential image of π ∗ . The identity type x : X,y : X Id X ( x, y ) is constant with respect to ω . Proof. Recall that we have for γ, γ ′ ∈ X ( I, n ) .   But since · m is an isomorphism we have γ m = γ ′ m if and only if γ = γ ′ , which concludes the proof. Since all the sets are chosen singletons or the empty set the relevant restrictions are then trivially identity functions. Using the assumptions stated above we have the following proposition. 7 A perhaps more natural definition would require this function to be a bijection. However since this is a technical definition used only in this section we state it only in the generality we need. Thus for any m ≤ n ## Proposition 4.26. Assume Hence we have  And because A is constant we further have  (by assumption k ≤ m and n = m +1 .  and further that A is constant with respect to ω . The canonical morphism from left to right in  is an isomorphism. The canonical morphism is derived from the term λf.λx. next [ ξ, f ′ ← f ] . ( f ′ x ) . Proof. We need to establish an isomorphism of two presheaves on the category of elements of Γ . Since we already have one of the directions we will first define the other direction explicitly. We define  Let I ∈ C , n ∈ ω and γ ∈ Γ( I, n ) . Take α ∈ (Π( x : A ) .ξ .B ) ( I, n, γ ) . If n = 0 then we have only one choice.  So assume that n = m +1 . Then we need to provide an element of  Which means that for each f : J → I and each k ≤ m we need to give a dependent function  Because Γ A we have  where π : Γ , Γ ′ → Γ is the composition of projections. By naturality we have  Now π I,m = ( π ) I,n and so we have (because ξ is a delayed substitution)  Now α f,k +1 is a dependent function  And we have  (because the relevant restriction of A is the identity). Now  Thus, we can define  The fact that β is a natural family follows from the fact that α is a natural family. Naturality of F follows easily by the fact that restrictions for Π types are defined by precomposition. The fact that it is the inverse to the canonical morphism follows by a tedious computation.  Corollary 4.27. If Γ ϕ : ❋ then we have an isomorphism of types Proof. Using Proposition 4.26 it suffices to show that Γ [ ϕ ] is constant with respect to ω . Using Lemmas 4.24 and 4.25 it further suffices to show that the presheaf ❋ is in the essential image of π ∗ , which is exactly what Lemma 4.18 states. 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 ξ is a morphism  Hence we can treat it as a term of type (Γ , Γ ′ ) in context Γ . Further given a morphism γ : ■ ω → Γ we can form the morphism Lemma 4.28. Given γ and ξ as above then for any type Γ , Γ ′ A we have the equality of types ξ ◦ γ : ■ ω → (Γ , Γ ′ ) . Finally by using Proposition 4.26 we can transport ξ ◦ γ : ■ ω → (Γ , Γ ′ ) to a term ξ ◦ γ : ( ■ ω → Γ , Γ ′ ) in the empty context. For this term we have the following equality.  Here ξγ ( i ) is the delayed substitution : ■ ω \_ Γ , Γ ′ obtained by substitution in terms of ξ . Proof. Proof by computation; we require the unfolding of the definition of the isomorphism in Proposition 4.26. ## 4.5.3 Interpreting later types The type part of the delayed substitution type is interpreted using delayed substitutions in the language L ′ . 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 ξ.A is a wellformed type in context Γ and we have a composition term c A : Φ(Γ , Γ ′ ; A ) , then there is a composition term c : Φ(Γ; ξ.A ) . 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:  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 ϕ . This is equivalent to saying that the type  is inhabited. We transform the type as follows:  where the last equality uses that ˜ u is defined using the inverse of λfλx. next ξ [ f ′ ← f ] . f ′ x (Proposition 4.26). By assumption it is the case that (Id( a 0 , u 0)) ϕ 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 ϕ . Assuming ϕ , we get by the properties of c A that  and by the definition of ˜ u (Proposition 4.26) we have that  as desired. Note that in the lemma above we do not require that the types in Γ ′ are fibrant. ## 4.6 Summary of the semantics of GCTT The interpretation of the syntax of GCTT follows the pattern for interpreting dependent type theory outlined in Cohen et al. [12, sec 8.2]. In summary, the following judgements need to be interpreted. - J Γ K - J Γ A K - J Γ t : A K - J ρ : Γ → Γ ′ K - J ξ : Γ \_ Γ ′ K where the last one is a context morphism. We have shown the constructions needed to interpret these judgements, but we do not show the details of their interpretations and the verification of the equations. These follow straightforwardly from the properties of semantic objects we have established. In summary, the interpretations of the judgements are constructed in three stages. 1. Every presheaf topos with a non-trivial internal De Morgan algebra ■ satisfying the disjunction property can be used to give semantics to the subset of the cubical type theory CTT without glueing and the universe. Further, for any category D , the category of presheaves on C × D has an interval ■ , which is the inclusion of the interval in presheaves over the category of cubes C . This was done in Sections 4.4.1 and 4.4.2. 2. The topos of presheaves C × D for any small category D with an initial object gives a semantics of the entire CTT . This was done in Sections 4.4.3 and 4.4.4. 3. In Section 4.5, we showed that the category of presheaves on C × ω gives semantics for 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 J Γ A K and J Γ B K are interpreted as the same object. If  is derivable then the terms J Γ t : A K and J Γ s : A K are interpreted as equal. As a consequence, the judgement t : Path N 0 1 is not derivable for any closed term t . This completes the construction of a model of GCTT , as outlined in the beginning of Section 4. ## 5 Conclusion In this paper we have made the following contributions: - We introduce guarded cubical type theory ( GCTT ), which combines features of cubical type theory ( CTT ) and guarded dependent type theory ( GDTT ). The path equality of CTT is shown to support reasoning about extensional properties of guarded recursive operations, and we use the interval of CTT to constrain the unfolding of fixed-points. - We show that 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 ∀ . Most of these constructions are done via the internal logic. We then show that a class of presheaf models of the form ̂ C × D , for any small category D with an initial object, satisfy the above axioms and hence gives rise to a model of CTT . - We give semantics to GCTT in the topos of presheaves over C × ω . Further work. We wish to establish key syntactic properties of GCTT , namely decidable type-checking and canonicity for base types. Our prototype implementation establishes some confidence in these properties. We wish to further extend GCTT with clock quantification [3], such as is present in 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 GDTT with multiple clocks [9]. The main challenges lie in ensuring decidable type checking ( 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 8 , 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 8 http://www.nuprl.org/wip/Mathematics/cubical!type!theory/ 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 D is an internal category in ˆ C , then ˆ C D ≡ Ĉ × 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 ˆ π 1 : ̂ C × ω → ˆ 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 GCTT relates to the model of simplicial presheaves over ω in Birkedal et al. [5]. 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 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 ( OTT ) [2]. We found CTT 's prototype implementation, its presheaf semantics, and its interval as a tool for controlling unfoldings, most convenient for developing our combination with GDTT , but extending 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 CTT . Recent independent work by Orton and Pitts [29] axiomatises a model for 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 CTT . Acknowledgements. We gratefully acknowledge our discussions with Thierry Coquand, and the comments of our reviewers of the conference version of this article [4], and of this article. This research was supported in part by the ModuRes Sapere Aude Advanced Grant from The Danish Council for Independent Research for the Natural Sciences (FNU), and in part by the Guarded homotopy type theory project, funded by the Villum Foundation. Aleš Bizjak was supported in part by a Microsoft Research PhD grant. ## References - [1] Andreas Abel and Andrea Vezzosi. A formalized proof of strong normalization for guarded recursive types. In APLAS , pages 140-158, 2014. 2, 11 - [2] Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. Observational equality, now! In PLPV , pages 57-68, 2007. 39 - [3] Robert Atkey and Conor McBride. Productive coprogramming with guarded recursion. In ICFP , pages 197-208, 2013. 2, 38 - [4] Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In CSL , 2016. 3, 39 - [5] Lars Birkedal and Rasmus Ejlers Møgelberg. Intensional type theory with guarded recursive types qua fixed points on universes. In LICS , pages 213-222, 2013. 6, 39 - [6] Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. LMCS , 8(4), 2012. 2, 31, 32 - [7] Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, and Hongseok Yang. Step-indexed Kripke models over recursive worlds. In POPL , pages 119-132, 2011. 1, 11 - [8] Garrett Birkhoff. Rings of sets. Duke Mathematical Journal , 3(3):443-454, 1937. 24 - [9] Aleš Bizjak and Rasmus Ejlers Møgelberg. A model of guarded recursion with clock synchronisation. In MFPS , pages 83-101, 2015. 38 - [10] Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg, and Lars Birkedal. Guarded dependent type theory with coinductive types. In FoSSaCS , pages 20-35, 2016. 2, 6, 31, 32 - [11] Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. The guarded lambda-calculus: Programming and reasoning with guarded recursion for coinductive types. Logical Methods in Computer Science , 12(3), 2016. 2 - [12] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. Unpublished, 2016. 2, 3, 5, 11, 13, 17, 20, 24, 37 - [13] Thierry Coquand. Internal version of the uniform Kan filling condition. Unpublished, 2015. URL: http://www.cse.chalmers.se/~coquand/shape.pdf . 11, 18, 39 - [14] William Cornish and Peter Fowler. Coproducts of de Morgan algebras. Bulletin of the Australian Mathematical Society , 16(1):1-13, 1977. 24 - [15] Peter Dybjer. Internal type theory. In TYPES '95 , pages 120-134, 1996. 12, 17 - [16] Martin Hofmann. Extensional constructs in intensional type theory . Springer, 1997. 2 - [17] Martin Hofmann and Thomas Streicher. Lifting Grothendieck universes. Unpublished, 1999. URL: http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf . 39 - [18] Simon Huber. Canonicity for Cubical Type Theory. arXiv:1607.04156 , 2016. 2 - [19] Peter T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium . OUP, 2002. 12, 26, 39 - [20] Chris Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky). arXiv:1211.2851, 2012. 23 - [21] Saunders Mac Lane. Categories for the working mathematician , volume 5. Springer Science & Business Media, 1978. 26 - [22] Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic . Springer, 1992. 27 - [23] Per Martin-Löf. An intuitionistic theory of types: predicative part. In Logic Colloquium '73 , pages 73-118, 1975. 4 - [24] The Coq development team. The Coq proof assistant reference manual . LogiCal Project, 2004. Version 8.0. 2 - [25] Conor McBride and Ross Paterson. Applicative programming with effects. J. Funct. Programming , 18(1):1-13, 2008. 6, 31 - [26] Rasmus Ejlers Møgelberg. A type theory for productive coprogramming via guarded recursion. In CSL-LICS , 2014. 2 - [27] Hiroshi Nakano. A modality for recursion. In LICS , pages 255-266, 2000. 2 - [28] Ulf Norell. Towards a practical programming language based on dependent type theory . PhD thesis, Chalmers University of Technology, 2007. 2 - [29] Ian Orton and Andrew M. Pitts. Axioms for modelling cubical type theory in a topos. In CSL , 2016. 39 - [30] Wesley Phoa. An introduction to fibrations, topos theory, the effective topos and modest sets. Technical Report ECS-LFCS-92-208, LFCS, University of Edinburgh, 1992. 12, 21 - [31] Jorge Luis Sacchini. Well-founded sized types in the calculus of constructions. TYPES 2015 talk, 2015. URL: http://cs.ioc.ee/types15/programme-slides.html . 8 - [32] Bas Spitters. Cubical sets as a classifying topos. TYPES , 2015. 39 - [33] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for Mathematics . Institute for Advanced Study, 2013. 2, 10 - [34] Steven Vickers. Locales and toposes as spaces. In Handbook of spatial logics , pages 429-496. Springer, 2007. 27 - [35] V. Voevodsky. Martin-Lof identity types in the C-systems defined by a universe category. ArXiv: 1505.06446 , 2015. 39 ## A zipWith Preserves Commutativity We provide a formalisation of Section 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. ``` ```

Rendering Paper...