A.19:5.2.1.1 - Subspace — projection

For a space CS_I with basis I and a subset S, the projection pi_S^I : CS_I -> CS_S keeps the Coordinates in S and discards the others. The type-correct laws are pi_I^I = identity_CS_I and, for T subseteq S subseteq I, pi_T^S after pi_S^I = pi_T^I. A projection preserves an order, topology, or other structure only when that fact follows from the named overlays; projection alone makes no such promise.