1: \begin{abstract}

2: The $\PiLang$ family of reversible programming languages for boolean circuits is presented as a syntax of combinators

3: witnessing type isomorphisms of algebraic datatypes. In this paper, we give a denotational semantics for this language,

4: using the language of weak groupoids \`{a} la Homotopy Type Theory, and show how to derive an equational theory for it,

5: presented by 2-combinators witnessing equivalences of reversible circuits.

6: 

7: We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent

8: subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the

9: universe, which is shown to be sound and complete for both levels, establishing full abstraction and adequacy. We extend

10: the already established Curry-Howard correspondence for $\PiLang$ to a Curry-Howard-Lambek correspondence between

11: Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of $\PiLang$

12: is presented by the free symmetric rig groupoid, given by finite sets and permutations. Our proof uses techniques from

13: the theory of group presentations and rewriting systems to solve the word problem for symmetric groups.

14: 

15: Using the formalisation of our results, we show how to perform normalisation-by-evaluation, verification, and synthesis

16: of reversible logic gates, motivated by examples from quantum computing.

17: \end{abstract}

18: