Refactoring `CategoryTheory.Paths` as a one-field struct

Stream: mathlib4

[Robin Carlier]

The current docs#CategoryTheory.Paths is a "direct type alias", i.e

/-- A type synonym for the category of paths in a quiver.-/
def Paths (V : Type u₁) : Type u₁ := V

This particular type alias is very prone to defeq abuse, and I’m getting more and more disatisfied with it when working with it in practice (Paths is a necessary ingredient for any kind of category presented by generators and relations.). One of the few pain points are:

• The absence of a good coercion functions to and from the original type. We do have docs#CategoryTheory.Paths.of, which allows in theory to use its obj and map fields as "coercions", but for instance docs#CategoryTheory.Paths.of_obj is marked simp, which is very bad (it clearly abuses the defeq V = Paths V).
• Similary docs#CategoryTheory.Paths.of_map is also simp which abuses the defeq x ⟶ y = Quiver.Hom.Path x y for x y : Paths V (in the latter form, lean sometimes has trouble unifying with morphisms in a category). This leads to inconsistent writing in the API, where some declarations coerce from morphisms in the quiver to Paths via Paths.of, while some other do it using Quiver.Hom.toPath.

As a result, working with Paths often result in either erw hell or with a change-fest (see e.g here or here).

I think the situation would be much better if we could enforce a stronger barrier between Paths and the original type. Concretely, I propose we refactor things in the following way:

• Paths become a one-field structure, i.e

structure Paths (V : Type u₁) : Type u₁ where as : V

• The Homs for the category struct remain defeq to Quiver.Path but we stop using Quiver.Hom.toPath to coerce morphisms in V to morphisms in Paths V, and we generally ban Quiver.Hom.toPath in the "categorical" API (it remains a valid coercion in the Quiver API). The way to translate from the quiver to the path category becomes exclusively Paths.of, which gets un-simped.

Are there objections?

[Joël Riou]

This looks good to me.

[Robin Carlier]

I’m currently experimenting with this and it breaks an unexpected amount of things around Cat.FreeRefl and SSet.HomotopyCategory... Things might not be as easy as I initially made it and may need to wait for a refactor making this part of the library more robust first.

[Joël Riou]

It may also break the construction of the localized category (but there the fix should be relatively easy).

[Robin Carlier]

Yes, the breakages around Localization/Construction were easy to fix ;)

[Emily Riehl]

@Mario Carneiro might be able to diagnose the issues here as he and I are responsible for that code ... :sweat_smile:

[Emily Riehl]

But I'm a big fan of anything that will ultimately make SSet.HomotopyCategory easier to work with. It now features in the construction of the strict bicategory of quasicategories.

[Joël Riou]

Independently of the refactor of CategoryTheory.Paths, I believe I have found how to make things more practical for doing computations in SSet.HomotopyCategory, in a way that will be consistent with the construction of the fundamental groupoid of a Kan complex, and also get a computable isomorphism for the commutation of hoFunctor to binary products.
https://github.com/joelriou/mathlib4/blob/hofunctor-monoidal/Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean (most of the sorries there should be easy)
May I proceed to the appropriate refactor of SSet.HomotopyCategory?

[Robin Carlier]

I'm not in a huge hurry for refactoring Paths (I have experimented, but will probably finish the thing in ~2 weeks), so I think there won't be "work clashing" here if you proceed.

[Joël Riou]

I have refactored most of the material about the homotopy category of a simplicial set and the nerve adjunction in #31174 (very draft).

[Joël Riou]

In order to make the refactor PR a little bit smaller, the first basic PR is #31248.

[Joël Riou]

The next two are:

• feat(AlgebraicTopology): Edge and CompStruct for 2-truncated simplicial sets #31254

[Joël Riou]

• feat(AlgebraicTopology): inductive construction of StrictSegal structures #31250

[Robin Carlier]

Currently having a look at #31250

[Joël Riou]

Thanks @Robin Carlier for the reviews!

[Joël Riou]

The computable version of the commutation of the homotopy category functor (from simplicial sets or 2-truncated simplicial sets) is now sorry-free #31325