Lemma to_binop_inv_comm_1 {x y : PA} (f g : PA⟦x, y⟧) : to_binop _ _ (to_inv f) g = to_inv (to_binop _ _ f (to_inv g)). Proof. apply (to_rcan (to_binop x y f (to_inv g))). rewrite linvax. rewrite (to_commax' f). rewrite to_assoc. rewrite <- (to_assoc g). rewrite rinvax. rewrite to_lunax'. rewrite linvax. apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Core.Functors.