∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ p₂ : Path x₀ x₁} (F : p₀.Homotopy p₁) (G : p₁.Homotopy p₂)
  (x : ↑unitInterval × ↑unitInterval),
  (F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)