English
Extensionality for four-step composable arrows: two such arrows are equal if and only if their corresponding vertex objects are equal and their four connecting maps coincide up to the obvious conjugation by equalities on the vertices.
Русский
Экстенсиональность для четырехступенчатых композиционных стрел: два таких стрелки равны тогда и только тогда, когда равны их вершины и соответствующие четыре отображения между ними совпадают с учётом эквивалентностей на вершинах.
LaTeX
$$$\forall f,g : \text{ComposableArrows } C\ 4,\; (h_0 : f.obj' 0 = g.obj' 0) (h_1 : f.obj' 1 = g.obj' 1) (h_2 : f.obj' 2 = g.obj' 2) (h_3 : f.obj' 3 = g.obj' 3) (h_4 : f.obj' 4 = g.obj' 4) \\\quad (w_0 : f.map' 0 1 = eqToHom h_0 ≫ g.map' 0 1 ≫ eqToHom h_1.symm) \\\quad (w_1 : f.map' 1 2 = eqToHom h_1 ≫ g.map' 1 2 ≫ eqToHom h_2.symm) \\\quad (w_2 : f.map' 2 3 = eqToHom h_2 ≫ g.map' 2 3 ≫ eqToHom h_3.symm) \\\quad (w_3 : f.map' 3 4 = eqToHom h_3 ≫ g.map' 3 4 ≫ eqToHom h_4.symm) \\Rightarrow f = g$$$
Lean4
theorem ext₄ {f g : ComposableArrows C 4} (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) (h₄ : f.obj' 4 = g.obj' 4)
(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)
(w₃ : f.map' 3 4 = eqToHom h₃ ≫ g.map' 3 4 ≫ eqToHom h₄.symm) : f = g :=
ext_succ h₀ (ext₃ h₁ h₂ h₃ h₄ w₁ w₂ w₃) w₀
