proposition: Lemma X_aux_type_contr_eq (b : D) (anot : C) (hnot : unitary dagD (H anot) b) (Euniv : is_univalent_dagger dagE) : ∏ 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 := daggerisotoid Euniv ((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 _ _ (unitary_comp h (unitary_inv hnot))). set (qhelp := q1 (tpair _ a h)(tpair _ anot hnot) (pr1 gah)). simpl in *. assert (feedtoqhelp : #H (fH^-1 (pr1 h · pr1 (unitary_inv hnot)))· pr1 hnot = pr1 h). { inv_functor fH a anot. refine (assoc' _ _ _ @ _ @ id_right _). apply maponpaths. exact (pr22 hnot). } assert (quack := qhelp feedtoqhelp). simpl in *. intermediate_path (unitary_comp (dagger_functor_on_unitary dagF _ _ (fH^-i _ _ (unitary_comp h (unitary_inv hnot)))) (idtodaggeriso _ _ _ w) ). - generalize w; intro w0. induction w0. apply unitary_eq. apply pathsinv0, id_right. - apply unitary_eq. simpl. unfold w. refine (_ @ quack). do 2 apply maponpaths. apply idtodaggeriso_daggerisotoid. } apply pathsinv0. apply (total2_paths_f Hpr1). apply proofirrelevance. repeat (apply impred; intro). apply homset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.TotalCategoryFacts UniMath.CategoryTheory.precomp_fully_faithful UniMath.CategoryTheory.DaggerCategories.Categories UniMath.CategoryTheory.DaggerCategories.Functors UniMath.CategoryTheory.DaggerCategories.Transformations UniMath.CategoryTheory.DaggerCategories.Unitary UniMath.CategoryTheory.DaggerCategories.Univalence UniMath.CategoryTheory.DaggerCategories.FunctorCategory UniMath.CategoryTheory.DaggerCategories.Functors.FullyFaithful UniMath.CategoryTheory.DaggerCategories.Functors.WeakEquivalences