Re: [HoTT] homotopy groups in CCHM cubical type theory

[Michael Shulman <shulman@sandiego.edu>]

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.