Lemma other_adjoint {X Y} (f : X -> Y) (g : Y -> X) (p : ∏ y : Y, f (g y) = y) (q : ∏ x : X, g (f x) = x) (h : ∏ x : X, maponpaths f (q x) = p (f x)) : ∏ y : Y, maponpaths g (p y) = q (g y). Proof. intros. apply pathsinv0. intermediate_path ( !(maponpaths g (p (f (g y)))) @' maponpaths g (p (f (g y))) @' q (g y)). { rewrite pathsinv0l. reflexivity. } intermediate_path ( !(maponpaths g (maponpaths f (q (g y)))) @' maponpaths g (p (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. apply (maponpaths pathsinv0). apply (maponpaths (maponpaths g)). set (y' := g y). apply pathsinv0. exact (h y'). } intermediate_path ( !(maponpaths g (maponpaths f (q (g y)))) @' maponpaths g (p (f (g y))) @' ((!q (g (f (g y)))) @' q (g (f (g y))) @' q (g y))). { rewrite pathsinv0l. reflexivity. } intermediate_path ( !(maponpaths g (maponpaths f (q (g y)))) @' maponpaths g (p (f (g y))) @' ((!q (g (f (g y)))) @' (maponpaths g (p (f (g y))) @' !(maponpaths g (p (f (g y)))) @' q (g (f (g y)))) @' q (g y))). { maponpaths_pre_post_cat. apply path_inv_rotate_rr. reflexivity. } apply path_inverse_from_right. repeat rewrite path_assoc. intermediate_path ( !(maponpaths g (p y)) @' !(maponpaths g (maponpaths f (q (g y)))) @' !(q (g (f (g (f (g y)))))) @' maponpaths (funcomp f g) (maponpaths g (p (f (g y)))) @' maponpaths g (p (f (g y))) @' !(maponpaths g (p (f (g y)))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. apply path_inv_rotate_lr. rewrite <- path_assoc. apply path_inv_rotate_rl. apply pathsinv0. rewrite <- (maponpathscomp f g). set (y' := f (g y)). assert (r := maponpaths_fun_fun_fun_natl p g q y'). simpl in r. rewrite (maponpathscomp f). rewrite (maponpathscomp g). rewrite (maponpathscomp g (λ x : X, g (f x))) in r. rewrite maponpathsidfun in r. exact r. } intermediate_path ( !(maponpaths g (p y)) @' !(maponpaths g (maponpaths f (q (g y)))) @' !(q (g (f (g (f (g y)))))) @' maponpaths g (maponpaths f (maponpaths g (p (f (g y))))) @' maponpaths g (p (f (g y))) @' !(maponpaths g (p (f (g y)))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. rewrite <- (maponpathscomp f g). reflexivity. } intermediate_path ( !(maponpaths g (p y)) @' !(maponpaths g (maponpaths f (q (g y)))) @' !(q (g (f (g (f (g y)))))) @' maponpaths g (maponpaths f (maponpaths g (p (f (g y)))) @' p (f (g y))) @' !(maponpaths g (p (f (g y)))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. rewrite <- (maponpathscomp0 g). reflexivity. } intermediate_path ( !(maponpaths g (p y)) @' !(maponpaths g (maponpaths f (q (g y)))) @' !(q (g (f (g (f (g y)))))) @' maponpaths g (maponpaths (funcomp g f) (p (f (g y))) @' p (f (g y))) @' !(maponpaths g (p (f (g y)))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. rewrite <- (maponpathscomp g f). reflexivity. } intermediate_path ( !(maponpaths g (p y)) @' !(maponpaths g (maponpaths f (q (g y)))) @' !(q (g (f (g (f (g y)))))) @' maponpaths g (p (f (g (f (g y)))) @' p (f (g y))) @' !(maponpaths g (p (f (g y)))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. rewrite <- (maponpathscomp g f). apply (maponpaths (maponpaths g)). generalize (f (g y)); clear y; intro y. assert (r := maponpaths_fun_fun_natl p p y); simpl in r. assert (s := maponpathsidfun (p y)); unfold idfun in s. rewrite s in r; clear s. rewrite (maponpathscomp g). exact r. } intermediate_path ( !(maponpaths g (p y)) @' !(maponpaths g (maponpaths f (q (g y)))) @' !(q (g (f (g (f (g y)))))) @' maponpaths g (p (f (g (f (g y))))) @' maponpaths g (p (f (g y))) @' !(maponpaths g (p (f (g y)))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. rewrite <- (maponpathscomp0 g). reflexivity. } intermediate_path ( !(maponpaths g (p y)) @' !(maponpaths g (maponpaths f (q (g y)))) @' !(q (g (f (g (f (g y)))))) @' maponpaths g (p (f (g (f (g y))))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. repeat rewrite <- path_assoc. rewrite pathsinv0r. rewrite pathscomp0rid. reflexivity. } intermediate_path ( maponpaths g ((!p y) @' maponpaths f (!q (g y))) @' !(q (g (f (g (f (g y)))))) @' maponpaths g (p (f (g (f (g y))))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. repeat rewrite <- maponpathsinv0. rewrite <- (maponpathscomp0 g). reflexivity. } intermediate_path ( !(q (g y)) @' maponpaths (funcomp f g) (maponpaths g ((!p y) @' maponpaths f (!q (g y)))) @' maponpaths g (p (f (g (f (g y))))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. repeat rewrite maponpathscomp0. repeat rewrite <- (maponpathscomp f g). repeat rewrite maponpathsinv0. repeat rewrite path_comp_inv_inv. apply (maponpaths pathsinv0). assert (r := ! maponpaths_fun_fun_fun_natl q (funcomp f g) q (g y)); simpl in r. rewrite maponpathsidfun in r. repeat rewrite <- (maponpathscomp f g) in r. simpl in r. repeat rewrite path_assoc. rewrite r. maponpaths_pre_post_cat. clear r. assert (r := ! maponpaths_fun_fun_fun_natl p g q y); simpl in r. rewrite maponpathsidfun in r. rewrite (maponpathscomp f). rewrite (maponpathscomp g). rewrite (maponpathscomp g) in r. exact r. } intermediate_path ( !(q (g y)) @' maponpaths g (maponpaths (funcomp g f) ((!p y) @' maponpaths f (!q (g y)))) @' maponpaths g (p (f (g (f (g y))))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. rewrite <- (maponpathscomp g f). rewrite <- (maponpathscomp f g). reflexivity. } intermediate_path ( !(q (g y)) @' maponpaths g (maponpaths (funcomp g f) ((!p y) @' maponpaths f (!q (g y))) @' p (f (g (f (g y))))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. rewrite <- maponpathscomp0. apply (maponpaths (maponpaths g)). reflexivity. } intermediate_path ( !(q (g y)) @' maponpaths g (p y @' ((!p y) @' maponpaths f (!q (g y)))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. rewrite <- (maponpathscomp g f). repeat rewrite maponpathscomp0. repeat rewrite maponpathsinv0. repeat rewrite <- path_assoc. repeat apply path_inv_rotate_ll. repeat rewrite path_assoc. repeat apply path_inv_rotate_rr. apply pathsinv0. repeat rewrite <- (maponpathscomp0 g). apply (maponpaths (maponpaths g)). rewrite h. assert (r := ! maponpaths_fun_fun_natl p p (f (g y))); simpl in r. rewrite maponpathsidfun in r. simpl in *. repeat rewrite <- (maponpathscomp g f) in r. repeat rewrite (path_assoc _ _ (p y)). rewrite r. repeat rewrite <- (path_assoc _ _ (p y)). apply (maponpaths pre_cat). clear r. assert (r := maponpaths_fun_fun_natl p p y); simpl in r. rewrite maponpathsidfun in r. repeat rewrite <- (maponpathscomp g f) in r. exact r. } intermediate_path ( (!q (g y)) @' maponpaths g (maponpaths f (!q (g y))) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. repeat rewrite <- maponpathsinv0. apply (maponpaths (maponpaths g)). rewrite pathsinv0r. reflexivity. } intermediate_path ( (!q (g y)) @' maponpaths (funcomp f g) (!q (g y)) @' q (g (f (g y))) @' q (g y)). { maponpaths_pre_post_cat. rewrite <- (maponpathscomp f g). reflexivity. } intermediate_path ((!q (g y)) @' q (g y) @' (!q (g y)) @' q (g y)). { maponpaths_pre_post_cat. rewrite <- (maponpathscomp f g). apply path_inv_rotate_ll. repeat rewrite path_assoc. apply path_inv_rotate_rr. assert (r := ! maponpaths_fun_fun_natl q q (g y)); simpl in r. rewrite maponpathsidfun in r. rewrite (maponpathscomp f g). exact r. } rewrite pathsinv0l. simpl. rewrite pathsinv0l. reflexivity. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.