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. 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.
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.