This module is based on the content of the functional pearl How to Take the Inverse of a Type by Daniel Marshall and Dominic Orchard
Quadruple : Type -> Type