In this file, the homotopy extension property (HEP) of the pair $(I^n, ∂I^n)$ is derived from the HEP of $(D^n, ∂D^n)$.

instance Cube.boundaryIncl_isCofibration (n : ℕ) : IsCofibration (TopCat.ofHom (boundaryIncl n))

  ∂𝔻 n ---φ---> ∂I^n ------h---> C(I, Y)
  |       ≃       |                |
  i               ι            pathStart
  |               |                |
  v       ≃       v                v
  𝔻 n ----Φ--> I^ (Fin n) ---f---> Y

instance Cube.boundaryIncl_prod_unitInterval_isCofibration (n : ℕ) : IsCofibration (TopCat.ofHom ((boundaryIncl n).prodMap (ContinuousMap.id ↑unitInterval)))

theorem Cube.boundaryIncl_hasHEP (n : ℕ) (Y : Type) [TopologicalSpace Y] : HasHomotopyExtensionProperty (boundaryIncl n) Y

theorem Cube.boundaryIncl_prod_unitInterval_hasHEP (n : ℕ) (Y : Type) [TopologicalSpace Y] : HasHomotopyExtensionProperty ((boundaryIncl n).prodMap (ContinuousMap.id ↑unitInterval)) Y

The universe-polymorphic version of the above theorems

instance TopCat.cubeBoundaryIncl_isCofibration (n : ℕ) : IsCofibration (cubeBoundaryIncl n)

instance TopCat.cubeBoundaryIncl_prod_unitInterval_isCofibration (n : ℕ) : IsCofibration (ofHom ((Hom.hom (cubeBoundaryIncl n)).prodMap (ContinuousMap.id ↑unitInterval)))

theorem TopCat.cubeBoundaryIncl_hasHEP (n : ℕ) (Y : Type u) [TopologicalSpace Y] : HasHomotopyExtensionProperty (Hom.hom (cubeBoundaryIncl n)) Y

theorem TopCat.cubeBoundaryIncl_prod_unitInterval_hasHEP (n : ℕ) (Y : Type u) [TopologicalSpace Y] : HasHomotopyExtensionProperty ((Hom.hom (cubeBoundaryIncl n)).prodMap (ContinuousMap.id ↑unitInterval)) Y