S2_to_TwoSphere o TwoSphere_to_S2 == idmap. Proof. refine (TwoSphere_ind _ 1 _). rhs_V rapply concat_p1. rhs refine (@concat_Ap (base = base) _ _ (fun p => (p^ @ ap S2_to_TwoSphere (ap TwoSphere_to_S2 p))^) (fun x => (transport_paths_FFlr x 1) @ ap (fun u => u @ x) (concat_p1 _) @ ap (fun w => _ @ w) (inv_V x)^ @ (inv_pp _ _)^) 1 1 surf). rhs rapply concat_1p. rhs refine (ap_compose (fun p => p^ @ ap S2_to_TwoSphere (ap TwoSphere_to_S2 p)) inverse surf). refine (@ap _ _ (ap inverse) 1 _ _). rhs_V rapply concat2_ap_ap. rhs refine (ap (fun w => inverse2 surf @@ w) (ap_compose (ap TwoSphere_to_S2) (ap S2_to_TwoSphere) surf)). lhs_V refine (concat_Vp_inverse2 _ _ surf). lhs rapply concat_p1. refine (ap (fun p : 1 = 1 => inverse2 surf @@ p) _). symmetry. lhs refine ((ap (ap (ap S2_to_TwoSphere)) (TwoSphere_rec_beta_surf (Sphere 2) North _))). lhs refine (ap_transport (concat_pV (merid North)) (fun z => @ap _ _ _ z z) (ap (fun u => merid u @ (merid North)^) (merid North @ (merid South)^))). lhs_V refine (ap (transport (fun z => ap S2_to_TwoSphere z = ap S2_to_TwoSphere z) (concat_pV (merid North))) (ap_compose (fun u => merid u @ (merid North)^) (ap S2_to_TwoSphere) (merid North @ (merid South)^))). apply transport_paths_FlFr'; symmetry. lhs_V refine (1 @@ ap_pp_concat_pV S2_to_TwoSphere (merid North)). lhs_V refine (1 @@ (1 @@ (1 @@ (concat_pV_inverse2 (ap S2_to_TwoSphere (merid North)) _ (Susp_rec_beta_merid North))))). lhs refine (@concat_Ap (Sphere 1) _ (fun x => ap S2_to_TwoSphere (merid x @ (merid North)^)) (fun x => Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x @ 1) (fun x => ap_pp S2_to_TwoSphere (merid x) (merid North)^ @ ((1 @@ ap_V S2_to_TwoSphere (merid North)) @ ((Susp_rec_beta_merid x @@ inverse2 (Susp_rec_beta_merid North)) @ 1))) North North (merid North @ (merid South)^)). f_ap. { rhs_V refine (ap_pp_concat_pV _ _). exact (1 @@ (1 @@ (concat_pV_inverse2 _ _ _))). } lhs_V refine (concat2_ap_ap (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec)) (fun _ => 1) (merid North @ (merid South)^)). lhs refine (ap (fun w => _ @@ w) (ap_const _ _)). lhs rapply whiskerR_p1_1. lhs refine (ap_pp _ (merid North) (merid South)^). rhs_V rapply concat_p1. f_ap. - exact (Susp_rec_beta_merid North). - lhs rapply ap_V. refine (@inverse2 _ _ _ _ 1 _). exact (Susp_rec_beta_merid South). Defined.
Require Import Basics Types. Require Import WildCat.Equiv. Require Import NullHomotopy. Require Import Homotopy.Suspension. Require Import Pointed. Require Import Truncations. Require Import Spaces.Circle Spaces.TwoSphere.