English
Extensionality for five-step arrows: if five vertex equalities hold and five map equalities hold, then f = g.
Русский
Экстенсиональность для пятиступенчатых стрелок: при соблюдении пяти равенств вершин и пяти равенств отображений получаем равенство f = g.
LaTeX
$$$\forall f,g : ComposableArrows C 5, (h_0: f.obj' 0 = g.obj' 0) \dots (h_5: f.obj' 5 = g.obj' 5) \Rightarrow (w_0: f.map' 0 1 = eqToHom h_0 ≫ g.map' 0 1 ≫ eqToHom h_1.symm) \dots (w_4: f.map' 4 5 = eqToHom h_4 ≫ g.map' 4 5 ≫ eqToHom h_5.symm) \Rightarrow f = g$$$
Lean4
theorem ext₅ {f g : ComposableArrows C 5} (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) (h₅ : f.obj' 5 = g.obj' 5)
(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)
(w₄ : f.map' 4 5 = eqToHom h₄ ≫ g.map' 4 5 ≫ eqToHom h₅.symm) : f = g :=
ext_succ h₀ (ext₄ h₁ h₂ h₃ h₄ h₅ w₁ w₂ w₃ w₄) w₀
