the homotopy category functor and the nerve adjunction

Stream: Infinity-Cosmos

[Emily Riehl]

Thanks to the tireless work of @Joël Riou, the functor
hoFunctor : SSet.{u} ⥤ Cat.{u, u}
that takes a simplicial set to its homotopy category is now in Mathlib!

Now there is only one PR (#16784) from last summer's work with @Mario Carneiro remaining: the construction of

nerveAdjunction : hoFunctor ⊣ nerveFunctor

There is (at least) one aspect of this construction that could use some golfing, and I thought I'd start a discussion here to solicit suggestions.

[Emily Riehl]

The nerveAdjunction is actually defined as a composite of two other adjunctions:

coskAdj 2 : truncation.{u} 2 ⊣ Truncated.cosk 2

between simplicial sets and 2-truncated simplicial sets and

nerve₂Adj : hoFunctor₂.{u} ⊣ nerveFunctor₂

which involves similar functors but using 2-truncated simplicial sets instead of simplicial sets. The bulk of the work in PR #16784 is in constructing nerve₂Adj .

[Emily Riehl]

The construction directly defines the unit and counit and checks the triangle equalities. The counit is straightforward: its components are functors mapping out of hoFunctor₂ (nerveFunctor₂ C) for some category C and hoFunctor₂ is a quotient of some other category, so has a mapping out universal property. After pre-composing with the quotient functor, the counit component is, up to isomorphism, the counit component ReflQuiv.adj.counit.app Cof another adjunction .

[Emily Riehl]

The construction of the unit components are much more interesting. We have an analogous unit component ReflQuiv.adj.counit.app and morally the unit component is obtained by postcomposing this with the quotient functor, with one big caveat: the map I just described is a map of ReflQuivers (morally 1-truncated simplicial sets) and we require a map of 2-truncated simplicial sets. But because this map is valued in nerveFunctor₂ (hoFunctor₂ X) for some 2-truncated simplicial set X and nerves of categories are 2-coskeletal, the map of reflexive quivers lifts to define the map we want.

[Emily Riehl]

Here's way the proof needs golfing: in establishing the infrastructure needed to make the lift; see lines 96-442 (the bulk) of the PR.

This was written before @Joël Riou suggested we re-prove 2-coskeletality in a more abstract way using StrictSegal simplicial sets. My instinct is that these stuff could be streamlined via something like that abstraction.

I've started to implement this in a draft PR #20090 but this seems to require a lot of new infrastructure, because all of the strict segal stuff was developed for simplicial sets rather than 2-truncated simplicial sets. Thus, I'd love some advice about whether we can reuse any of this or whether we have to simply redevelop it. See the file Truncated in that PR which contains all the new development. Any thoughts @Nick Ward or anyone? Suggestions or help would be very welcome.

[Johan Commelin]

I'll just say that I hope messages 2,3,4 in this thread will end up in some form in the module docstring in mathlib, in whatever form this gets merged.

[Johan Commelin]

Also, I agree that it's good to take a step back and think about how the new infrastructure can be reused here. Maybe by appropriately abstracting. But I haven't thought about this particular question before, so I don't have any concrete advice atm.

[Joël Riou]

Emily Riehl said:

I've started to implement this in a draft PR #20090 but this seems to require a lot of new infrastructure, because all of the strict segal stuff was developed for simplicial sets rather than 2-truncated simplicial sets. Thus, I'd love some advice about whether we can reuse any of this or whether we have to simply redevelop it. See the file Truncated in that PR which contains all the new development. Any thoughts Nick Ward or anyone? Suggestions or help would be very welcome.

I have just added some suggestion of a slightly more general design.

[Nick Ward]

Exciting to see mathlib4#16783 merged!

I will take a closer look, but I think I generally agree with @Joël Riou that rather than outright duplicating existing constructions, it might make sense to redefine them in terms of the most natural truncation level. This probably requires some thought around how best to unify constructions defined in terms of different truncation levels.

[Emily Riehl]

@Nick Ward if you have any ideas about how best to implement this, I'd be very grateful. @Joël Riou's suggest to redefine paths using 1-truncated simplicial sets makes sense to me but we should also think about whether and how to try to unify this notion with the existing infrastructure of Paths in Quivers. The just merged PR also contains the definition of the underlying ReflQuiver of a 2-truncated simplicial set (because this is the thing we need to define the homotopy category). Should this be generalized to 1-truncated simplicial sets (which we don't need right now) or will that just make it harder to use in the case we care about? This isn't so clear to me...

[Joël Riou]

There are some subtleties about the exact types of paths we consider. For simplicial sets, we have Path X n for a fixed n, without any condition about the source and target 0-simplex, because we want to relate this type with X_ [n]. In the context of quivers, we have a type of paths from a to b (without any condition on the length). These notions have quite distinct uses.

[Nick Ward]

@Emily Riehl I will play around with redefining Path and some of the StrictSegal infrastructure and see if that inspires any concrete ideas.

My only thought right now (which may be obvious), is that we should try to maintain a canonical definition of each construction (e.g. defining Path₁ and then defining Path X as Path₁ <| (SSet.truncation 1).obj X). I think duplication of some APIs is inevitable (and not necessarily a bad thing), but hopefully we can avoid ad hoc duplication of translations between the different definitions.

[Nick Ward]

Whether the canonical definition needs to be the "right one" is also a good question. I think, for instance, whether we should first define the underlying ReflQuiver in terms of 1-truncated simplicial sets depends a lot on how hard it is to work with the truncation functor, which I don't have a great idea of yet.

[Joël Riou]

The truncation functor has very good definitional properties. (You will probably need to define the functors SimplexCategory.Truncated n ⥤ SimplexCategory.Truncated m when n ≤ m.)

[Nick Ward]

I still have relatively little to contribute here, but I have discovered that the following slight generalization of the X _[0]₂ notation is valid. I'm sure any metaprogramming experts will be able to improve what I have here (or explain why it is a bad idea altogether).

import Mathlib.AlgebraicTopology.SimplicialSet.Basic
import Mathlib.Util.Superscript

namespace SSet.Truncated

scoped macro:1000 X:term " _[" n:term "]"t:subscript(term) : term =>
    `(($X : SSet.Truncated $(⟨t.raw[0]⟩)).obj
      (Opposite.op ⟨SimplexCategory.mk $n, by decide⟩))

end SSet.Truncated

universe u
variable (X : SSet.Truncated.{u} 1) (Y : SSet.Truncated.{u} 2)

open scoped SSet.Truncated

#check X _[0]₁
#check Y _[0]₂

[Nick Ward]

It's still just a sketch, but here is what I've been thinking for redefining the StrictSegal infrastructure.

The short summary is that SSet.StrictSegal would be defined in terms of SSet.Truncated.StrictSegal, and the same for SSet.Path and SSet.spine. I believe this is approximately what @Joël Riou has suggested, though I suspect at least the definition of SSet.StrictSegal can be still be improved significantly.

[Nick Ward]

I think the next steps would be to make sure this is actually helpful for the work in mathlib4#20090, then to work on a PR that replaces the existing definitions. It's possible @Emily Riehl is already way ahead of me on this, though.

[Nick Ward]

(I also haven't touched on the questions related to quivers yet).

[Joël Riou]

At first glance, it looks like what I was thinking of. I recently noticed that the design of StrictSegal could be slightly improved. Currently there is the data of an inverse map in the definition. I suggest we should make StrictSegal a structure (not a class), and define IsStrictSegal X : Prop which could be used by lemmas that do not depend on the definitional properties of the StrictSegal structure, like this one I found today:

lemma SSet.mono_iff_of_strictSegal {X Y : SSet} (f : X ⟶ Y) [X.StrictSegal] :
  Mono f ↔ Function.Injective (f.app (op [1]))

[Joël Riou]

The refactor for the truncated case could be an occasion to do this other refactor at the same time.

[Emily Riehl]

@Nick Ward this looks really great. Thanks for taking it on. I've done no work at all on this in the last few weeks but am slowly coming back online.

For experimental purposes, it looks like I could just copy the code from your Elephant file into #20090 and see what I can do with it. That PR was always meant to be experimental (and will either be overwritten or deleted) once we've got a more concrete plan. Or is there another workflow that you'd suggest?

Happy new year everyone!

[Nick Ward]

@Emily Riehl if it's helpful in its current state, certainly feel free to copy any code into #20090. However, I suspect we won't really know if the StrictSegal machinery is helpful for #16784 until we have a more complete development of the truncated versions of things beyond just the definitions themselves.

Assuming nothing looks obviously wrong with the definitions I proposed here, I will work on a proper PR that replaces the current definitions (and works through any bugs in the proposed definitions). Looking briefly at #16784, it should be relatively easy to rebase on top of such a PR in order to experiment further with SSet.Truncated.StrictSegal.

[Nick Ward]

One quick question: are we sure that an n-truncated simplicial set should be considered SSet.Truncated.StrictSegal if its n-simplices are uniquely determined by their spine? It occurred to me that we could also ask for all m-simplices for m ≤ n to be uniquely determined by their m-spine. I do think that the former translates more cleanly into the un-truncated definition, though.

[Emily Riehl]

Ah, sorry, it should definitely mean the latter (m-simplices determined by their spine for all $m \leq n$). I was just thinking of the case $n=2$ where these notions coincide.

[Nick Ward]

Oh that makes more sense, thank you! I obviously just copied your definition for n = 2 without giving it enough thought.

[Nick Ward]

I have opened a WIP PR redefining StrictSegal and related constructions in terms of truncated simplicial sets at #20668. There are still a lot of changes to be made, but there should be enough work in place to enable experimenting with the new definitions. Any feedback is of course also appreciated.

[Nick Ward]

Some of the TODOs include:

• Cleaning up the new / replacement proofs
• Getting rid of lots of erws
• Deciding on namespaces, notation, etc.
• Adding IsStrictSegal : Prop

[Nick Ward]

mathlib4#20688 breaks out the truncated notations [m]ₙ and X _[m]ₙ from #20668.

[Emily Riehl]

I'm very into these truncated notions, the former of which is broken in the experimental PR I'm working with (for reasons I don't understand) and is making everything very verbose. Will you ping me when these are merged?

[Emily Riehl]

I'll have a look at the rest of the PR tomorrow afternoon.

[Emily Riehl]

@Nick Ward can you explain why StrictSegal is no longer an instance?

[Emily Riehl]

Regarding API, I also added a version of your Path₁.ext' (but for Path instead of Path₁) in my experimental extension of your code. I used this to define the following (a bit long winded):

/-- Two simplices in a `StrictSegal` truncated simplicial set agree iff their spines agree. -/
theorem ext' {m : ℕ} (hmn : m ≤ n + 1) (Δ Δ' : X _[m]ₙ₊₁) :
    X.spine hmn Δ = X.spine hmn Δ' → Δ = Δ' := fun hyp => spineInjective hmn hyp

/-- Two simplices in a `StrictSegal` truncated simplicial set agree iff the 1-simplices along their
spines agree. -/
theorem ext'' {m : ℕ} (hmn' : m + 1 ≤ n + 1) (Δ Δ' : X _[m + 1]ₙ₊₁)
    (hyp : (i : Fin (m + 1)) →
      (X.map (SimplexCategory.mkOfSucc i : ⟨[1], Nat.le_add_left 1 n⟩ ⟶ ⟨[m + 1], hmn'⟩).op Δ) =
      (X.map (SimplexCategory.mkOfSucc i : ⟨[1], Nat.le_add_left 1 n⟩ ⟶ ⟨[m + 1], hmn'⟩).op Δ')) :
    Δ = Δ' := ext' _ _ _ (Path.ext' hyp)

[Emily Riehl]

But in the horrible thing toStrictSegal₂.mk that I'm trying to prove what was most useful was the following:

section
variable (Y : SSet.Truncated.{u} 2) [StrictSegal Y]

/-- This is similiar to one of the famous Segal maps, except valued in a product rather than a
pullback.-/
noncomputable def seagull : Y _[2]₂ ⟶ Y _[1]₂ ⨯ Y _[1]₂ :=
  prod.lift (Y.map (.op (mkOfSucc 0))) (Y.map (.op (mkOfSucc 1)))

instance : Mono (seagull Y) where
  right_cancellation {X} (f g : X → Y _[2]₂) eq := by
    ext x
    simp [seagull] at eq
    have eq1 := congr($eq ≫ prod.fst)
    have eq2 := congr($eq ≫ prod.snd)
    simp at eq1 eq2
    replace eq1 := congr_fun eq1 x
    replace eq2 := congr_fun eq2 x
    simp at eq1 eq2
    apply StrictSegal.ext''
    intro i
    match i with
    | 0 => exact eq1
    | 1 => exact eq2

end

which could be generalized from 2 to any $n \geq 2$. The point is then this allows be to reason using composition identities in SimplexCategory rather than applications of the composition identities in a situation where the ext'' might otherwise be used.

[Emily Riehl]

So essentially what I'm suggesting is a version of this monomorphism exactly where your Path₁.ext' is defined (with a better name).

[Nick Ward]

Emily Riehl said:

Nick Ward can you explain why StrictSegal is no longer an instance?

This is unrelated to the "truncation" refactor, and was suggested by @Joël Riou here. However, I haven't actually gotten around to finishing this portion of the refactor.

[Nick Ward]

Emily Riehl said:

So essentially what I'm suggesting is a version of this monomorphism exactly where your Path₁.ext' is defined.

I'm all in favor of the above, which looks rather elegant. I'm still trying to understand if this suggestion somehow excludes the existence of Path₁.ext' (which I have no particular attachment to), or if you just mean that is where it belongs in the file.

[Joël Riou]

Nick Ward said:

Emily Riehl said:

Nick Ward can you explain why StrictSegal is no longer an instance?

This is unrelated to the "truncation" refactor, and was suggested by Joël Riou here. However, I haven't actually gotten around to finishing this portion of the refactor.

The idea is that instead, there will be a IsStrictSegal instance (as a property, which does not involve the data of the inverse maps).

[Emily Riehl]

This was meant as an addition to Path₁.ext' rather than a replacement of it. I suspect we'll find both versions useful.

A naive question: since Path is just an abbreviation for Path₁ we don't also need a Path.ext' I assume?

[Nick Ward]

Emily Riehl said:

since Path is just an abbreviation for Path₁ we don't also need a Path.ext' I assume?

I'm actually not sure yet. I found that restating many of the lemmas for Path (and proving them in terms of the Path₁ version) helped type inference and made other lemmas easier to state without dropping down to Path₁. But, maybe this is too much duplication.

[Nick Ward]

I've just merged #20719 into #20668. This should fix the CI issues (which were related to #20355).

@Emily Riehl would it be helpful if we took the time to rebase #20090 on top of #20668? It might take some tedious work, and #20668 isn't particularly clean or stable yet. The upside is that we would be working with the same definitions again, and you wouldn't need to manually fix all the bugs in my original truncated definitions.

[Nick Ward]

mathlib4#20668 has reached a reviewable state. The two notation PRs it depends on have not been reviewed yet, so be aware that the diff is large and subject to change. But, if anyone has spare cycles for a first-pass review, feedback is of course appreciated.

[Emily Riehl]

Maybe I'll chat here so I don't clutter the review...

First Q: did you write an "leq" tactic, or did that exist? I've wasted ages trying to find the proofs that 1 ≤ 2 or whatever. Does the code (h : m ≤ n + 1 := by leq) mean that even though this is an explicit argument of various things a user might be able to get away by just supplying the explicit argument m?

[Emily Riehl]

Second Q: should a lemma like spine_spineToSimplex_apply be tagged for simp? I never know when this is appropriate.

[Emily Riehl]

(I left one comment on the PR because it seemed more important than the above.)

[Nick Ward]

Thank you for the feedback!

[Nick Ward]

I did write the leq tactic (here), though it really just tries to apply a few lemmas and then delegates to omega. There were a few places in the PR where I replaced omega with leq for conformity, but for the most part I only used leq in places where the goal was solved without delegating to omega.

[Nick Ward]

The notation (h : m ≤ n + 1 := by leq) is indeed a "default argument" which sometimes the caller can get away without providing explicitly. However, I think my usage of these leaves something to be desired. I suspect there may be some heuristics like "use default arguments for defs but not for lemmas", because they often seem to actually require specifying more arguments when rewriting.

[Emily Riehl]

Is there a worry that some term won't definitionally equal some other term because leq (or the user) found different proofs of the inequality in each case?

[Nick Ward]

I think you are probably correct that spine_spineToSimplex_apply should be a simp lemma. I did have some trouble tagging many lemmas that I thought should be in the simpset because the lhs contained an abbrev that further simplified, but I don't think thats the case here (at least for Truncated.StrictSegal.spine_spineToSimplex_apply).

[Nick Ward]

Emily Riehl said:

Is there a worry that some term won't definitionally equal some other term because leq (or the user) found different proofs of the inequality in each case?

As I understand it, lean's kernel treats any any two terms inhabiting a proposition P : Prop as definitionally equal. I'm not confident enough to say that this would never be a concern, though.

[Emily Riehl]

That could totally be right. I don't know one way or the other.

[Kevin Buzzard]

Yeah all proofs of a theorem are equal by definition in lean, this is different from HoTT and has a name (proof irrelevance I think?)

example (P : Prop) (h1 : P) (h2 : P) : h1 = h2 := rfl

[Kim Morrison]

I'm skeptical that leq is a good idea. Does it actually solve anything that omega can't do by itself? In practice on small problems omega is quite fast. I'd be skeptical if leq is ever 1000 heartbeats faster than omega. If you just use omega the proof are more robust, and more portable.

[Nick Ward]

Kim Morrison said:

Does it actually solve anything that omega can't do by itself?

It does not.

It is essentially the ComposableArrows valid tactic. My only real motivation for adding it was that we already needed a small wrapper for omega for the notation [m]ₙ (dsimp only [SimplexCategory.len_mk]; omega), and the vast majority of the proofs ended up being by decide or assumption. From #9594, which added the valid tactic, I inferred that we might save some cycles by fishing for an assumption before deferring to omega.

It sounds like that is not the case, though!

[Nick Ward]

Is it generally worth trying anything before deferring to omega, or would you recommend just replacing the whole wrapper with dsimp only [SimplexCategory.len_mk]; omega?

[Kim Morrison]

I'd be inclined to do unfolding (and translating any custom types in Int, if irrelevant), but not attempt to do any arithmetic yourself. That's what the black boxes are for. :-)

[Kim Morrison]

run #count_heartbeats on things and make sure you are saving at least 1000 heartbeats, preferably 10,000, before optimising black box tactics.

[Kim Morrison]

(and then tell the black box authors about the performance problem before rolling your own!)

[Nick Ward]

That's a very helpful guideline, thanks @Kim Morrison!

[Nick Ward]

If anyone is able to point me in the right direction, I'd be quite curious to learn more about omega and grind. I'm particularly interested in their performance characteristics, but any information is appreciated.

[Nick Ward]

Thanks to @Kim Morrison's insights, the trunc tactic is now much simpler. This automates the truncation proofs for the notations [m]ₙ and X _[m]ₙ.

I have temporarily removed the leq tactic, though I still find myself wanting a simple omega wrapper for autoParams that tries assumption before deferring to omega. Maybe it's the result of too much HoTT, but I see the benefit being that you can state a lemma without providing the autoParam and still know that it found your hypothesis of the same type, rather than a long omega proof that could have just been h.

Some rudimentary #check_heartbeats benchmarking suggests that such a tactic is justified (or at least break-even) in the context of SimplexCategory.Truncated. But, is it too confusing to see an unfamiliar tactic in a default argument (would you rather just see h : m ≤ n := by omega everywhere)?

[Emily Riehl]

I can't comment on omega vs leq; that's way above my expertise.

Could you tell us more about the tactic trunc, what is does, and when to use it?

[Nick Ward]

@Emily Riehl trunc is really just an implementation detail of the [m]ₙ notation for the m-dimensional simplex in the n-truncated simplex category. Every instance of [m]ₙ could be more verbosely written as [m, by trunc]ₙ, where by trunc is a proof that [m].len ≤ n. The trunc tactic itself tries decide and assumption, then simplifies the goal to m ≤ n before asking omega to solve it.

macro "trunc" : tactic =>
  `(tactic| first | decide | assumption | dsimp only [SimplexCategory.len_mk]; omega |
    fail "Failed to prove truncation property.")

[Nick Ward]

While I have also used it for some autoParams, probably the more useful thing to know is what to do when it doesn't work. If you write [m]ₙ and get the error "Failed to prove truncation property", you can instead write [m, by ...]ₙ to prove the truncation property manually.

[Nick Ward]

@Joël Riou if you have a chance, could you take a quick look at the two comment threads on #20668? I am in the midst of refactoring the refactor, and I'm not sure what to do with the case n = 0. The problem seems to be that both the spine and the StrictSegal condition make sense for 0-simplices / paths of length 0 in a simplicial set, but not for truncated simplicial sets (because Path is not defined for 0-truncated simplicial sets).

[Kim Morrison]

Nick Ward said:

While I have also used it for some autoParams, probably the more useful thing to know is what to do when it doesn't work. If you write [m]ₙ and get the error "Failed to prove truncation property", you can instead write [m, by ...]ₙ to prove the truncation property manually.

This suggests that the error message should be replaced with "Failed to prove truncation property, try writing [m, by ...]ₙ."!

[Nick Ward]

#21331 is an experiment with yet another definition of paths for truncated simplicial sets. The basic definitions are below.

Mathlib/AlgebraicTopology/SimplicialSet/Path.lean

import Mathlib.AlgebraicTopology.SimplicialSet.Horn

universe v u
open CategoryTheory Opposite Simplicial SimplexCategory

namespace SSet
namespace Truncated

open SimplexCategory.Truncated Hom SimplicialObject.Truncated

/-- A path of length `m` in a 0-truncated simplicial set `X` consists of `m + 1`
0-simplices in `X`. -/
@[ext]
structure Path₀ (X : SSet.Truncated.{u} 0) (m : ℕ) where
  vertex (i : Fin (m + 1)) : X _[0]₀

/-- A path `f` of length `m` in a 1-truncated simplicial set `X` is a directed
path of `m` edges. The vertices of `f` live in the further 0-truncation of `X`.  -/
@[ext]
structure Path₁ (X : SSet.Truncated.{u} 1) (m : ℕ)
    extends Path₀ ((trunc 1 0).obj X) m where
  /-- A path includes the data of `m` 1-simplices in `X`. -/
  arrow (i : Fin m) : X _[1]₁
  /-- The source of a 1-simplex in a path is identified with the source vertex
  in the further 0-truncation of `X`. -/
  arrow_src (i : Fin m) : X.map (tr (δ 1)).op (arrow i) = vertex i.castSucc
  /-- The target of a 1-simplex in a path is identified with the target vertex
  in the further 0-truncation of `X`. -/
  arrow_tgt (i : Fin m) : X.map (tr (δ 0)).op (arrow i) = vertex i.succ

/-- A path of length `m` in an `n`-truncated simplicial set `X` includes the
data of `m + 1` vertices — 0-simplices in the further 0-truncation of `X`. If
`X` contains 1-simplices (`n > 0`), then a path in `X` additionally contains the
data of `m` arrows — 1-simplices in the further 1-truncation of `X`. -/
def Path {n : ℕ} : SSet.Truncated.{u} n → ℕ → Type u := by
  induction n with
  | zero => exact Path₀
  | succ n => exact Path₁ ∘ (trunc (n + 1) 1).obj

end Truncated

/-- A path of length `n` in a simplicial set `X` is defined by 1-truncating `X`,
then taking the 1-truncated path. -/
abbrev Path (X : SSet.{u}) (n : ℕ) := truncation 1 |>.obj X |>.Path n

-- Alternatively, the below definition works well with the inductive definition
-- of `StrictSegal`.

/-- Unfolding the definition of `Truncated.Path`, a path of length `n + 1` in a
simplicial set `X` is defined as a `Truncated.Path₁` structure on the
1-truncation of `X`. A path of length 0 in `X` is defined as a `Truncated.Path₀`
structure on the 0-truncation of `X`. -/
abbrev Path' (X : SSet.{u}) (n : ℕ) := truncation n |>.obj X |>.Path n

end SSet

[Nick Ward]

I think we have a variety of alternative definitions now that we can "plug and play". This version of truncated paths is a bit more complicated, but it does allow us to talk about paths in 0-truncated simplicial sets.

The next step is probably to choose the simplest combination of these definitions that work for what we need right now, then we can always incorporate more complexity if we find that it's needed.

[Joël Riou]

(deleted)

[Joël Riou]

My preference is to simply ignore 0-truncated simplicial sets when defining paths and StrictSegal.

[Joël Riou]

(Note that the definition Path₀ above is not very sound, mathematically speaking. According to it, if X is 0-truncated, there would be a path of length 1 between two arbitrary 0-simplices, which we certainly do not want.)

[Nick Ward]

Yes, I think calling Path₀ a path is a bit of a stretch.

[Nick Ward]

I appreciate all the input on my various experiments here. I think the conclusion is that we want to keep the definitions in #21146 (although I'm not sure of the state of that branch). I will get it cleaned up and back into a reviewable state.

[Nick Ward]

@Emily Riehl do you foresee needing Path or StrictSegal to be defined for 0-truncated simplicial sets?

It seems to me that we mostly want to work with truncated simplicial sets where the truncation level is fixed (and nonzero), so I'm inclined to agree with @Joël Riou's suggestion to ignore 0-truncated simplicial sets for now. It shouldn't be too difficult to go back and include them in the definitions if we discover a need for them.

[Emily Riehl]

I agree that makes sense as the best way forward.

[Emily Riehl]

I've been (mostly) holding off reworking the proof that the homotopy category functor is left adjoint to the nerve until this is done, but you can see a few of the constructions I'll need in #20090.

[Emily Riehl]

One thing I use is this where OneTruncation₂ is the underlying ReflQuiver of a 2-truncated simplicial set. Note this is definable in fact for 1-truncated simplicial sets though we use it in the 2-truncated case. One thing I'll have to experiment with, I guess, is whether giving the more general forms of the construction make them less usable:

/-- A refl prefunctor between the underlying refl quivers of a 2-truncated simplicial sets induces a
map on paths. -/
def reflPrefunctorPathMap {X Y : SSet.Truncated.{u} 2} (F : OneTruncation₂ X ⥤rq OneTruncation₂ Y)
    {n : ℕ} (σ : Path₂ X n) : Path₂ Y n where
      vertex i := F.obj (σ.vertex i)
      arrow i := (F.map ⟨σ.arrow i, σ.arrow_src i, σ.arrow_tgt i⟩).edge
      arrow_src i := (F.map ⟨σ.arrow i, σ.arrow_src i, σ.arrow_tgt i⟩).src_eq
      arrow_tgt i := (F.map ⟨σ.arrow i, σ.arrow_src i, σ.arrow_tgt i⟩).tgt_eq

[Emily Riehl]

That is used to show that under a hypothesis a ReflPrefunctor between reflexive quivers that arise in this way actually extends to a map of 2-truncated simplicial sets:

/-- The components of a map of 2-truncated simplicial sets built from a map on underlying reflexive
quivers, under the assumption that the codomain is `StrictSegal`. -/
def toStrictSegal₂.mk.app {X Y : SSet.Truncated 2} [StrictSegal₂ Y]
    (F : OneTruncation₂ X ⥤rq OneTruncation₂ Y)
    (n : SimplexCategory.Truncated 2) : X.obj (op n) ⟶ Y.obj (op n) := by
  obtain ⟨n, hn⟩ := n
  induction' n using SimplexCategory.rec with n
  match n with
  | 0 => exact fun x => F.obj x
  | 1 => exact fun f => (F.map ⟨f, rfl, rfl⟩).edge
  | 2 => exact fun φ => StrictSegal₂.spineToSimplex₂ (reflPrefunctorPathMap F (X.spine₂ φ))

and

def toStrictSegal₂.mk {X Y : SSet.Truncated 2} [StrictSegal₂ Y]
    (F : OneTruncation₂ X ⥤rq OneTruncation₂ Y)
    (hyp : (φ : X _[2]₂) → (F.map (ev02₂ φ)).edge =
      StrictSegal₂.spineToDiagonal₂ (reflPrefunctorPathMap F (spine₂ X φ))) : X ⟶ Y where
  app := fun n => toStrictSegal₂.mk.app F n.unop
  naturality := by

where the proof of naturality is long and tedious. This is used to construct the unit of the adjunction.

[Nick Ward]

This is all helpful, thanks.

[Nick Ward]

Emily Riehl said:

I've been (mostly) holding off reworking the proof that the homotopy category functor is left adjoint to the nerve until this is done.

Hopefully this refactor will be in a more stable state soon. It will still be blocked on the question of notation, but there are some options for working around this so that it doesn't hold up any other work:

• Make #20668 independent of the notation PRs.
• Rebase #20090 on top of #20668 once the latter is more stable.

[Joël Riou]

I assume you mean #21146 instead of #20668?

[Nick Ward]

That was confusing, apologies. My plan is to merge #21146 into #20668 for review, but I am indeed talking about the content currently in #21146.

[Emily Riehl]

I like this plan. I feel like the notation will be easy to update later so if we can avoid being blocked on this now, that would be great! I appreciate your diligent efforts on all of this <3

[Nick Ward]

#20668 is now notation-free and ready for review. Thanks to everyone who has already given feedback on the new definitions.

[Nick Ward]

@Joël Riou should I rebase #20668 on top of #21090? As I think we definitely want your proofs wherever the two conflict.

[Joël Riou]

Nick Ward said:

Joël Riou should I rebase #20668 on top of #21090? As I think we definitely want your proofs wherever the two conflict.

This would be less work for me if you do so, then I would not say no!

[Nick Ward]

Nick Ward said:

Joël Riou should I rebase #20668 on top of #21090?

Done in commit 0b22a2e. In the process I uncovered some ugliness that I believe is caused by the change to the definition of SSet.Path (specifically SSet.Path.arrow). I will see if I can't rectify this.

[Nick Ward]

You can see the problem by grepping for @id in the commit linked above.

[Joël Riou]

It seems you have found a solution :)

[Nick Ward]

Indeed! Although I have raised a related question on #20668 related to the definitional properties of SSet.Path.

[Nick Ward]

I think I mostly managed to avoid damaging any of the nice proofs in #21090.

[Nick Ward]

The truncated paths refactor in #20668 is now merged. Thanks to @Emily Riehl and @Joël Riou for lots of early feedback and review!

[Emily Riehl]

Congrats. I really REALLY appreciate this. Next week I'll try to apply this to golf some of the worst proofs in the nerve adjunction. I'm sure I'll have questions for you then.