Lemma are_inverse_comp_of_inverses {C : precategory} (a b c : C) (f : z_iso a b) (g : z_iso b c) : is_inverse_in_precat (f · g) (inv_from_z_iso g · inv_from_z_iso f). Proof. apply is_inverse_in_precat_comp. - apply (pr2 f). - apply (pr2 g). Qed.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories.