Lemma Y_contr_eq (b b' : B) (f : b --> b') (a0 : A) (h0 : z_iso (H a0) b) (a0' : A) (h0' : z_iso (H a0') b') : ∏ t : Y f, t = Y_inhab b b' f a0 h0 a0' h0'. Proof. intro t. apply pathsinv0. assert (Hpr : pr1 (Y_inhab b b' f a0 h0 a0' h0') = pr1 t). destruct t as [g1 r1]; simpl in *. rewrite <- assoc. apply z_iso_inv_on_right. set (hfh := h0 · f · inv_from_z_iso h0'). set (l0 := fH^-1 hfh). apply (r1 a0 h0 a0' h0' l0). unfold l0. inv_functor fH a0 a0' . unfold hfh. repeat rewrite <- assoc. rewrite z_iso_after_z_iso_inv, id_right. apply idpath. apply (total2_paths_f Hpr). apply proofirrelevance. repeat (apply impred; intro). apply C. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. 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.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering.