A Library of Reversible Circuit Transformations (Work in Progress)

Isomorphisms between finite types directly correspond to combinational, reversible, logical gates. Categorically they are morphisms in special classes of (bi-)monoidal categories. The coherence conditions for these categories determine sound and complete equivalences between isomorphisms. These equivalences were previously shown to correspond to a second-level of isomorphisms between the gate-modeling isomorphisms. In this work-in-progress …