*[HoTT] homotopy groups in CCHM cubical type theory@ 2018-07-13 20:12 Christian Sattler2018-07-14 19:46 ` Thierry Coquand 2018-07-20 22:29 ` Michael Shulman 0 siblings, 2 replies; 3+ messages in thread From: Christian Sattler @ 2018-07-13 20:12 UTC (permalink / raw) To: homotopytypetheory [-- Attachment #1: Type: text/plain, Size: 11068 bytes --] When computing homotopy groups of spheres in a version of cubical type theory, one might wonder whether this says anything about the corresponding homotopy groups of spheres in standard homotopy types; a priori, it might happen that we get different homotopy groups. Thierry Coquand has answered this question positively for CCHM [1] cubical type theory without reversals (from here on simply referred to as CCHM): given numbers n, k, a₁, …, aₜ, if we can derive ⊢ πₖ(Sⁿ) ≃ ℤ/(a₁) × … × ℤ/(aₜ) in CCHM, then we also have a corresponding external isomorphism πₖ(Sⁿ) ≃ ℤ/(a₁) × … × ℤ/(aₜ) for the standard k-th homotopy group of the n-sphere. This email serves to document his argument. Let □ denote the full subcategory of posets on objects [1]ᴵ for I a finite set (□ can also be described as the opposite of the Lawvere theory for distributive lattices). We wite cSet for the category of cubical sets, presheaves over □. The presheaf represented by [1]ᴵ will be written □ᴵ. Cubical sets form a model category where the cofibrations are the levelwise decidable monomorphisms and the fibrations are the maps admitting a uniform Kan filling operation in the sense of CCHM. We have a combinatorial description of homotopy groups πₖ(X, x₀) (as definable in any model category) of pointed fibrant objects (X, x₀) in cSet: the underlying set is the quotient of maps □ᵏ → X that are constantly x₀ on the boundary ∂□ᵏ by homotopy (relative to the boundary); the group structure is given by degeneracy and suitable Kan composition of cubes. Recall that CCHM has a model in cubical sets. We write ⟦-⟧ for the interpretation of types and terms and interpret types in the empty context as fibrant cubical sets. Given a pointed type (X, x₀) in the empty context, we can verify that the points of ⟦πₖ(X, x₀)⟧ are in bijection with πₖ(⟦X⟧, ⟦x₀⟧). A bit more (straightforward, though tedious) verification shows that the group operations of πₖ(X, x₀) defined internally in CCHM have as interpretations maps of presheaves whose actions on points correspond to the group operations of πₖ(⟦X⟧, ⟦x₀⟧). We can define ℤ/(a₁) × … × ℤ/(aₜ) in CCHM so that the interpretation of the type of group elements and the group operations is (up to isomorphism) constantly at every level the group ℤ/(a₁) × … × ℤ/(aₜ). Recall that Sⁿ in CCHM is defined as a higher inductive type generated by a base point b and an n-cube whose boundary is constantly b. This is interpreted as a fibrant replacement 1 +_{∂□ⁿ} □ⁿ → ⟦Sⁿ⟧ in cSet. Interpreting the derivation of ⊢ πₖ(Sⁿ) ≃ ℤ/(a₁) × … × ℤ/(aₜ) in cubical sets, we obtain an external group isomorphism πₖ(⟦Sⁿ⟧, ⟦b⟧) ≃ ℤ/(a₁) × … × ℤ/(aₜ). The type theoretic part of the argument is now finished. The rest of the argument relates homotopical aspects of cubical and simplicial sets. Let us briefly recall the relationship between these two settings. We assume classical logic from here on. Let Δ denote the simplex category, the full subcategory of posets on objects [n] for n ≥ 0. We write sSet for the category of simplicial sets, presheaves over Δ. The presheaf represented by [n] will be written Δⁿ. Recall the Kan model structure on sSet; it is the standard model for homotopy types. The cofibrations are the monomorphisms and the fibrations are Kan fibrations. Recall from Kapulkin and Voevodsky [2] that simplicial sets may be seen as a Grothendieck subtopos of cubical sets. We write C : sSet → cSet for this fully faithful functor; it can be defined as CA([1]ᴵ) = sSet((Δ¹)ᴵ, A). Its left adjoint S : cSet → sSet is the triangulation functor, the cocontinuous extension of □ → sSet sending [1]ᴵ to (Δ¹)ᴵ. We will also need that S has a further left adjoint L : sSet → cSet (see [2]), the cocontinuous extension of Δ → cSet sending the poset [n] to its cubical nerve, the cubical set that at level [1]ᴵ is Poset([1]ᴵ, [n]) (note that L and C agree on representables). This gives an adjoint triple L ⊣ S ⊣ C with L and C fully faithful. We include at the end of this text a few useful facts about the interaction of the functors L, S, C with the model structures on sSet and cSet that will be quoted in the following. Continuing with the main argument, recall that 1 +_{∂□ⁿ} □ⁿ → ⟦Sⁿ⟧ is a fibrant replacement in cSet. By (3.), S is both a left and a right Quillen functor, so we have that S(1 +_{∂□ⁿ} □ⁿ) → S(⟦Sⁿ⟧) is also a fibrant replacement in sSet. Note that S(1 +_{∂□ⁿ} □ⁿ) ≃ 1 +_{S(∂□ⁿ)} S(□ⁿ) (weakly equivalent to 1 +_{∂Δⁿ} Δⁿ) presents the n-sphere in simplicial sets. So S(⟦Sⁿ⟧) really is a fibrant model for the n-sphere in simplicial sets. Note that we have the same combinatorial description of homotopy groups for fibrant pointed objects (X, x₀) in simplicial sets as we did in cubical sets, with the underlying set of πₖ(X, x₀) given by the quotient of maps (Δ¹)ᵏ → X that are constantly x₀ on its boundary by homotopy and the group structure defined using degeneracy and the same Kan composition as for cubical sets. It remains to construct a group isomorphism πₖ(⟦Sⁿ⟧, ⟦b⟧) ≃ πₖ(S(⟦Sⁿ⟧), S(⟦b⟧)). We have a canonical function πₖ(⟦Sⁿ⟧, ⟦b⟧) → πₖ(S(⟦Sⁿ⟧), S(⟦b⟧)) given by the action of S on morphisms. This is a group homomorphism since S takes the combinatorial description of the homotopy groups in cubical sets to the one in simplicial sets. We are left to show that the function is a bijection. Surjectivity is given by (5.) with f' the constant map on ⟦b⟧. For injectivity, consider maps u, v : □ᵏ → ⟦Sⁿ⟧ constantly ⟦b⟧ on their boundary such that S(u) and S(v) are related by a homotopy H : Δ¹ × S□ᵏ → S(⟦Sⁿ⟧) that is constantly S(⟦b⟧) on S(∂□ᵏ). A lift of H to a homotopy between u and v (relative to their boundary) is then given by (5.) with f' given by u and v on two opposing sides and constantly ⟦b⟧ elsewhere and g given by H. Remarks: - Recall that there is more structure in a standard homotopy type than just its list of homotopy groups. It seems the above argument also applies to operations involving multiple groups simultaneously, for example the action of π₁ on πₙ, as long as we can combinatorially describe these operations using cubical filling in the same manner in both cubical and simplicial sets. - The argument generalized from spheres to other finite cubical cell complexes. Appendix. (1.) L preserves cofibrations and weak equivalences. Using cocontinuity of L, one sees that L(∂Δⁿ) is the subobject of L(Δⁿ) that at level [1]ᴵ contains the non-surjective poset maps [1]ᴵ → [n]. By cocontinuity, since L sends boundary inclusions to cofibrations, it preserves cofibrations. For preservation of weak equivalences, by Ken Brown's lemma and cocontinuity, it will suffice to show that L sends horn inclusions to weak equivalences. Using cocontinuity and 2-out-of-3, this can be further reduced in the standard way to showing that L sends representables to weakly contractible objects. Recall that L[n] is the cubical nerve of the poset [n]. Note that [n] has an initial object, hence is homotopy equivalent to 1. Applying the cubical nerve, we get a homotopy equivalence between L[n] and 1. (2.) S preserves cofibrations and weak equivalences. As a right adjoint, S preserves monomorphisms (i.e. cofibrations). It also preserves products and pushouts and sends the interval in sSet to the interval in cSet. Thus, it sends prism-style generating trivial cofibrations in sSet to trivial cofibrations in cSet. By cocontinuity, it preserves all trivial cofibrations. By Ken Brown's lemma, it preserves weak equivalences. So we obtain: (3.) both adjunctions L ⊣ S ⊣ C are Quillen adjunctions. In particular, S preserves all three classes of the model structure. (4.) The pushout application (Leibniz application) of the counit ε : LS → Id to the boundary inclusion ∂□ᴵ → □ᴵ is a weak equivalence. We generalize the claim to any face lattice subobject M → □ᴵ. Using cocontinuity of LS and closure properties of weak equivalences and trivial cofibrations, if the claim holds for two such subobjects M₁ and M₂ as well as their intersection, then also for their union. Thus, it remains to prove the claim for face map inclusions □ᴶ → □ᴵ and the empty subobject 0 → □ᴵ. Using cocontinuity and closure properties once more, this reduces to the claim just for 0 → □ᴵ. So we need to prove that ε_{□ᴷ} : LS□ᵏ → □ᵏ is a weak equivalence, i.e. that LS□ᴷ is weakly contractible. This can be seen via an explicit contracting homotopy based on the initial vertex. Alternatively, we may proceed as before and generalize the claim to LN where N is a union of injections Δᵐ → (Δ¹)ᴷ that preserve the initial and terminal vertex. Using cocontinuity of L and closure properties of weak equivalences and trivial cofibrations, the claim reduces to the case of LΔᵐ, which we already know from (1.). Note that the lack of a Reedy category structure on □ prevents us from using the preceding statement to show that ε is generally valued in weak equivalences. Note also that those cubical sets local (in the 1-categorical sense) with respect to ε_{□ᴵ} for all I are exactly the sheaves of Kapulkin and Voevodsky [2], i.e. the cubical sets coming from a simplicial set under application of C. (5.) Let X ∈ cSet be fibrant; given f' : ∂□ᴵ → X and g : (Δ¹)ᴵ → SX such that S(f') is g restricted to its boundary, there is f : □ᴵ → X extending f' such that S(f) = g. Taking the transpose of g, we obtain h : LS□ᴵ → X such that its restriction to LS(∂□ᴵ) agrees with f' restricted along ε_{□ᴵ}. We then construct f by lifting [h, f'] through LS□ᵏ +_{LS(∂□ᵏ)} ∂□ᵏ → □ᵏ, the pushout application of the counit ε : LS → Id to ∂□ᵏ → □ᵏ, which is a trivial cofibration by (4.). References. [1] Cohen, Coquand, Huber, Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom. https://arxiv.org/pdf/1611.02108 [2] Kapulkin, Voevodsky. Cubical approach to straightening. http://uwo.ca/math/faculty/kapulkin/papers/cubical-approach-to-straightening.pdf [3] https://arxiv.org/pdf/1805.04126 -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 11885 bytes --] ^ permalink raw reply [flat|nested] 3+ messages in thread

*Re: [HoTT] homotopy groups in CCHM cubical type theory2018-07-13 20:12 [HoTT] homotopy groups in CCHM cubical type theory Christian Sattler@ 2018-07-14 19:46 ` Thierry Coquand2018-07-20 22:29 ` Michael Shulman 1 sibling, 0 replies; 3+ messages in thread From: Thierry Coquand @ 2018-07-14 19:46 UTC (permalink / raw) To: Homotopy Theory [-- Attachment #1: Type: text/plain, Size: 13686 bytes --] Some further remarks on this message: -the reference [3] should be https://arxiv.org/abs/1805.04126 -we consider Dedekind cubical sets where cofibrations are decidable sieves -in the paper http://uwo.ca/math/faculty/kapulkin/papers/cubical-approach-to-straightening.pdf one result is that we can see simplicial sets exactly as special kind of cubical sets that are sheaves forcing the following 1 = x <= y \/ y <= x The original idea for connecting homotopy groups was to refine the notion of fibrant cubical sets by forcing \phi = x <= y \/ y <= x (1) to be a trivial cofibration. This amounts to consider the model where we look only at modal types for the modality X |-> X ^{[\phi]} More generally we can force to be a trivial cofibration also any sieve which becomes 1 by triangulation in the simplicial set model. (This should be a special case of Bousfield localisation, but all the arguments are effective.) In this way we can prove that homotopy groups coincide in the simplicial and cubical worlds. For instance, for pi_2 we use that x <= y <= z \/ y <= x <= z \/ x <= z <= y \/ z <= x <= y \/ y <=z <= x \/ z <= y <= x \/ x = 0 \/ x = 1 \/ y = 0 \/ y = 1 \/ z = 0 \/ z = 1 (2) becomes a trivial cofibration. Christian noticed that (1) or (2) are already a trivial cofibration in the original cubical set model. (For (1), this is because the map [\phi] -> 1 is an equivalence and by 3-out-of-2 the inclusion [\phi] in the square has to be an equivalence, hence it is a trivial cofibration.) More generally, all the maps that were needed to be trivial cofibration for the argument relating homotopy groups can already be shown to be trivial cofibration. So localisation is not needed for this argument. -it also follows from http://uwo.ca/math/faculty/kapulkin/papers/cubical-approach-to-straightening.pdf that C preserves fibrancy. Using the results in https://arxiv.org/abs/1805.04126 Christian could show that the triangulation functor S preserves fibrancy (the argument uses classical logic) which was needed to show that S commutes with fibrant replacement. Thierry On 13 Jul 2018, at 22:12, Christian Sattler <sattler.christian@gmail.com<mailto:sattler.christian@gmail.com>> wrote: When computing homotopy groups of spheres in a version of cubical type theory, one might wonder whether this says anything about the corresponding homotopy groups of spheres in standard homotopy types; a priori, it might happen that we get different homotopy groups. Thierry Coquand has answered this question positively for CCHM [1] cubical type theory without reversals (from here on simply referred to as CCHM): given numbers n, k, a₁, …, aₜ, if we can derive ⊢ πₖ(Sⁿ) ≃ ℤ/(a₁) × … × ℤ/(aₜ) in CCHM, then we also have a corresponding external isomorphism πₖ(Sⁿ) ≃ ℤ/(a₁) × … × ℤ/(aₜ) for the standard k-th homotopy group of the n-sphere. This email serves to document his argument. Let □ denote the full subcategory of posets on objects [1]ᴵ for I a finite set (□ can also be described as the opposite of the Lawvere theory for distributive lattices). We wite cSet for the category of cubical sets, presheaves over □. The presheaf represented by [1]ᴵ will be written □ᴵ. Cubical sets form a model category where the cofibrations are the levelwise decidable monomorphisms and the fibrations are the maps admitting a uniform Kan filling operation in the sense of CCHM. We have a combinatorial description of homotopy groups πₖ(X, x₀) (as definable in any model category) of pointed fibrant objects (X, x₀) in cSet: the underlying set is the quotient of maps □ᵏ → X that are constantly x₀ on the boundary ∂□ᵏ by homotopy (relative to the boundary); the group structure is given by degeneracy and suitable Kan composition of cubes. Recall that CCHM has a model in cubical sets. We write ⟦-⟧ for the interpretation of types and terms and interpret types in the empty context as fibrant cubical sets. Given a pointed type (X, x₀) in the empty context, we can verify that the points of ⟦πₖ(X, x₀)⟧ are in bijection with πₖ(⟦X⟧, ⟦x₀⟧). A bit more (straightforward, though tedious) verification shows that the group operations of πₖ(X, x₀) defined internally in CCHM have as interpretations maps of presheaves whose actions on points correspond to the group operations of πₖ(⟦X⟧, ⟦x₀⟧). We can define ℤ/(a₁) × … × ℤ/(aₜ) in CCHM so that the interpretation of the type of group elements and the group operations is (up to isomorphism) constantly at every level the group ℤ/(a₁) × … × ℤ/(aₜ). Recall that Sⁿ in CCHM is defined as a higher inductive type generated by a base point b and an n-cube whose boundary is constantly b. This is interpreted as a fibrant replacement 1 +_{∂□ⁿ} □ⁿ → ⟦Sⁿ⟧ in cSet. Interpreting the derivation of ⊢ πₖ(Sⁿ) ≃ ℤ/(a₁) × … × ℤ/(aₜ) in cubical sets, we obtain an external group isomorphism πₖ(⟦Sⁿ⟧, ⟦b⟧) ≃ ℤ/(a₁) × … × ℤ/(aₜ). The type theoretic part of the argument is now finished. The rest of the argument relates homotopical aspects of cubical and simplicial sets. Let us briefly recall the relationship between these two settings. We assume classical logic from here on. Let Δ denote the simplex category, the full subcategory of posets on objects [n] for n ≥ 0. We write sSet for the category of simplicial sets, presheaves over Δ. The presheaf represented by [n] will be written Δⁿ. Recall the Kan model structure on sSet; it is the standard model for homotopy types. The cofibrations are the monomorphisms and the fibrations are Kan fibrations. Recall from Kapulkin and Voevodsky [2] that simplicial sets may be seen as a Grothendieck subtopos of cubical sets. We write C : sSet → cSet for this fully faithful functor; it can be defined as CA([1]ᴵ) = sSet((Δ¹)ᴵ, A). Its left adjoint S : cSet → sSet is the triangulation functor, the cocontinuous extension of □ → sSet sending [1]ᴵ to (Δ¹)ᴵ. We will also need that S has a further left adjoint L : sSet → cSet (see [2]), the cocontinuous extension of Δ → cSet sending the poset [n] to its cubical nerve, the cubical set that at level [1]ᴵ is Poset([1]ᴵ, [n]) (note that L and C agree on representables). This gives an adjoint triple L ⊣ S ⊣ C with L and C fully faithful. We include at the end of this text a few useful facts about the interaction of the functors L, S, C with the model structures on sSet and cSet that will be quoted in the following. Continuing with the main argument, recall that 1 +_{∂□ⁿ} □ⁿ → ⟦Sⁿ⟧ is a fibrant replacement in cSet. By (3.), S is both a left and a right Quillen functor, so we have that S(1 +_{∂□ⁿ} □ⁿ) → S(⟦Sⁿ⟧) is also a fibrant replacement in sSet. Note that S(1 +_{∂□ⁿ} □ⁿ) ≃ 1 +_{S(∂□ⁿ)} S(□ⁿ) (weakly equivalent to 1 +_{∂Δⁿ} Δⁿ) presents the n-sphere in simplicial sets. So S(⟦Sⁿ⟧) really is a fibrant model for the n-sphere in simplicial sets. Note that we have the same combinatorial description of homotopy groups for fibrant pointed objects (X, x₀) in simplicial sets as we did in cubical sets, with the underlying set of πₖ(X, x₀) given by the quotient of maps (Δ¹)ᵏ → X that are constantly x₀ on its boundary by homotopy and the group structure defined using degeneracy and the same Kan composition as for cubical sets. It remains to construct a group isomorphism πₖ(⟦Sⁿ⟧, ⟦b⟧) ≃ πₖ(S(⟦Sⁿ⟧), S(⟦b⟧)). We have a canonical function πₖ(⟦Sⁿ⟧, ⟦b⟧) → πₖ(S(⟦Sⁿ⟧), S(⟦b⟧)) given by the action of S on morphisms. This is a group homomorphism since S takes the combinatorial description of the homotopy groups in cubical sets to the one in simplicial sets. We are left to show that the function is a bijection. Surjectivity is given by (5.) with f' the constant map on ⟦b⟧. For injectivity, consider maps u, v : □ᵏ → ⟦Sⁿ⟧ constantly ⟦b⟧ on their boundary such that S(u) and S(v) are related by a homotopy H : Δ¹ × S□ᵏ → S(⟦Sⁿ⟧) that is constantly S(⟦b⟧) on S(∂□ᵏ). A lift of H to a homotopy between u and v (relative to their boundary) is then given by (5.) with f' given by u and v on two opposing sides and constantly ⟦b⟧ elsewhere and g given by H. Remarks: - Recall that there is more structure in a standard homotopy type than just its list of homotopy groups. It seems the above argument also applies to operations involving multiple groups simultaneously, for example the action of π₁ on πₙ, as long as we can combinatorially describe these operations using cubical filling in the same manner in both cubical and simplicial sets. - The argument generalized from spheres to other finite cubical cell complexes. Appendix. (1.) L preserves cofibrations and weak equivalences. Using cocontinuity of L, one sees that L(∂Δⁿ) is the subobject of L(Δⁿ) that at level [1]ᴵ contains the non-surjective poset maps [1]ᴵ → [n]. By cocontinuity, since L sends boundary inclusions to cofibrations, it preserves cofibrations. For preservation of weak equivalences, by Ken Brown's lemma and cocontinuity, it will suffice to show that L sends horn inclusions to weak equivalences. Using cocontinuity and 2-out-of-3, this can be further reduced in the standard way to showing that L sends representables to weakly contractible objects. Recall that L[n] is the cubical nerve of the poset [n]. Note that [n] has an initial object, hence is homotopy equivalent to 1. Applying the cubical nerve, we get a homotopy equivalence between L[n] and 1. (2.) S preserves cofibrations and weak equivalences. As a right adjoint, S preserves monomorphisms (i.e. cofibrations). It also preserves products and pushouts and sends the interval in sSet to the interval in cSet. Thus, it sends prism-style generating trivial cofibrations in sSet to trivial cofibrations in cSet. By cocontinuity, it preserves all trivial cofibrations. By Ken Brown's lemma, it preserves weak equivalences. So we obtain: (3.) both adjunctions L ⊣ S ⊣ C are Quillen adjunctions. In particular, S preserves all three classes of the model structure. (4.) The pushout application (Leibniz application) of the counit ε : LS → Id to the boundary inclusion ∂□ᴵ → □ᴵ is a weak equivalence. We generalize the claim to any face lattice subobject M → □ᴵ. Using cocontinuity of LS and closure properties of weak equivalences and trivial cofibrations, if the claim holds for two such subobjects M₁ and M₂ as well as their intersection, then also for their union. Thus, it remains to prove the claim for face map inclusions □ᴶ → □ᴵ and the empty subobject 0 → □ᴵ. Using cocontinuity and closure properties once more, this reduces to the claim just for 0 → □ᴵ. So we need to prove that ε_{□ᴷ} : LS□ᵏ → □ᵏ is a weak equivalence, i.e. that LS□ᴷ is weakly contractible. This can be seen via an explicit contracting homotopy based on the initial vertex. Alternatively, we may proceed as before and generalize the claim to LN where N is a union of injections Δᵐ → (Δ¹)ᴷ that preserve the initial and terminal vertex. Using cocontinuity of L and closure properties of weak equivalences and trivial cofibrations, the claim reduces to the case of LΔᵐ, which we already know from (1.). Note that the lack of a Reedy category structure on □ prevents us from using the preceding statement to show that ε is generally valued in weak equivalences. Note also that those cubical sets local (in the 1-categorical sense) with respect to ε_{□ᴵ} for all I are exactly the sheaves of Kapulkin and Voevodsky [2], i.e. the cubical sets coming from a simplicial set under application of C. (5.) Let X ∈ cSet be fibrant; given f' : ∂□ᴵ → X and g : (Δ¹)ᴵ → SX such that S(f') is g restricted to its boundary, there is f : □ᴵ → X extending f' such that S(f) = g. Taking the transpose of g, we obtain h : LS□ᴵ → X such that its restriction to LS(∂□ᴵ) agrees with f' restricted along ε_{□ᴵ}. We then construct f by lifting [h, f'] through LS□ᵏ +_{LS(∂□ᵏ)} ∂□ᵏ → □ᵏ, the pushout application of the counit ε : LS → Id to ∂□ᵏ → □ᵏ, which is a trivial cofibration by (4.). References. [1] Cohen, Coquand, Huber, Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom. https://arxiv.org/pdf/1611.02108 [2] Kapulkin, Voevodsky. Cubical approach to straightening. http://uwo.ca/math/faculty/kapulkin/papers/cubical-approach-to-straightening.pdf [3] http://uwo.ca/math/faculty/kapulkin/papers/cubical-approach-to-straightening.pdf -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 18546 bytes --] ^ permalink raw reply [flat|nested] 3+ messages in thread

*2018-07-13 20:12 [HoTT] homotopy groups in CCHM cubical type theory Christian Sattler 2018-07-14 19:46 ` Thierry CoquandRe: [HoTT] homotopy groups in CCHM cubical type theory@ 2018-07-20 22:29 ` Michael Shulman1 sibling, 0 replies; 3+ messages in thread From: Michael Shulman @ 2018-07-20 22:29 UTC (permalink / raw) To: Christian Sattler;+Cc:homotopytypetheory It seems to me like this fact should follow from an abstract oo-categorical argument. In a previous thread, we concluded that a (different) category of cubical sets presented a Grothendieck oo-topos (since it is locally presentable, locally cartesian closed, and has van Kampen pushouts), and that the singular-realization adjunction defined a point of this oo-topos (a geometric morphism from ooGpd). But all the constructions that go into defining spheres (terminal object, homotopy pushouts) or more general finite cell complexes, homotopy groups (loop spaces, being certain pullbacks, and truncations), and concrete finitely presented abelian groups (integers, set-quotients, products) are preserved by inverse image functors of oo-geometric morphisms. So if some homotopy group of a finite cell complex is isomorphic to some concrete finitely presented abelian group in any Grothendieck oo-topos that has a point, this isomorphism should be preserved by the inverse image functor of the point and yield a similar isomorphism in ooGpd. (This is essentially the same as the argument that the homotopy groups of finite cell complexes are the same in all Grothendieck oo-toposes, turned around.) Do CCHM cubical sets also present a Grothendieck oo-topos with a point? Which kinds of cubical sets do (or don't)? Are any of them equivalent to ooGpd? On Fri, Jul 13, 2018 at 1:12 PM, Christian Sattler <sattler.christian@gmail.com> wrote: > When computing homotopy groups of spheres in a version of cubical type > theory, one might wonder whether this says anything about the corresponding > homotopy groups of spheres in standard homotopy types; a priori, it might > happen that we get different homotopy groups. Thierry Coquand has answered > this question positively for CCHM [1] cubical type theory without reversals > (from here on simply referred to as CCHM): given numbers n, k, a₁, …, aₜ, if > we can derive ⊢ πₖ(Sⁿ) ≃ ℤ/(a₁) × … × ℤ/(aₜ) in CCHM, then we also have a > corresponding external isomorphism πₖ(Sⁿ) ≃ ℤ/(a₁) × … × ℤ/(aₜ) for the > standard k-th homotopy group of the n-sphere. This email serves to document > his argument. > > Let □ denote the full subcategory of posets on objects [1]ᴵ for I a finite > set (□ can also be described as the opposite of the Lawvere theory for > distributive lattices). We wite cSet for the category of cubical sets, > presheaves over □. The presheaf represented by [1]ᴵ will be written □ᴵ. > Cubical sets form a model category where the cofibrations are the levelwise > decidable monomorphisms and the fibrations are the maps admitting a uniform > Kan filling operation in the sense of CCHM. We have a combinatorial > description of homotopy groups πₖ(X, x₀) (as definable in any model > category) of pointed fibrant objects (X, x₀) in cSet: the underlying set is > the quotient of maps □ᵏ → X that are constantly x₀ on the boundary ∂□ᵏ by > homotopy (relative to the boundary); the group structure is given by > degeneracy and suitable Kan composition of cubes. > > Recall that CCHM has a model in cubical sets. We write ⟦-⟧ for the > interpretation of types and terms and interpret types in the empty context > as fibrant cubical sets. Given a pointed type (X, x₀) in the empty context, > we can verify that the points of ⟦πₖ(X, x₀)⟧ are in bijection with πₖ(⟦X⟧, > ⟦x₀⟧). A bit more (straightforward, though tedious) verification shows that > the group operations of πₖ(X, x₀) defined internally in CCHM have as > interpretations maps of presheaves whose actions on points correspond to the > group operations of πₖ(⟦X⟧, ⟦x₀⟧). We can define ℤ/(a₁) × … × ℤ/(aₜ) in CCHM > so that the interpretation of the type of group elements and the group > operations is (up to isomorphism) constantly at every level the group ℤ/(a₁) > × … × ℤ/(aₜ). Recall that Sⁿ in CCHM is defined as a higher inductive type > generated by a base point b and an n-cube whose boundary is constantly b. > This is interpreted as a fibrant replacement 1 +_{∂□ⁿ} □ⁿ → ⟦Sⁿ⟧ in cSet. > Interpreting the derivation of ⊢ πₖ(Sⁿ) ≃ ℤ/(a₁) × … × ℤ/(aₜ) in cubical > sets, we obtain an external group isomorphism πₖ(⟦Sⁿ⟧, ⟦b⟧) ≃ ℤ/(a₁) × … × > ℤ/(aₜ). > > The type theoretic part of the argument is now finished. The rest of the > argument relates homotopical aspects of cubical and simplicial sets. Let us > briefly recall the relationship between these two settings. We assume > classical logic from here on. > > Let Δ denote the simplex category, the full subcategory of posets on objects > [n] for n ≥ 0. We write sSet for the category of simplicial sets, presheaves > over Δ. The presheaf represented by [n] will be written Δⁿ. Recall the Kan > model structure on sSet; it is the standard model for homotopy types. The > cofibrations are the monomorphisms and the fibrations are Kan fibrations. > > Recall from Kapulkin and Voevodsky [2] that simplicial sets may be seen as a > Grothendieck subtopos of cubical sets. We write C : sSet → cSet for this > fully faithful functor; it can be defined as CA([1]ᴵ) = sSet((Δ¹)ᴵ, A). Its > left adjoint S : cSet → sSet is the triangulation functor, the cocontinuous > extension of □ → sSet sending [1]ᴵ to (Δ¹)ᴵ. We will also need that S has a > further left adjoint L : sSet → cSet (see [2]), the cocontinuous extension > of Δ → cSet sending the poset [n] to its cubical nerve, the cubical set that > at level [1]ᴵ is Poset([1]ᴵ, [n]) (note that L and C agree on > representables). This gives an adjoint triple L ⊣ S ⊣ C with L and C fully > faithful. We include at the end of this text a few useful facts about the > interaction of the functors L, S, C with the model structures on sSet and > cSet that will be quoted in the following. > > Continuing with the main argument, recall that 1 +_{∂□ⁿ} □ⁿ → ⟦Sⁿ⟧ is a > fibrant replacement in cSet. By (3.), S is both a left and a right Quillen > functor, so we have that S(1 +_{∂□ⁿ} □ⁿ) → S(⟦Sⁿ⟧) is also a fibrant > replacement in sSet. Note that S(1 +_{∂□ⁿ} □ⁿ) ≃ 1 +_{S(∂□ⁿ)} S(□ⁿ) (weakly > equivalent to 1 +_{∂Δⁿ} Δⁿ) presents the n-sphere in simplicial sets. So > S(⟦Sⁿ⟧) really is a fibrant model for the n-sphere in simplicial sets. Note > that we have the same combinatorial description of homotopy groups for > fibrant pointed objects (X, x₀) in simplicial sets as we did in cubical > sets, with the underlying set of πₖ(X, x₀) given by the quotient of maps > (Δ¹)ᵏ → X that are constantly x₀ on its boundary by homotopy and the group > structure defined using degeneracy and the same Kan composition as for > cubical sets. > > It remains to construct a group isomorphism πₖ(⟦Sⁿ⟧, ⟦b⟧) ≃ πₖ(S(⟦Sⁿ⟧), > S(⟦b⟧)). We have a canonical function πₖ(⟦Sⁿ⟧, ⟦b⟧) → πₖ(S(⟦Sⁿ⟧), S(⟦b⟧)) > given by the action of S on morphisms. This is a group homomorphism since S > takes the combinatorial description of the homotopy groups in cubical sets > to the one in simplicial sets. We are left to show that the function is a > bijection. Surjectivity is given by (5.) with f' the constant map on ⟦b⟧. > For injectivity, consider maps u, v : □ᵏ → ⟦Sⁿ⟧ constantly ⟦b⟧ on their > boundary such that S(u) and S(v) are related by a homotopy H : Δ¹ × S□ᵏ → > S(⟦Sⁿ⟧) that is constantly S(⟦b⟧) on S(∂□ᵏ). A lift of H to a homotopy > between u and v (relative to their boundary) is then given by (5.) with f' > given by u and v on two opposing sides and constantly ⟦b⟧ elsewhere and g > given by H. > > Remarks: > - Recall that there is more structure in a standard homotopy type than just > its list of homotopy groups. It seems the above argument also applies to > operations involving multiple groups simultaneously, for example the action > of π₁ on πₙ, as long as we can combinatorially describe these operations > using cubical filling in the same manner in both cubical and simplicial > sets. > - The argument generalized from spheres to other finite cubical cell > complexes. > > Appendix. > > (1.) L preserves cofibrations and weak equivalences. > Using cocontinuity of L, one sees that L(∂Δⁿ) is the subobject of L(Δⁿ) that > at level [1]ᴵ contains the non-surjective poset maps [1]ᴵ → [n]. By > cocontinuity, since L sends boundary inclusions to cofibrations, it > preserves cofibrations. For preservation of weak equivalences, by Ken > Brown's lemma and cocontinuity, it will suffice to show that L sends horn > inclusions to weak equivalences. Using cocontinuity and 2-out-of-3, this can > be further reduced in the standard way to showing that L sends > representables to weakly contractible objects. Recall that L[n] is the > cubical nerve of the poset [n]. Note that [n] has an initial object, hence > is homotopy equivalent to 1. Applying the cubical nerve, we get a homotopy > equivalence between L[n] and 1. > > (2.) S preserves cofibrations and weak equivalences. > As a right adjoint, S preserves monomorphisms (i.e. cofibrations). It also > preserves products and pushouts and sends the interval in sSet to the > interval in cSet. Thus, it sends prism-style generating trivial cofibrations > in sSet to trivial cofibrations in cSet. By cocontinuity, it preserves all > trivial cofibrations. By Ken Brown's lemma, it preserves weak equivalences. > > So we obtain: > (3.) both adjunctions L ⊣ S ⊣ C are Quillen adjunctions. > > In particular, S preserves all three classes of the model structure. > > (4.) The pushout application (Leibniz application) of the counit ε : LS → Id > to the boundary inclusion ∂□ᴵ → □ᴵ is a weak equivalence. > We generalize the claim to any face lattice subobject M → □ᴵ. Using > cocontinuity of LS and closure properties of weak equivalences and trivial > cofibrations, if the claim holds for two such subobjects M₁ and M₂ as well > as their intersection, then also for their union. Thus, it remains to prove > the claim for face map inclusions □ᴶ → □ᴵ and the empty subobject 0 → □ᴵ. > Using cocontinuity and closure properties once more, this reduces to the > claim just for 0 → □ᴵ. So we need to prove that ε_{□ᴷ} : LS□ᵏ → □ᵏ is a weak > equivalence, i.e. that LS□ᴷ is weakly contractible. This can be seen via an > explicit contracting homotopy based on the initial vertex. Alternatively, we > may proceed as before and generalize the claim to LN where N is a union of > injections Δᵐ → (Δ¹)ᴷ that preserve the initial and terminal vertex. Using > cocontinuity of L and closure properties of weak equivalences and trivial > cofibrations, the claim reduces to the case of LΔᵐ, which we already know > from (1.). > > Note that the lack of a Reedy category structure on □ prevents us from using > the preceding statement to show that ε is generally valued in weak > equivalences. > > Note also that those cubical sets local (in the 1-categorical sense) with > respect to ε_{□ᴵ} for all I are exactly the sheaves of Kapulkin and > Voevodsky [2], i.e. the cubical sets coming from a simplicial set under > application of C. > > (5.) Let X ∈ cSet be fibrant; given f' : ∂□ᴵ → X and g : (Δ¹)ᴵ → SX such > that S(f') is g restricted to its boundary, there is f : □ᴵ → X extending f' > such that S(f) = g. > Taking the transpose of g, we obtain h : LS□ᴵ → X such that its restriction > to LS(∂□ᴵ) agrees with f' restricted along ε_{□ᴵ}. We then construct f by > lifting [h, f'] through LS□ᵏ +_{LS(∂□ᵏ)} ∂□ᵏ → □ᵏ, the pushout application > of the counit ε : LS → Id to ∂□ᵏ → □ᵏ, which is a trivial cofibration by > (4.). > > References. > > [1] Cohen, Coquand, Huber, Mörtberg. Cubical Type Theory: a constructive > interpretation of the univalence axiom. https://arxiv.org/pdf/1611.02108 > [2] Kapulkin, Voevodsky. Cubical approach to straightening. > http://uwo.ca/math/faculty/kapulkin/papers/cubical-approach-to-straightening.pdf > [3] https://arxiv.org/pdf/1805.04126 > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 3+ messages in thread

end of thread, other threads:[~2018-07-20 22:29 UTC | newest]Thread overview:3+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-07-13 20:12 [HoTT] homotopy groups in CCHM cubical type theory Christian Sattler 2018-07-14 19:46 ` Thierry Coquand 2018-07-20 22:29 ` Michael Shulman

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).