IsKan

Mathlib.CategoryTheory.Bicategory.Kan.IsKan

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

Lean4

/-- A left Kan lift of `g` along `f` is an initial object in `LeftLift f g`. -/
abbrev IsKan (t : LeftLift f g) :=
  t.IsUniversal

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

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

Разделы

Аффилиация

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