English
Every four-step ComposableArrows X is determined by five objects X0,...,X4 and arrows f0,...,f3, such that X is exactly the composite mk4 f0 f1 f2 f3.
Русский
Каждый четырехступенчатый ComposableArrows X задаётся пятью объектами X0,...,X4 и морфизмами f0,...,f3 так, что X есть именно композиция mk4 f0 f1 f2 f3.
LaTeX
$$$\forall X : ComposableArrows C 4,\; \exists X_0,X_1,X_2,X_3,X_4 : C\; \exists f_0:X_0\to X_1\;\exists f_1:X_1\to X_2\;\exists f_2:X_2\to X_3\;\exists f_3:X_3\to X_4,\; X = mk₄ f_0 f_1 f_2 f_3$$$
Lean4
theorem mk₄_surjective (X : ComposableArrows C 4) :
∃ (X₀ X₁ X₂ X₃ X₄ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (f₃ : X₃ ⟶ X₄), X = mk₄ f₀ f₁ f₂ f₃ :=
⟨_, _, _, _, _, X.map' 0 1, X.map' 1 2, X.map' 2 3, X.map' 3 4,
ext₄ rfl rfl rfl rfl rfl (by simp) (by simp) (by simp) (by simp)⟩
