English
For p, q, r paths, one has equality of concatenations after the reparametrization by trans_assoc_reparam.
Русский
Для путей p, q, r выполняется равенство склейки после переparamетризации trans_assoc_reparam.
LaTeX
$$$$ (p.trans q).trans r = (p.trans (q.trans r)).reparam \\Bigl( \\lambda t. \\langle \\mathrm{transAssocReparamAux}(t), \\mathrm{transAssocReparamAux\\_mem\\_I}(t)\\rangle \\Bigr) $$$$
Lean4
/-- For paths `p q r`, we have a homotopy from `(p.trans q).trans r` to `p.trans (q.trans r)`. -/
def transAssoc {x₀ x₁ x₂ x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃) :
Homotopy ((p.trans q).trans r) (p.trans (q.trans r)) :=
((Homotopy.reparam (p.trans (q.trans r)) (fun t => ⟨transAssocReparamAux t, transAssocReparamAux_mem_I t⟩)
(by fun_prop) (Subtype.ext transAssocReparamAux_zero) (Subtype.ext transAssocReparamAux_one)).cast
rfl (trans_assoc_reparam p q r).symm).symm
