Commit 2024-02-20 22:17 55a538bd

View on Github →

feat(CategoryTheory/WithTerminal): Add pseudofunctors (#10533) Defined the pseudofunctors from Cat to Cat induced by WithTerminal and WithInitial.

Estimated changes

Modified Mathlib/CategoryTheory/WithTerminal.lean

added def CategoryTheory.WithInitial.mapComp

added def CategoryTheory.WithInitial.mapId

added def CategoryTheory.WithInitial.map₂

added def CategoryTheory.WithInitial.pseudofunctor

added def CategoryTheory.WithTerminal.mapComp

added def CategoryTheory.WithTerminal.mapId

added def CategoryTheory.WithTerminal.map₂

added def CategoryTheory.WithTerminal.pseudofunctor