Def CategoryTheory.hoFunctor.unitHomEquiv

Modification history

2026-01-12 14:46
Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
feat(AlgebraicTopology): a computable monoidal functor instance for `hoFunctor` (#31325) …
Deleted CategoryTheory.hoFunctor.unitHomEquivView on Github →
2025-11-23 17:11
Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
feat(Algebraic Topology): the strict bicategory of quasicategories (#31101) …
Added CategoryTheory.hoFunctor.unitHomEquivView on Github →