Theorem SSet.Truncated.HomotopyCategory.square

Modification history

2026-01-12 14:46
Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean
feat(AlgebraicTopology): a computable monoidal functor instance for `hoFunctor` (#31325) …
Deleted SSet.Truncated.HomotopyCategory.squareView on Github →
2025-12-26 18:30
Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean
feat(AlgebraicTopology): prerequisites for the commutation of `HomotopyCategory` with binary products (#33201)
Added SSet.Truncated.HomotopyCategory.squareView on Github →