Def CategoryTheory.Functor.RightExtension.postcomp₁

Modification history

2024-05-24 09:21

Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean

feat(CategoryTheory): transport Kan extensions via equivalences (#12785) …

Added CategoryTheory.Functor.RightExtension.postcomp₁ View on Github →