[HoTT] homotopy groups in CCHM cubical type theory

[HoTT] homotopy groups in CCHM cubical type theory

[Christian Sattler]

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

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

[Thierry Coquand]

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

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

[Michael Shulman]

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.