Def CategoryTheory.Functor.fullyFaithfulCurry₃

Modification history

2025-12-26 18:30

Mathlib/CategoryTheory/Functor/CurryingThree.lean

feat(AlgebraicTopology): prerequisites for the commutation of `HomotopyCategory` with binary products (#33201)

Added CategoryTheory.Functor.fullyFaithfulCurry₃ View on Github →