Homotopy of Morphisms of Species of Types [008V]

Let and be species of types and let and be morphisms of species of types between and . We define the type of homotopies between and as the type of pointwise homotopies, in symbols .