Commit 2024-07-11 15:48 37031938

View on Github →

feat(Bicategory/Functor/Lax): define lax functors (#14303) We define lax functors and provide ways to construct pseudofunctors from a given a lax functor.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean

added structure CategoryTheory.LaxFunctor.PseudoCore

added def CategoryTheory.LaxFunctor.comp

added def CategoryTheory.LaxFunctor.id

added theorem CategoryTheory.LaxFunctor.mapComp_assoc_left

added theorem CategoryTheory.LaxFunctor.mapComp_assoc_right

added theorem CategoryTheory.LaxFunctor.map₂_leftUnitor_hom

added theorem CategoryTheory.LaxFunctor.map₂_rightUnitor_hom

added structure CategoryTheory.LaxFunctor

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

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

added def CategoryTheory.Pseudofunctor.mkOfLax

added def CategoryTheory.Pseudofunctor.toLax

deleted theorem CategoryTheory.Pseudofunctor.to_oplax_map

deleted theorem CategoryTheory.Pseudofunctor.to_oplax_mapComp

deleted theorem CategoryTheory.Pseudofunctor.to_oplax_mapId

deleted theorem CategoryTheory.Pseudofunctor.to_oplax_map₂

deleted theorem CategoryTheory.Pseudofunctor.to_oplax_obj

Modified Mathlib/CategoryTheory/WithTerminal.lean