(P : Type) (b : P) (p : b = b) : ap (Sph1_rec P b p) (merid North @ (merid South)^) = p. Proof. rewrite ap_pp. rewrite ap_V. rewrite 2 Susp_rec_beta_merid. apply concat_p1. Defined.
Require Import Classes.interfaces.canonical_names. Require Import Cubical.DPath Cubical.PathSquare. Require Import Homotopy.Suspension. Require Import Homotopy.HSpace.Core. Require Import Homotopy.HSpace.Coherent. Require Import Spaces.Spheres.