towards the homotopy category of a quasi-category

Stream: Infinity-Cosmos

[Emily Riehl]

@Kunhong Du are you still working on defining the various homotopy relations on 1-simplices via a 2-simplex? If you've made any preliminary progress, would you mind sharing your code (even if incomplete)?

[Kunhong Du]

@Emily Riehl Sure, please see here. I have only finished the definition and showed the reflexivity holds. Compared from this pr, I define the homotopy on morphisms rather than on objects, I think it is more consistent with other notions of homotopy. Also, I define the homotopy as sturcture rather than class as recommended by this comment.

I guess for further properties we need a complete api for horn filling. The pr mentioned before already did some work on that. Maybe I should first merge them into our repository?

[Emily Riehl]

This looks great. Would you mind creating a PR for us (it's okay to still have sorries; we have several in the repository) to review? There are various things that aren't obvious to me that are worth discussing, e.g.:

• should the 1-simplices be terms of type f g : Δ[1] ⟶ A or of type f g : A _[1]?
• If the latter should the 1-simplices be parametrized over zero simplices x y : A _[0] and come already with proofs that they are parallel from x to y?

[Emily Riehl]

Part of the reason I ask is that @Nick Ward is looking for something new to do and one thought was to suggest he work on re-defining the homotopy category functor in the special case where the simplicial set is a quasi-category.

[Emily Riehl]

While @Kunhong Du is working on something like this

Emily Riehl said:

... since the hoFunctor PR is still being reviewed (#16783), I think it makes sense to start with results that don't require it.

Maybe we call the thing where the degenerate 1-simplex is the 0-th face of a 2-simplex a left homotopy; "left" because it defines a 1-simplex in Hom^L(x,y). The other case, where the degenerate 1-simplex is the 2nd face of a 2-simplex is then a right homotopy.

Your first task would be to show that if the ambient simplicial set is a quasi-category then left and right homotopy are each equivalence relations and moreover coincide.

Perhaps @Nick Ward could work on defining a functor from QCat to Cat that sends a quasi-category X to the category whose type of objects is X _[0] and whose type of morphisms is a further question of the homs defined in #16783:

/-- A simplicial set `S` has an underlying refl quiver with `S _[0]` as its underlying type.-/
def SSet.OneTruncation (S : SSet) := S _[0]

/-- The source vertex of `f : S _[1]` for use in defining the underlying refl quiver.-/
def SSet.OneTruncation.src {S : SSet} (f : S _[1]) : OneTruncation S := S.δ 1 f

/-- The target vertex of `f : S _[1]` for use in defining the underlying refl quiver.-/
def SSet.OneTruncation.tgt {S : SSet} (f : S _[1]) : OneTruncation S := S.δ 0 f

/-- The hom-types of the refl quiver underlying a simplicial set `S` are subtypes of `S _[1]`.-/
def SSet.OneTruncation.Hom {S : SSet} (X Y : OneTruncation S) :=
  {p : S _[1] // src p = X ∧ tgt p = Y}

[Emily Riehl]

The further quotienting is then by the homotopy relation.

Unlike the construction of def SSet.hoFunctor' : SSet.{u} ⥤ Cat.{u,u} which first forms a free category on a ReflQuiver and then quotients by a hom relation, in this case once can show directly that the quotiented homs defined above have a well-defined composition function.

[Emily Riehl]

The proof would require several lemmas about the homotopy relation that @Kunhong Du could state sooner (and then prove later) so that @Nick Ward could work on this in parallel.

[Emily Riehl]

If this sounds vaguely interesting, let me know, and I'll see if I can whip up a blueprint with more details about all of the above. One thing that should be achievable once this is done is the proof that if X is StrictSegal, then an explicit map η from X to the nerve of its homotopy category (via the construction above) is an isomorphism.

[Nick Ward]

@Emily Riehl sounds great!

@Kunhong Du if it's alright I might bother you with some questions as I try to get a feel for the interface here. I'm also happy to work at the same time on some of the background stuff that might be needed (e.g. the more complete api for horn filling that you mentioned).

[Emily Riehl]

In the meanwhile @Nick Ward, if you have any suggestions for #16783 they would be very welcome.

[Kunhong Du]

@Emily Riehl I just opened a PR.

For your question, I think A _[1] might be easier to work with when we want to prove the properties of homotopy relations, but is it the case that in the context of $\infty$-category, we talk about morphisms more frequently? If so, maybe it would be helpful to define two versions of homotopy and state that they are somehow equivalent via Yoneda.

For the second question, I did require the 1-simplicies to be parametrized by 0-simplcies in my first approach.

structure ParallelPair {A : SSet.{u}} (x y : Δ[0] ⟶ A) where
  hom : Δ[1] ⟶ A
  src : Interval.src ≫ hom = x
  tgt : Interval.tgt ≫ hom = y

variable {A : SSet.{u}} {x y : Δ[0] ⟶ A} (f g : ParallelPair x y)

structure HomotopyL where
  homotopy : Δ[2] ⟶ A
  face0 : standardSimplex.map (δ 0) ≫ homotopy = standardSimplex.map (σ 0) ≫ y
  face1 : standardSimplex.map (δ 1) ≫ homotopy = g.hom
  face2 : standardSimplex.map (δ 2) ≫ homotopy = f.hom

Bad thing about this is being redundant, but we do have that f and g are parallel definitionally, rather than propositional equalities for the correpsonding vertices. And I believe not being equal definitionally may cause many problems when working on catgeories in Lean. Under this consideration, maybe an explicit parametrization may be better.

[Kunhong Du]

@Nick Ward Feel free to ask me any questions. I'm glad that I could help. You can tell me what lemmas you may want for your proof and I can state them. And we can discuss about the API for horn fillings, which should be interesting :big_smile:

[Emily Riehl]

@Nick Ward it occurred to me to also suggest that as a warmup you define this simpler version of the homotopy category first for StrictSegal simplicial sets. I don't know that we'll want that version in mathlib but you could PR it to the Infinity-Cosmos repository for folks to play around with.

[Emily Riehl]

For StrictSegal things two 1-simplices will be related by @Kunhong Du's homotopy relation iff they are equal so the homotopy category doesn't have any quotienting. Instead you are showing that the underlying reflQuiver of a strict segal simplicial set already has a category structure with composition defined by taking the diagonal of the 2-simplex formed by a path of length 2.

[Emily Riehl]

By request @Kunhong Du opened up an early PR containing the following definitions

open SimplexCategory

variable {A : SSet.{u}} (f g : Δ[1] ⟶ A)

structure HomotopyL where
  homotopy : Δ[2] ⟶ A
  face0 : standardSimplex.map (δ 0) ≫ homotopy =
    standardSimplex.map (σ 0) ≫ standardSimplex.map (δ 0) ≫ f
  face1 : standardSimplex.map (δ 1) ≫ homotopy = g
  face2 : standardSimplex.map (δ 2) ≫ homotopy = f

structure HomotopyR where
  homotopy : Δ[2] ⟶ A
  face0 : standardSimplex.map (δ 0) ≫ homotopy = f
  face1 : standardSimplex.map (δ 1) ≫ homotopy = g
  face2 : standardSimplex.map (δ 2) ≫ homotopy =
    standardSimplex.map (σ 0) ≫ standardSimplex.map (δ 1) ≫ f

def HomotopicL : Prop :=
    Nonempty (HomotopyL f g)

def HomotopicR : Prop :=
    Nonempty (HomotopyR f g)

Now we'd be grateful for some advice on the best way to handle these structures and relations.

[Emily Riehl]

A few that aren't obvious to me that are worth discussing, e.g.:

• should the 1-simplices be terms of type f g : Δ[1] ⟶ A or of type f g : A _[1]?
• If the latter should the 1-simplices be parametrized over zero simplices x y : A _[0] and come already with proofs that they are parallel from x to y?

[Emily Riehl]

Future theorems will show, for instance, that when A is a quasi-category:

• HomotopicL and HomotopyR are equivalence relations
• in fact they are the same equivalence relation
• moreover, these relations precisely capture the class of 1-simplices that are sent to the same arrow in the homotopy category of A.

[Dean Young]

@Jack McKoen's code had some of these things, right?

[Jack McKoen]

I had some early sketches of things like this, but nothing worth digging up

[Emily Riehl]

@Kunhong Du I think the easiest thing might be to just merge your branch now and just do some experiments on the main branch. Do you have any objections?

[Nick Ward]

Maybe we can open a github issue to organize any discussion? Alternatively, I think keeping all of the discussion here has its benefits as well.

[Emily Riehl]

Seems like a good idea to me. Go for it, if you like!

[Kunhong Du]

Please do the merge. I think the further experiments can tell which of the possible definitions is better.

[Nick Ward]

Nick Ward said:

Maybe we can open a github issue to organize any discussion?

cosmos#60

[Pietro Monticone]

Let me know if you want me to port the dashboard-based workflow into InfinityCosmos (see #FLT > Project Dashboard for more info).

It will just require a few steps for @Emily Riehl, but it would allow us to have have an issue per task, claim tasks directly on GitHub and having technical discussions within the same issue and / or related PR which is supposed to close it.

I'll be able to assist with that tomorrow.

[Nick Ward]

Emily Riehl said:

Nick Ward it occurred to me to also suggest that as a warmup you define this simpler version of the homotopy category first for StrictSegal simplicial sets.

cosmos#61 includes a (partial) definition of the homotopy category for StrictSegal simplicial sets. I don't know that we'll actually want to merge this one. My intention is to open a competing PR that uses @Kunhong Du's definition of the homotopy relations in cosmos#51 for comparison. Hopefully this will provide some insight into which version of the homotopy relations might be easier to work with.

[Nick Ward]

Emily Riehl said:

• should the 1-simplices be terms of type f g : Δ[1] ⟶ A or of type f g : A _[1]?

I will try to better express this opinion on the github issue once I have a bit more evidence to back it up, but so far working on cosmos#61 I have strongly preferred the definition of the homotopy relations using 1-simplices f g : A _[1]. I believe this is primarily because the Path structure and StrictSegal class are defined on arrows of the same type. It has proven fairly tedious translating back and forth between these definitions.

That being said, it's possible that this will start to matter less once the basics of quasicategories are out of the way. Additionally, there is always the option of altering the definition of Path to use 1-simplices f : Δ[1] ⟶ A if there are advantages to this approach. But, my opinion would be that it's best to pick a preferred form for 1-simplices and use it consistently in definitions.

[Kunhong Du]

I opened a PR, where I redefined HomotopyL and HomotopyR according to @Nick Ward 's suggestions.

[Kunhong Du]

I noticed that my commits include [Merge remote-tracking branch 'upstream/main'], which seems a little messy. Do I need to clean it?

[Kevin Buzzard]

In FLT we're squash merging when merging PRs to main

[Nick Ward]

This is great @Kunhong Du! I would be curious to know if anyone else thinks working with 1-simplices f g : Δ[1] ⟶ A might be easier in the long run. It's possible my opinion is influenced by mostly working with StrictSegal things thus far rather than Quasicategory.

It looks to me like the infinity-cosmos repo is also set up for squash merging, so I wouldn't worry about altering your commits.

[Nick Ward]

@Kunhong Du have you made any progress toward an improved api for defining maps from the horn? I have also found myself blocked by this while sketching out the construction of the homotopy category of a quasicategory here.

I'm happy to work on this, but don't want to duplicate efforts too much.

[Kunhong Du]

@Nick Ward Ah I happen to be working with it right now. I actually sort of finished the framework months ago but it's a total mess and probably only understandable to myself. It'd be great if we could work on it together.

[Nick Ward]

Yeah sounds great! I think the best way is probably either opening an infinity-cosmos PR or we could collaborate directly on a mathlib branch. Depending on where your work so far is maybe there's another way that's easier for you, though.

[Nick Ward]

No need to clean things up for my sake, but also no rush if it's a hassle to move your existing work over to infinity-cosmos or mathlib.

[Emily Riehl]

I see I've missed a lot of work from @Kunhong Du and @Nick Ward while I've been offline. Congrats to both of you.

Do you have advice on the correct order to review and integrate your respective PRs?

[Nick Ward]

@Emily Riehl I won't speak for @Kunhong Du, but I think cosmos#63 is fairly independent and probably just a matter of deciding which form of the homotopy relations are best to have on main for the time being.

cosmos#61 is probably not ready to be merged at this point (with inevitable merge conflicts being among the reasons). The two things of interest are StrictSegal.homotopic_iff_eq and the anonymous Category (OneTruncation S) instance. My guess is that StrictSegal.homotopic_iff_eq is worth cleaning up and merging, possibly in a separate PR. I'm not as sure about the StrictSegal homotopy category instance. I have a complete proof scattered across two branches at this point, but I am unsure whether to clean it up now or just view it as a warm-up for the homotopy category of a quasicategory.

[Kunhong Du]

Nick Ward said:

I won't speak for Kunhong Du, but I think cosmos#63 is fairly independent and probably just a matter of deciding which form of the homotopy relations are best to have on main for the time being.

I agree. I think it can be merged to main now.

[Emily Riehl]

Just left a review (finally). The code looks good but I think style conventions suggest we need more evocative names for the fields of the structure. I like "simplex" and then perhaps something like δ₀_eq which is a conventional way to name equalities.

[Emily Riehl]

But modulo a name change to something like the above I agree this is ready to merge.

[Emily Riehl]

@Kunhong Du I suggested a name change on your PR. How do you feel about it?

[Kunhong Du]

@Emily Riehl Changed. Sorry for the delay. I've been a little busy.

[Emily Riehl]

No rush and no need to apologize. It just occurred to me that perhaps you missed the comments from earlier. Anyway, merged!

[Nick Ward]

mathlib4#20448 provides a description of the boundary ∂Δ[n] as a colimit of the standard simplices.

The tentative plan is to use this as the basis for an api that makes it easier to define maps out of the horn / boundary. We will presumably need a very similar proof for the colimit description of Λ[n, i], so any feedback is very appreciated.

[Joël Riou]

Nick Ward said:

The tentative plan is to use this as the basis for an api that makes it easier to define maps out of the horn / boundary. We will presumably need a very similar proof for the colimit description of Λ[n, i], so any feedback is very appreciated.

I had not planned to make this public as early, but I am currently working on constructing the standard model category structures on TopCat and SSet, and as part of this work (which is at an early stage, following my work on the small object argument), I have thought about the following design. In https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Sites/Subsheaf.html we have the notion of a Subpresheaf of a presheaf of types (the presheaf part of this file should be moved to a better place), and I have verified that it is a complete lattice. In this file https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/Boundary.lean I define the faces of the standard simplex (face S for S : Set (Fin (n + 1))) and show the following lemmas:

lemma face_inter_face (S₁ S₂ : Set (Fin (n + 1))) :
    face S₁ ⊓ face S₂ = face (S₁ ⊓ S₂) := by
  aesop

lemma subcomplexBoundary_eq_iSup :
    subcomplexBoundary.{u} n = ⨆ (i : Fin (n + 1)), standardSimplex.face {i}ᶜ  := ...

lemma subcomplexHorn_eq_iSup (i : Fin (n + 1)) :
    subcomplexHorn.{u} n i =
      ⨆ (j : ({i}ᶜ : Set (Fin (n + 1)))), standardSimplex.face {j.1}ᶜ := ...

In general, if a subcomplex is the ⨆ of subcomplexes Z i, then it should be easy to show there is a multicoequalizer diagram involving the Z i and the Z i ⊓ Z j (it suffices to show this in a category of sets instead of the category of presheaves). In the situation above, the subcomplexes Z i and their intersections are (empty or) representable in the simplex category.

[Nick Ward]

@Joël Riou very neat, thanks for sharing!

[Nick Ward]

If I understand correctly, this would subsume the work in mathlib4#20448 and perhaps even provide a better "backend" for a horn filling api. Do you have an opinion on the best place to draw the interface between your work and such an api?

[Joël Riou]

Yes, from the colimit cocone I suggest, yours should be obtained (up to reindexing) by excluding i = j and focusing on i < j (which is obviously possible). I will test a little bit my API while working on the various descriptions of the Gabriel-Zisman anodyne extensions, and then I will PR the basic subcomplexes API. It may take a few weeks before I start PRing this.

[Nick Ward]

@Joël Riou do you see any reason to push mathlib4#20448 forward in the meantime (or anything that should be salvaged into a separate PR)? If not, I will close it.

[Nick Ward]

Also, I'm happy to help port the subcomplexes api when the time comes, although I assume it is still evolving along with the other work you shared.

[Joël Riou]

I think it is better to wait for the subcomplexes API. (I just want to prove a few basic lemmas using it so that it stabilizes before PRing it; it should not be too long.)

[Nick Ward]

I'm inclined to agree. No rush of course!

[Joël Riou]

See #mathlib4 > Name suggestions for lattice/category theory notions? for a call for suggestions for the name of some new definitions related to the above discussion.

[Joël Riou]

I would like to mention that while working on the homotopy theory of simplicial sets, I have done significant steps towards the construction of the fundamental groupoid of a Kan complex. It seems (?) that the homotopy category of a quasi-category https://emilyriehl.github.io/infinity-cosmos/blueprint/sec-simplicial-sets.html#lem:htpy-cat-of-qcat is obtained using the same arguments. For the fundamental groupoid, we use outer horns in order to obtain left and right inverses, but otherwise, it would suffice to check the argumentation only requires inner horns. For example, when showing the associativity of the composition, I use an (inner) horn in Δ[3]. The uniqueness of path composition up to homotopy is more tricky as it uses the inclusion of the union of {0, 1} × Δ[2] and Δ[1] × Λ[2, 1] in Δ[1] × Δ[2], which requires general results on anodyne extensions. I have reduced one of the most technical lemmas about anodyne extensions (as initially defined by Gabriel and Zisman) to an equality of two subcomplexes (hopefully, I did not do mistakes with the indices...), but this will need some more work. (And Jack is working specifically on inner anodyne extensions.) I do not intend to work on quasi-categories (as I am very much focusing on the model category structure on topological spaces and simplicial sets), but there are significant chunks of code that will be useful for the infinity-cosmos project.
This is https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/FundamentalGroupoid.lean and https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/AnodyneExtensions.lean
I will do mathlib PRs about some general API about subpresheaves and gluing as it was mentionned above (see for example https://github.com/joelriou/topcat-model-category/blob/e6e1c795171ab4e27551eaf433d004202aa553e9/TopCatModelCategory/SSet/Horn.lean#L310 ).

[Nick Ward]

@Joël Riou let me know if I can be of any help in the mathlib port.

[Emily Riehl]

Thanks for sharing @Joël Riou. This does sound very helpful.

Getting this construction of the homotopy of a quasi-category and proving that the homotopy category functor preserves products are high priorities as far as I'm concerned that I was hoping to renew interest in as soon as some current PRs are merged.

[Nick Ward]

@Emily Riehl I think interest is still high! It's just that @Joël Riou has come up with a much better solution to our problems than I managed to, so we are patiently awaiting these fancy new tools.

[Emily Riehl]

I'm grateful also that you've fixed all the truncated segal stuff so that maybe one day I'll finally be able to merge that PR from september...

[Joël Riou]

Modulo a very mild sorry, I have obtained that the inclusion of the union of {1} ⊗ Δ[n] and Δ[1] ⊗ ∂Δ[n] in Δ[1] ⊗ Δ[n] is an anodyne extension (here it is a finite composition of pushouts of horn inclusions) (and the proof for {0} ⊗ Δ[n] instead of {1} ⊗ Δ[n] should be very similar) https://github.com/joelriou/topcat-model-category/blob/28ae20d3b8b50b2f379a17d112c8745d19a5bcdd/TopCatModelCategory/SSet/AnodyneExtensions.lean#L319-L321
This is one of main technical results towards the description of anodyne extensions (not inner anodyne extensions), and this uses heavily the API that I have started to PR to mathlib, see #20840, #21090, #21096, #21098, #21103, #21174, and which should be soon usable for the infinity cosmos project...

[Jack McKoen]

This is great, I think I'll also be able to use some of this!

[Nick Ward]

@Joël Riou my only complaint is that I can't keep up! I will try to work my way through your recent PRs, but please don't hesitate to flag any that need more (unsophisticated) opinions or review.

[Joël Riou]

I have mostly formalized the fundamental groupoid of a Kan complex, and it turns out the proofs can be done by using very directly the lifting with respect to horn inclusions (instead of more intricate anodyne extensions).

[Joël Riou]

The most useful tool in this work is the following definition CompStruct, where FundamentalGroupoid X is a type synonym for X and Edge x₀ x₁ is a 1-simplex "from x₀ to x₁":

variable {x₀ x₁ x₂ x₃ : FundamentalGroupoid X}

structure CompStruct (p₀₁ : Edge x₀ x₁) (p₁₂ : Edge x₁ x₂) (p₀₂ : Edge x₀ x₂) where
  map : Δ[2] ⟶ X
  h₀₁ : stdSimplex.δ 2 ≫ map = p₀₁.map := by aesop_cat
  h₁₂ : stdSimplex.δ 0 ≫ map = p₁₂.map := by aesop_cat
  h₀₂ : stdSimplex.δ 1 ≫ map = p₀₂.map := by aesop_cat

(https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/FundamentalGroupoid.lean)

[Joël Riou]

This structure expresses that the homotopy class of p₀₂ is the composition of p₀₁ and p₁₂. That there is such a structure for some p₀₂ when p₀₁ and p₁₂ are given uses the inner horn inclusion in Δ[2]. The homotopy relation HomotopyL and HomotopyR mentionned above in this thread are special cases of CompStruct. Then, two "associativity" lemmas using the two inner horns in Δ[3] can be used in order to show the equivalence of HomotopyL/R and to prove the compatibilities required in order to get the category structure on homotopy classes of "paths". The outer horns are used only in order to get the groupoid structure. (I have also mostly formalized the higher dimensional analogues of this in order to define the homotopy groups of a Kan complex.)

[Joël Riou]

(In this ongoing formalization work of simplicial homotopy theory, I found that details about the homotopy relation(s) on simplices are left under the carpet in the reference book I am mostly following. Here, the homotopy relation on paths may also be defined as a particular case of the general homotopy relation using homotopies X ⊗ Δ[1] ⟶ Y, i.e. as maps from the square Δ[1] ⊗ Δ[1], which contains two non degenerate 2-simplices. I do not see how to prove certain results without using CompStruct or HomotopyL/R...)

[Joël Riou]

As the construction of the category structure only use inner horns, the definition of the fundamental groupoid of a Kan complex should be done as a particular case of the homotopy category of a quasi-category.

[Nick Ward]

Joël Riou said:

The homotopy relation HomotopyL and HomotopyR mentionned above in this thread are special cases of CompStruct.

@Kunhong Du just flagging this as something that we will need.

[Nick Ward]

@Joël Riou thanks for all this work, and for your patience in explaining it to us.

[Nick Ward]

Would you be willing to share more info on the reference book you mentioned?

[Joël Riou]

I am using Simplicial homotopy theory by Goerss-Jardine. They define the homotopy relation by using maps X ⊗ Δ[1] ⟶ Y, but when we need a more precise result (Lemma I.7.4: an n-simplex s of a pointed Kan complex (X, x) represents the trivial element of the homotopy group iff there is a n+1-simplex whose faces are (x, ...,x, s) [Actually, s can be put in any place in the list]), they just left this as an exercice without any hint (this appears when doing the homotopy sequence of a fibration between Kan complexes). I could fill in the details only by looking at the original paper by Daniel Kan, Ann. of Math. 67 (1958).

[Nick Ward]

Thanks, these should be helpful resources in my efforts to follow along here.

[Joël Riou]

Given X : Type u, A : Set X, U : ι → Set X and V : ι → ι → Set X such that A is the union of the U i, and the V i j are the intersections (this is CompleteLattice.MulticoequalizerDiagram A U V), I show in #23872 that the type A is the multicoequalizer of the U is along the V i js. This depends on a few other PRs: #23364, #23339, #22205, #21032, #22203, #21026. In a subsequent PR, a similar result will be deduced for SSet.Subcomplex instead of Set, and this will allow the construction of maps from horns.

[Emily Riehl]

After seeing how much pain @Julian Komaromy had to endure to work with 2-truncated quasi-categories in resolving issue #103. I've been worried that my suggested blueprint, to develop the homotopy category of a quasi-category in the 2-truncated setting, was a mistake.

I've just opened a PR that adapts his code to the non-truncated setting . Using this and some code I stole from @Joël Riou's work on the fundamental groupoid of a Kan complex linked above, modulo some incomplete dualization and one sorry, the following PR addresses issue #104 (proving the left and right homotopy relations are equivalence relations and coincide in a quasi-category). I'm very curious what both of you think.

Essentially what made this easier (besides the fact that all of the hard work had been done by @Julian Komaromy and @Joël Riou) was the fact that the infrastructure for non-truncated simplicial sets is better developed. In particular we have things like δ_comp_δ_apply (that were surprisingly hard to use because of issues I think with the inequality arguments; if a lean wizard could golf my code to try to avoid the erws that would be great).

[Emily Riehl]

There's one other thing to note in the PR: I introduced also the notion of an AlgebraicQuasicategory:

structure AlgebraicQuasicategory (S : SSet) where
  hornFilling' : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n+3)⦄ (σ₀ : (Λ[n+2, i] : SSet) ⟶ S)
    (_h0 : 0 < i) (_hn : i < Fin.last (n+2)), Δ[n+2] ⟶ S
  hornFilling_comm' :  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n+3)⦄ (σ₀ : (Λ[n+2, i] : SSet) ⟶ S)
    (_h0 : 0 < i) (_hn : i < Fin.last (n+2)),
    σ₀ = Λ[n + 2, i].ι ≫ hornFilling' σ₀ _h0 _hn

where the difference is that horn fillers are specified. Note that the main example of quasi-categories in mathlib, @Johan Commelin and @Nick Ward's nerves of categories, can be made algebraic, essentially as just demonstrated by @Aaron Liu (because strict segal simplicial sets define algebraic quasi-categories). (An algebraic Kan complex would of course also define an algebraic quasi-category.) So I'd argue that we should actually change Quasicategory to refer to this notion and introduce IsQuasicategory for the predicate on simplicial sets. The rationale is that this makes the following constructive, where this would all be tagged as noncomputable otherwise:

/-- In a quasi-category, the left homotopy relation is symmetric. -/
def HomotopyL.symm (h : HomotopyL p q) : HomotopyL q p :=
  CompStruct.assoc Q h (CompStruct.compId _) (CompStruct.compId p)

/-- In a quasi-category, the right homotopy relation is symmetric. -/
def HomotopyR.symm (h : HomotopyR p q) : HomotopyR q p :=
  CompStruct.assoc' Q (CompStruct.idComp _) h (CompStruct.idComp p)

/-- In a quasi-category, left homotopy implies right homotopy. -/
def HomotopyL.homotopyR (h : HomotopyL p q) : HomotopyR p q :=
  HomotopyR.symm Q (CompStruct.assoc' Q (CompStruct.idComp p) h (CompStruct.compId p))

/-- In a quasi-category, right homotopy implies left homotopy. -/
def HomotopyR.homotopyL (h : HomotopyR p q) : HomotopyL p q :=
  HomotopyL.symm Q (CompStruct.assoc Q h (CompStruct.compId p) (CompStruct.idComp p))

/-- In a quasi-category, the left homotopy relation is transitive. -/
def HomotopyL.trans (h : HomotopyL p q) (h' : HomotopyL q r) :
    HomotopyL p r :=
  CompStruct.assoc Q (CompStruct.idComp p) h (HomotopyL.homotopyR Q h')

/-- In a quasi-category, the right homotopy relation is transitive. -/
def HomotopyR.trans (h : HomotopyR p q) (h' : HomotopyR q r) :
    HomotopyR p r :=
  CompStruct.assoc' Q h (CompStruct.compId p) (HomotopyR.homotopyL Q h')

[Emily Riehl]

With apologies to @Kunhong Du, @Nick Ward, I had to comment some of their past work on this to avoid duplication of names. So this PR should be considered a draft. And apologies to @Julian Komaromy for moving some of his stuff from the SSetnamespace (where it belongs) to SSet.Truncated for the same reason. Apologies to all.

[Joël Riou]

Some notions can be defined and made computable in the "algebraic" context, with specified horn fillers, but I think this may lead to issues when studying the stability properties of quasicategories/Kan complexes. I do not think that AlgebraicQuasiCategory should replace the definition of QuasiCategory, and I would be extremely unhappy if a notion of AlgebraicKanComplex were to replace the notion of KanComplex. For example, if i : A ⟶ B is a monomorphism, p : X ⟶ Y is a Kan fibration, and sq is a commutative square (a map from the arrow i to the arrow p), the subcomplex of (ihom B).obj X consisting of "morphisms" B ⟶ X which makes the two triangles commute is a Kan complex.
https://github.com/joelriou/topcat-model-category/blob/4b4b46eda5c6038efa64d7c70e9c46cfb6e5b6dd/TopCatModelCategory/SSet/Fibrations.lean#L386-L389
If we wanted to define an AlgebraicKanComplex instance for this, we may have to know that p is an "algebraic" Kan fibration and as we would have to track down all the uses of lifting properties, we would have to replace the notion of anodyne extension (which is a property) with data saying that for any algebraic Kan fibration, we have a specified lift in all squares involving algebraic Kan fibrations, etc. Even monomorphisms would have to include data because we may need a computable way of making them transfinite compositions of boundary inclusions. This seems extremely unpractical to me. I do not know the details about how to construct quasicategories out of other quasicategories, but similar issues would certainly arise when replacing anodyne extensions with inner anodyne extensions.
Including data may make the definition of the composition of maps in the homotopy category computable, but I certainly do not expect we could get a DecidableEq instance on the type of maps! Then, is it really so important to have computable definitions? Does it outweight the serious issues I have mentionned?

[Johan Commelin]

Would it make sense to write the main API in terms of the current notion of quasicategory, but to allow algebraic quasicats for certain constructions, where the computability pays of?

[Robin Carlier]

I agree with @Joël Riou's objection. Making quasicategories "algebraic" is likely to turn proofs of facts like "internal hom from a simplicial set to a quasicategory is a quasicategory", stability of isofibrations with respect to joins (required to show that "slices" of quasicategories are quasicategories), or basically anything about it the Joyal model structure into a lot of pain.

[Emily Riehl]

Robin Carlier said:

I agree with Joël Riou's objection. Making quasicategories "algebraic" is likely to turn proofs of facts like "internal hom from a simplicial set to a quasicategory is a quasicategory", stability of isofibrations with respect to joins (required to show that "slices" of quasicategories are quasicategories), or basically anything about it the Joyal model structure into a lot of pain.

I would argue it's already a lot of pain. But I guess I take the point that since anything defined using the universal property of a limit or a colimit is noncomputable (according to Mathlib) anyway, the benefit is less than I was expecting.

It does bother me every time I have to tag something as noncomputable when the proof gives an explicit construction. But I'll let this go until it bothers someone else enough to be worth revisiting.

[Robin Carlier]

I totally agree with the second paragraph, my way to cope with it has been to tag sections noncomputable so that the compiler doesn't remind me about it every time.

[Kevin Buzzard]

I certainly don't know much about computability but this conversation feels very reminiscent of e.g. the two ways of defining finiteness of a set in mathlib; we have S : Finset X (data, computable) and S : Set X + hS : Set.Finite S (a prop, noncomputable), and API for both constructions, with some proofs on one side just "stolen" from the other side (e.g. the API for the noncomputable finsum, sums over noncomputable sets which gives the sum if it's finite and 0 if it's infinite, was often written by "if it's infinite then the sum is 0 and the lemma is easy, else use the axiom of choice, make a Finset, apply the Finset sum lemma and convert back". Because everything was a proof this worked fine. There are advantages and disadvantages to this approach, the most obvious disadvantage being that it's an instance of https://xkcd.com/927/ and the most obvious advantage being that everyone can have what they want (it's just that it might be hard for everyone to talk to each other).

There is a constant tension in mathlib between "those that want to compute" and "those that want to prove". The first time I understood this properly was when there were a lot of people intensely discussing computability of polynomials and how it was making proofs more annoying, and then mathlib was updated to make polynomials noncomputable and all of a sudden a student of mine who had defined Chebyshev polynomials when formalizing a past Imperial exam question suddenly found that their proof of things like "the 4th Chebyshev polynomial is (blah) by rfl" stopped working, and they now had to use ring. Fortunately for them, the tactic was there when they needed it, because it had been written a few months earlier by Mario. If the analogous quasicategory tactic is not there in category theory then I can imagine that a noncomputable API might be frustrating for those that want to compute.

I don't think it makes sense for mathlib to have two definitions of a polynomial, the whole philosophy of mathlib is that there's one definition of everything, and unfortunately most of the active people in the community were not around when the decision to make them noncomputable was made (and I didn't understand the discussion at the time so it's difficult to summarise it). But sometimes people talk about a solution to this problem being @[csimp]. I have absolutely no idea whether this helps here (indeed I only have the vaguest idea about what @[csimp] does). If this doesn't help, dare you consider developing both a computable and a noncomputable theory like we have for finite sets, and trying to glue them together somehow (like we do for finite sums)?

[Joël Riou]

I do not understand what @[csimp] does and if it is relevant here, but what is happening here is that we are defining the homotopy category of a simplicial set X. It is possible to define it by generators and relations in general, but in the favourable case of quasicategories, it is a quotient category. Given two vertices x and y, the morphims x ⟶ y identify to a quotient of a type of edges from x to y. In order to define the composition, we need to define the homotopy class of the composition of an edge from x to y and an edge from y to z. The quasicategory axioms involve lifting properties which allow to find a 2-simplex t, which can be thought as a "triangle", such that two sides correspond to two given edges, and the composition shall be defined as the remaining side of the triangle (and its homotopy class is independent of the choices). If we have some magic data which gives us the triangle t, we can make the composition law in the homotopy category computable. I have argued that in downstream applications, including data in the definitions would have very bad consequences. And the gain would be very little because the composition law is defined on a quotient type, where we certainly do not have a decidable equality (there is no easy way to determine that two edges are homotopic). Roughly, it is likely that the only case where we can prove f ≫ g = h by rfl is when h is exactly the third side of the very specific triangle that would be part of the magic data. Something would be "computable" in the Lean sense, but it would be completely inoperative. (The situation is much worse as compared to polynomials, where definitions are "noncomputable", but we can still make computations using the ring tactic.)

[Joël Riou]

(Mostly, it is like attempting computations in the quotient of a ring by an ideal you do not know much about.)

[Mario Carneiro]

Kevin Buzzard said:

But sometimes people talk about a solution to this problem being @[csimp]. I have absolutely no idea whether this helps here (indeed I only have the vaguest idea about what @[csimp] does).

Just to give extra context on this: There are two ways to "compute" in lean, kernel and interpreted. (Actually three if you include compiled to C but it's mostly the same as interpreted, just faster.) Kernel computation is used when you use by decide or rfl to prove a theorem, and interpreted computation is used when you use by native_decide or #eval, or run a tactic (the tactic itself is interpreted, the proof it generates is kernel checked).

As a result of this, most discussion around polynomials being computable is about kernel computation. That's what will let you prove things by rfl. @[csimp] is an attribute which lets the interpreter use a different evaluation strategy than the kernel, so it is not useful for improving kernel computation.