proposition: 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: Proof. induction e. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Core.Functors