Def CategoryTheory.Bicategory.Adj.forget₁

Modification history

2025-11-03 17:34
Mathlib/CategoryTheory/Bicategory/Adjunction/Adj.lean
chore(Pseudofunctor): add notation of pseudofunctors (#31171) …
Modified CategoryTheory.Bicategory.Adj.forget₁View on Github →
2025-06-25 10:15
Mathlib/CategoryTheory/Bicategory/Adjunction/Adj.lean
feat: the bicategory of adjunctions in a bicategory (#25977) …
Added CategoryTheory.Bicategory.Adj.forget₁View on Github →