Lemma is_functor_preimage_functor_data : is_functor preimage_functor_data. Proof. split. - unfold functor_idax. simpl. intro b. assert (PR2 : ∏ (a : C) (h : unitary _ (H a) b) (a' : C) (h' : unitary _ (H a') b) (l : a --> a'), #H l· h' = h· identity b -> #F l· k b a' h' = k b a h· identity (Go b)). { intros a h a' h' l LL. rewrite id_right. apply (q b (tpair _ a h) (tpair _ a' h') l). rewrite id_right in LL. apply LL. } set (Gbrtilde := tpair _ (identity (Go b)) PR2 : Y (identity b)). set (H' := pr2 (Y_iscontr b b (identity b)) Gbrtilde). set (H'' := base_paths _ _ H'). simpl in H'. rewrite <- H'. apply idpath. - intros b b' b'' f f'. assert (HHHH : isaprop (pr1 (pr1 (Y_iscontr b b'' (f· f'))) = pr1 (pr1 (Y_iscontr b b' f))· pr1 (pr1 (Y_iscontr b' b'' f')))). { apply homset_property. } apply (pr1 wH b (tpair (λ x, isaprop x) (pr1 (pr1 (Y_iscontr b b'' (f· f'))) = pr1 (pr1 (Y_iscontr b b' f))· pr1 (pr1 (Y_iscontr b' b'' f'))) HHHH)). intros [a0 h0]; simpl. apply (pr1 wH b' (tpair (λ x, isaprop x) (pr1 (pr1 (Y_iscontr b b'' (f· f'))) = pr1 (pr1 (Y_iscontr b b' f))· pr1 (pr1 (Y_iscontr b' b'' f'))) HHHH)). intros [a0' h0']; simpl. apply (pr1 wH b'' (tpair (λ x, isaprop x) (pr1 (pr1 (Y_iscontr b b'' (f· f'))) = pr1 (pr1 (Y_iscontr b b' f))· pr1 (pr1 (Y_iscontr b' b'' f'))) HHHH)). intros [a0'' h0'']. simpl; clear HHHH. set (l0 := fH^-1 (h0 · f · unitary_inv h0')). set (l0' := fH^-1 (h0' · f' · unitary_inv h0'')). set (l0'' := fH^-1 (h0 · (f· f') · unitary_inv h0'')). assert (L : l0 · l0' = l0''). { apply (invmaponpathsweq (weq_from_fully_faithful fH a0 a0'')). simpl; rewrite functor_comp. unfold l0'. inv_functor fH a0' a0''. unfold l0. inv_functor fH a0 a0'. intermediate_path (h0 · f · (unitary_inv h0' · h0') · f' · unitary_inv h0''). { repeat rewrite assoc; apply idpath. } etrans. { do 2 apply maponpaths_2. apply maponpaths. apply h0'. } rewrite id_right. unfold l0''. inv_functor fH a0 a0''. repeat rewrite assoc; apply idpath. } assert (PR2 : ∏ (a : C) (h : unitary _ (H a) b)(a' : C) (h' : unitary _ (H a') b') (l : a --> a'), #H l· h' = h· f -> #F l· k b' a' h' = k b a h· ((unitary_inv (k b a0 h0)· #F l0)· k b' a0' h0') ). { intros a h a' h' l. intro alpha. set (m := fH^-i _ _ (unitary_comp h0 (unitary_inv h))). set (m' := fH^-i _ _ (unitary_comp h0' (unitary_inv h'))). assert (sss : unitary_comp (dagger_functor_on_unitary dagF _ _ m) (k b a h) = k b a0 h0). { apply unitary_eq; simpl. apply (q b (tpair _ a0 h0) (tpair _ a h) m). simpl. inv_functor fH a0 a. rewrite <- assoc. refine (_ @ id_right _). apply maponpaths, h. } assert (ssss : unitary_comp (dagger_functor_on_unitary dagF _ _ m') (k b' a' h') = k b' a0' h0'). { apply unitary_eq; simpl. apply (q b' (tpair _ a0' h0') (tpair _ a' h') m'); simpl. inv_functor fH a0' a'. rewrite <- assoc. refine (_ @ id_right _). apply maponpaths, h'. } assert (sssss : #H (l0 · m') = #H (m · l)). { rewrite functor_comp. unfold m'; simpl. inv_functor fH a0' a'. unfold l0. inv_functor fH a0 a0'. intermediate_path (h0 · f · (unitary_inv h0' · h0') · unitary_inv h'). { repeat rewrite assoc; apply idpath. } etrans. { apply maponpaths_2, maponpaths , h0'. } rewrite id_right, functor_comp. inv_functor fH a0 a. repeat rewrite <- assoc. apply maponpaths. apply pathsinv0. apply unitary_inv_on_right. { apply h. } rewrite assoc. apply unitary_inv_on_left. { apply h'. } apply pathsinv0. apply alpha. } assert (star5 : unitary_inv m · l0 = l · unitary_inv m'). { apply unitary_inv_on_right. { apply m. } rewrite assoc. apply unitary_inv_on_left. { apply m'. } apply (invmaponpathsweq (weq_from_fully_faithful fH a0 a' )). apply pathsinv0. apply sssss. } clear sssss. set (sss':= base_paths _ _ sss); simpl in sss'. assert (sss'' : k b a h · unitary_inv (k b a0 h0) = unitary_inv (dagger_functor_on_unitary dagF _ _ m)). { apply pathsinv0. apply unitary_inv_on_left. { apply k. } apply pathsinv0. apply unitary_inv_on_right. { apply dagger_functor_on_unitary. } apply pathsinv0. apply sss'. } repeat rewrite assoc. rewrite sss''. clear sss'' sss' sss. etrans. 2: { do 2 apply maponpaths_2. apply pathsinv0, dagger_functor_on_unitary_inv_on_ob. } rewrite <- functor_comp. etrans. 2: { apply maponpaths_2, maponpaths. refine (! star5 @ _). apply maponpaths_2. apply (Isos.inverse_unique_precat _ _ m) ; apply m. } clear star5. rewrite functor_comp. etrans. 2: { apply maponpaths_2, maponpaths. exact (dagger_functor_on_unitary_inv_on_ob dagF _ _ m'). } assert (star4 : unitary_inv (dagger_functor_on_unitary dagF _ _ m') · k b' a0' h0' = k b' a' h' ). { apply unitary_inv_on_right. { apply dagger_functor_on_unitary. } set (ssss' := base_paths _ _ ssss). apply pathsinv0. simpl in ssss'. simpl. apply ssss'; clear ssss'. } rewrite <- assoc. apply maponpaths. apply pathsinv0, star4. } assert (HGf : G f = unitary_inv (k b a0 h0) · #F l0 · k b' a0' h0'). { set (Gbrtilde := tpair _ (unitary_inv (k b a0 h0) · #F l0 · k b' a0' h0') PR2 : Y f). set (H' := pr2 (Y_iscontr b b' f) Gbrtilde). set (H'' := base_paths _ _ H'). simpl in H'. unfold G. rewrite <- H'. apply idpath. } clear PR2. assert (PR2 : ∏ (a : C) (h : unitary _ (H a) b') (a' : C) (h' : unitary _ (H a') b'') (l : a --> a'), #H l· h' = h· f' -> #F l· k b'' a' h' = k b' a h· ((unitary_inv (k b' a0' h0')· #F l0')· k b'' a0'' h0'')). { intros a' h' a'' h'' l'. intro alpha. set (m := fH^-i _ _ (unitary_comp h0' (unitary_inv h'))). set (m' := fH^-i _ _ (unitary_comp h0'' (unitary_inv h''))). assert (sss : unitary_comp (dagger_functor_on_unitary dagF _ _ m) (k b' a' h') = k b' a0' h0'). { apply unitary_eq; simpl. apply (q b' (tpair _ a0' h0') (tpair _ a' h') m); simpl. inv_functor fH a0' a'. rewrite <- assoc. refine (_ @ id_right _). apply maponpaths. apply h'. } assert (ssss : unitary_comp (dagger_functor_on_unitary dagF _ _ m') (k b'' a'' h'') = k b'' a0'' h0''). { apply unitary_eq; simpl. apply (q b'' (tpair _ a0'' h0'') (tpair _ a'' h'') m'); simpl. inv_functor fH a0'' a''. rewrite <- assoc. refine (_ @ id_right _). apply maponpaths. apply h''. } assert (sssss : #H (l0' · m') = #H (m · l')). { rewrite functor_comp. unfold m'. simpl. inv_functor fH a0'' a''. unfold l0'. inv_functor fH a0' a0''. intermediate_path (h0' · f' · (unitary_inv h0'' · h0'') · unitary_inv h''). { repeat rewrite assoc; apply idpath. } etrans. { apply maponpaths_2, maponpaths, h0''. } rewrite id_right, functor_comp. inv_functor fH a0' a'. repeat rewrite <- assoc. apply maponpaths, pathsinv0, unitary_inv_on_right. { apply h'. } rewrite assoc. apply unitary_inv_on_left. { apply h''. } apply pathsinv0, alpha. } assert (star5 : unitary_inv m · l0' = l' · unitary_inv m'). { apply unitary_inv_on_right. { apply m. } rewrite assoc. apply unitary_inv_on_left. { apply m'. } apply (invmaponpathsweq (weq_from_fully_faithful fH a0' a'' )), pathsinv0, sssss. } set (sss':= base_paths _ _ sss); simpl in sss'. assert (sss'' : k b' a' h' · unitary_inv (k b' a0' h0') = unitary_inv (dagger_functor_on_unitary dagF _ _ m)). { apply pathsinv0, unitary_inv_on_left, pathsinv0, unitary_inv_on_right. - apply k. - apply dagger_functor_on_unitary. - apply pathsinv0, sss'. } repeat rewrite assoc. rewrite sss''. clear sss'' sss' sss. etrans. 2: { do 2 apply maponpaths_2. exact (! dagger_functor_on_unitary_inv_on_ob dagF _ _ m). } rewrite <- functor_comp. etrans. 2: apply maponpaths_2, maponpaths, pathsinv0, star5. clear star5 sssss. rewrite functor_comp. etrans. 2: { apply maponpaths_2, maponpaths. exact (dagger_functor_on_unitary_inv_on_ob dagF _ _ m'). } assert (star4 : unitary_inv (dagger_functor_on_unitary dagF _ _ m') · k b'' a0'' h0'' = k b'' a'' h'' ). { apply unitary_inv_on_right. { apply dagger_functor_on_unitary. } set (ssss' := base_paths _ _ ssss). apply pathsinv0. simpl in *; apply ssss'. } rewrite <- assoc. apply maponpaths. exact (! star4). } assert (HGf' : G f' = unitary_inv (k b' a0' h0') · #F l0' · k b'' a0'' h0''). { set (Gbrtilde := tpair _ (unitary_inv (k b' a0' h0') · #F l0' · k b'' a0'' h0'') PR2 : Y f'). set (H' := pr2 (Y_iscontr b' b'' f') Gbrtilde). unfold G. rewrite <- (base_paths _ _ H'). apply idpath. } clear PR2. assert (PR2 : ∏ (a : C) (h : unitary _ (H a) b) (a' : C) (h' : unitary _ (H a') b'') (l : a --> a'), #H l· h' = h· (f· f') -> #F l· k b'' a' h' = k b a h· ((unitary_inv (k b a0 h0)· #F l0'')· k b'' a0'' h0'')). { intros a h a'' h'' l. intro alpha. set (m := fH^-i _ _ (unitary_comp h0 (unitary_inv h))). set (m' := fH^-i _ _ (unitary_comp h0'' (unitary_inv h''))). assert (sss : unitary_comp (dagger_functor_on_unitary dagF _ _ m) (k b a h) = k b a0 h0). { apply unitary_eq. apply (q b (tpair _ a0 h0) (tpair _ a h) m); simpl. inv_functor fH a0 a. rewrite <- assoc. refine (_ @ id_right _). apply maponpaths. apply h. } assert (ssss : unitary_comp (dagger_functor_on_unitary dagF _ _ m') (k b'' a'' h'') = k b'' a0'' h0''). { apply unitary_eq. apply (q b'' (tpair _ a0'' h0'') (tpair _ a'' h'') m'). simpl; inv_functor fH a0'' a''. rewrite <- assoc. refine (_ @ id_right _). apply maponpaths. apply h''. } assert (sssss : #H (l0'' · m') = #H (m · l)). { rewrite functor_comp. unfold m'. simpl. inv_functor fH a0'' a''. unfold l0''. inv_functor fH a0 a0''. intermediate_path (h0 · (f · f') · (unitary_inv h0'' · h0'') · unitary_inv h''). { repeat rewrite assoc; apply idpath. } etrans. { apply maponpaths_2, maponpaths, h0''. } rewrite id_right, functor_comp. inv_functor fH a0 a. repeat rewrite <- assoc. apply maponpaths, pathsinv0, unitary_inv_on_right. { apply h. } repeat rewrite assoc. apply unitary_inv_on_left, pathsinv0. { apply h''. } repeat rewrite <- assoc. apply alpha. } assert (star5 : unitary_inv m · l0'' = l · unitary_inv m'). { apply unitary_inv_on_right. { apply m. } rewrite assoc. apply unitary_inv_on_left. { apply m'. } apply (invmaponpathsweq (weq_from_fully_faithful fH a0 a'' )). apply pathsinv0, sssss. } set (sss':= base_paths _ _ sss); simpl in sss'. assert (sss'' : k b a h · unitary_inv (k b a0 h0) = unitary_inv (dagger_functor_on_unitary dagF _ _ m)). { apply pathsinv0, unitary_inv_on_left, pathsinv0, unitary_inv_on_right. - apply k. - apply dagger_functor_on_unitary. - apply pathsinv0, sss'. } repeat rewrite assoc. rewrite sss''. clear sss'' sss' sss. etrans. 2: { do 2 apply maponpaths_2. exact (! dagger_functor_on_unitary_inv_on_ob dagF _ _ m). } rewrite <- functor_comp. etrans. 2: apply maponpaths_2, maponpaths, (! star5). clear star5 sssss. rewrite functor_comp. etrans. 2: { apply maponpaths_2, maponpaths. exact (dagger_functor_on_unitary_inv_on_ob dagF _ _ m'). } assert (star4 : unitary_inv (dagger_functor_on_unitary dagF _ _ m') · k b'' a0'' h0'' = k b'' a'' h''). { apply unitary_inv_on_right, pathsinv0, (base_paths _ _ ssss). apply dagger_functor_on_unitary. } rewrite <- assoc. apply maponpaths. exact (! star4). } assert (HGff' : G (f · f') = unitary_inv (k b a0 h0) · #F l0'' · k b'' a0'' h0''). { set (Gbrtilde := tpair _ (unitary_inv (k b a0 h0) · #F l0'' · k b'' a0'' h0'') PR2 : Y (f · f')). unfold G. rewrite <- (pr2 (Y_iscontr b b'' (f · f')) Gbrtilde). apply idpath. } clear PR2. fold (G (f · f')). fold (G (f)) (G f'). rewrite HGf, HGf'. intermediate_path (unitary_inv (k b a0 h0)· #F l0· (k b' a0' h0'· unitary_inv (k b' a0' h0'))· #F l0'· k b'' a0'' h0''). { etrans. 2: { do 2 apply maponpaths_2. apply maponpaths, pathsinv0, k. } rewrite id_right, HGff'. repeat rewrite <- assoc. apply maponpaths. rewrite <- L. rewrite functor_comp. repeat rewrite <- assoc. apply idpath. } now repeat rewrite <- assoc. 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.