Rig categories provide a categorical foundation for the semantics of quantum programming languages, but their formalisation in Agda is hindered by the treatment of monoidal structures as \emph{weak}: every structural equation must be stated explicitly, even when it carries no computational content. Because rig categories involve a large number of coherence conditions, formal proofs quickly become overwhelmed by structural bookkeeping.

Here, we show that Agda’s rewrite rule feature can be used to overcome this problem. By promoting selected structural equivalences to definitional equalities, we effectively model semi-strict rig categories (known as bipermutative categories), allowing proofs to focus on computationally meaningful content.

We demonstrate this approach on $\sqrt\Pi$, a computationally universal intermediate language for unitary quantum programming equipped with a complete equational theory for standard gate sets. In Agda, proofs of identities in $\sqrt\Pi$ follow the same structure as their pen-and-paper counterparts, without explicit structural rearrangements.