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