Lemma transport_source_to_binop {x y z : ob PA} (f g : y --> z) (e : y = x) : to_binop _ _ (transportf (λ x' : ob PA, precategory_morphisms x' z) e f) (transportf (λ x' : ob PA, precategory_morphisms x' z) e g) = transportf (λ x' : ob PA, precategory_morphisms x' z) e (to_binop _ _ f g). Proof. induction e. 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.