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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.TotalCategoryFacts. Require Import UniMath.CategoryTheory.precomp_fully_faithful. Require Import UniMath.CategoryTheory.DaggerCategories.Categories. Require Import UniMath.CategoryTheory.DaggerCategories.Functors. Require Import UniMath.CategoryTheory.DaggerCategories.Transformations. Require Import UniMath.CategoryTheory.DaggerCategories.Unitary. Require Import UniMath.CategoryTheory.DaggerCategories.Univalence. Require Import UniMath.CategoryTheory.DaggerCategories.FunctorCategory. Require Import UniMath.CategoryTheory.DaggerCategories.Functors.FullyFaithful. Require Import UniMath.CategoryTheory.DaggerCategories.Functors.WeakEquivalences.