TwoSphere_to_S2 o S2_to_TwoSphere == idmap. Proof. intro x. refine ((Susp_rec_eta_homotopic (TwoSphere_to_S2 o S2_to_TwoSphere) x) @ _). symmetry. generalize dependent x. refine (Susp_ind _ 1 (merid North)^ _). intro x. refine ((transport_paths_FlFr (f := fun y => y) _ _) @ _). rewrite_moveR_Vp_p. refine ((concat_1p _) @ _). refine (_ @ (ap (fun w => w @ _) (ap_idmap _)^)). refine ((Susp_rec_beta_merid _) @ _). path_via (ap TwoSphere_to_S2 (ap S2_to_TwoSphere (merid x))). { apply (ap_compose S2_to_TwoSphere TwoSphere_to_S2 (merid x)). } path_via (ap TwoSphere_to_S2 (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec) x)). { repeat f_ap. apply Susp_rec_beta_merid. } symmetry. generalize dependent x. simple refine (Susp_ind _ (concat_pV (merid North)) _ _). - refine (_ @ (concat_pV (merid North))). apply (ap (fun w => merid w @ (merid North)^) (merid South)^). - intro x. refine ((transport_paths_FlFr (merid x) (concat_pV (merid North))) @ _). rewrite_moveR_Vp_p. symmetry. refine ((dpath_path_lr _ _ _)^-1 _). refine ((ap (transport _ _) (ap_pp _ (merid x) (merid South)^)^) @ _). refine (_ @ (ap_compose (Susp_rec 1 1 (Susp_rec surf 1 Empty_rec)) (ap TwoSphere_to_S2) (merid x))^). refine (_ @ (ap (ap02 TwoSphere_to_S2) (Susp_rec_beta_merid _)^)). symmetry. generalize dependent x. simple refine (Susp_ind _ _ _ _). + refine (TwoSphere_rec_beta_surf _ _ _). + refine (_ @ (ap (fun w => transport _ _ (ap _ w)) (concat_pV (merid South))^)). refine (_ @ (transport_paths_lr _ _)^). refine (_ @ (ap (fun w => w @ _) (concat_p1 _)^)). refine (concat_Vp _)^. + apply Empty_ind. 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.