forall (P : TwoSphere -> Type) (b : P base) (s : idpath b = transport2 P surf b), apD02 (TwoSphere_ind P b s) surf = s @ (concat_p1 _)^.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.