Lemma is_iso_comp_of_is_isos {C : precategory} {a b c : ob C} (f : a --> b) (g : b --> c) (H1 : is_iso f) (H2 : is_iso g) : is_iso (f · g). Proof. set (i1 := make_iso f H1). set (i2 := make_iso g H2). exact (is_iso_comp_of_isos i1 i2). 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.