Def CategoryTheory.Functor.fullyFaithfulCurry

Modification history

2025-12-26 18:30
Mathlib/CategoryTheory/Functor/Currying.lean
feat(AlgebraicTopology): prerequisites for the commutation of `HomotopyCategory` with binary products (#33201)
Added CategoryTheory.Functor.fullyFaithfulCurryView on Github →