[HoTT] homotopy groups in CCHM cubical type theory

[Christian Sattler <sattler.christian@gmail.com>]

[-- 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 --]