Access the full text.
Sign up today, get DeepDyve free for 14 days.
C. Cohen, T. Coquand, Simon Huber, Anders Mörtberg (2015)
Cubical Type Theory: A Constructive Interpretation of the Univalence AxiomFLAP, 4
S. Awodey, M. Warren (2007)
Homotopy theoretic models of identity typesMathematical Proceedings of the Cambridge Philosophical Society, 146
M. Bezem, T. Coquand, Simon Huber (2013)
A Model of Type Theory in Cubical Sets
Andrew Swan (2014)
An algebraic weak factorisation system on 01-substitution sets: a constructive proofJ. Log. Anal., 8
Richard Garner (2007)
Understanding the Small Object ArgumentApplied Categorical Structures, 17
(2013)
A remark on contractible families of types, Unpublished note available at http://www.cse.chalmers.se/~coquand/contr.pdf
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 deﬁne cubical sets as contravariant presheaves on the opposite of the category used there, that is, the category of cubes C contains as objects ﬁnite 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 deﬁned 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(Δ) deﬁned 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 ﬁller 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 deﬁned on J, i. In this case we deﬁne 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) ﬁlls open boxes: for any ρ ∈ Γ(I ) and open box m in A over ρ we get a ﬁller κρ m of m subject to the uniformity condition (κ ρ m) f = κ(ρ f )(mf ) for all f : K → I allowed for m. Any Kan structure κ deﬁnes 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σ) deﬁned 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 reﬂexivity 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 deﬁned in Sect. 4. Recall that the path type Path u v ∈ Ty(Γ ) for A ∈ Ty(Γ ) and u,v ∈ Ter(Γ , A) is deﬁned 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 deﬁned 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. Deﬁnition 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 deﬁned by (Γ ∗ Δ)(I ) ={(u,v) ∈ Γ(I ) × Δ(I ) | u # v}⊆ (Γ × Δ)(I ). The restrictions are inherited from Γ × Δ, that is, they are deﬁned 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 deﬁned 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 ﬁrst 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 deﬁnition of an equivalence as a map having contractible ﬁbers and then derive an operation for contractible and Kan types. To enhance readability we deﬁne the following types using variable names: 123 162 M. Bezem et al. isContr A = Σ(x : A)Π(y : A) Path xy ﬁb t v = Σ(x : A) Path (tx)v isEquiv t = Π(y : B) isContr(ﬁbty) 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 ﬁrst 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). Deﬁnition 2 A (uniform) acyclic-ﬁbration structure on a type A ∈ Ty(Γ ) is givenbyan operation ext uniformly ﬁlling 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 deﬁned on J we have (ext ρ [J → u]) f = ext (ρ f ) [Jf → u f ]. We denote the set of acyclic-ﬁbration 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).Todeﬁne ϕκ 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; ﬁlling 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 structureweﬁrstﬁll 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 ﬁlling. To deﬁne ψ 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 deﬁne 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 deﬁne 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 ﬁber 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 ﬁbers 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 deﬁned as the set of paths in B connecting ta and b. However, since we must be able to recover the startpoint a,wedeﬁne 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 deﬁne the operation G ﬁrst on cubical sets and then explain how it lifts to Kan structures. It satisﬁes 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. Deﬁnition 3 Assume the premiss of (1) and deﬁne 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 deﬁned on i,wehave f − i : J − f (i ) → I − i and we deﬁne (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 deﬁnition 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, ﬁb t ). By Lemma 1 this is the case whenever A and B have Kan structures and the ﬁbers 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, ﬁb t ) returns G κ κ ext ∈ Fill(Γ ∗ I, G t ). This operation satisﬁes 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 deﬁne (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 ﬁll), 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 ﬁts w.Wewanttodeﬁne 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 simpliﬁed 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 satisﬁes 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 ﬁlling 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 ﬁlling is opposite to t,and therefore we have to use ext which expresses that ﬁb t is contractible. The family m deﬁned by m := (w , i v ) ∈ (ﬁb 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 ﬁb t ∈ i1 Ty(Γ .B). So we can extend this tube to obtain (u,ω) = ext (ρ − i,w ) [J → m]∈ (ﬁb 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 ﬁber of w under t. i1 This concludes the deﬁnition of the ﬁlling operations of G t. To see that this ﬁlling operation is uniform, note that for an f : K → I deﬁned on j, J and on i the case which deﬁnes the ﬁlling of [J → w; ( j, a) → w ] f coincides with ja the case used to deﬁned [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 deﬁnition of the ﬁlling. If f is only deﬁned on j, J but not on i, 123 166 M. Bezem et al. the ﬁrst 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 reﬁne the Kan structure G κ κ ext given in Theorem 1 such that it A B satisﬁes (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 modiﬁed 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 deﬁne (G κ κ ext)(ρ, i ) [(i, 0) → u ]= (u , tρ u ). That this deﬁnition remains A B i0 i0 i0 uniform is proved as in Theorem 1 using the observation that |J|=|Jf | for f deﬁned on J . In addition we retain stability under substitution. Remark 1 It is also possible to change the Kan structure such that it satisﬁes −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 deﬁnition 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 deﬁnable using ext. Let us recall the deﬁnition 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 ﬁller function for open boxes in A over (J, f ). Of particular interest are the small set A(I, id ) and ﬁller 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 deﬁned 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 ﬁrst 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 reﬂexivity using our reﬁned 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 justiﬁes 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 deﬁne a factorization as α = p i with i : A → M and p : M → B. Furthermore, i will be a coﬁbration α α α α α α α 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 ﬁbration as formulated in Corollary 2)and p will be equipped with an acyclic-ﬁbration structure. This factorization corresponds to Garner’s factorization using the reﬁned small object argument [5] specialized to cubical sets. For ρ in Γ(I ) we will deﬁne 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 deﬁned on J . Note that restrictions do not increase the syntactic complexity of an element m ∈ M ρ. This deﬁnes 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 deﬁne this factorization is to ﬁrst inductively deﬁne 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 deﬁne 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 deﬁnition 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 speciﬁed 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 reﬂexivity paths is not necessarily the identity function. One could solve this problem if one could recognize the reﬂexivity paths, which is not possible in Path . Swan’s [7] solution to this problem is to deﬁne a type equivalent to Path in which one can recognize (representations of) reﬂexivity paths. This is the type M with α : A → Path α A mapping each a in A to its reﬂexivity path. The representation of the reﬂexivity path of a in M is i a, with i a constructor of the inductively deﬁned type M , and recognizing i a is α α done through pattern matching. All the rest of the complicated deﬁnition 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-ﬁbration α α structure which (uniformly) ﬁlls tubes [J → u] in M ρ over a ﬁlled cube v in Bρ. Thus to, say, construct a path between speciﬁed 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 coﬁbration followed by a ﬁbration (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 deﬁne 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 ﬁnd 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 deﬁne 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-ﬁbration structure as in Deﬁnition 2, that is, if we can ﬁll 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 coﬁbration. α α Corollary 1 Given D ∈ Ty(Γ .M ) equipped with an acyclic-ﬁbration structure and a sec- tion s ∈ Ter(Γ .A, Di ) it is possible to deﬁne 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 ﬁller. This also implies the following result, which expresses that i : A → M is a acyclic α α coﬁbration 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 sufﬁcient 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-ﬁbration 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 ﬁlling 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 deﬁne this line using a composition on the open box speciﬁed 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 ﬁller given by τ a @ k @ j (where k extends vertically), and thus also a ﬁller in M since p has an acyclic-ﬁbration 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 speciﬁed endpoints Path over a type A and α a is the constant path a. We get a factorization with Id := M , reﬂ := i , and where the right vertical map is given by taking endpoints: A α α 123 The Univalence Axiom in Cubical Sets 171 This α satisﬁes the hypothesis of Corollary 2 using the properties of path-types from [2, Section 8.2], and hence reﬂ : 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 ﬁxed 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 of Automated Reasoning – Springer Journals
Published: Jun 26, 2018
You can share this free article with as many people as you like with the url below! We hope you enjoy this feature!
Read and print from thousands of top scholarly journals.
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.
To save an article, log in first, or sign up for a DeepDyve account if you don’t already have one.
Copy and paste the desired citation format or use the link below to download a file formatted for EndNote
Access the full text.
Sign up today, get DeepDyve free for 14 days.
All DeepDyve websites use cookies to improve your online experience. They were placed on your computer when you launched this website. You can change your cookie settings through your browser.