(P : TwoSphere -> Type) (b : P base) (s : idpath b = transport2 P surf b) : forall (x : TwoSphere), P x := fun x => match x with base => fun _ => b end s.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.