English
Let f and g be objects in the category of 2-step composable arrows. Suppose we are given three arrows app0, app1, and app2 between corresponding components of f and g, together with two commutativity conditions w0 and w1 expressing the compatibility of these component arrows with the face maps. Then there exists a morphism homMk₂ app0 app1 app2 w0 w1 : f ⟶ g, whose components are precisely app0, app1, and app2, and which satisfies the given coherence relations.
Русский
Пусть f и g — объекты в категории 2‑ступенчатых композиционных стрел. Пусть даны три дуги между соответствующими компонентами f и g: app0, app1, app2, а также две совместимости w0, w1. Тогда существует морфизм homMk₂ app0 app1 app2 w0 w1 : f ⟶ g, компоненты которого равны app0, app1, app2 и который удовлетворяет данному соотношению когерентности.
LaTeX
$$$\\exists \\phi:\\, f \\to g,\\quad \\phi_0 = app_0 \\land \\phi_1 = app_1 \\land \\phi_2 = app_2 \\\\ \\\\ \\\\ (f.map' 0 1 \\gg \\phi_1) = (\\phi_0 \\gg g.map' 0 1) \\land (f.map' 1 2 \\gg \\phi_2) = (\\phi_1 \\gg g.map' 1 2).$$$
Lean4
/-- Constructor for morphisms in `ComposableArrows C 2`. -/
def homMk₂ : f ⟶ g :=
homMkSucc app₀ (homMk₁ app₁ app₂ w₁) w₀
