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