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.

[Julian Komaromy]

@Emily Riehl the CompStruct version is now on the PR, so it's ready for a second review.

[Emily Riehl]

@Julian Komaromy sorry to be so slow. I just left you a bunch of annoying renaming suggestions (to get a little closer to mathlib style, for the future when ultimately this may go into mathlib). But once that's done, let's merge and close this issue.

[Emily Riehl]

I'm curious about your experience with the refactoring. Do you like the new CompStructure set up?

Also it's still unclear to me whether the right definition of 2-truncated quasi-category uses Nonempty but it doesn't seem to make a huge difference in practice so we can change this later if we choose.

[Julian Komaromy]

@Emily Riehl I really should have paid more attention the the naming convention, that's my bad, but I think all is fixed and ready for merging now.

Refactoring from the Pathstuff was very straightforward. CompStruct makes everything almost frustratingly symmetric, such that the amount of duplicated code alarms me. However, I could not come up with sensible lemmas to generalize the duplicated blocks because of the finicky combinatorics ("which edge of which face do I need here?").

I am not sure about the Nonempty either, but it is easy to change (and matches the Prop-valued Quasicategory).

[Emily Riehl]

Great. I'll bump mathlib as you suggest and merge now.

[Joël Riou]

About symmetries, there is a kind of "duality" on simplicial sets. As the simplex category is equivalent to the category of totally ordered nonempty finite sets, and for any totally ordered set, we can consider the same set with the reverse order, there is a "covariant involution" SimplexCategory ⥤ SimplexCategory, which induces similar "operations" on simplicial sets (or truncated simplicial sets). Via this duality, the nerve of a category and the nerve of its opposite category should correspond, and also the (3, 1)-filling should be dual to the (3, 2)-filling, so that, in principle, proofs related to the (3, 1)-filling could be dualised in order to deduce formally the other case, but it is likely that it would take more time to explore this duality as compared to duplicating the code of proofs...

[Emily Riehl]

Congrats @Julian Komaromy. The PR is merged and the issue closed :octopus:

[Julian Komaromy]

Great, thanks for all the help!

[Julian Komaromy]

I haven't kept up with the project in the last couple of weeks, but I finally got around to working on left and right homotopy relations for 2-truncated quasicats. This was actually surprisingly straightforward using
CompStruct, a small example:

abbrev HomotopicL {x y : A _⦋0⦌₂} (f g : Edge x y) := Nonempty (CompStruct f (idEdge y) g)

def HomotopicL.symm {x y : A _⦋0⦌₂} {f g : Edge x y} (hfg : HomotopicL f g) :
    HomotopicL g f := by
  rcases hfg with ⟨hfg⟩
  exact Quasicategory₂.fill31 hfg (idCompStruct y) (doubleEdge₀ f)

To me, this shows that it is not infeasable to do the rest of the 2-truncated stuff (and the δ₂ relations that are now in mathlib are great!) if there is still interest in going down this route.

I have opened a draft PR: https://github.com/emilyriehl/infinity-cosmos/pull/133

[Joël Riou]

This was even shorter in my original code https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/FundamentalGroupoid.lean#L510-L528
This is the reason why I pushed for using this structure CompStruct...

[Emily Riehl]

@Joël Riou I think ultimately the mathlib construction of the fundamental groupoid of a Kan complex should be a special case of the homotopy category of a quasi-category. Do you have a sense of whether it's better to develop this in the 2-truncated setting or the untruncated setting? I don't want @Julian Komaromy to have to refactor too much when this is ultimately PRed to mathlib.

[Joël Riou]

Yes, doing the homotopy category in the 2-truncated setting seems to be the best approach.

[Emily Riehl]

Julian Komaromy said:

I haven't kept up with the project in the last couple of weeks, but I finally got around to working on left and right homotopy relations for 2-truncated quasicats. This was actually surprisingly straightforward using
CompStruct, a small example:

abbrev HomotopicL {x y : A _⦋0⦌₂} (f g : Edge x y) := Nonempty (CompStruct f (idEdge y) g)

def HomotopicL.symm {x y : A _⦋0⦌₂} {f g : Edge x y} (hfg : HomotopicL f g) :
    HomotopicL g f := by
  rcases hfg with ⟨hfg⟩
  exact Quasicategory₂.fill31 hfg (idCompStruct y) (doubleEdge₀ f)

To me, this shows that it is not infeasable to do the rest of the 2-truncated stuff (and the δ₂ relations that are now in mathlib are great!) if there is still interest in going down this route.

I have opened a draft PR: https://github.com/emilyriehl/infinity-cosmos/pull/133

@Julian Komaromy I finally had a chance to look at your code and indeed it seems the API finally makes this as straightforward as it should be. Congrats. Let's have one more think about the term naming and then I'll merge.

Specifically, I'm hoping we can use an ambient namespace like "QCat" (or whatever is most appropriate for the 2-truncated quasi-category setting) so that we can call the comp structures witnessing the identity laws by "comp_id" and "id_comp". This would then align with the 1-categorical names.

[Emily Riehl]

A final question: is there anything in PR #123 that's worth keeping? I wouldn't mind deleting it as a bit of housecleaning now that you've shown we can go forward with the 2-truncated approach.

[Emily Riehl]

@ me again when you're ready for a final review and merge. Well done!

[Julian Komaromy]

I also have most of the corollaries about homotopy equivalence and composition, so I will probably get those into the PR as well.

I will try to get back to you on all this by Wednesday!

[Emily Riehl]

No rush. Just wanted to make sure I'm not slowing you down.

[Julian Komaromy]

@Emily Riehl I have updated the names as you suggested and added some further statements from the blueprint. I have left a comment on GitHub with some more details.

In my opinion, PR #123 can be removed if you want. Most of the contents have been now put into the 2-truncated setting.

[Emily Riehl]

Great, will do. And your PR is merged. Congrats.

The only thing that's now out of date is the issue dashboard. @Pietro Monticone, @Julian Komaromy just merged the code resolving issue #104 without previously claiming that issue. Is there an easy way to update to show this is closed now after the fact?

[Julian Komaromy]

Emily Riehl said:

Great, will do. And your PR is merged. Congrats.

The only thing that's now out of date is the issue dashboard. Pietro Monticone, Julian Komaromy just merged the code resolving issue #104 without previously claiming that issue. Is there an easy way to update to show this is closed now after the fact?

@Pietro Monticone note that my PR #133 has also resolved issue #105.

[Pietro Monticone]

Hi @Emily Riehl and @Julian Komaromy, done.

[Julian Komaromy]

Thanks!

[Pietro Monticone]

Just a quick note: to properly refer to issues and PRs of this project, you might want to use the associated linkifier (e.g. cosmos#104). The #N is reserved for Mathlib.

[Julian Komaromy]

@Emily Riehl PR cosmos#136 defines the homotopy category of a 2-truncated quasicategory and proves that this is isomorphic to the usual homotopy category. This result is obtained pretty much exactly as the proof of 1.3.8 is spelled out in the blueprint, which is nice (working with ReflPrefunctors went mostly smoothly).

I mention two potential issues / rooms for improvement in the PR message, but aside from that (and naming conventions, which I still struggle with), I am optimistic that we can merge this quite quickly.

[Emily Riehl]

Congrats!

Our semester starts tomorrow and I'm teaching a new course (using Lean in fact) so I may be a little slow to review this. But I'm excited to see your progress.

[Kevin Buzzard]

Emily Riehl said:

Congrats!

Our semester starts tomorrow and I'm teaching a new course (using Lean in fact)

You can make a PR changing this file and this will add the course to the list at https://leanprover-community.github.io/teaching/courses.html (if you didn't already! I didn't spot it glancing through...)

[Emily Riehl]

Done.

[Emily Riehl]

Julian Komaromy said:

Emily Riehl PR cosmos#136 defines the homotopy category of a 2-truncated quasicategory and proves that this is isomorphic to the usual homotopy category. This result is obtained pretty much exactly as the proof of 1.3.8 is spelled out in the blueprint, which is nice (working with ReflPrefunctors went mostly smoothly).

I mention two potential issues / rooms for improvement in the PR message, but aside from that (and naming conventions, which I still struggle with), I am optimistic that we can merge this quite quickly.

@Julian Komaromy I'm sorry for being so ridiculously slow with this; I've been behind on everything for weeks.

Your code looks great. You were right of course about your improved versions of HomotopyL.refl and HomotopyR.refl so I just cut the old ones. I also implemented some very minor renaming of two terms and used .mp and .mpr for the implications of your iff, which seems to be the preferred mathlib style.

[Emily Riehl]

This is certainly ready to merge into our repository whenever you think it's ready. We can also discuss merging some of this into mathlib if that interests you? (I wasn't sure if that's what you meant about ReflPrefunctor.congr_hom. If it's just for us, it's probably okay to leave it where it is.)

[Emily Riehl]

Anyway nice work and apologies again!

[Julian Komaromy]

@Emily Riehl
Thanks for taking a look. I'll have a final look at the PR next week and then we can merge it. Down the line, I'd love to help get stuff merged into mathlib (whether its this particular stuff or something else in the infty-cosmos repo).

[Joël Riou]

After #31254 is merged (definition of Edge and CompStruct for 2-truncated simplicial sets), would you @Julian Komaromy like to PR the definition of 2-truncated quasicategories, the definition of the left/right homotopy relations, show that they define the same equivalence relation on edges in the case of 2-truncated quasicategories, etc, until the definition of the homotopy category of a (2-truncated) quasicategory? (Meanwhile, after the cleanup PR #31258 is merged, I intend to add various lemmas and definitions to produce pushouts and multicoequalizer diagrams for horn and boundaries, which will allow to show that the 2-truncated nerve of a category is a 2-truncated quasicategory.)
Then, after introducing a notion of 2-truncated Kan complex, we can get the fundamental groupoid of a Kan complex (https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/FundamentalGroupoid.lean).

[Julian Komaromy]

@Joël Riou Sounds good, I think I should be able to do that.

[Julian Komaromy]

@Joël Riou I opened PR #31552 containing:

• the definition of a 2-truncated quasicategory
• left & right homotopy relations and basic theorems

I left a comment about the definition of a 2-truncated quasicategory, but everything is as previously discussed in this channel.

[Joël Riou]

Apart from very small details, this looks good to me. The docstring of Quasicategory₂ is very nice!
The phrasing of fill21 with a sigma type is very much ok (any version would be fine for me).

[Joël Riou]

What I have understood formalizing the model category of simplicial sets is that there are basically two kinds of simplicial sets for which we have quite canonical horn liftings (to the point it might be possible to make them computable) are nerves of categories (inner horns only) (or groupoids) and singular simplicial sets attached to topological spaces (in that case, the horn filling is given by a continuous retraction of the inclusion of the horns in the topological simplex). However, I do not think it is a problem to have nonconstructive definitions for the composition of morphisms in the homotopy category of a (2-truncated) quasicategory: one of the reasons is that the equality of morphisms (i.e. the homotopy relation) is not decidable.

[Emily Riehl]

I was the one pushing the "algebraic" point of view beforehand but now I agree. An important design choice in the quasi-categorical model of (∞,1)-categories is exactly this: that composition is not specified. The diagonal edge of any 2-simplex is equally the composite of the edges along its spine. In the case of a nerve of a 1-category then these spine fillers are unique (StrictSegal) so we really are in an "algebraic" setting. In the case iof the singular complex of a topological space I'd argue that the perspective of not choosing composites is still the right one because the choices can't be made coherently anyway from the point of view of n-ary composition of edges.

[Joël Riou]

I have just PRed #31797 which deals with pushouts and multicoequalizers of subcomplexes of a simplicial set. Soon, other PRs about specific multicoequalizer and pushout diagrams will follow...

[Julian Komaromy]

Nice. I will have a look once thats merged to incorporate it into the proof that the 2-truncation of a QC is a 2-truncated QC. Meanwhile my PR #31630 defines the homotopy category of a 2-truncated QC.

[Joël Riou]

I have added #31802 which gives a description of horns in Δ[2] as pushouts, and the draft PR #31805 expresses horns in Δ[n] as multicoequalizers (in particular, I provide API for inner horns in Δ[3]). This should be sufficient to get that quasicategories induce 2-truncated quasicategories.