Def CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁

Modification history

2024-02-11 09:45
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
feat(CategoryTheory): the typeclass Functor.HasRightKanExtension (#10384) …
Added CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁View on Github →