proposition: Lemma X_aux_type_contr_eq (b : B) (anot : A) (hnot : z_iso (H anot) b) : ∏ t : X b, t = X_aux_type_center_of_contr b anot hnot.
proof: Proof. intro t. assert (Hpr1 : pr1 (X_aux_type_center_of_contr b anot hnot) = pr1 t). { set (w := isotoid _ Ccat ((pr2 (pr1 t)) anot hnot) : pr1 (pr1 (X_aux_type_center_of_contr b anot hnot)) = pr1 (pr1 t)). apply (total2_paths_f w). simpl. destruct t as [[c1 k1] q1]. simpl in *. apply funextsec; intro a. apply funextsec; intro h. set (gah := fH^-i (z_iso_comp h (z_iso_inv_from_z_iso hnot))). set (qhelp := q1 (tpair _ a h)(tpair _ anot hnot) gah). simpl in *. assert (feedtoqhelp : #H (fH^-1 (h· inv_from_z_iso hnot))· hnot = h). { inv_functor fH a anot. rewrite <- assoc. rewrite z_iso_after_z_iso_inv. apply id_right. } assert (quack := qhelp feedtoqhelp). simpl in *. intermediate_path (z_iso_comp (functor_on_z_iso F (fH^-i (z_iso_comp h (z_iso_inv_from_z_iso hnot)))) (idtoiso w) ). { generalize w; intro w0. induction w0. simpl. apply z_iso_eq. simpl. simpl. rewrite id_right. apply idpath. } apply z_iso_eq. simpl. unfold w. rewrite idtoiso_isotoid. apply quack. } apply pathsinv0. apply (total2_paths_f Hpr1). apply proofirrelevance. repeat (apply impred; intro). apply C. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering