Lemma X_aux_type_center_of_contr_proof (b : B) (anot : A) (hnot : z_iso (H anot) b) : ∏ (t t' : total2 (λ a : A, z_iso (H a) b)) (f : pr1 t --> pr1 t'), #H f· pr2 t' = pr2 t -> #F f· #F (fH^-1 (pr2 t'· inv_from_z_iso hnot)) = #F (fH^-1 (pr2 t· inv_from_z_iso hnot)). Proof. intros t t' f. destruct t as [a h]. destruct t' as [a' h']. simpl in *. intro star. rewrite <- functor_comp. apply maponpaths. apply (invmaponpathsweq (weq_from_fully_faithful fH a anot)). simpl. rewrite functor_comp. inv_functor fH a' anot. rewrite assoc. inv_functor fH a anot. rewrite <- star. apply idpath. 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.