Commit 2025-12-05 11:03 f337188d

refactor(AlgebraicTopology): refactor the homotopy category and the nerve adjunction (#31174) This PR completely refactors the adjunction between quivers and reflexive quivers, the homotopy category of a simplicial set, and the adjunction between (2-truncated) simplicial sets and Cat (which involves the homotopy category of a simplicial set and the nerve of a category). The general principle which is applied here is that for any (strictly functorial) construction involving quivers, refl. quivers or categories, the constructions and the basic API are first done in the unbundled setting (a type with a Category/Quiver/... instance), and only at the very end, the functors involving Cat/Quiv/... and the adjunctions are defined in the bundled situation. This gives cleaner code and improves automation. The adjunctions are now constructed by defining the homEquiv rather than by constructing the unit/counit. This emphasizes a little bit more the universal properties of the constructions. The unit/counit can be recovered from the homEquiv (and it seems they are definitionally to the previous definitions).