Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.

Local Open Scope path_scope.

(** * Theorems about the 2-sphere [S^2]. *)

(* ** Definition of the 2-sphere. *)

Module Export TwoSphere.

  Private Inductive TwoSphere : Type0 :=
    | base : TwoSphere.

  Axiom surf : idpath base = idpath base.

  Definition TwoSphere_ind (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.

  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 _)^.

End TwoSphere.

(* ** The non-dependent eliminator *)

Definition TwoSphere_rec (P : Type) (b : P) (s : idpath b = idpath b)
  : TwoSphere -> P
  := TwoSphere_ind (fun _ => P) b (s @ (transport2_const surf b) @ (concat_p1 _)).

Definition TwoSphere_rec_beta_surf (P : Type) (b : P) (s : idpath b = idpath b)
  : ap02 (TwoSphere_rec P b s) surf = s.
P: Type
b: P
s: 1 = 1
ap02 (TwoSphere_rec P b s) surf = s
Proof.
P: Type
b: P
s: 1 = 1
ap02 (TwoSphere_rec P b s) surf = s
  apply (cancel2L (transport2_const surf b)).
P: Type
b: P
s: 1 = 1
transport2_const surf b @@ ap02 (TwoSphere_rec P b s) surf =
transport2_const surf b @@ s
  apply (cancelL (apD_const (TwoSphere_rec P b s) (idpath base))).
P: Type
b: P
s: 1 = 1
apD_const (TwoSphere_rec P b s) 1 @
(transport2_const surf b @@ ap02 (TwoSphere_rec P b s) surf) =
apD_const (TwoSphere_rec P b s) 1 @ (transport2_const surf b @@ s)
  apply (cancelR _ _ (concat_p_pp _ (transport_const _ b) _)^).
P: Type
b: P
s: 1 = 1
(apD_const (TwoSphere_rec P b s) 1 @
 (transport2_const surf b @@ ap02 (TwoSphere_rec P b s) surf)) @
(concat_p_pp (transport2 (fun _ : TwoSphere => P) surf b)
   (transport_const 1 b) (ap (TwoSphere_rec P b s) 1))^ =
(apD_const (TwoSphere_rec P b s) 1 @ (transport2_const surf b @@ s)) @
(concat_p_pp (transport2 (fun _ : TwoSphere => P) surf b)
   (transport_const 1 b) (ap (TwoSphere_rec P b s) 1))^
  apply (cancelR _ _ (whiskerL (transport2 _ surf b) (apD_const _ _)^)).
P: Type
b: P
s: 1 = 1
((apD_const (TwoSphere_rec P b s) 1 @
  (transport2_const surf b @@ ap02 (TwoSphere_rec P b s) surf)) @
 (concat_p_pp (transport2 (fun _ : TwoSphere => P) surf b)
    (transport_const 1 b) (ap (TwoSphere_rec P b s) 1))^) @
whiskerL (transport2 (fun _ : TwoSphere => P) surf b)
  (apD_const (fun _ : TwoSphere => b) 1)^ =
((apD_const (TwoSphere_rec P b s) 1 @ (transport2_const surf b @@ s)) @
 (concat_p_pp (transport2 (fun _ : TwoSphere => P) surf b)
    (transport_const 1 b) (ap (TwoSphere_rec P b s) 1))^) @
whiskerL (transport2 (fun _ : TwoSphere => P) surf b)
  (apD_const (fun _ : TwoSphere => b) 1)^
  refine ((apD02_const (TwoSphere_rec P b s) surf)^ @ _).
P: Type
b: P
s: 1 = 1
apD02 (TwoSphere_rec P b s) surf =
((apD_const (TwoSphere_rec P b s) 1 @ (transport2_const surf b @@ s)) @
 (concat_p_pp (transport2 (fun _ : TwoSphere => P) surf b)
    (transport_const 1 b) (ap (TwoSphere_rec P b s) 1))^) @
whiskerL (transport2 (fun _ : TwoSphere => P) surf b)
  (apD_const (fun _ : TwoSphere => b) 1)^
  refine ((TwoSphere_ind_beta_surf _ _ _) @ _).
P: Type
b: P
s: 1 = 1
((s @ transport2_const surf b) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) @
(concat_p1 (transport2 (fun _ : TwoSphere => P) surf b))^ =
((apD_const (TwoSphere_rec P b s) 1 @ (transport2_const surf b @@ s)) @
 (concat_p_pp (transport2 (fun _ : TwoSphere => P) surf b)
    (transport_const 1 b) (ap (TwoSphere_rec P b s) 1))^) @
whiskerL (transport2 (fun _ : TwoSphere => P) surf b)
  (apD_const (fun _ : TwoSphere => b) 1)^
  refine (_ @ (ap (fun w => _ @ w) 
                  (triangulator 
                     (transport2 (fun _ : TwoSphere => P) surf b) _))).
P: Type
b: P
s: 1 = 1
((s @ transport2_const surf b) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) @
(concat_p1 (transport2 (fun _ : TwoSphere => P) surf b))^ =
((apD_const (TwoSphere_rec P b s) 1 @ (transport2_const surf b @@ s)) @
 (concat_p_pp (transport2 (fun _ : TwoSphere => P) surf b)
    (transport_const 1 b) (ap (TwoSphere_rec P b s) 1))^) @
(concat_p_pp (transport2 (fun _ : TwoSphere => P) surf b) 1
   (apD
      (TwoSphere_ind (fun _ : TwoSphere => P) b
         ((s @ transport2_const surf b) @
          concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)))
      1) @
 whiskerR (concat_p1 (transport2 (fun _ : TwoSphere => P) surf b))
   (apD
      (TwoSphere_ind (fun _ : TwoSphere => P) b
         ((s @ transport2_const surf b) @
          concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)))
      1)) 
  cbn.
P: Type
b: P
s: 1 = 1
((s @ transport2_const surf b) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) @
(concat_p1 (transport2 (fun _ : TwoSphere => P) surf b))^ =
((1 @ (transport2_const surf b @@ s)) @
 match
   transport2 (fun _ : TwoSphere => P) surf b as p in (_ = a)
   return (p @ 1 = (p @ 1) @ 1)
 with
 | 1 => 1
 end^) @
(match
   transport2 (fun _ : TwoSphere => P) surf b as p in (_ = a)
   return (p @ 1 = (p @ 1) @ 1)
 with
 | 1 => 1
 end @ whiskerR (concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) 1) refine (_ @ (ap (fun w => (w @ _) @ _) (concat_1p _)^)).
P: Type
b: P
s: 1 = 1
((s @ transport2_const surf b) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) @
(concat_p1 (transport2 (fun _ : TwoSphere => P) surf b))^ =
((transport2_const surf b @@ s) @
 match
   transport2 (fun _ : TwoSphere => P) surf b as p in (_ = a)
   return (p @ 1 = (p @ 1) @ 1)
 with
 | 1 => 1
 end^) @
(match
   transport2 (fun _ : TwoSphere => P) surf b as p in (_ = a)
   return (p @ 1 = (p @ 1) @ 1)
 with
 | 1 => 1
 end @ whiskerR (concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) 1)
  
  refine (_ @ (concat_p_pp _ _ _)).
P: Type
b: P
s: 1 = 1
((s @ transport2_const surf b) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) @
(concat_p1 (transport2 (fun _ : TwoSphere => P) surf b))^ =
(transport2_const surf b @@ s) @
(match
   transport2 (fun _ : TwoSphere => P) surf b as p in (_ = a)
   return (p @ 1 = (p @ 1) @ 1)
 with
 | 1 => 1
 end^ @
 (match
    transport2 (fun _ : TwoSphere => P) surf b as p in (_ = a)
    return (p @ 1 = (p @ 1) @ 1)
  with
  | 1 => 1
  end @ whiskerR (concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) 1))
  refine (_ @ (ap (fun w => _ @ w) (concat_pp_p _ _ _))).
P: Type
b: P
s: 1 = 1
((s @ transport2_const surf b) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) @
(concat_p1 (transport2 (fun _ : TwoSphere => P) surf b))^ =
(transport2_const surf b @@ s) @
((match
    transport2 (fun _ : TwoSphere => P) surf b as p in (_ = a)
    return (p @ 1 = (p @ 1) @ 1)
  with
  | 1 => 1
  end^ @
  match
    transport2 (fun _ : TwoSphere => P) surf b as p in (_ = a)
    return (p @ 1 = (p @ 1) @ 1)
  with
  | 1 => 1
  end) @
 whiskerR (concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) 1)
  refine (_ @ (ap (fun w => _ @ (w @ _)) (concat_Vp _)^)).
P: Type
b: P
s: 1 = 1
((s @ transport2_const surf b) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) @
(concat_p1 (transport2 (fun _ : TwoSphere => P) surf b))^ =
(transport2_const surf b @@ s) @
(1 @ whiskerR (concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) 1)
  refine (_ @ (ap (fun w => _ @ (w @ _)) 
                  (concat_pV (concat_p1 
                                (transport2 (fun _ : TwoSphere => P) surf b @ 1))))).
P: Type
b: P
s: 1 = 1
((s @ transport2_const surf b) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) @
(concat_p1 (transport2 (fun _ : TwoSphere => P) surf b))^ =
(transport2_const surf b @@ s) @
((concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1) @
  (concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1))^) @
 whiskerR (concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) 1)
  refine (_ @ (ap (fun w => _ @ w) (concat_p_pp _ _ _))).
P: Type
b: P
s: 1 = 1
((s @ transport2_const surf b) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) @
(concat_p1 (transport2 (fun _ : TwoSphere => P) surf b))^ =
(transport2_const surf b @@ s) @
(concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1) @
 ((concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1))^ @
  whiskerR (concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) 1))
  refine (_ @ (concat_pp_p _ _ _)).
P: Type
b: P
s: 1 = 1
((s @ transport2_const surf b) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) @
(concat_p1 (transport2 (fun _ : TwoSphere => P) surf b))^ =
((transport2_const surf b @@ s) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1)) @
((concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1))^ @
 whiskerR (concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) 1) apply moveR_pV.
P: Type
b: P
s: 1 = 1
(s @ transport2_const surf b) @
concat_p1 (transport2 (fun _ : TwoSphere => P) surf b) =
(((transport2_const surf b @@ s) @
  concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1)) @
 ((concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1))^ @
  whiskerR (concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) 1)) @
concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)
  refine (_ @ (concat_p_pp _ _ _)).
P: Type
b: P
s: 1 = 1
(s @ transport2_const surf b) @
concat_p1 (transport2 (fun _ : TwoSphere => P) surf b) =
((transport2_const surf b @@ s) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1)) @
(((concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1))^ @
  whiskerR (concat_p1 (transport2 (fun _ : TwoSphere => P) surf b)) 1) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b))
  refine (_ @ (ap (fun w => _ @ w) (whiskerR_p1 _)^)).
P: Type
b: P
s: 1 = 1
(s @ transport2_const surf b) @
concat_p1 (transport2 (fun _ : TwoSphere => P) surf b) =
((transport2_const surf b @@ s) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1)) @
concat_p1 (transport2 (fun _ : TwoSphere => P) surf b) f_ap.
P: Type
b: P
s: 1 = 1
s @ transport2_const surf b =
(transport2_const surf b @@ s) @
concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1)
  refine ((ap (fun w => w @ _) (whiskerL_1p_1 _)^) @ _).
P: Type
b: P
s: 1 = 1
whiskerL 1 s @ transport2_const surf b =
(transport2_const surf b @@ s) @
concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1)
  refine ((ap (fun w => _ @ w) (whiskerR_p1 _)^) @ _).
P: Type
b: P
s: 1 = 1
whiskerL 1 s @
(((concat_p1 (1 @ 1))^ @ whiskerR (transport2_const surf b) 1) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1)) =
(transport2_const surf b @@ s) @
concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1) cbn.
P: Type
b: P
s: 1 = 1
whiskerL 1 s @
((1 @ whiskerR (transport2_const surf b) 1) @
 concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1)) =
(transport2_const surf b @@ s) @
concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1)
  refine ((concat_p_pp _ _ _) @ _).
P: Type
b: P
s: 1 = 1
(whiskerL 1 s @ (1 @ whiskerR (transport2_const surf b) 1)) @
concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1) =
(transport2_const surf b @@ s) @
concat_p1 (transport2 (fun _ : TwoSphere => P) surf b @ 1) f_ap.
P: Type
b: P
s: 1 = 1
whiskerL 1 s @ (1 @ whiskerR (transport2_const surf b) 1) =
transport2_const surf b @@ s
  refine ((ap (fun w => _ @ w) (concat_1p _)) @ _).
P: Type
b: P
s: 1 = 1
whiskerL 1 s @ whiskerR (transport2_const surf b) 1 =
transport2_const surf b @@ s
  refine ((concat_whisker 1 _ _ 1 (transport2_const surf b) s)^ @ _).
P: Type
b: P
s: 1 = 1
whiskerR (transport2_const surf b) 1 @
whiskerL (transport2 (fun _ : TwoSphere => P) surf b @ transport_const 1 b) s =
transport2_const surf b @@ s
  
  symmetry.
P: Type
b: P
s: 1 = 1
transport2_const surf b @@ s =
whiskerR (transport2_const surf b) 1 @
whiskerL (transport2 (fun _ : TwoSphere => P) surf b @ transport_const 1 b) s
  refine ((ap (fun w => w @@ _) (concat_p1 _)^) @ _).
P: Type
b: P
s: 1 = 1
(transport2_const surf b @ 1) @@ s =
whiskerR (transport2_const surf b) 1 @
whiskerL (transport2 (fun _ : TwoSphere => P) surf b @ transport_const 1 b) s
  refine ((ap (fun w => _ @@ w) (concat_1p _)^) @ _).
P: Type
b: P
s: 1 = 1
(transport2_const surf (transport (fun _ : TwoSphere => P) 1 b) @ 1) @@
(1 @ s) =
whiskerR (transport2_const surf b) 1 @
whiskerL (transport2 (fun _ : TwoSphere => P) surf b @ transport_const 1 b) s
  refine ((concat_concat2 _ _ _ _)^ @ _).
P: Type
b: P
s: 1 = 1
(transport2_const surf (transport (fun _ : TwoSphere => P) 1 b) @@ 1) @
(1 @@ s) =
whiskerR (transport2_const surf b) 1 @
whiskerL (transport2 (fun _ : TwoSphere => P) surf b @ transport_const 1 b) s f_ap.
Defined.