Lemma transport_source_to_inv {x y z : ob PA} (f : y --> z) (e : y = x) : to_inv (transportf (λ x' : ob PA, precategory_morphisms x' z) e f) = transportf (λ x' : ob PA, precategory_morphisms x' z) e (to_inv f). 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.