2-truncated quasicategories

Stream: Infinity-Cosmos

[Julian Komaromy]

I have opened a PR (https://github.com/emilyriehl/infinity-cosmos/pull/120) for implementing 2-truncated quasicategories.

There is certainly some things to be tidied up, but I would love to hear some feedback, for example regarding the definition of Quasicategory₂ which is the structure modelling definition 1.3.1 in the blueprint.

[Emily Riehl]

Great. I'll have a look right now. Tagging @Joël Riou and @Nick Ward and @Kunhong Du who might be interested as well.

[Emily Riehl]

Does anyone have opinions on how the simplices (and other data) should be linearly ordered here?

structure horn_data {X : Truncated 2} (f : X.Path 3) where
  σ₃ : X _⦋2⦌₂
  σ₀ : X _⦋2⦌₂
  σ₂ : X _⦋2⦌₂
  h₃ : spine X 2 _ σ₃ = f.interval 0 2
  h₀ : spine X 2 _ σ₀ = f.interval 1 2
  h₂₂ : X.map (tr (δ 2)).op σ₂ = f.arrow 0
  h₂₀ : X.map (tr (δ 0)).op σ₂ = X.map (tr (δ 1)).op σ₀

I totally get the logic behind this ordering but wonder in the future if we'd prefer something monotone (either increasing or decreasing) in the subscript index.

[Emily Riehl]

I'll bring a few more points here for ease of discussion. My instinct is that perhaps this structure should be made more algebraic by using a sigma type rather than an existential quantifier as the codomain of the filling operations. Or are these the same thing in Lean?

/--
A 2-truncated quasicategory is a 2-truncated simplicial set with 3 properties:
  (2, 1)-filling
  (3, 1)-filling
  (3, 2)-filling
See `fill31.horn_data` and `fill31.filling_simplex` for the details of (3, 1)-filling,
and `fill32.horn_data` and `fill32.filling_simplex` for the details of (3, 2)-filling.
-/
structure Quasicategory₂ (X : Truncated 2) where
  fill21 (f : Path X 2) : ∃ (σ : X _⦋2⦌₂), spine X 2 _ σ = f
  fill31 {f : Path X 3} (a : fill31.horn_data f) : ∃ σ₁ : X _⦋2⦌₂, fill31.filling_simplex a σ₁
  fill32 {f : Path X 3} (a : fill32.horn_data f) : ∃ σ₁ : X _⦋2⦌₂, fill32.filling_simplex a σ₁

I wonder also whether it would be nice to make the filling_simplex structure type valued rather than prop valued and include the simplex as its first field?

[Joël Riou]

This numbering of simplices is consistent with what I have used when working with the fundamental groupoid of a Kan complex.

[Julian Komaromy]

Emily Riehl said:

I'll bring a few more points here for ease of discussion. My instinct is that perhaps this structure should be made more algebraic by using a sigma type rather than an existential quantifier as the codomain of the filling operations. Or are these the same thing in Lean?

/--
A 2-truncated quasicategory is a 2-truncated simplicial set with 3 properties:
  (2, 1)-filling
  (3, 1)-filling
  (3, 2)-filling
See `fill31.horn_data` and `fill31.filling_simplex` for the details of (3, 1)-filling,
and `fill32.horn_data` and `fill32.filling_simplex` for the details of (3, 2)-filling.
-/
structure Quasicategory₂ (X : Truncated 2) where
  fill21 (f : Path X 2) : ∃ (σ : X _⦋2⦌₂), spine X 2 _ σ = f
  fill31 {f : Path X 3} (a : fill31.horn_data f) : ∃ σ₁ : X _⦋2⦌₂, fill31.filling_simplex a σ₁
  fill32 {f : Path X 3} (a : fill32.horn_data f) : ∃ σ₁ : X _⦋2⦌₂, fill32.filling_simplex a σ₁

I wonder also whether it would be nice to make the filling_simplex structure type valued rather than prop valued and include the simplex as its first field?

Re this: I wanted to do it this way, but I chose to make it Prop valued to align with the definition of a Quasicategory, which is an existential statement.

[Emily Riehl]

We should wait for @Joël Riou and @Johan Commelin to weigh in on this point.

Overall the draft PR is great. It's cool to see the horn API used relatively seamlessly. Do you have any pain points that would be useful for the group to think about?

Btw I left you a bunch of mathlib style comments (and once you integrate these I'll share a few more).

[Joël Riou]

About the design, I would suggest taking inspiration from https://github.com/joelriou/topcat-model-category/blob/6961e86c2cefabca4a1cedd729174c3e4a020fb5/TopCatModelCategory/SSet/FundamentalGroupoid.lean#L313-L317 which is a structure CompStruct expressing that three "edges" (1-simplices which connect specific vertices) are the faces of a certain 2-simplex. This structure is very essential in my formalization of the fundamental groupoid of a Kan complex. Indeed, the equivalence relation on edges can be expressed using CompStruct (in two a priori different ways), and the associativity of the composition of homotopy classes follows from https://github.com/joelriou/topcat-model-category/blob/6961e86c2cefabca4a1cedd729174c3e4a020fb5/TopCatModelCategory/SSet/FundamentalGroupoid.lean#L388-L393 It seems to me that the statement of this assoc definition is a convenient phrasing of the (3, 1)-filling that is expected for 2-truncated quasicategories, and the proof is the fact that a quasicategory induces a 2-truncated quasicategory. Similarly, assoc' should be the (3,2)-filling. (In the definition of 2-truncated quasicategories, I think it should be a Prop, and the API should provide a def which chooses a filling.)

[Joël Riou]

It would be nice to define also a "2-truncated Kan complex" (I do not know if this is standard terminology) by extending the 2-truncated quasicategory class and adding the horn filling property for the 1-dimensional outer horns in Δ[2], so that we could define the homotopy category of a 2-truncated quasi-category X, show that it is a groupoid when it is a 2-truncated Kan complex. Then, define the fundamental groupoid of a Kan complex as the homotopy category of its 2-truncation. Following this approach would just mean refactoring the content of the file https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/FundamentalGroupoid.lean which already contains all the necessary material.

[Julian Komaromy]

Joël Riou said:

It seems to me that the statement of this assoc definition is a convenient phrasing of the (3, 1)-filling that is expected for 2-truncated quasicategories, and the proof is the fact that a quasicategory induces a 2-truncated quasicategory.

This is indeed the same property. The main difference in formulation is that currenty the (3, 1)-filling property is formulated in terms of paths which should eventually be the spine of the filled 3-simplex.

Inherently, this distinguishes 2 of the 2-simplices as those whose spine is along this path. I am not sure what advantages and disadvantages this "asymmetric" definition has compared to the symmetric definition as in assoc.

[Joël Riou]

Using CompStruct makes it very easy to construct the homotopy category/the fundamental groupoid.

[Emily Riehl]

Hi @Joël Riou. If I'm reading your code correctly (on the web, so I can't click through to find all the definitions), Edge x0 x1 is basically the type of 1-simplices from x0 to x1 while Hom x0 x1 is basically the type of homotopy classes of such 1-simplices (the hom in the fundamental groupoid).

Two questions:

(1) the actual definition of Edge x0 x1 seems more complicated than the (horribly named) hom in the underlying refl Quiver of a (2-truncated) simplicial set here. Can you explain?

(2) Similarly I'd like to understand exactly what is going on with the definition Hom x0 x1.

It does seem like having something like CompStruct to work with seems like a good idea for understanding the homotopy category/fundamental groupoid. A key lemma is that if you have any three 1-simplices in a 2-truncated quasi-category then the corresponding arrows in the homotopy category satisfy a composition relation f . g = h iff there is a 2-simplex whose boundary is given by f, g, and h, which is very naturally stated using this CompStruct.

[Julian Komaromy]

When it comes to refactoring the PR, I don't see how one could get by only using CompStruct, because the edges to be filled in with a 2-simplex are not part of the data given. I guess one could do something like the following:

structure FilledSpine {X : Truncated 2} (e₀₁ : X _⦋1⦌₂) (e₁₂ : X _⦋1⦌₂)  where
  σ : X _⦋2⦌₂
  h₀₁ : X.map (tr (δ 2)).op σ = e₀₁
  h₁₂ : X.map (tr (δ 0)).op σ = e₁₂

def comp {X : Truncated 2} {e₀₁ : X _⦋1⦌₂} {e₁₂ : X _⦋1⦌₂} (c : FilledSpine e₀₁ e₁₂) : X _⦋1⦌₂ :=
  X.map (tr (δ 1)).op c.σ

structure horn_data' {X : Truncated 2} (f : X.Path 3) where
  c₃ : FilledSpine (f.arrow 0) (f.arrow 1)
  c₀ : FilledSpine (f.arrow 1) (f.arrow 2)
  c₁ : FilledSpine (f.arrow 2) (comp c₃)

[Joël Riou]

I defined Edge x₀ x₁ as the type of morphisms Δ[1] ⟶ X whose restriction to the boundary ∂Δ[1] correspond to sending 0 to x₀ and 1 to x₁. (Similarly, for higher homotopy groups, I am considering maps Δ[n] ⟶ X that are constant on the boundary.) As this type of morphisms is a particular case of what I denoted Subcomplex.RelativeMorphism, I automatically get a notion of homotopy for edges and a type for the homotopy classes of these (where homotopies are defined using morphisms Δ[1] ⊗ Δ[1] ⟶ X; and later I show that this is equivalent to homotopies given by maps Δ[2] ⟶ X which are "constant" on one of the faces).

Of course, here, we need to take a more down to earth definition so that it applies to truncated simplicial sets. As we are doing multiple things with this notion of edge, I would suggest we define a type Edge x₀ x₁ rather than using the quiver notation x₀ ⟶ x₁.

[Joël Riou]

Julian Komaromy said:

When it comes to refactoring the PR, I don't see how one could get by only using CompStruct, because the edges to be filled in with a 2-simplex are not part of the data given. I guess one could do something like the following:

Instead of working wih plain 1-simplices, it is easier to work with the dependent type Edge x₀ x₁. Then, everything can be phrased in terms of CompStruct.

[Julian Komaromy]

I'm afraid that I still do not quite understand. Is the suggestion to have

fill31 {f₀₁ : Edge x₀ x₁} {f₁₂ : Edge x₁ x₂} {f₂₃ : Edge x₂ x₃}
    {f₀₂ : Edge x₀ x₂} {f₁₃ : Edge x₁ x₃} {f₀₃ : Edge x₀ x₃}
    (h₀₂ : CompStruct f₀₁ f₁₂ f₀₂)
    (h₁₃ : CompStruct f₁₂ f₂₃ f₁₃)
    (h : CompStruct f₀₁ f₁₃ f₀₃) :
    CompStruct f₀₂ f₂₃ f₀₃

i.e. without using the Path API, with a definition of
Edge for the case of 2-truncated simplicial sets?

[Joël Riou]

Yes!

[Emily Riehl]

@Julian Komaromy will you ping me when you'd like another review of your PR? I don't want to keep you waiting just because I haven't been paying attention.

[Julian Komaromy]

Yes of course, I will be refactoring the PR to useCompStruct and I will let you know once its ready for review (probably this shouldn't take too long).

[Julian Komaromy]

So from our discussion, this is the API that I have now mostly proven (but I still need to substantially clean everything up):

structure Quasicategory₂ (X : Truncated 2) where
  fill21 {x₀ x₁ x₂ : X _⦋0⦌₂}
      (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) :
      Nonempty (Σ e₀₂ : Edge x₀ x₂, CompStruct e₀₁ e₁₂ e₀₂)
  fill31 {x₀ x₁ x₂ x₃ : X _⦋0⦌₂}
      {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₂₃ : Edge x₂ x₃}
      {e₀₂ : Edge x₀ x₂} {e₁₃ : Edge x₁ x₃} {e₀₃ : Edge x₀ x₃}
      (f₃ : CompStruct e₀₁ e₁₂ e₀₂)
      (f₀ : CompStruct e₁₂ e₂₃ e₁₃)
      (f₂ : CompStruct e₀₁ e₁₃ e₀₃) :
      Nonempty (CompStruct e₀₂ e₂₃ e₀₃)
    -- ditto for fill32

where

structure Edge (x₀ : X _⦋0⦌₂) (x₁ : X _⦋0⦌₂) where
  simplex : X _⦋1⦌₂
  h₀ : X.map (tr (δ 1)).op simplex = x₀
  h₁ : X.map (tr (δ 0)).op simplex = x₁

structure CompStruct (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) (e₀₂ : Edge x₀ x₂) where
  simplex : X _⦋2⦌₂
  h₀₁ : X.map (tr (δ 2)).op simplex = e₀₁.simplex
  h₁₂ : X.map (tr (δ 0)).op simplex = e₁₂.simplex
  h₀₂ : X.map (tr (δ 1)).op simplex = e₀₂.simplex

Notable is now the absence of Path, replaced by Edge and CompStruct, as well as the Nonempty statements making everything Prop typed, as in the definition of quasicategories.

Is this as everyone here imagined? I want to make sure before I clean up the proofs and publish the new PR...

[Joël Riou]

I would make Quasicategory₂ a class, but otherwise, this looks good to me.

[Emily Riehl]

Like you, I was thinking in path speak, which is how we defined the homotopy category functor on simplicial sets. But this formulation feels nice and intuitive. Thanks for the reviews and clean up.

[Emily Riehl]

Ping me again when you want another review. We tend to merge things fairly quickly into the InfinityCosmos repository once they are fairly stable so if you don't want that to happen, let me know as well.