English
The product of representative paths lifts to the product of their quotient classes; i.e., prod of ⟦p1⟧ and ⟦p2⟧ equals ⟦p1.prod p2⟧.
Русский
Произведение представительных путей поднимается до произведения их классов; тождество: prod ⟦p1⟧ ⊦p2⟧ = ⟦p1.prod p2⟧.
LaTeX
$$$\mathrm{prod}_\text{lift} : \mathrm{prod}(\langle p_1 \rangle, \langle p_2 \rangle) = \langle p_1.prod p_2 \rangle$$$
Lean4
/-- The product of path classes q₁ and q₂. This is `Path.prod` descended to the quotient. -/
def prod (q₁ : Path.Homotopic.Quotient a₁ a₂) (q₂ : Path.Homotopic.Quotient b₁ b₂) :
Path.Homotopic.Quotient (a₁, b₁) (a₂, b₂) :=
Quotient.map₂ Path.prod (fun _ _ h₁ _ _ h₂ => Nonempty.map2 prodHomotopy h₁ h₂) q₁ q₂
