Def CategoryTheory.Functor.rightExtensionEquivalenceOfIso₁

Modification history

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