∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h₁ : ContinuousMap.HomotopyEquiv X Y) (h₂ : ContinuousMap.HomotopyEquiv Y Z),
  ((h₂.toFun.comp h₁.toFun).comp (h₁.invFun.comp h₂.invFun)).Homotopic (ContinuousMap.id Z)