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. unfold compose2h_iso. use subtypePath. { intro ; apply isaprop_is_z_isomorphism. } apply idpath. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.Equivalences.Core.