English
Two 2-morphisms with source and target t.lift into k are equal if their whiskerings with the associated triangle 2-morphisms are equal; i.e., equality of the 2-morphisms is detected by their whiskered composites with the left Kan lift’s unit.
Русский
Две 2-морфизмы с источником и мишенью t.lift в k равны, если их обходы через соответствующие треугольные 2-морфизмы совпадают; то есть равенство 2-морфизмов определяется их обходами.
LaTeX
$$$\\forall B,\\ a,b,c, {f,g:\\ t.lift\\to k}, \\ H:\\ IsKan\\ t:\\quad w:\\ t.unit \\;≫\\; τ \\;▷ f = t.unit \\;≫\\; τ' \\;▷ f \\Rightarrow τ = τ'. $$$
Lean4
/-- Two 2-morphisms out of a left Kan lift are equal if their compositions with
each triangle 2-morphism are equal. -/
theorem hom_ext (H : IsKan t) {k : c ⟶ b} {τ τ' : t.lift ⟶ k} (w : t.unit ≫ τ ▷ f = t.unit ≫ τ' ▷ f) : τ = τ' :=
StructuredArrow.IsUniversal.hom_ext H w
