∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Y, Z)} (G : g₀.Homotopy g₁) (F : f₀.Homotopy f₁)
  (x : ↑unitInterval × X), (G.comp F) x = G (x.1, F x)