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 > 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. 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.