Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

The Univalence Axiom in Cubical Sets

The Univalence Axiom in Cubical Sets J Autom Reasoning (2019) 63:159–171 https://doi.org/10.1007/s10817-018-9472-6 1 2 Marc Bezem · Thierry Coquand · Simon Huber Received: 20 November 2016 / Accepted: 4 June 2018 / Published online: 26 June 2018 © The Author(s) 2018 Abstract In this note we show that Voevodsky’s univalence axiom holds in the model of type theory based on cubical sets as described in Bezem et al. (in: Matthes and Schubert (eds.) 19th international conference on types for proofs and programs (TYPES 2013), Leibniz international proceedings in informatics (LIPIcs), Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, vol 26, pp 107–128, 2014. https://doi.org/10.4230/LIPIcs. TYPES.2013.107. http://drops.dagstuhl.de/opus/volltexte/2014/4628) and Huber (A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg, 2015). We will also discuss Swan’s construction of the identity type in this variation of cubical sets. This proves that we have a model of type theory supporting dependent products, dependent sums, univalent universes, and identity types with the usual judgmental equality, and this model is formulated in a constructive metatheory. Keywords Dependent type theory · Univalence axiom · Cubical sets 1 Review of the Cubical Set Model We give a brief overview of the cubical set model, introducing some different notations, but will otherwise assume the reader is familiar with [2,6]. B Marc Bezem bezem@ii.uib.no Simon Huber simon.huber@cse.gu.se Thierry Coquand thierry.coquand@cse.gu.se Department of Informatics, University of Bergen, Postboks 7800, 5020 Bergen, Norway Department of Computer Science and Engineering, University of Gothenburg, 412 96 Göteborg, Sweden 123 160 M. Bezem et al. As opposed to [2,6] let us define cubical sets as contravariant presheaves on the opposite of the category used there, that is, the category of cubes C contains as objects finite sets I ={i ,..., i } (n ≥ 0) of names and a morphism f : J → I is given by a set-theoretic 1 n map I → J ∪{0, 1} which is injective when restricted to the preimage of J ; we will write op compositions in applicative order. The category of cubical sets is the category [C , Set] of presheaves on C . A morphism f : J → I in C can be viewed as a substitution. If f (i ) ∈ J , we call f defined on i.For i ∈ / I , the face morphisms are denoted by (i /0), (i /1) : I → I, i and are induced by setting i to 0 and 1, respectively; degenerating along i ∈ / I is denoted by s : I, i → I and is induced by the inclusion I ⊆ I, i. If Γ is a cubical set, we write Ty(Γ ) for the collection/class of presheaves on the category of elements of Γ [2,6]. Such a presheaf A ∈ Ty(Γ ) is given by a family of sets A(I,ρ) for I ∈ C and ρ ∈ Γ(I ) together with restriction functions. As ρ ∈ Γ(I ) determines I we simply write Aρ for A(I,ρ).Given A ∈ Ty(Γ ) and a natural transformation (substitution) σ : Δ → Γ we get Aσ ∈ Ty(Δ) defined as (Aσ)ρ = A(σρ) which extends canonically to the restrictions. For A ∈ Ty(Γ ) we denote the set of sections of A by Ter(Γ , A);so a ∈ Ter(Γ , A) is given by a family aρ ∈ Aρ for ρ ∈ Γ(I ) such that (aρ) f = a(ρ f ) for f : J → I . Substitution also extends to terms via (aσ)ρ = a(σρ). Let us recall the construction of Π-types: Π AB ∈ Ty(Γ ) for A ∈ Ty(Γ ) and B ∈ Ty(Γ .A) is given by letting each element w of (Π AB)ρ (with ρ ∈ Γ(I )) be a family of w a ∈ B(ρ f, a) for f : J → I and a ∈ Aρ satisfying (w a)g = w (ag); the restriction f f fg of such a w is given by (w f ) = w . In the sequel we will however only have to refer to g fg w when f is the identity, and will thus simply write w a for w a. We also occasionally f id switch between sections in Ter(Γ .A, B) and Ter(Γ , Π AB) without warning the reader. Let A ∈ Ty(Γ ), ρ ∈ Γ(I ),and J ⊆ I.A J -tube in A over ρ is given by a family u of elements u ∈ Aρ( j/c) for ( j, c) ∈ J ×{0, 1} which is adjacent compatible, that jc is, u (k/d) = u ( j/c) for ( j, c), (k, d) ∈ J ×{0, 1}.For (i, a) ∈ (I − J ) ×{0, 1} we jc kd say that an element u ∈ Aρ(i /a) is a lid of such a tube u if u (i /a) = u ( j/c) for all ia jc ia ( j, c) ∈ J ×{0, 1}. In this situation we call the pair [J → u; (i, a) → u ] an open box in ia A over ρ.A filler for such an open box is an element u ∈ Aρ such that u( j/c) = u for jc ( j, c) ∈{(i, a)}∪ (J ×{0, 1}). In case J is empty, we simply write [(i, a) → u ]. ia Given f : K → I and an open box m =[J → u; (i, a) → u ] in A over ρ we call f ia allowed for m if f is defined on J, i. In this case we define the open box mf in A in ρ f to be [Jf → u f ; ( f (i ), a) → u ( f − i )] where u f is given by (u f ) = u ( f − j ) with ia f ( j ) c jc f − i : K − f (i ) → I − i being like f but skipping i,and Jf is the image of J under f . Recall from [2, Section 4] that a (uniform) Kan structure for a type A ∈ Ty(Γ ) is given by an operation κ which (uniformly) fills open boxes: for any ρ ∈ Γ(I ) and open box m in A over ρ we get a filler κρ m of m subject to the uniformity condition (κ ρ m) f = κ(ρ f )(mf ) for all f : K → I allowed for m. Any Kan structure κ defines a composition operation κ ¯ which provides the missing lid of the open box, given by: κρ ¯ [J → u; (i, 0) → u ]= (κ ρ [J → u; (i, 0) → u ])(i /1) i0 i0 κρ ¯ [J → u; (i, 1) → u ]= (κ ρ [J → u; (i, 1) → u ])(i /0) i1 i1 We denote the set of all Kan structures on A ∈ Ty(Γ ) as Fill(Γ , A).If σ : Δ → Γ and κ is an element in Fill(Γ , A), we get an element κσ in Fill(Δ, Aσ) defined by (κσ ) ρ = κ(σρ). 123 The Univalence Axiom in Cubical Sets 161 Given a cubical set Γ a Kan type is a pair (A,κ) where A ∈ Ty(Γ ) and κ ∈ Fill(Γ , A). We denote the collection of all such Kan types by KTy(Γ ).In[2] we showed that Kan types are closed under dependent products and sums constituting a model of type theory. 2 Path Types In [2] we introduced identity types which were however only “weak”, e.g., transport along reflexivity is only propositionally equal to the identity function but not necessarily judgmen- tally equal. For this reason we will call these types path types and reserve Id for the identity type with the usual judgmental equality defined in Sect. 4. Recall that the path type Path u v ∈ Ty(Γ ) for A ∈ Ty(Γ ) and u,v ∈ Ter(Γ , A) is defined by the sets (Path u v)ρ containing equivalence classes i w where i ∈ / I and w ∈ Aρs with w(i /0) = uρ and w(i /1) = vρ. Restrictions are defined as expected, and we showed that Kan types are closed under forming path types [2]. It will be convenient below to introduce paths using separated products. Definition 1 Given cubical sets Γ and Δ, we say that u ∈ Γ(I ) and v ∈ Δ(I ) are separated, denoted by u # v, if they come through degeneration from cubes with disjoint sets of directions. More precisely, if there are J ⊆ I , K ⊆ I with J ∩ K =∅ and u ∈ Γ(J ), v ∈ Δ(K ) such that u = u s and v = v s with s and s induced by the inclusion J ⊆ I and K ⊆ I , respectively. The separated product Γ ∗ Δ of Γ and Δ is the cubical set defined by (Γ ∗ Δ)(I ) ={(u,v) ∈ Γ(I ) × Δ(I ) | u # v}⊆ (Γ × Δ)(I ). The restrictions are inherited from Γ × Δ, that is, they are defined component wise. It can be shown that −∗− extends to a functor, and that −∗ Δ has a right adjoint. Of particular interest is Γ ∗ I where I is the interval defined by I(J ) = J ∪{0, 1} (see [2, Section 6.1]). Then (Γ ∗ I)(I ) = (Γ (I ) ×{0, 1}) ∪{(ρs , i ) | i ∈ I ∧ ρ ∈ Γ(I − i )}. If (ρ , i ) ∈ (Γ ∗ I)(I ) with i ∈ I,then ρ = ρ s for a uniquely determined ρ which we denote by ρ − i. We can use Γ ∗ I to formulate the following introduction rule for path types where [0], [1]: Γ → Γ ∗ I are induced by the global elements 0 and 1 of I, respectively, and p : Γ ∗ I → Γ is the first projection. The binding operation is interpreted by ( w)ρ = i w(ρs , i ) with i a fresh name (see [2, Section 8.2]). Given an element i w ∈ (Path u v)ρ with ρ ∈ Γ(I ),weset (i w) @ a = w(i /a) where a is 0, 1, or a fresh name. 3 Equivalences and Univalence We will now recall the definition of an equivalence as a map having contractible fibers and then derive an operation for contractible and Kan types. To enhance readability we define the following types using variable names: 123 162 M. Bezem et al. isContr A = Σ(x : A)Π(y : A) Path xy fib t v = Σ(x : A) Path (tx)v isEquiv t = Π(y : B) isContr(fibty) Equiv AB = Σ(t : A → B) isEquiv t where A and B are types, t : A → B,and v : B (all in an ambient context Γ ). This can of course also be formally written name-free: for example, the first type can be written as Σ AΠ Ap (Path qp q) ∈ Ty(Γ ) and the second one as Σ Ap (Path app(tpp, q) qp) ∈ App Bpp Ty(Γ .B). Definition 2 A (uniform) acyclic-fibration structure on a type A ∈ Ty(Γ ) is givenbyan operation ext uniformly filling any tube, that is, given ρ ∈ Γ(I ), J ⊆ I,a J -tube u in Aρ, we have ext ρ [J → u]∈ Aρ extending u (so (ext ρ [J → u])(i /a) = u for (i, a) ∈ J ×{0, 1})and for f : K → I ia defined on J we have (ext ρ [J → u]) f = ext (ρ f ) [Jf → u f ]. We denote the set of acyclic-fibration structures on A ∈ Ty(Γ ) by Contr(Γ , A). Note that given ext ∈ Contr(Γ , A) and σ : Δ → Γ we obtain ext σ ∈ Contr(Δ, Aσ) via (ext σ) ρ = ext (σρ). Lemma 1 Given a type A in Ty(Γ ) we have maps with ϕ ψ ,ψ = id. Moreover, these maps are natural: if σ : Δ → Γ ,then (ϕ κ p)σ = 0 1 ϕ(κσ) (pσ), (ψ ext)σ = ψ (ext σ), and (ψ ext)σ = ψ (ext σ). 0 0 1 1 Proof Let κ ∈ Fill(Γ , A) and p ∈ Ter(Γ , isContr A).Todefine ϕκ p ∈ Contr(Γ , A),let ρ ∈ Γ(I ) and u a J -tube in A over ρ.Wetakeafresh dimension i and form an open box with the center of contraction pρ.1 at the closed end and u at the open end, connected by pρ.2; filling this gives us an extension of u. Formally: ϕκ p ρ [J → u]= κ( ¯ ρs ) [J → (pρ.2 u) @ i ; (i, 0) → pρ.1] where (pρ.2 u) @ i is the J -tube given by (p(ρ( j/c)).2 u ) @ i at side ( j, c) ∈ J ×{0, 1}. jc Conversely, let ext ∈ Contr(Γ , A).Toget aKan structurewefirstfill themissing lid and then the interior, that is, we set ψ ext ρ [J → u; (i, 0) → u ] 0 i0 = ext ρ [J → u,(i, 0) → u ,(i, 1) → ext ρ(i /1) [J → u(i /1)]], i0 and likewise for the other filling. To define ψ ext ρ we choose ext ρ [] as center of contraction, which is connected to any a ∈ Aρ by the path i ext (ρs ) [(i, 0) → ext ρ [],(i, 1) → a]. One can show uniformity, naturality, and that ψ ,ψ is a section of ϕ. 0 1 123 The Univalence Axiom in Cubical Sets 163 Next we will define an operation G which allows us to transform an equivalence into a “path”. This operation was introduced in [4] and motivated the “glueing” operation of [3]. We will define it in such a way that the associated transport of this path is given by underlying map of the equivalence. A useful analogy is provided by the notion of pathover, a heterogeneous path lying over another path. We shortly review this notion from type theory with inductive equality. Given a type family P : T → U and a path p : x = y with its transport function p : Px → Py. T ∗ If Px and Py are different types, there is no ordinary path connecting u : Px and v : Py. Therefore the pathovers connecting u and v are taken to be the paths of type p u = v (in ∗ Py the fiber Py). We apply the same idea to G t, which should be a path from A to B in U such that transport along this path is t : A → B. For the type family P we take id such that A and B indeed are fibers of P. Intuitively, a path from A to B is a set of heterogeneous paths between elements a of A and b of B.Wewant t to be the transport function along the path from A to B.By analogy we would take G t to be the set of pathovers connecting a : A and b : B defined as the set of paths in B connecting ta and b. However, since we must be able to recover the startpoint a,wedefine G t to be the set of pairs consisting of a : A and a path connecting ta and b. (Unlike a, the endpoint b can be recovered from the pathover and need not be remembered.) With the above informal explanation in mind, we define the operation G first on cubical sets and then explain how it lifts to Kan structures. It satisfies the rules: (1) (2) The latter rule expresses stability under substitutions. Here and below G (and ug below) have A and B as implicit arguments. Definition 3 Assume the premiss of (1) and define for every ρ ∈ Γ(I ): (G t )(ρ , 0) = Aρ, with restrictions as in A, (G t )(ρ , 1) = Bρ, with restrictions as in B,and (3) (G t )(ρ , i ) ={(u,v) | u ∈ A(ρ − i ) ∧ v ∈ Bρ ∧ v(i /0) = t (ρ − i ) u}. In the last case ρ # i,so ρ = (ρ − i )s . The restrictions in the latter case are a little involved. We need (u,v) f ∈ (G t )(ρ f, f (i )) for f : J → I.If f (i ) = 0, we take (u,v) f = us f , indeed in Aρ f .If f (i ) = 1, we take (u,v) f = v f , indeed in Bρ f . Finally, if f is defined on i,wehave f − i : J − f (i ) → I − i and we define (u,v) f = (u( f − i ), v f ),which is indeed correct as (ρ − i )( f − i ) = ρ f − f (i ) under the given assumptions. It can then be checked that the restrictions satisfy the presheaf requirements. This concludes the definition of G t. We haveamap ug ∈ Ter(Γ ∗ I. G t, Bp) given by: We will see later that this indeed induces a path in a universe whenever both types A and B are small. 123 164 M. Bezem et al. The fact that a map t ∈ Ter(Γ , A → B) is an equivalence can be represented as an element of Contr(Γ .B, fib t ). By Lemma 1 this is the case whenever A and B have Kan structures and the fibers of t are contractible. Theorem 1 The operation G can be lifted to Kan structures provided t is an equivalence, i.e., there is an operation G which given the premiss of (1) and κ ∈ Fill(Γ , A), κ ∈ Fill(Γ , B), A B and ext ∈ Contr(Γ .B, fib t ) returns G κ κ ext ∈ Fill(Γ ∗ I, G t ). This operation satisfies A B (G κ κ ext)[0]= κ A B A (G κ κ ext)[1]= κ A B B (G κ κ ext)(σ ∗ id) = G (κ σ) (κ σ) (ext (σ p, q)) A B A B where σ : Δ → Γ . Proof To define (G κ κ ext)(ρ , r ) for (ρ , r ) ∈ (Γ ∗ I)(I ) we argue by cases. For r = 0, 1 A B we take: (G κ κ ext)(ρ , 0) = κ ρ A B A (G κ κ ext)(ρ , 1) = κ ρ A B B Let us now consider the main case where r = i ∈ I is a name and thus ρ # i, ρ = (ρ −i )s .We are given j (the name along which we fill), w a J -tube in (G t ) over (ρ , i ) (with J ⊆ I − j), and w ∈ (G t )(ρ , i )( j/a) for a = 0or 1, which fits w.Wewanttodefine ja w := (G κ κ ext)(ρ, i ) [J → w; ( j, a) → w ] A B ja in (G t )(ρ , i ). For this we have to construct w = (u,v) with u ∈ A(ρ − i ) and v ∈ Bρ such that v(i /0) = t (ρ − i ) u. We can map w , w using ug and obtain an open box v , v in B over ρ given by ja ja v := ug((ρ , i )(k/b), w ) ∈ Bρ(k/b). kb kb There are four cases to consider depending on how the open box relates to the direction i. Each case will be illustrated afterwards with simplified J . Note that in all these pictures the part in A is mapped by t to the left face of the part in B. Here are the four cases: Case i = j and i ∈ / J . We extend the J -tube w to J, i-tube by constructing w and w i0 i1 and then proceed as in the next case with the tube w,w ,w .Notethatwewant i0 i1 w ∈ (G t )(ρ , i )(i /0) = A(ρ − i ), and i0 w ∈ (G t )(ρ , i )(i /1) = B(ρ − i ), i1 so we can take w = κ (ρ − i ) [J → w(i /0); ( j, a) → w (i /0)], and (4) i0 A ja w = κ (ρ − i ) [J → w(i /1); ( j, a) → w (i /1)]. (5) i1 B ja The resulting open box is compatible by construction. Note that this (together with the cases for r = 0and r = 1) also ensures that the Kan structure satisfies the equations in (1). We illustrate this case in the picture below. Here and below the left part is in A and on the right we have the open box v in B. For simplicity we also omit ρ. We construct w and w i0 i1 by filling the open boxes indicated by thicker lines on the left and on the right, respectively. 123 The Univalence Axiom in Cubical Sets 165 Case i = j and i ∈ J . In this case v = ug((ρ(i /0), 0), w ) = tρ(i /0)w = i0 i0 i0 t (ρ − i)w since ρ # i. We can therefore take w = (w ,v) ∈ (G t )(ρ , i ) where v = i0 i0 κ (ρ − i ) [J → v; ( j, a) → v ]. This can be illustrated by: B ja Case j = i and a = 0. Like in the previous case we can take w = (w ,v) ∈ (G w)(ρ, i ) i0 where v = κ (ρ − i ) [J → v; ( j, a) → v ]. This case is illustrated as follows: B ja Cases j = i and a = 1. In this case the direction of the filling is opposite to t,and therefore we have to use ext which expresses that fib t is contractible. The family m defined by m := (w , i v ) ∈ (fib t )((ρ − i )(k/b), w (k/b)) kb kb kb i1 for (k, b) ∈ J ×{0, 1} constitutes a J -tube over (ρ − i,w ) in the contractible type fib t ∈ i1 Ty(Γ .B). So we can extend this tube to obtain (u,ω) = ext (ρ − i,w ) [J → m]∈ (fib t )(ρ − i,w ) i1 i1 and we can take w := (u,ω @ i ) ∈ (G t )(ρ , i ). Let us illustrate this case: we are given the two dots on the left and the solid lines on the right in the picture below, and we want to construct the dashed line and a square on the right such that the dashed line is mapped to the dotted line via t, that is, we basically want to construct an element in the fiber of w under t. i1 This concludes the definition of the filling operations of G t. To see that this filling operation is uniform, note that for an f : K → I defined on j, J and on i the case which defines the filling of [J → w; ( j, a) → w ] f coincides with ja the case used to defined [J → w; ( j, a) → w ] by the injectivity requirement on f — ja uniformity then follows for each case separately since we only used operations that suitably commutewith f in the definition of the filling. If f is only defined on j, J but not on i, 123 166 M. Bezem et al. the first case has to apply—to simplify notation assume f is (i /c)—then by construction (Eqs. 4, 5) (G κ κ ext)(ρ, i ) [J → w; ( j, a) → w ] (i /c) A B ja = (G κ κ ext)(ρ − i, c) [J → w(i /c); ( j, a) → (w (i /c))], A B ja concluding the proof. Theorem 2 We can refine the Kan structure G κ κ ext given in Theorem 1 such that it A B satisfies (G κ κ ext)(ρ, i ) [(i, 0) → u]= tρ u. A B Proof We modify the Kan structure given in the proof of Theorem 1 to obtain the above equations. The last two cases in the proof above where i = j are modified by an additional case distinction on whether J is empty or not. If J is not empty or a = 1, proceed as before. In case J is empty and a = 0, then we are given u ∈ A(ρ − i ) andanempty tube and i0 can define (G κ κ ext)(ρ, i ) [(i, 0) → u ]= (u , tρ u ). That this definition remains A B i0 i0 i0 uniform is proved as in Theorem 1 using the observation that |J|=|Jf | for f defined on J . In addition we retain stability under substitution. Remark 1 It is also possible to change the Kan structure such that it satisfies −1 (G κ κ ext)(ρ, i ) [(i, 1) → u]= t ρ u, A B −1 where t is the inverse of t which can be constructed from ext. For this one also has to −1 −1 modify the case where J is empty and a = 1 from the definition of G using t and that t is a (point-wise) right inverse of t (in the sense of path types). The latter is also definable using ext. Let us recall the definition of a universe U of small Kan types (assuming a Grothendieck universe of small sets in the ambient set theory). A type A ∈ Ty(Γ ) is small if all the sets Aρ for ρ ∈ Γ(I ) are so. A Kan type (A,κ) ∈ KTy(Γ ) is small if A ∈ Ty(Γ ) is small. We denote the set of all such small types and Kan types by Ty (Γ ) and KTy (Γ ), respectively. 0 0 Substitution makes both Ty and KTy into presheaves on the category of cubical sets. The 0 0 universe U is now given as U = KTy ◦ y where y denotes the Yoneda embedding. For an I -cube (A,κ) ∈ U(I ) = KTy (y I ) we have that A is a presheaf on the category of elements of y I,and A(J, f ) is a small set for every element (J, f : J → I ). Moreover, κ(J, f ) is a filler function for open boxes in A over (J, f ). Of particular interest are the small set A(I, id ) and filler function κ(I, id ). I I Given a ∈ Ter(Γ , U) we can associate a small type El a in Ty (Γ ) by (El a)ρ = A(I, id ) where aρ = (A,κ). We equip El a with the Kan structure El a defined by (El a)ρ = κ(I, id ). This results in an isomorphism which is natural in Γ : where X ρ = X ρˆ ∈ U(I ) for X ∈ KTy (Γ ).Here ρˆ : y I → Γ is the associated substitution of ρ ∈ Γ(I ),thatis, ρˆ f = ρ f ∈ Γ(J ) for any f : J → I . Since moreover Hom(Γ , U) = Ter(Γ , U),weget that KTy is representable. Theorem 3 U has a Kan structure. Proof [6, Theorem 4.2]. 123 The Univalence Axiom in Cubical Sets 167 We are now ready for the first main result of this paper. Theorem 4 (Univalence) The type Π(a : U) isContr Σ(b : U) Equiv (El a)(El b) in Ty(1) has a section, where 1 denotes the empty context. Proof Because our operation G preserves smallness we obtain an operation turning an equiv- alence between small Kan types into a path in U:given a ∈ Ter(Γ , U) and b ∈ Ter(Γ , U) with t ∈ Ter(Γ , Equiv (El a)(El b)) we get a small type G(t.1) ∈ Ty (Γ ∗ I) which has the Kan structure κ = G (El a)(El b) ext by Theorem 1 where ext is constructed from El a, El b, and t using Lemma 1. Hence (G(t.1), κ) ∈ Ter(Γ ∗ I, U) with (G(t.1), κ)[0]= (G(t.1)[0],κ[0]) = (El a, El a) = a and likewise (G(t.1), κ)[1]=b.Finally,wegetapath  (G(t.1), κ) ∈ Ter(Γ , Path ab). Choosing a : U, b : U, t : Equiv (El a)(El b) as the context Γ above we get using currying ua ∈ Ter 1,Π(ab : U)(Equiv (El a)(El b) → Path ab) . Observe that we didn’t use that G and its Kan structure commute with substitutions to derive ua. In addition to ua we obtain a section ua of Π(ab : U)Π(t : Equiv (El a)(El b)) Path (T (ua t )) (t.1) El a→El b El where T : Path ab → El a → El b is the transport operation for paths for (El q, El q) in El U KTy (U) (see the operation T in [2, Section 8.2]). Indeed, the path to justify ua is given by reflexivity using our refined Kan structure from Theorem 2 plus that T is given in terms of El composition with an empty tube. The transport operation T can easily be extended to an operation El Equiv T : Path ab → Equiv (El a)(El b) El Equiv which goes in the opposite direction as ua. Actually, ua and T constitute a section- El retraction pair because of ua and the fact that isEquiv t.1 is a proposition, that is, all its inhabitants are path-equal. Hence Σ(b : U) Equiv (El a)(El b) is a retract of Σ(b : U) Path ab.Since U has a Kan structure by Theorem 3, the latter type is contractible (see [2, Section 8.2]) and thus so is the former, concluding the proof. 4 Identity Types We will now describe the identity type which justifies the usual judgmental equality for its eliminator following Swan [7]. Let Γ be a cubical set and A, B ∈ Ty(Γ ), i.e., A and B are presheaves on the category of elements of Γ . For natural transformations α : A → B we are going to define a factorization as α = p i with i : A → M and p : M → B. Furthermore, i will be a cofibration α α α α α α α Natural transformations α : A → B correspond to sections in Ter(Γ , A → B), and also to maps between the projections Γ.A → Γ and Γ.B → Γ in the slice over Γ . To simplify notation, we will write α for either of these. 123 168 M. Bezem et al. (i.e., has the lifting property w.r.t. any acyclic fibration as formulated in Corollary 2)and p will be equipped with an acyclic-fibration structure. This factorization corresponds to Garner’s factorization using the refined small object argument [5] specialized to cubical sets. For ρ in Γ(I ) we will define the sets M ρ together with the restriction maps M ρ → α α M (ρ f ) (for f : J → I ) and the components M ρ → Bρ of the natural transformation p α α α by an inductive process (see Remark 2 below). The elements of M ρ are either of the form i u with u in Aρ (and i considered as a constructor) and we set in this case (i u) f = i(uf ) and p (i u) = α u. Or the elements are of the form (v, [J → u]) where v ∈ Bρ, J ⊆ I,and u is a J -tube in M ρ over v (meaning p u = v( j/b)). In thelattercaseweset p (v, [J → α α jb α u]) = v and for the restrictions (v, [J → u]) f = u ( f − j ) if f ( j ) = b ∈{0, 1} for some jb j ∈ J,and (v, [J → u]) f = (v f, [Jf → u f ]) if f is defined on J . Note that restrictions do not increase the syntactic complexity of an element m ∈ M ρ. This defines M ∈ Ty(Γ ) α α and we set i u = i u. Remark 2 This construction is rather subtle in a set-theoretic framework. One possible way to define this factorization is to first inductively define larger sets M ρ containing all formal elements i u with u ∈ Aρ,and (v, [J → u]) with v ∈ Bρ and where u is represented by a family of elements u ∈ M (ρ f ) indexedbyall f : K → I with fj = 0 or1forsome j ∈ J , but without requiring compatibility. On these sets one can then define maps M ρ → M (ρ f ) α α and M ρ → Bρ. Given these maps, we can single out the sets M ρ ⊆ M ρ of the well- α α formed elements as in the definition above, on which the corresponding maps then induce restriction operations (satisfying the required equations) and the natural transformation p . We use M , i , p in the following way. Let A be a Kan type and let B = Path be the α α α A Kan type of paths over A without specified endpoints. (The Kan structure on A induces the Kan structure on B, much in the same way as shown in [2] for types Path ab.) As mentioned in Sect. 2, transport along reflexivity paths is not necessarily the identity function. One could solve this problem if one could recognize the reflexivity paths, which is not possible in Path . Swan’s [7] solution to this problem is to define a type equivalent to Path in which one can recognize (representations of) reflexivity paths. This is the type M with α : A → Path α A mapping each a in A to its reflexivity path. The representation of the reflexivity path of a in M is i a, with i a constructor of the inductively defined type M , and recognizing i a is α α done through pattern matching. All the rest of the complicated definition above is to make sure that M has the right Kan structure (Lemma 2), and that elimination generally has the right properties (Corollary 1). Constructors of the form (v, [J → u]) equip p : M → B with an acyclic-fibration α α structure which (uniformly) fills tubes [J → u] in M ρ over a filled cube v in Bρ. Thus to, say, construct a path between specified endpoints in M it is enough to give a path in B between the images of the endpoints under p . There are two important observations to make at this point: First, this construction preserves smallness, i.e., M ∈ Ty (Γ ) whenever A, B ∈ Ty (Γ ). And, second, this con- 0 0 struction is stable under substitution: given σ : Δ → Γ we have M σ = M , i σ = i , α ασ α ασ and p σ = p . Neither of these properties holds for the corresponding factorization into α ασ an acyclic cofibration followed by a fibration (sketched in [6, Section 3.5] for a special case). Lemma 2 Given κ ∈ Fill(Γ , B) there is M κ ∈ Fill(Γ , M ). Moreover, this assignment is stable under substitution, i.e., (M κ)σ = M (κσ ) for σ : Δ → Γ . α ασ Proof Let ρ ∈ Γ(I ) and, say, m =[J → m; (i, 0) → m ] be an open box in M over ρ. i0 α We get an open box v =[J → v; (i, 0) → v ] in B over ρ by setting v = p m .We i0 jb α jb define 123 The Univalence Axiom in Cubical Sets 169 M κρ m = (κ ρ v, [J, i → m, m , m ]) i0 i1 with m = (κρ ¯ v, [J → m(i /1)]). i1 Lemma 3 Given a Kan type (D,κ ) ∈ KTy(Γ .M ) and sections s ∈ Ter(Γ .A, Di ) and D α α s ∈ Ter(Γ .M , D) together with a homotopy e ∈ Ter Γ, Π(a : A) Path (s (i a)) (sa) , D(i a) α it is possible to find a section s˜ ∈ Ter(Γ .M , D) such that si ˜ = s ∈ Ter(Γ .A, Di ).Or α α α stated as a diagram, we are given a commuting square where the upper left triangle only commutes up to the homotopy e and the lower triangle commutes strictly, and we get a new diagonal lift where both triangles commute strictly. Moreover, this assignment is stable under substitutions, i.e., given σ : Δ → Γ , substituting the chosen diagonal lift s˜ (for the data α, D,κ , s, s , e) along (σ p, q) : Δ.M → Γ.M D ασ α results in the chosen diagonal lift for the substituted data (where σ is weakened appropriately if needed). Proof For ρ ∈ Γ(I ) and m ∈ M ρ we define s˜(ρ , m) ∈ D(ρ , m) and a path e ˜(ρ , m) between s (ρ , m) and s˜(ρ , m) in D(ρ , m) by induction on the syntactic complexity of m ∈ M ρ such that (s˜(ρ , m)) f =˜s(ρ f, mf ) and (e ˜(ρ , m)) f =˜e(ρ f, mf ). In case m = i u for u ∈ Aρ,we set s˜(ρ , i u) = s(ρ , u) and e ˜(ρ , i u) = e(ρ , u). In case m = (v, [J → m]),weset e ˜(ρ , m) =i κ (ρs ) [J → w; (i, 0) → s (ρ , m)] D i where w =˜e(ρ( j/b), m ) @ i, and correspondingly s˜(ρ , m) =˜e(ρ , m) @ 1. jb jb If the Kan structure is an acyclic-fibration structure as in Definition 2, that is, if we can fill tubes without a closing lid, the above proof can be carried out without s . This implies the following result, which expresses that i : A → M is a cofibration. α α Corollary 1 Given D ∈ Ty(Γ .M ) equipped with an acyclic-fibration structure and a sec- tion s ∈ Ter(Γ .A, Di ) it is possible to define a section s˜ ∈ Ter(Γ .M , D) such that α α si ˜ = s ∈ Ter(Γ .A, Di ). That is, there is a diagonal lift in the diagram: α α Moreover, this assignment is stable under substitution. Proof By Lemma 1 we know that D has a Kan structure and is contractible. From the contractibility we get a section s ∈ Ter(Γ .M , D) and a homotopy between s i and s,and α α can thus apply Lemma 3 to get a strict diagonal filler. This also implies the following result, which expresses that i : A → M is a acyclic α α cofibration as soon as α has a well-behaved homotopy inverse. Recall that application ap α p ∈ Ter(Γ , Path (α u)(α v)) of α : A → B to a path p ∈ Ter(Γ , Path u v) is B A given by (ap α p)ρ =i α(pρ @ i ) (see [6, Section 3.3.2]). 123 170 M. Bezem et al. Corollary 2 Let α : A → B and assume we are given β : B → A and sections η ∈ Ter Γ, Π(a : A) Path (β(α a)) a , ε ∈ Ter Γ, Π(b : B) Path (α(β b)) b , and τ ∈ Ter Γ, Π(a : A) Path (ε(α a)) (ap α(η a)) , where the omitted subscript of the path-type in τ is Path (α (β(α a))) (α a). Then given D ∈ Ty(Γ .M ) with Kan structure κ we can extend any section s ∈ Ter(Γ .A, Di ) to a α D α section s˜ ∈ Ter(Γ .M , D) satisfying si ˜ = s. Moreover, this assignment is stable under α α substitution. Proof It is sufficient to construct s and e as in Lemma 3. To enhance readability we omit the arguments from Γ . First, given m ∈ M we have a path m connecting i (β(p m)) to m, since the images α α α of the endpoints under p are α(β(p m)) and p m which are connected by ε(p m). Thus α α α α the acyclic-fibration structure on p givesusadesiredpath m , which moreover lies over ε(p m), i.e., p (m @ j ) = ε(p m) @ j for fresh j.(6) α α Next,wehave s(β(p m)) ∈ D(i (β(p m))) which we then can transport to Dm using α α α theKan structureand thepath m . Thus we set s m := κ ¯ (m @ j ) [( j, 0) → s(β(p m))]. (7) D α It remains to give a path ea connecting s (i a) to sa in D(i a) for a ∈ A.Wehavethe α α two horizontal lines (in direction j)in (8) where the top line is given by s(η a @ j ) in D(i (η a @ j )) and the bottom line is given by a filling in D((i a) @ j ) following the construction (7)of s . We want to construct the vertical dashed line in D(i a). We can define this line using a composition on the open box specified in (8) as soon as we can provide an interior of the following square in M over which (8) is an open box: But by (6), mapping this square to B using p has a filler given by τ a @ k @ j (where k extends vertically), and thus also a filler in M since p has an acyclic-fibration structure, α α concluding the proof. The representation of the identity type with the usual judgmental equality for its eliminator follows from these results by considering the case where B is the type of paths without specified endpoints Path over a type A and α a is the constant path a. We get a factorization with Id := M , refl := i , and where the right vertical map is given by taking endpoints: A α α 123 The Univalence Axiom in Cubical Sets 171 This α satisfies the hypothesis of Corollary 2 using the properties of path-types from [2, Section 8.2], and hence refl : A → Id has diagonal lifts against types with Kan structure. These diagonal lifts serve as the interpretation of the eliminator (cf. [1, p. 52]) and their choice is stable under substitution, allowing us thus to interpret identity types. One can also explain Id with fixed endpoints as Kan type in context Γ.A.Ap and then show that Id u v is Path-equivalent to Path u v. It follows that a type is Path-contractible A A if, and only if, it is Id-contractible. The univalence axiom for Path-types (Theorem 4) hence also holds formulated with Id-types. We can summarize the results of this section as: Theorem 5 The cubical set model of [2,6] supports identity types and validates the univa- lence axiom. Acknowledgements We want to thank Cyril Cohen and Anders Mörtberg for several discussions around an implementation of this system, as well as Andrew Swan for discussions on the representation of the identity type in the cubical set model. Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 Interna- tional License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made. References 1. Awodey, S., Warren, M.A.: Homotopy theoretic models of identity types. Math. Proc. Camb. Philos. Soc. 146(1), 45–55 (2009) 2. Bezem, M., Coquand, T., Huber, S.: A model of type theory in cubical sets. In: Matthes, R., Schubert, A. (eds.) 19th International Conference on Types for Proofs and Programs (TYPES 2013), Leibniz Inter- national Proceedings in Informatics (LIPIcs), vol. 26, pp. 107–128. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2014). https://doi.org/10.4230/LIPIcs.TYPES.2013.107. http://drops. dagstuhl.de/opus/volltexte/2014/4628 3. Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom (2015). To appear in the proceedings of TYPES 2015 4. Coquand, T.: A remark on contractible families of types (2013). Unpublished note available at http://www. cse.chalmers.se/~coquand/contr.pdf 5. Garner, R.: Understanding the small object argument. Appl. Categ. Struct. 17(3), 247–285 (2009) 6. Huber, S.: A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg (2015) 7. Swan, A.: An algebraic weak factorisation system on 01-substitution sets: a constructive proof (2014). Preprint arXiv:1409.1829 [math.LO] http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of Automated Reasoning Springer Journals

The Univalence Axiom in Cubical Sets

Loading next page...
 
/lp/springer-journals/the-univalence-axiom-in-cubical-sets-76k38yvE2P

References (6)

Publisher
Springer Journals
Copyright
Copyright © 2018 by The Author(s)
Subject
Computer Science; Mathematical Logic and Formal Languages; Artificial Intelligence; Mathematical Logic and Foundations; Symbolic and Algebraic Manipulation
ISSN
0168-7433
eISSN
1573-0670
DOI
10.1007/s10817-018-9472-6
Publisher site
See Article on Publisher Site

Abstract

J Autom Reasoning (2019) 63:159–171 https://doi.org/10.1007/s10817-018-9472-6 1 2 Marc Bezem · Thierry Coquand · Simon Huber Received: 20 November 2016 / Accepted: 4 June 2018 / Published online: 26 June 2018 © The Author(s) 2018 Abstract In this note we show that Voevodsky’s univalence axiom holds in the model of type theory based on cubical sets as described in Bezem et al. (in: Matthes and Schubert (eds.) 19th international conference on types for proofs and programs (TYPES 2013), Leibniz international proceedings in informatics (LIPIcs), Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, vol 26, pp 107–128, 2014. https://doi.org/10.4230/LIPIcs. TYPES.2013.107. http://drops.dagstuhl.de/opus/volltexte/2014/4628) and Huber (A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg, 2015). We will also discuss Swan’s construction of the identity type in this variation of cubical sets. This proves that we have a model of type theory supporting dependent products, dependent sums, univalent universes, and identity types with the usual judgmental equality, and this model is formulated in a constructive metatheory. Keywords Dependent type theory · Univalence axiom · Cubical sets 1 Review of the Cubical Set Model We give a brief overview of the cubical set model, introducing some different notations, but will otherwise assume the reader is familiar with [2,6]. B Marc Bezem bezem@ii.uib.no Simon Huber simon.huber@cse.gu.se Thierry Coquand thierry.coquand@cse.gu.se Department of Informatics, University of Bergen, Postboks 7800, 5020 Bergen, Norway Department of Computer Science and Engineering, University of Gothenburg, 412 96 Göteborg, Sweden 123 160 M. Bezem et al. As opposed to [2,6] let us define cubical sets as contravariant presheaves on the opposite of the category used there, that is, the category of cubes C contains as objects finite sets I ={i ,..., i } (n ≥ 0) of names and a morphism f : J → I is given by a set-theoretic 1 n map I → J ∪{0, 1} which is injective when restricted to the preimage of J ; we will write op compositions in applicative order. The category of cubical sets is the category [C , Set] of presheaves on C . A morphism f : J → I in C can be viewed as a substitution. If f (i ) ∈ J , we call f defined on i.For i ∈ / I , the face morphisms are denoted by (i /0), (i /1) : I → I, i and are induced by setting i to 0 and 1, respectively; degenerating along i ∈ / I is denoted by s : I, i → I and is induced by the inclusion I ⊆ I, i. If Γ is a cubical set, we write Ty(Γ ) for the collection/class of presheaves on the category of elements of Γ [2,6]. Such a presheaf A ∈ Ty(Γ ) is given by a family of sets A(I,ρ) for I ∈ C and ρ ∈ Γ(I ) together with restriction functions. As ρ ∈ Γ(I ) determines I we simply write Aρ for A(I,ρ).Given A ∈ Ty(Γ ) and a natural transformation (substitution) σ : Δ → Γ we get Aσ ∈ Ty(Δ) defined as (Aσ)ρ = A(σρ) which extends canonically to the restrictions. For A ∈ Ty(Γ ) we denote the set of sections of A by Ter(Γ , A);so a ∈ Ter(Γ , A) is given by a family aρ ∈ Aρ for ρ ∈ Γ(I ) such that (aρ) f = a(ρ f ) for f : J → I . Substitution also extends to terms via (aσ)ρ = a(σρ). Let us recall the construction of Π-types: Π AB ∈ Ty(Γ ) for A ∈ Ty(Γ ) and B ∈ Ty(Γ .A) is given by letting each element w of (Π AB)ρ (with ρ ∈ Γ(I )) be a family of w a ∈ B(ρ f, a) for f : J → I and a ∈ Aρ satisfying (w a)g = w (ag); the restriction f f fg of such a w is given by (w f ) = w . In the sequel we will however only have to refer to g fg w when f is the identity, and will thus simply write w a for w a. We also occasionally f id switch between sections in Ter(Γ .A, B) and Ter(Γ , Π AB) without warning the reader. Let A ∈ Ty(Γ ), ρ ∈ Γ(I ),and J ⊆ I.A J -tube in A over ρ is given by a family u of elements u ∈ Aρ( j/c) for ( j, c) ∈ J ×{0, 1} which is adjacent compatible, that jc is, u (k/d) = u ( j/c) for ( j, c), (k, d) ∈ J ×{0, 1}.For (i, a) ∈ (I − J ) ×{0, 1} we jc kd say that an element u ∈ Aρ(i /a) is a lid of such a tube u if u (i /a) = u ( j/c) for all ia jc ia ( j, c) ∈ J ×{0, 1}. In this situation we call the pair [J → u; (i, a) → u ] an open box in ia A over ρ.A filler for such an open box is an element u ∈ Aρ such that u( j/c) = u for jc ( j, c) ∈{(i, a)}∪ (J ×{0, 1}). In case J is empty, we simply write [(i, a) → u ]. ia Given f : K → I and an open box m =[J → u; (i, a) → u ] in A over ρ we call f ia allowed for m if f is defined on J, i. In this case we define the open box mf in A in ρ f to be [Jf → u f ; ( f (i ), a) → u ( f − i )] where u f is given by (u f ) = u ( f − j ) with ia f ( j ) c jc f − i : K − f (i ) → I − i being like f but skipping i,and Jf is the image of J under f . Recall from [2, Section 4] that a (uniform) Kan structure for a type A ∈ Ty(Γ ) is given by an operation κ which (uniformly) fills open boxes: for any ρ ∈ Γ(I ) and open box m in A over ρ we get a filler κρ m of m subject to the uniformity condition (κ ρ m) f = κ(ρ f )(mf ) for all f : K → I allowed for m. Any Kan structure κ defines a composition operation κ ¯ which provides the missing lid of the open box, given by: κρ ¯ [J → u; (i, 0) → u ]= (κ ρ [J → u; (i, 0) → u ])(i /1) i0 i0 κρ ¯ [J → u; (i, 1) → u ]= (κ ρ [J → u; (i, 1) → u ])(i /0) i1 i1 We denote the set of all Kan structures on A ∈ Ty(Γ ) as Fill(Γ , A).If σ : Δ → Γ and κ is an element in Fill(Γ , A), we get an element κσ in Fill(Δ, Aσ) defined by (κσ ) ρ = κ(σρ). 123 The Univalence Axiom in Cubical Sets 161 Given a cubical set Γ a Kan type is a pair (A,κ) where A ∈ Ty(Γ ) and κ ∈ Fill(Γ , A). We denote the collection of all such Kan types by KTy(Γ ).In[2] we showed that Kan types are closed under dependent products and sums constituting a model of type theory. 2 Path Types In [2] we introduced identity types which were however only “weak”, e.g., transport along reflexivity is only propositionally equal to the identity function but not necessarily judgmen- tally equal. For this reason we will call these types path types and reserve Id for the identity type with the usual judgmental equality defined in Sect. 4. Recall that the path type Path u v ∈ Ty(Γ ) for A ∈ Ty(Γ ) and u,v ∈ Ter(Γ , A) is defined by the sets (Path u v)ρ containing equivalence classes i w where i ∈ / I and w ∈ Aρs with w(i /0) = uρ and w(i /1) = vρ. Restrictions are defined as expected, and we showed that Kan types are closed under forming path types [2]. It will be convenient below to introduce paths using separated products. Definition 1 Given cubical sets Γ and Δ, we say that u ∈ Γ(I ) and v ∈ Δ(I ) are separated, denoted by u # v, if they come through degeneration from cubes with disjoint sets of directions. More precisely, if there are J ⊆ I , K ⊆ I with J ∩ K =∅ and u ∈ Γ(J ), v ∈ Δ(K ) such that u = u s and v = v s with s and s induced by the inclusion J ⊆ I and K ⊆ I , respectively. The separated product Γ ∗ Δ of Γ and Δ is the cubical set defined by (Γ ∗ Δ)(I ) ={(u,v) ∈ Γ(I ) × Δ(I ) | u # v}⊆ (Γ × Δ)(I ). The restrictions are inherited from Γ × Δ, that is, they are defined component wise. It can be shown that −∗− extends to a functor, and that −∗ Δ has a right adjoint. Of particular interest is Γ ∗ I where I is the interval defined by I(J ) = J ∪{0, 1} (see [2, Section 6.1]). Then (Γ ∗ I)(I ) = (Γ (I ) ×{0, 1}) ∪{(ρs , i ) | i ∈ I ∧ ρ ∈ Γ(I − i )}. If (ρ , i ) ∈ (Γ ∗ I)(I ) with i ∈ I,then ρ = ρ s for a uniquely determined ρ which we denote by ρ − i. We can use Γ ∗ I to formulate the following introduction rule for path types where [0], [1]: Γ → Γ ∗ I are induced by the global elements 0 and 1 of I, respectively, and p : Γ ∗ I → Γ is the first projection. The binding operation is interpreted by ( w)ρ = i w(ρs , i ) with i a fresh name (see [2, Section 8.2]). Given an element i w ∈ (Path u v)ρ with ρ ∈ Γ(I ),weset (i w) @ a = w(i /a) where a is 0, 1, or a fresh name. 3 Equivalences and Univalence We will now recall the definition of an equivalence as a map having contractible fibers and then derive an operation for contractible and Kan types. To enhance readability we define the following types using variable names: 123 162 M. Bezem et al. isContr A = Σ(x : A)Π(y : A) Path xy fib t v = Σ(x : A) Path (tx)v isEquiv t = Π(y : B) isContr(fibty) Equiv AB = Σ(t : A → B) isEquiv t where A and B are types, t : A → B,and v : B (all in an ambient context Γ ). This can of course also be formally written name-free: for example, the first type can be written as Σ AΠ Ap (Path qp q) ∈ Ty(Γ ) and the second one as Σ Ap (Path app(tpp, q) qp) ∈ App Bpp Ty(Γ .B). Definition 2 A (uniform) acyclic-fibration structure on a type A ∈ Ty(Γ ) is givenbyan operation ext uniformly filling any tube, that is, given ρ ∈ Γ(I ), J ⊆ I,a J -tube u in Aρ, we have ext ρ [J → u]∈ Aρ extending u (so (ext ρ [J → u])(i /a) = u for (i, a) ∈ J ×{0, 1})and for f : K → I ia defined on J we have (ext ρ [J → u]) f = ext (ρ f ) [Jf → u f ]. We denote the set of acyclic-fibration structures on A ∈ Ty(Γ ) by Contr(Γ , A). Note that given ext ∈ Contr(Γ , A) and σ : Δ → Γ we obtain ext σ ∈ Contr(Δ, Aσ) via (ext σ) ρ = ext (σρ). Lemma 1 Given a type A in Ty(Γ ) we have maps with ϕ ψ ,ψ = id. Moreover, these maps are natural: if σ : Δ → Γ ,then (ϕ κ p)σ = 0 1 ϕ(κσ) (pσ), (ψ ext)σ = ψ (ext σ), and (ψ ext)σ = ψ (ext σ). 0 0 1 1 Proof Let κ ∈ Fill(Γ , A) and p ∈ Ter(Γ , isContr A).Todefine ϕκ p ∈ Contr(Γ , A),let ρ ∈ Γ(I ) and u a J -tube in A over ρ.Wetakeafresh dimension i and form an open box with the center of contraction pρ.1 at the closed end and u at the open end, connected by pρ.2; filling this gives us an extension of u. Formally: ϕκ p ρ [J → u]= κ( ¯ ρs ) [J → (pρ.2 u) @ i ; (i, 0) → pρ.1] where (pρ.2 u) @ i is the J -tube given by (p(ρ( j/c)).2 u ) @ i at side ( j, c) ∈ J ×{0, 1}. jc Conversely, let ext ∈ Contr(Γ , A).Toget aKan structurewefirstfill themissing lid and then the interior, that is, we set ψ ext ρ [J → u; (i, 0) → u ] 0 i0 = ext ρ [J → u,(i, 0) → u ,(i, 1) → ext ρ(i /1) [J → u(i /1)]], i0 and likewise for the other filling. To define ψ ext ρ we choose ext ρ [] as center of contraction, which is connected to any a ∈ Aρ by the path i ext (ρs ) [(i, 0) → ext ρ [],(i, 1) → a]. One can show uniformity, naturality, and that ψ ,ψ is a section of ϕ. 0 1 123 The Univalence Axiom in Cubical Sets 163 Next we will define an operation G which allows us to transform an equivalence into a “path”. This operation was introduced in [4] and motivated the “glueing” operation of [3]. We will define it in such a way that the associated transport of this path is given by underlying map of the equivalence. A useful analogy is provided by the notion of pathover, a heterogeneous path lying over another path. We shortly review this notion from type theory with inductive equality. Given a type family P : T → U and a path p : x = y with its transport function p : Px → Py. T ∗ If Px and Py are different types, there is no ordinary path connecting u : Px and v : Py. Therefore the pathovers connecting u and v are taken to be the paths of type p u = v (in ∗ Py the fiber Py). We apply the same idea to G t, which should be a path from A to B in U such that transport along this path is t : A → B. For the type family P we take id such that A and B indeed are fibers of P. Intuitively, a path from A to B is a set of heterogeneous paths between elements a of A and b of B.Wewant t to be the transport function along the path from A to B.By analogy we would take G t to be the set of pathovers connecting a : A and b : B defined as the set of paths in B connecting ta and b. However, since we must be able to recover the startpoint a,wedefine G t to be the set of pairs consisting of a : A and a path connecting ta and b. (Unlike a, the endpoint b can be recovered from the pathover and need not be remembered.) With the above informal explanation in mind, we define the operation G first on cubical sets and then explain how it lifts to Kan structures. It satisfies the rules: (1) (2) The latter rule expresses stability under substitutions. Here and below G (and ug below) have A and B as implicit arguments. Definition 3 Assume the premiss of (1) and define for every ρ ∈ Γ(I ): (G t )(ρ , 0) = Aρ, with restrictions as in A, (G t )(ρ , 1) = Bρ, with restrictions as in B,and (3) (G t )(ρ , i ) ={(u,v) | u ∈ A(ρ − i ) ∧ v ∈ Bρ ∧ v(i /0) = t (ρ − i ) u}. In the last case ρ # i,so ρ = (ρ − i )s . The restrictions in the latter case are a little involved. We need (u,v) f ∈ (G t )(ρ f, f (i )) for f : J → I.If f (i ) = 0, we take (u,v) f = us f , indeed in Aρ f .If f (i ) = 1, we take (u,v) f = v f , indeed in Bρ f . Finally, if f is defined on i,wehave f − i : J − f (i ) → I − i and we define (u,v) f = (u( f − i ), v f ),which is indeed correct as (ρ − i )( f − i ) = ρ f − f (i ) under the given assumptions. It can then be checked that the restrictions satisfy the presheaf requirements. This concludes the definition of G t. We haveamap ug ∈ Ter(Γ ∗ I. G t, Bp) given by: We will see later that this indeed induces a path in a universe whenever both types A and B are small. 123 164 M. Bezem et al. The fact that a map t ∈ Ter(Γ , A → B) is an equivalence can be represented as an element of Contr(Γ .B, fib t ). By Lemma 1 this is the case whenever A and B have Kan structures and the fibers of t are contractible. Theorem 1 The operation G can be lifted to Kan structures provided t is an equivalence, i.e., there is an operation G which given the premiss of (1) and κ ∈ Fill(Γ , A), κ ∈ Fill(Γ , B), A B and ext ∈ Contr(Γ .B, fib t ) returns G κ κ ext ∈ Fill(Γ ∗ I, G t ). This operation satisfies A B (G κ κ ext)[0]= κ A B A (G κ κ ext)[1]= κ A B B (G κ κ ext)(σ ∗ id) = G (κ σ) (κ σ) (ext (σ p, q)) A B A B where σ : Δ → Γ . Proof To define (G κ κ ext)(ρ , r ) for (ρ , r ) ∈ (Γ ∗ I)(I ) we argue by cases. For r = 0, 1 A B we take: (G κ κ ext)(ρ , 0) = κ ρ A B A (G κ κ ext)(ρ , 1) = κ ρ A B B Let us now consider the main case where r = i ∈ I is a name and thus ρ # i, ρ = (ρ −i )s .We are given j (the name along which we fill), w a J -tube in (G t ) over (ρ , i ) (with J ⊆ I − j), and w ∈ (G t )(ρ , i )( j/a) for a = 0or 1, which fits w.Wewanttodefine ja w := (G κ κ ext)(ρ, i ) [J → w; ( j, a) → w ] A B ja in (G t )(ρ , i ). For this we have to construct w = (u,v) with u ∈ A(ρ − i ) and v ∈ Bρ such that v(i /0) = t (ρ − i ) u. We can map w , w using ug and obtain an open box v , v in B over ρ given by ja ja v := ug((ρ , i )(k/b), w ) ∈ Bρ(k/b). kb kb There are four cases to consider depending on how the open box relates to the direction i. Each case will be illustrated afterwards with simplified J . Note that in all these pictures the part in A is mapped by t to the left face of the part in B. Here are the four cases: Case i = j and i ∈ / J . We extend the J -tube w to J, i-tube by constructing w and w i0 i1 and then proceed as in the next case with the tube w,w ,w .Notethatwewant i0 i1 w ∈ (G t )(ρ , i )(i /0) = A(ρ − i ), and i0 w ∈ (G t )(ρ , i )(i /1) = B(ρ − i ), i1 so we can take w = κ (ρ − i ) [J → w(i /0); ( j, a) → w (i /0)], and (4) i0 A ja w = κ (ρ − i ) [J → w(i /1); ( j, a) → w (i /1)]. (5) i1 B ja The resulting open box is compatible by construction. Note that this (together with the cases for r = 0and r = 1) also ensures that the Kan structure satisfies the equations in (1). We illustrate this case in the picture below. Here and below the left part is in A and on the right we have the open box v in B. For simplicity we also omit ρ. We construct w and w i0 i1 by filling the open boxes indicated by thicker lines on the left and on the right, respectively. 123 The Univalence Axiom in Cubical Sets 165 Case i = j and i ∈ J . In this case v = ug((ρ(i /0), 0), w ) = tρ(i /0)w = i0 i0 i0 t (ρ − i)w since ρ # i. We can therefore take w = (w ,v) ∈ (G t )(ρ , i ) where v = i0 i0 κ (ρ − i ) [J → v; ( j, a) → v ]. This can be illustrated by: B ja Case j = i and a = 0. Like in the previous case we can take w = (w ,v) ∈ (G w)(ρ, i ) i0 where v = κ (ρ − i ) [J → v; ( j, a) → v ]. This case is illustrated as follows: B ja Cases j = i and a = 1. In this case the direction of the filling is opposite to t,and therefore we have to use ext which expresses that fib t is contractible. The family m defined by m := (w , i v ) ∈ (fib t )((ρ − i )(k/b), w (k/b)) kb kb kb i1 for (k, b) ∈ J ×{0, 1} constitutes a J -tube over (ρ − i,w ) in the contractible type fib t ∈ i1 Ty(Γ .B). So we can extend this tube to obtain (u,ω) = ext (ρ − i,w ) [J → m]∈ (fib t )(ρ − i,w ) i1 i1 and we can take w := (u,ω @ i ) ∈ (G t )(ρ , i ). Let us illustrate this case: we are given the two dots on the left and the solid lines on the right in the picture below, and we want to construct the dashed line and a square on the right such that the dashed line is mapped to the dotted line via t, that is, we basically want to construct an element in the fiber of w under t. i1 This concludes the definition of the filling operations of G t. To see that this filling operation is uniform, note that for an f : K → I defined on j, J and on i the case which defines the filling of [J → w; ( j, a) → w ] f coincides with ja the case used to defined [J → w; ( j, a) → w ] by the injectivity requirement on f — ja uniformity then follows for each case separately since we only used operations that suitably commutewith f in the definition of the filling. If f is only defined on j, J but not on i, 123 166 M. Bezem et al. the first case has to apply—to simplify notation assume f is (i /c)—then by construction (Eqs. 4, 5) (G κ κ ext)(ρ, i ) [J → w; ( j, a) → w ] (i /c) A B ja = (G κ κ ext)(ρ − i, c) [J → w(i /c); ( j, a) → (w (i /c))], A B ja concluding the proof. Theorem 2 We can refine the Kan structure G κ κ ext given in Theorem 1 such that it A B satisfies (G κ κ ext)(ρ, i ) [(i, 0) → u]= tρ u. A B Proof We modify the Kan structure given in the proof of Theorem 1 to obtain the above equations. The last two cases in the proof above where i = j are modified by an additional case distinction on whether J is empty or not. If J is not empty or a = 1, proceed as before. In case J is empty and a = 0, then we are given u ∈ A(ρ − i ) andanempty tube and i0 can define (G κ κ ext)(ρ, i ) [(i, 0) → u ]= (u , tρ u ). That this definition remains A B i0 i0 i0 uniform is proved as in Theorem 1 using the observation that |J|=|Jf | for f defined on J . In addition we retain stability under substitution. Remark 1 It is also possible to change the Kan structure such that it satisfies −1 (G κ κ ext)(ρ, i ) [(i, 1) → u]= t ρ u, A B −1 where t is the inverse of t which can be constructed from ext. For this one also has to −1 −1 modify the case where J is empty and a = 1 from the definition of G using t and that t is a (point-wise) right inverse of t (in the sense of path types). The latter is also definable using ext. Let us recall the definition of a universe U of small Kan types (assuming a Grothendieck universe of small sets in the ambient set theory). A type A ∈ Ty(Γ ) is small if all the sets Aρ for ρ ∈ Γ(I ) are so. A Kan type (A,κ) ∈ KTy(Γ ) is small if A ∈ Ty(Γ ) is small. We denote the set of all such small types and Kan types by Ty (Γ ) and KTy (Γ ), respectively. 0 0 Substitution makes both Ty and KTy into presheaves on the category of cubical sets. The 0 0 universe U is now given as U = KTy ◦ y where y denotes the Yoneda embedding. For an I -cube (A,κ) ∈ U(I ) = KTy (y I ) we have that A is a presheaf on the category of elements of y I,and A(J, f ) is a small set for every element (J, f : J → I ). Moreover, κ(J, f ) is a filler function for open boxes in A over (J, f ). Of particular interest are the small set A(I, id ) and filler function κ(I, id ). I I Given a ∈ Ter(Γ , U) we can associate a small type El a in Ty (Γ ) by (El a)ρ = A(I, id ) where aρ = (A,κ). We equip El a with the Kan structure El a defined by (El a)ρ = κ(I, id ). This results in an isomorphism which is natural in Γ : where X ρ = X ρˆ ∈ U(I ) for X ∈ KTy (Γ ).Here ρˆ : y I → Γ is the associated substitution of ρ ∈ Γ(I ),thatis, ρˆ f = ρ f ∈ Γ(J ) for any f : J → I . Since moreover Hom(Γ , U) = Ter(Γ , U),weget that KTy is representable. Theorem 3 U has a Kan structure. Proof [6, Theorem 4.2]. 123 The Univalence Axiom in Cubical Sets 167 We are now ready for the first main result of this paper. Theorem 4 (Univalence) The type Π(a : U) isContr Σ(b : U) Equiv (El a)(El b) in Ty(1) has a section, where 1 denotes the empty context. Proof Because our operation G preserves smallness we obtain an operation turning an equiv- alence between small Kan types into a path in U:given a ∈ Ter(Γ , U) and b ∈ Ter(Γ , U) with t ∈ Ter(Γ , Equiv (El a)(El b)) we get a small type G(t.1) ∈ Ty (Γ ∗ I) which has the Kan structure κ = G (El a)(El b) ext by Theorem 1 where ext is constructed from El a, El b, and t using Lemma 1. Hence (G(t.1), κ) ∈ Ter(Γ ∗ I, U) with (G(t.1), κ)[0]= (G(t.1)[0],κ[0]) = (El a, El a) = a and likewise (G(t.1), κ)[1]=b.Finally,wegetapath  (G(t.1), κ) ∈ Ter(Γ , Path ab). Choosing a : U, b : U, t : Equiv (El a)(El b) as the context Γ above we get using currying ua ∈ Ter 1,Π(ab : U)(Equiv (El a)(El b) → Path ab) . Observe that we didn’t use that G and its Kan structure commute with substitutions to derive ua. In addition to ua we obtain a section ua of Π(ab : U)Π(t : Equiv (El a)(El b)) Path (T (ua t )) (t.1) El a→El b El where T : Path ab → El a → El b is the transport operation for paths for (El q, El q) in El U KTy (U) (see the operation T in [2, Section 8.2]). Indeed, the path to justify ua is given by reflexivity using our refined Kan structure from Theorem 2 plus that T is given in terms of El composition with an empty tube. The transport operation T can easily be extended to an operation El Equiv T : Path ab → Equiv (El a)(El b) El Equiv which goes in the opposite direction as ua. Actually, ua and T constitute a section- El retraction pair because of ua and the fact that isEquiv t.1 is a proposition, that is, all its inhabitants are path-equal. Hence Σ(b : U) Equiv (El a)(El b) is a retract of Σ(b : U) Path ab.Since U has a Kan structure by Theorem 3, the latter type is contractible (see [2, Section 8.2]) and thus so is the former, concluding the proof. 4 Identity Types We will now describe the identity type which justifies the usual judgmental equality for its eliminator following Swan [7]. Let Γ be a cubical set and A, B ∈ Ty(Γ ), i.e., A and B are presheaves on the category of elements of Γ . For natural transformations α : A → B we are going to define a factorization as α = p i with i : A → M and p : M → B. Furthermore, i will be a cofibration α α α α α α α Natural transformations α : A → B correspond to sections in Ter(Γ , A → B), and also to maps between the projections Γ.A → Γ and Γ.B → Γ in the slice over Γ . To simplify notation, we will write α for either of these. 123 168 M. Bezem et al. (i.e., has the lifting property w.r.t. any acyclic fibration as formulated in Corollary 2)and p will be equipped with an acyclic-fibration structure. This factorization corresponds to Garner’s factorization using the refined small object argument [5] specialized to cubical sets. For ρ in Γ(I ) we will define the sets M ρ together with the restriction maps M ρ → α α M (ρ f ) (for f : J → I ) and the components M ρ → Bρ of the natural transformation p α α α by an inductive process (see Remark 2 below). The elements of M ρ are either of the form i u with u in Aρ (and i considered as a constructor) and we set in this case (i u) f = i(uf ) and p (i u) = α u. Or the elements are of the form (v, [J → u]) where v ∈ Bρ, J ⊆ I,and u is a J -tube in M ρ over v (meaning p u = v( j/b)). In thelattercaseweset p (v, [J → α α jb α u]) = v and for the restrictions (v, [J → u]) f = u ( f − j ) if f ( j ) = b ∈{0, 1} for some jb j ∈ J,and (v, [J → u]) f = (v f, [Jf → u f ]) if f is defined on J . Note that restrictions do not increase the syntactic complexity of an element m ∈ M ρ. This defines M ∈ Ty(Γ ) α α and we set i u = i u. Remark 2 This construction is rather subtle in a set-theoretic framework. One possible way to define this factorization is to first inductively define larger sets M ρ containing all formal elements i u with u ∈ Aρ,and (v, [J → u]) with v ∈ Bρ and where u is represented by a family of elements u ∈ M (ρ f ) indexedbyall f : K → I with fj = 0 or1forsome j ∈ J , but without requiring compatibility. On these sets one can then define maps M ρ → M (ρ f ) α α and M ρ → Bρ. Given these maps, we can single out the sets M ρ ⊆ M ρ of the well- α α formed elements as in the definition above, on which the corresponding maps then induce restriction operations (satisfying the required equations) and the natural transformation p . We use M , i , p in the following way. Let A be a Kan type and let B = Path be the α α α A Kan type of paths over A without specified endpoints. (The Kan structure on A induces the Kan structure on B, much in the same way as shown in [2] for types Path ab.) As mentioned in Sect. 2, transport along reflexivity paths is not necessarily the identity function. One could solve this problem if one could recognize the reflexivity paths, which is not possible in Path . Swan’s [7] solution to this problem is to define a type equivalent to Path in which one can recognize (representations of) reflexivity paths. This is the type M with α : A → Path α A mapping each a in A to its reflexivity path. The representation of the reflexivity path of a in M is i a, with i a constructor of the inductively defined type M , and recognizing i a is α α done through pattern matching. All the rest of the complicated definition above is to make sure that M has the right Kan structure (Lemma 2), and that elimination generally has the right properties (Corollary 1). Constructors of the form (v, [J → u]) equip p : M → B with an acyclic-fibration α α structure which (uniformly) fills tubes [J → u] in M ρ over a filled cube v in Bρ. Thus to, say, construct a path between specified endpoints in M it is enough to give a path in B between the images of the endpoints under p . There are two important observations to make at this point: First, this construction preserves smallness, i.e., M ∈ Ty (Γ ) whenever A, B ∈ Ty (Γ ). And, second, this con- 0 0 struction is stable under substitution: given σ : Δ → Γ we have M σ = M , i σ = i , α ασ α ασ and p σ = p . Neither of these properties holds for the corresponding factorization into α ασ an acyclic cofibration followed by a fibration (sketched in [6, Section 3.5] for a special case). Lemma 2 Given κ ∈ Fill(Γ , B) there is M κ ∈ Fill(Γ , M ). Moreover, this assignment is stable under substitution, i.e., (M κ)σ = M (κσ ) for σ : Δ → Γ . α ασ Proof Let ρ ∈ Γ(I ) and, say, m =[J → m; (i, 0) → m ] be an open box in M over ρ. i0 α We get an open box v =[J → v; (i, 0) → v ] in B over ρ by setting v = p m .We i0 jb α jb define 123 The Univalence Axiom in Cubical Sets 169 M κρ m = (κ ρ v, [J, i → m, m , m ]) i0 i1 with m = (κρ ¯ v, [J → m(i /1)]). i1 Lemma 3 Given a Kan type (D,κ ) ∈ KTy(Γ .M ) and sections s ∈ Ter(Γ .A, Di ) and D α α s ∈ Ter(Γ .M , D) together with a homotopy e ∈ Ter Γ, Π(a : A) Path (s (i a)) (sa) , D(i a) α it is possible to find a section s˜ ∈ Ter(Γ .M , D) such that si ˜ = s ∈ Ter(Γ .A, Di ).Or α α α stated as a diagram, we are given a commuting square where the upper left triangle only commutes up to the homotopy e and the lower triangle commutes strictly, and we get a new diagonal lift where both triangles commute strictly. Moreover, this assignment is stable under substitutions, i.e., given σ : Δ → Γ , substituting the chosen diagonal lift s˜ (for the data α, D,κ , s, s , e) along (σ p, q) : Δ.M → Γ.M D ασ α results in the chosen diagonal lift for the substituted data (where σ is weakened appropriately if needed). Proof For ρ ∈ Γ(I ) and m ∈ M ρ we define s˜(ρ , m) ∈ D(ρ , m) and a path e ˜(ρ , m) between s (ρ , m) and s˜(ρ , m) in D(ρ , m) by induction on the syntactic complexity of m ∈ M ρ such that (s˜(ρ , m)) f =˜s(ρ f, mf ) and (e ˜(ρ , m)) f =˜e(ρ f, mf ). In case m = i u for u ∈ Aρ,we set s˜(ρ , i u) = s(ρ , u) and e ˜(ρ , i u) = e(ρ , u). In case m = (v, [J → m]),weset e ˜(ρ , m) =i κ (ρs ) [J → w; (i, 0) → s (ρ , m)] D i where w =˜e(ρ( j/b), m ) @ i, and correspondingly s˜(ρ , m) =˜e(ρ , m) @ 1. jb jb If the Kan structure is an acyclic-fibration structure as in Definition 2, that is, if we can fill tubes without a closing lid, the above proof can be carried out without s . This implies the following result, which expresses that i : A → M is a cofibration. α α Corollary 1 Given D ∈ Ty(Γ .M ) equipped with an acyclic-fibration structure and a sec- tion s ∈ Ter(Γ .A, Di ) it is possible to define a section s˜ ∈ Ter(Γ .M , D) such that α α si ˜ = s ∈ Ter(Γ .A, Di ). That is, there is a diagonal lift in the diagram: α α Moreover, this assignment is stable under substitution. Proof By Lemma 1 we know that D has a Kan structure and is contractible. From the contractibility we get a section s ∈ Ter(Γ .M , D) and a homotopy between s i and s,and α α can thus apply Lemma 3 to get a strict diagonal filler. This also implies the following result, which expresses that i : A → M is a acyclic α α cofibration as soon as α has a well-behaved homotopy inverse. Recall that application ap α p ∈ Ter(Γ , Path (α u)(α v)) of α : A → B to a path p ∈ Ter(Γ , Path u v) is B A given by (ap α p)ρ =i α(pρ @ i ) (see [6, Section 3.3.2]). 123 170 M. Bezem et al. Corollary 2 Let α : A → B and assume we are given β : B → A and sections η ∈ Ter Γ, Π(a : A) Path (β(α a)) a , ε ∈ Ter Γ, Π(b : B) Path (α(β b)) b , and τ ∈ Ter Γ, Π(a : A) Path (ε(α a)) (ap α(η a)) , where the omitted subscript of the path-type in τ is Path (α (β(α a))) (α a). Then given D ∈ Ty(Γ .M ) with Kan structure κ we can extend any section s ∈ Ter(Γ .A, Di ) to a α D α section s˜ ∈ Ter(Γ .M , D) satisfying si ˜ = s. Moreover, this assignment is stable under α α substitution. Proof It is sufficient to construct s and e as in Lemma 3. To enhance readability we omit the arguments from Γ . First, given m ∈ M we have a path m connecting i (β(p m)) to m, since the images α α α of the endpoints under p are α(β(p m)) and p m which are connected by ε(p m). Thus α α α α the acyclic-fibration structure on p givesusadesiredpath m , which moreover lies over ε(p m), i.e., p (m @ j ) = ε(p m) @ j for fresh j.(6) α α Next,wehave s(β(p m)) ∈ D(i (β(p m))) which we then can transport to Dm using α α α theKan structureand thepath m . Thus we set s m := κ ¯ (m @ j ) [( j, 0) → s(β(p m))]. (7) D α It remains to give a path ea connecting s (i a) to sa in D(i a) for a ∈ A.Wehavethe α α two horizontal lines (in direction j)in (8) where the top line is given by s(η a @ j ) in D(i (η a @ j )) and the bottom line is given by a filling in D((i a) @ j ) following the construction (7)of s . We want to construct the vertical dashed line in D(i a). We can define this line using a composition on the open box specified in (8) as soon as we can provide an interior of the following square in M over which (8) is an open box: But by (6), mapping this square to B using p has a filler given by τ a @ k @ j (where k extends vertically), and thus also a filler in M since p has an acyclic-fibration structure, α α concluding the proof. The representation of the identity type with the usual judgmental equality for its eliminator follows from these results by considering the case where B is the type of paths without specified endpoints Path over a type A and α a is the constant path a. We get a factorization with Id := M , refl := i , and where the right vertical map is given by taking endpoints: A α α 123 The Univalence Axiom in Cubical Sets 171 This α satisfies the hypothesis of Corollary 2 using the properties of path-types from [2, Section 8.2], and hence refl : A → Id has diagonal lifts against types with Kan structure. These diagonal lifts serve as the interpretation of the eliminator (cf. [1, p. 52]) and their choice is stable under substitution, allowing us thus to interpret identity types. One can also explain Id with fixed endpoints as Kan type in context Γ.A.Ap and then show that Id u v is Path-equivalent to Path u v. It follows that a type is Path-contractible A A if, and only if, it is Id-contractible. The univalence axiom for Path-types (Theorem 4) hence also holds formulated with Id-types. We can summarize the results of this section as: Theorem 5 The cubical set model of [2,6] supports identity types and validates the univa- lence axiom. Acknowledgements We want to thank Cyril Cohen and Anders Mörtberg for several discussions around an implementation of this system, as well as Andrew Swan for discussions on the representation of the identity type in the cubical set model. Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 Interna- tional License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made. References 1. Awodey, S., Warren, M.A.: Homotopy theoretic models of identity types. Math. Proc. Camb. Philos. Soc. 146(1), 45–55 (2009) 2. Bezem, M., Coquand, T., Huber, S.: A model of type theory in cubical sets. In: Matthes, R., Schubert, A. (eds.) 19th International Conference on Types for Proofs and Programs (TYPES 2013), Leibniz Inter- national Proceedings in Informatics (LIPIcs), vol. 26, pp. 107–128. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2014). https://doi.org/10.4230/LIPIcs.TYPES.2013.107. http://drops. dagstuhl.de/opus/volltexte/2014/4628 3. Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom (2015). To appear in the proceedings of TYPES 2015 4. Coquand, T.: A remark on contractible families of types (2013). Unpublished note available at http://www. cse.chalmers.se/~coquand/contr.pdf 5. Garner, R.: Understanding the small object argument. Appl. Categ. Struct. 17(3), 247–285 (2009) 6. Huber, S.: A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg (2015) 7. Swan, A.: An algebraic weak factorisation system on 01-substitution sets: a constructive proof (2014). Preprint arXiv:1409.1829 [math.LO]

Journal

Journal of Automated ReasoningSpringer Journals

Published: Jun 26, 2018

There are no references for this article.