English
Given two CompTriples κ and κ', the two ways of composing yield an equivalent CompTriple: CompTriple φ1 φ23 φ123 ↔ CompTriple φ12 φ3 φ123.
Русский
Дано два CompTriple κ и κ', две способы сочетания дают эквивалентный CompTriple: CompTriple φ1 φ23 φ123 ↔ CompTriple φ12 φ3 φ123.
LaTeX
$$$$ \text{CompTriple }(\varphi_1, \varphi_{23}, \varphi_{123}) \iff \text{CompTriple }(\varphi_{12}, \varphi_3, \varphi_{123}). $$$$
Lean4
theorem comp_assoc {Q : Type*} [Monoid Q] {φ₁ : M →* N} {φ₂ : N →* P} {φ₁₂ : M →* P} (κ : CompTriple φ₁ φ₂ φ₁₂)
{φ₃ : P →* Q} {φ₂₃ : N →* Q} (κ' : CompTriple φ₂ φ₃ φ₂₃) {φ₁₂₃ : M →* Q} :
CompTriple φ₁ φ₂₃ φ₁₂₃ ↔ CompTriple φ₁₂ φ₃ φ₁₂₃ := by
constructor <;>
· rintro ⟨h⟩
exact ⟨by simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]⟩
