English
For any p, q, r, there exists a homotopy witnessing that (p trans q) trans r is equal to p trans (q trans r).
Русский
Для любых путей p, q, r существует гомотопия, доказывающая, что (p⋆q)⋆r равно p⋆(q⋆r).
LaTeX
$$$$ (p \\trans q) \\trans r = (p \\trans (q \\trans r)).reparam\\bigl( t \\mapsto \\langle \\mathrm{TransAssocReparamAux}(t), \\mathrm{TransAssocReparamAux\\_mem\\_I}(t) \\rangle \\bigr). $$$$
Lean4
instance : CategoryTheory.Groupoid (FundamentalGroupoid X)
where
Hom x y := Path.Homotopic.Quotient x.as y.as
id x := ⟦Path.refl x.as⟧
comp {_ _ _} := Path.Homotopic.Quotient.comp
id_comp {x _}
f :=
Quotient.inductionOn f fun a =>
show ⟦(Path.refl x.as).trans a⟧ = ⟦a⟧ from Quotient.sound ⟨Path.Homotopy.reflTrans a⟩
comp_id {_ y}
f :=
Quotient.inductionOn f fun a =>
show ⟦a.trans (Path.refl y.as)⟧ = ⟦a⟧ from Quotient.sound ⟨Path.Homotopy.transRefl a⟩
assoc {_ _ _ _} f g
h :=
Quotient.inductionOn₃ f g h fun p q r =>
show ⟦(p.trans q).trans r⟧ = ⟦p.trans (q.trans r)⟧ from Quotient.sound ⟨Path.Homotopy.transAssoc p q r⟩
inv {x y}
p :=
Quotient.lift (fun l : Path x.as y.as => ⟦l.symm⟧)
(by
rintro a b ⟨h⟩
simp only
rw [Quotient.eq]
exact ⟨h.symm₂⟩)
p
inv_comp {_ y}
f :=
Quotient.inductionOn f fun a =>
show ⟦a.symm.trans a⟧ = ⟦Path.refl y.as⟧ from Quotient.sound ⟨(Path.Homotopy.reflSymmTrans a).symm⟩
comp_inv {x _}
f :=
Quotient.inductionOn f fun a =>
show ⟦a.trans a.symm⟧ = ⟦Path.refl x.as⟧ from Quotient.sound ⟨(Path.Homotopy.reflTransSymm a).symm⟩
