Interacting Hopf algebras

We introduce the theory IHRIHR of interacting Hopf algebras, parametrised over a principal ideal domain RR. The axioms of IHRIHR are derived using Lack's approach to composing PROPs: they feature two Hopf algebra and two Frobenius algebra structures on four different monoid–comonoid pairs. This construction is instrumental in showing that IHRIHR is isomorphic to the PROP of linear relations (i.e. subspaces) over the field of fractions of RR.