(P : Type) (b : P) (s : idpath b = idpath b) : TwoSphere -> P := TwoSphere_ind (fun _ => P) b (s @ (transport2_const surf b) @ (concat_p1 _)).
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.