proposition: 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: Proof. set (i1 := make_iso f H1). set (i2 := make_iso g H2). exact (is_iso_comp_of_isos i1 i2). Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories