English
If f and g are 3-step arrows and their obj' data agree, and the corresponding maps agree on all face maps, then f=g.
Русский
Если f и g — стрелы из ComposableArrows C 3 и их данные объектов совпадают, а соответствующие отображения совпадают на гранях, то f=g.
LaTeX
$$$\\forall f,g:\\, (f.obj'0 = g.obj'0) \\land (f.obj'1 = g.obj'1) \\land (f.obj'2 = g.obj'2) \\land (f.obj'3 = g.obj'3) \\\\ \\land (f.map'0 1 = \\dots) \\land (f.map'1 2 = \\dots) \\land (f.map'2 3 = \\dots) \\\\Rightarrow f = g$$$
Lean4
theorem ext₃ {f g : ComposableArrows C 3} (h₀ : f.obj' 0 = g.obj' 0) (h₁ : f.obj' 1 = g.obj' 1)
(h₂ : f.obj' 2 = g.obj' 2) (h₃ : f.obj' 3 = g.obj' 3) (w₀ : f.map' 0 1 = eqToHom h₀ ≫ g.map' 0 1 ≫ eqToHom h₁.symm)
(w₁ : f.map' 1 2 = eqToHom h₁ ≫ g.map' 1 2 ≫ eqToHom h₂.symm)
(w₂ : f.map' 2 3 = eqToHom h₂ ≫ g.map' 2 3 ≫ eqToHom h₃.symm) : f = g :=
ext_succ h₀ (ext₂ h₁ h₂ h₃ w₁ w₂) w₀
