English
Let t be a left Kan lift of f and g in a bicategory B, equipped with an IsKan structure H. Then for every left lift s : LeftLift f g, we have t.unit followed by the whisker of H.desc s by f equals s.unit; i.e. t.unit ≫ (H.desc s) ▷ f = s.unit.
Русский
Пусть t — левое кан-образование (левое расширение Канна) маппинга f и g в двоичной теории категорий B, снабжённое структурой IsKan. Тогда для любого левого подъёма s: LeftLift f g выполняется равенство t.unit ≫ (H.desc s) ▷ f = s.unit.
LaTeX
$$$\\forall B\\, [\\text{Bicategory } B], \\ a,b,c \\in B, \\ f: b\\to a, \\ g: c\\to a, \\ t\\in \\text{LeftLift } f\\ g, \\ H:\\ IsKan\\ t, \\ s:\\ LeftLift f g:\\quad t.unit \\;\\gg\\; H.desc\\,s \\,▷\\, f = s.unit.$$$
Lean4
@[reassoc (attr := simp)]
theorem fac (H : IsKan t) (s : LeftLift f g) : t.unit ≫ H.desc s ▷ f = s.unit :=
StructuredArrow.IsUniversal.fac H s
