Lemma is_preimage_for_pre_composition : functor_composite H GG = F. Proof. apply (functor_eq _ _ E (functor_composite H GG) F). apply (total2_paths_f extphi). apply funextsec; intro a0; apply funextsec; intro a0'; apply funextsec; intro f. rewrite FunctorCategory.transport_of_functor_map_is_pointwise. unfold extphi. unfold Univalence.double_transport. rewrite toforallpaths_funextsec. rewrite <- Univalence.idtoiso_postcompose. rewrite <- Univalence.idtoiso_precompose. rewrite Univalence.idtoiso_inv. rewrite <- assoc. assert (PSIf : ∏ (a : C) (h : unitary _ (H a) (H a0)) (a' : C) (h' : unitary _ (H a') (H a0')) (l : a --> a'), #H l· h' = h· #H f -> #F l· k (H a0') a' h' = k (H a0) a h· ((pr1 (idtodaggeriso dagE _ _ (phi a0)) · #F f) · unitary_inv (idtodaggeriso dagE _ _ (phi a0')))). { intros a h a' h' l alpha. rewrite assoc. apply unitary_inv_on_left. { apply idtodaggeriso. } unfold phi. repeat rewrite assoc. rewrite (Xkphi_idtoiso (H a0) (XtripleF a0)). repeat rewrite <- assoc. rewrite (Xkphi_idtoiso (H a0') (XtripleF a0')). simpl. assert (HH4 : fH^-1 h · f = l · fH^-1 h'). { apply (invmaponpathsweq (weq_from_fully_faithful fH a a0')). simpl; repeat rewrite functor_comp. inv_functor fH a a0. inv_functor fH a' a0'. apply pathsinv0, alpha. } intermediate_path (#F (fH^-1 h· f)). { now rewrite functor_comp. } rewrite HH4. now rewrite functor_comp. } set (Ybla := tpair _ (idtodaggeriso _ _ _ (phi a0) · #F f · unitary_inv (idtodaggeriso _ _ _ (phi a0'))) PSIf : Y (#H f)). set (Ycontr := pr2 (Y_iscontr _ _ (#(pr1 H) f)) Ybla). set (Ycontr2 := base_paths _ _ Ycontr); simpl in *. change (H a0) with (pr1 H a0). change (H a0') with (pr1 H a0'). change (G (#H f)) with (G (#(pr1 H) f)). change (#H f) with (# (pr1 H) f). rewrite <- Ycontr2. repeat rewrite assoc. etrans. { do 3 apply maponpaths_2. refine (_ @ idpath (identity _)). generalize (phi a0). intro p ; induction p ; apply id_right. } rewrite id_left. repeat rewrite <- assoc. etrans. { apply maponpaths. refine (_ @ idpath (identity _)). rewrite dagger_of_idtodaggeriso. etrans. { apply maponpaths_2, idtodaggeriso_is_dagger_of_idtodaggeriso. } refine (_ @ pr22 (idtodaggeriso dagE _ _ (phi a0'))). rewrite pathsinv0inv0. apply maponpaths. generalize (phi a0'). intro p ; induction p ; apply idpath. } apply id_right. 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.