Theorem SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality

Modification history

2026-01-12 14:46

Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean

feat(AlgebraicTopology): a computable monoidal functor instance for `hoFunctor` (#31325) …

Added SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality View on Github →