Commit 2025-02-26 16:56 713a397b
View on Github →feat(AlgebraicTopology/NerveAdjunction): nerve adjunction infrastructure (#21885)
This develops preliminaries for the construction of the adjunction between the 2-truncated nerve and the 2-truncated homotopy category functor. The key technical result is toNerve₂.mk and toNerve₂.ext, which demonstrates that a map of 2-truncated simplicial sets valued in a 2-truncated nerve is determined uniquely by the underlying refl prefunctor provided a composition hypothesis is met.