Def CategoryTheory.Functor.RightExtension.precomp

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.precomp View on Github →