Lemma is_functor_preimage_functor_data : is_functor preimage_functor_data. Proof. split. - unfold functor_idax. simpl. intro b. assert (PR2 : ∏ (a : A) (h : z_iso (H a) b) (a' : A) (h' : z_iso (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 C. } apply (p 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 (p 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 (p 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 · inv_from_z_iso h0')). set (l0' := fH^-1 (h0' · f' · inv_from_z_iso h0'')). set (l0'' := fH^-1 (h0 · (f· f') · inv_from_z_iso 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 · (inv_from_z_iso h0' · h0') · f' · inv_from_z_iso h0''). { repeat rewrite assoc; apply idpath. } rewrite z_iso_after_z_iso_inv, id_right. unfold l0''. inv_functor fH a0 a0''. repeat rewrite assoc; apply idpath. } assert (PR2 : ∏ (a : A) (h : z_iso (H a) b)(a' : A) (h' : z_iso (H a') b') (l : a --> a'), #H l· h' = h· f -> #F l· k b' a' h' = k b a h· ((inv_from_z_iso (k b a0 h0)· #F l0)· k b' a0' h0') ). { intros a h a' h' l. intro alpha. set (m := fH^-i (z_iso_comp h0 (z_iso_inv_from_z_iso h))). set (m' := fH^-i (z_iso_comp h0' (z_iso_inv_from_z_iso h'))). assert (sss : z_iso_comp (functor_on_z_iso F m) (k b a h) = k b a0 h0). { apply z_iso_eq; simpl. apply (q b (tpair _ a0 h0) (tpair _ a h) m). simpl. inv_functor fH a0 a. rewrite <- assoc. rewrite z_iso_after_z_iso_inv. apply id_right. } assert (ssss : z_iso_comp (functor_on_z_iso F m') (k b' a' h') = k b' a0' h0'). { apply z_iso_eq; simpl. apply (q b' (tpair _ a0' h0') (tpair _ a' h') m'); simpl. inv_functor fH a0' a'. rewrite <- assoc. rewrite z_iso_after_z_iso_inv. apply id_right. } 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 · (inv_from_z_iso h0' · h0') · inv_from_z_iso h'). { repeat rewrite assoc; apply idpath. } rewrite z_iso_after_z_iso_inv, id_right, functor_comp. inv_functor fH a0 a. repeat rewrite <- assoc. apply maponpaths. apply pathsinv0. apply z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left. apply pathsinv0. apply alpha. } assert (star5 : inv_from_z_iso m · l0 = l · inv_from_z_iso m'). { apply z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left. 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 · inv_from_z_iso (k b a0 h0) = inv_from_z_iso (functor_on_z_iso F m)). { apply pathsinv0. apply z_iso_inv_on_left. apply pathsinv0. apply z_iso_inv_on_right. unfold m; simpl. apply pathsinv0. apply sss'. } repeat rewrite assoc. rewrite sss''. clear sss'' sss' sss. rewrite <- functor_on_inv_from_z_iso. rewrite <- functor_comp. rewrite star5, functor_comp, functor_on_inv_from_z_iso. clear star5. assert (star4 : inv_from_z_iso (functor_on_z_iso F m')· k b' a0' h0' = k b' a' h' ). { apply z_iso_inv_on_right. set (ssss' := base_paths _ _ ssss). apply pathsinv0. simpl in ssss'. simpl. apply ssss'; clear ssss'. } rewrite <- assoc. rewrite star4. apply idpath. } assert (HGf : G f = inv_from_z_iso (k b a0 h0) · #F l0 · k b' a0' h0'). { set (Gbrtilde := tpair _ (inv_from_z_iso (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'. rewrite <- H'. apply idpath. } clear PR2. assert (PR2 : ∏ (a : A) (h : z_iso (H a) b') (a' : A) (h' : z_iso (H a') b'') (l : a --> a'), #H l· h' = h· f' -> #F l· k b'' a' h' = k b' a h· ((inv_from_z_iso (k b' a0' h0')· #F l0')· k b'' a0'' h0'')). { intros a' h' a'' h'' l'. intro alpha. set (m := fH^-i (z_iso_comp h0' (z_iso_inv_from_z_iso h'))). set (m' := fH^-i (z_iso_comp h0'' (z_iso_inv_from_z_iso h''))). assert (sss : z_iso_comp (functor_on_z_iso F m) (k b' a' h') = k b' a0' h0'). { apply z_iso_eq; simpl. apply (q b' (tpair _ a0' h0') (tpair _ a' h') m); simpl. inv_functor fH a0' a'. rewrite <- assoc. rewrite z_iso_after_z_iso_inv. apply id_right. } assert (ssss : z_iso_comp (functor_on_z_iso F m') (k b'' a'' h'') = k b'' a0'' h0''). { apply z_iso_eq; simpl. apply (q b'' (tpair _ a0'' h0'') (tpair _ a'' h'') m'); simpl. inv_functor fH a0'' a''. rewrite <- assoc. rewrite z_iso_after_z_iso_inv. apply id_right. } 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' · (inv_from_z_iso h0'' · h0'') · inv_from_z_iso h''). { repeat rewrite assoc; apply idpath. } rewrite z_iso_after_z_iso_inv, id_right, functor_comp. inv_functor fH a0' a'. repeat rewrite <- assoc. apply maponpaths, pathsinv0, z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left, pathsinv0, alpha. } assert (star5 : inv_from_z_iso m · l0' = l' · inv_from_z_iso m'). { apply z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left, (invmaponpathsweq (weq_from_fully_faithful fH a0' a'' )), pathsinv0, sssss. } set (sss':= base_paths _ _ sss); simpl in sss'. assert (sss'' : k b' a' h' · inv_from_z_iso (k b' a0' h0') = inv_from_z_iso (functor_on_z_iso F m)). { apply pathsinv0, z_iso_inv_on_left, pathsinv0, z_iso_inv_on_right. unfold m; simpl; apply pathsinv0, sss'. } repeat rewrite assoc. rewrite sss''. clear sss'' sss' sss. rewrite <- functor_on_inv_from_z_iso. rewrite <- functor_comp. rewrite star5. clear star5 sssss. rewrite functor_comp, functor_on_inv_from_z_iso. assert (star4 : inv_from_z_iso (functor_on_z_iso F m')· k b'' a0'' h0'' = k b'' a'' h'' ). { apply z_iso_inv_on_right. set (ssss' := base_paths _ _ ssss). apply pathsinv0. simpl in *; apply ssss'. } rewrite <- assoc. rewrite star4. apply idpath. } assert (HGf' : G f' = inv_from_z_iso (k b' a0' h0') · #F l0' · k b'' a0'' h0''). { set (Gbrtilde := tpair _ (inv_from_z_iso (k b' a0' h0') · #F l0' · k b'' a0'' h0'') PR2 : Y f'). set (H' := pr2 (Y_iscontr b' b'' f') Gbrtilde). rewrite <- (base_paths _ _ H'). apply idpath. } clear PR2. assert (PR2 : ∏ (a : A) (h : z_iso (H a) b) (a' : A) (h' : z_iso (H a') b'') (l : a --> a'), #H l· h' = h· (f· f') -> #F l· k b'' a' h' = k b a h· ((inv_from_z_iso (k b a0 h0)· #F l0'')· k b'' a0'' h0'')). { intros a h a'' h'' l. intro alpha. set (m := fH^-i (z_iso_comp h0 (z_iso_inv_from_z_iso h))). set (m' := fH^-i (z_iso_comp h0'' (z_iso_inv_from_z_iso h''))). assert (sss : z_iso_comp (functor_on_z_iso F m) (k b a h) = k b a0 h0). { apply z_iso_eq. apply (q b (tpair _ a0 h0) (tpair _ a h) m); simpl. inv_functor fH a0 a. rewrite <- assoc. rewrite z_iso_after_z_iso_inv. apply id_right. } assert (ssss : z_iso_comp (functor_on_z_iso F m') (k b'' a'' h'') = k b'' a0'' h0''). { apply z_iso_eq. apply (q b'' (tpair _ a0'' h0'') (tpair _ a'' h'') m'). simpl; inv_functor fH a0'' a''. rewrite <- assoc. rewrite z_iso_after_z_iso_inv. apply id_right. } 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') · (inv_from_z_iso h0'' · h0'') · inv_from_z_iso h''). { repeat rewrite assoc; apply idpath. } rewrite z_iso_after_z_iso_inv, id_right, functor_comp. inv_functor fH a0 a. repeat rewrite <- assoc. apply maponpaths, pathsinv0, z_iso_inv_on_right. repeat rewrite assoc. apply z_iso_inv_on_left, pathsinv0. repeat rewrite <- assoc. apply alpha. } assert (star5 : inv_from_z_iso m · l0'' = l · inv_from_z_iso m'). { apply z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left. 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 · inv_from_z_iso (k b a0 h0) = inv_from_z_iso (functor_on_z_iso F m)). { apply pathsinv0, z_iso_inv_on_left, pathsinv0, z_iso_inv_on_right. unfold m; simpl. apply pathsinv0, sss'. } repeat rewrite assoc. rewrite sss''. clear sss'' sss' sss. rewrite <- functor_on_inv_from_z_iso. rewrite <- functor_comp. rewrite star5. clear star5 sssss. rewrite functor_comp, functor_on_inv_from_z_iso. assert (star4 : inv_from_z_iso (functor_on_z_iso F m')· k b'' a0'' h0'' = k b'' a'' h'' ). { apply z_iso_inv_on_right, pathsinv0, (base_paths _ _ ssss). } rewrite <- assoc. rewrite star4. apply idpath. } assert (HGff' : G (f · f') = inv_from_z_iso (k b a0 h0) · #F l0'' · k b'' a0'' h0''). { set (Gbrtilde := tpair _ (inv_from_z_iso (k b a0 h0) · #F l0'' · k b'' a0'' h0'') PR2 : Y (f · f')). rewrite <- (pr2 (Y_iscontr b b'' (f · f')) Gbrtilde). apply idpath. } clear PR2. rewrite HGf, HGf'. intermediate_path (inv_from_z_iso (k b a0 h0)· #F l0· (k b' a0' h0'· inv_from_z_iso (k b' a0' h0'))· #F l0'· k b'' a0'' h0''). { rewrite z_iso_inv_after_z_iso, id_right. rewrite HGff'. repeat rewrite <- assoc. apply maponpaths. rewrite <- L. rewrite functor_comp. repeat rewrite <- assoc. apply idpath. } repeat rewrite <- assoc. 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.