IsKan

Mathlib.CategoryTheory.Bicategory.Kan.IsKan

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bicategory.RightExtension.IsKan

Lean4

/-- A right Kan extension of `g` along `f` is a terminal object in `RightExtension f g`. -/
abbrev IsKan (t : RightExtension f g) :=
  t.IsUniversal

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru