Commit 2025-12-17 16:11 07ecd39a

View on Github →

feat(CategoryTheory/Cat/Basic): Turning 1- and 2-morphisms in Cat into a 1-field structure (#31807) This PR defines Cat.Hom and Cat.Hom₂, which are 1-field structures wrapping Functor and NatTrans respectively. In addition, it changes the Bicategory instance for Cat to use these wrappers instead. This PR adds such definitions as NatTrans.toCatHom2, Cat.Hom.toFunctor, Cat.Hom₂.toNatTrans, Cat.Hom.isoMk as well as simp lemmas for normalizing these to operations.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Pseudofunctor.lean

Modified Mathlib/AlgebraicTopology/Quasicategory/StrictBicategory.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

Modified Mathlib/CategoryTheory/Bicategory/CatEnriched.lean

modified theorem CategoryTheory.CatEnriched.id_eq

Modified Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean

Modified Mathlib/CategoryTheory/Bicategory/Grothendieck.lean

Modified Mathlib/CategoryTheory/Category/Cat.lean

added theorem CategoryTheory.Cat.Hom.comp_map

added theorem CategoryTheory.Cat.Hom.comp_obj

added theorem CategoryTheory.Cat.Hom.comp_toFunctor

added def CategoryTheory.Cat.Hom.equivFunctor

added theorem CategoryTheory.Cat.Hom.id_map

added theorem CategoryTheory.Cat.Hom.id_obj

added theorem CategoryTheory.Cat.Hom.id_toFunctor

added def CategoryTheory.Cat.Hom.isoMk

added theorem CategoryTheory.Cat.Hom.isoMk_toNatIso

added def CategoryTheory.Cat.Hom.toNatIso

added theorem CategoryTheory.Cat.Hom.toNatIso_associator

added theorem CategoryTheory.Cat.Hom.toNatIso_isoMk

added theorem CategoryTheory.Cat.Hom.toNatIso_leftUnitor

added theorem CategoryTheory.Cat.Hom.toNatIso_rightUnitor

added theorem CategoryTheory.Cat.Hom.toNatTrans_comp

added theorem CategoryTheory.Cat.Hom.toNatTrans_id

added structure CategoryTheory.Cat.Hom

added theorem CategoryTheory.Cat.Hom₂.comp_app

added theorem CategoryTheory.Cat.Hom₂.eqToHom_toNatTrans

added theorem CategoryTheory.Cat.Hom₂.ext

added theorem CategoryTheory.Cat.Hom₂.id_app

added structure CategoryTheory.Cat.Hom₂

added theorem CategoryTheory.Cat.associator_hom_toNatTrans

added theorem CategoryTheory.Cat.associator_inv_toNatTrans

deleted theorem CategoryTheory.Cat.comp_app

modified theorem CategoryTheory.Cat.comp_eq_comp

deleted theorem CategoryTheory.Cat.comp_map

deleted theorem CategoryTheory.Cat.comp_obj

modified theorem CategoryTheory.Cat.eqToHom_app

modified theorem CategoryTheory.Cat.ext

deleted theorem CategoryTheory.Cat.id_app

modified theorem CategoryTheory.Cat.id_eq_id

deleted theorem CategoryTheory.Cat.id_map

deleted theorem CategoryTheory.Cat.id_obj

modified theorem CategoryTheory.Cat.leftUnitor_hom_app

added theorem CategoryTheory.Cat.leftUnitor_hom_toNatTrans

modified theorem CategoryTheory.Cat.leftUnitor_inv_app

added theorem CategoryTheory.Cat.leftUnitor_inv_toNatTrans

modified theorem CategoryTheory.Cat.rightUnitor_hom_app

added theorem CategoryTheory.Cat.rightUnitor_hom_toNatTrans

modified theorem CategoryTheory.Cat.rightUnitor_inv_app

added theorem CategoryTheory.Cat.rightUnitor_inv_toNatTrans

modified theorem CategoryTheory.Cat.whiskerLeft_app

added theorem CategoryTheory.Cat.whiskerLeft_toNatTrans

modified theorem CategoryTheory.Cat.whiskerRight_app

added theorem CategoryTheory.Cat.whiskerRight_toNatTrans

added def CategoryTheory.Functor.equivCatHom

deleted def CategoryTheory.Functor.ofCatHom

deleted theorem CategoryTheory.Functor.of_toCatHom

modified def CategoryTheory.Functor.toCatHom

deleted theorem CategoryTheory.Functor.to_ofCatHom

added def CategoryTheory.NatTrans.toCatHom₂

added theorem CategoryTheory.NatTrans.toCatHom₂_comp

added theorem CategoryTheory.NatTrans.toCatHom₂_id

Modified Mathlib/CategoryTheory/Category/Cat/Adjunction.lean

Modified Mathlib/CategoryTheory/Category/Cat/AsSmall.lean

Modified Mathlib/CategoryTheory/Category/Cat/CartesianClosed.lean

Modified Mathlib/CategoryTheory/Category/Cat/Limit.lean

modified def CategoryTheory.Cat.HasLimits.limitConeLift

Modified Mathlib/CategoryTheory/Category/Cat/Op.lean

Modified Mathlib/CategoryTheory/Category/Cat/Terminal.lean

Modified Mathlib/CategoryTheory/Category/Grpd.lean

Modified Mathlib/CategoryTheory/Category/Quiv.lean

Modified Mathlib/CategoryTheory/Category/ReflQuiv.lean

Modified Mathlib/CategoryTheory/CodiscreteCategory.lean

Modified Mathlib/CategoryTheory/Comma/Over/Basic.lean

Modified Mathlib/CategoryTheory/Comma/StructuredArrow/Final.lean

Modified Mathlib/CategoryTheory/Comma/StructuredArrow/Functor.lean

Modified Mathlib/CategoryTheory/Elements.lean

Modified Mathlib/CategoryTheory/FiberedCategory/Grothendieck.lean

Modified Mathlib/CategoryTheory/Filtered/Grothendieck.lean

Modified Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean

Modified Mathlib/CategoryTheory/Grothendieck.lean

modified def CategoryTheory.Grothendieck.mapIdIso

modified theorem CategoryTheory.Grothendieck.map_id_eq

modified def CategoryTheory.Grothendieck.ιCompMap

modified def CategoryTheory.Grothendieck.ιNatTrans

Modified Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean

modified theorem CategoryTheory.Grpd.free_map

Modified Mathlib/CategoryTheory/IsomorphismClasses.lean

Modified Mathlib/CategoryTheory/Join/Pseudofunctor.lean

Modified Mathlib/CategoryTheory/Limits/Final.lean

modified theorem CategoryTheory.Grothendieck.final_map

Modified Mathlib/CategoryTheory/Limits/Shapes/Grothendieck.lean

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Cat.lean

modified def CategoryTheory.Cat.chosenTerminalIsTerminal

modified theorem CategoryTheory.Monoidal.leftUnitor_hom

modified theorem CategoryTheory.Monoidal.leftUnitor_inv

modified theorem CategoryTheory.Monoidal.rightUnitor_hom

modified theorem CategoryTheory.Monoidal.rightUnitor_inv

modified theorem CategoryTheory.Monoidal.whiskerLeft

Modified Mathlib/CategoryTheory/SingleObj.lean

Modified Mathlib/CategoryTheory/Sites/Descent/DescentData.lean

Modified Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean

Modified Mathlib/CategoryTheory/Sites/PseudofunctorSheafOver.lean

Modified Mathlib/CategoryTheory/WithTerminal/Basic.lean

Modified Mathlib/Order/Category/Preord.lean

Modified Mathlib/Tactic/CategoryTheory/ToApp.lean

added def CategoryTheory.toNatTransExpr

Modified MathlibTest/CategoryTheory/ToApp.lean