proposition: Lemma inv_horizontal_comp {C : prebicategory_id_comp} {a b c : C} {f f' : a -1-> b} {g g' : b -1-> c} (alpha : z_iso f f') (beta : z_iso g g') : (z_iso_inv_from_z_iso alpha) ;hi; (z_iso_inv_from_z_iso beta) = z_iso_inv_from_z_iso (alpha ;hi; beta).
proof: Proof. unfold compose2h_iso. use subtypePath. { intro ; apply isaprop_is_z_isomorphism. } apply idpath. Defined.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.Equivalences.Core