Spectrum homotopy (source code)

= Spectrum homotopy

A <spectrum homotopy> between compatible maps $D\to E$ is a map from the cylinder spectrum $D\wedge[0,1]_+$ restricting to them at the endpoints. Thus the homotopies at all levels must themselves respect the structure maps.