See the slides about “downcasing types” at this link - especially the pages called “Cartesianness (2)” and “Cleavages”.