Commit 2023-02-27 13:06 90a31589

View on Github →

feat: port CategoryTheory.Bicategory.Functor (#2301) Adam gave this me as a challenge at IPAM.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Bicategory/Functor.lean

added structure CategoryTheory.OplaxFunctor.PseudoCore

added def CategoryTheory.OplaxFunctor.comp

added def CategoryTheory.OplaxFunctor.id

added def CategoryTheory.OplaxFunctor.mapFunctor

added structure CategoryTheory.OplaxFunctor

added def CategoryTheory.PrelaxFunctor.comp

added def CategoryTheory.PrelaxFunctor.id

added structure CategoryTheory.PrelaxFunctor

added def CategoryTheory.Pseudofunctor.comp

added def CategoryTheory.Pseudofunctor.id

added def CategoryTheory.Pseudofunctor.mapFunctor

added def CategoryTheory.Pseudofunctor.mkOfOplax

added def CategoryTheory.Pseudofunctor.toOplax

added theorem CategoryTheory.Pseudofunctor.to_oplax_mapComp

added theorem CategoryTheory.Pseudofunctor.to_oplax_mapId

added theorem CategoryTheory.Pseudofunctor.to_oplax_obj

added structure CategoryTheory.Pseudofunctor