  The $\mathit{\Pi}$ family of reversible programming languages for boolean
circuits is presented as a syntax of combinators witnessing type isomorphisms
of algebraic datatypes. In this paper, we give a denotational semantics for
this language, using the language of weak groupoids \`a la Homotopy Type
Theory, and show how to derive an equational theory for it, presented by
2-combinators witnessing equivalences of reversible circuits. We establish a
correspondence between the syntactic groupoid of the language and a formally
presented univalent subuniverse of finite types. The correspondence relates
1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which
is shown to be sound and complete for both levels, establishing full
abstraction and adequacy. We extend the already established Curry-Howard
correspondence for $\mathit{\Pi}$ to a Curry-Howard-Lambek correspondence
between Reversible Logic, Reversible Programming Languages, and Symmetric Rig
Groupoids, by showing that the syntax of $\mathit{\Pi}$ is presented by the
free symmetric rig groupoid, given by finite sets and permutations. Our proof
uses techniques from the theory of group presentations and rewriting systems to
solve the word problem for symmetric groups. Using the formalisation of our
results, we show how to perform normalisation-by-evaluation, verification, and
synthesis of reversible logic gates, motivated by examples from quantum
computing.
