English
Extensionality for five-step composable arrows: equality is determined by vertex equalities and matching five map components through appropriate equalities.
Русский
Экстенсиональность для пятиступенчатых стрелок: равенство определяется равенствами вершин и совпадением пяти компонент отображений через соответствующие равенства.
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
@[ext]
theorem hom_ext₅ {f g : ComposableArrows C 5} {φ φ' : f ⟶ g} (h₀ : app' φ 0 = app' φ' 0) (h₁ : app' φ 1 = app' φ' 1)
(h₂ : app' φ 2 = app' φ' 2) (h₃ : app' φ 3 = app' φ' 3) (h₄ : app' φ 4 = app' φ' 4) (h₅ : app' φ 5 = app' φ' 5) :
φ = φ' :=
hom_ext_succ h₀ (hom_ext₄ h₁ h₂ h₃ h₄ h₅)
