Require Import Classes.interfaces.canonical_names.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Cubical.DPath Cubical.PathSquare.
Require Import Homotopy.Suspension.
Require Import Homotopy.HSpace.Core.
Require Import Homotopy.HSpace.Coherent.
Require Import Spaces.Spheres.

(** H-space structure on circle. *)

Section HSpace_S1.

  Context `{Univalence}.

  Definition Sph1_ind (P : Sphere 1 -> Type) (b : P North)
    (p : DPath P (merid North @ (merid South)^) b b)
    : forall x : Sphere 1, P x.
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
forall x : Sphere 1, P x
  Proof.
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
forall x : Sphere 1, P x
    srapply Susp_ind.
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
P North
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
P South
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
forall
x : Susp
      ((fix Sphere (n : trunc_index) : Type :=
          match n with
          | (_.+1 as n').+1 => Susp (Sphere n')
          | _ => Empty
          end) (-1)),
transport P (merid x) ?H_N = ?H_S
    1: exact b.
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
P South
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
forall
x : Susp
      ((fix Sphere (n : trunc_index) : Type :=
          match n with
          | (_.+1 as n').+1 => Susp (Sphere n')
          | _ => Empty
          end) (-1)), transport P (merid x) b = ?H_S
    1: exact (merid South # b).
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
forall
x : Susp
      ((fix Sphere (n : trunc_index) : Type :=
          match n with
          | (_.+1 as n').+1 => Susp (Sphere n')
          | _ => Empty
          end) (-1)),
transport P (merid x) b = transport P (merid South) b
    srapply Susp_ind; hnf.
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
transport P (merid North) b =
transport P (merid South) b
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
transport P (merid South) b =
transport P (merid South) b
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
forall x : Empty,
transport
  (fun y : Susp Empty =>
   transport P (merid y) b =
   transport P (merid South) b) (merid x) ?Goal =
?Goal0
    {
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
transport P (merid North) b =
transport P (merid South) b apply moveL_transport_p.
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
transport P (merid South)^
  (transport P (merid North) b) = b
      refine ((transport_pp _ _ _ _)^ @ _).
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
transport P (merid North @ (merid South)^) b = b
      exact p. }
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
transport P (merid South) b =
transport P (merid South) b
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
forall x : Empty,
transport
  (fun y : Susp Empty =>
   transport P (merid y) b =
   transport P (merid South) b) (merid x)
  (moveL_transport_p P (merid South)
     (transport P (merid North) b) b
     ((transport_pp P (merid North) (merid South)^ b)^ @
      p)) = ?Goal
    1: reflexivity.
H: Univalence
P: Sphere 1 -> Type
b: P North
p: DPath P (merid North @ (merid South)^) b b
forall x : Empty,
transport
  (fun y : Susp Empty =>
   transport P (merid y) b =
   transport P (merid South) b) (merid x)
  (moveL_transport_p P (merid South)
     (transport P (merid North) b) b
     ((transport_pp P (merid North) (merid South)^ b)^ @
      p)) = 1%path
    apply Empty_ind.
  Defined.

  Definition Sph1_rec (P : Type) (b : P) (p : b = b)
    : Sphere 1 -> P.
H: Univalence
P: Type
b: P
p: b = b
Sphere 1 -> P
  Proof.
H: Univalence
P: Type
b: P
p: b = b
Sphere 1 -> P
    srapply Susp_rec.
H: Univalence
P: Type
b: P
p: b = b
P
H: Univalence
P: Type
b: P
p: b = b
P
H: Univalence
P: Type
b: P
p: b = b
Susp
  ((fix Sphere (n : trunc_index) : Type :=
      match n with
      | (_.+1 as n').+1 => Susp (Sphere n')
      | _ => Empty
      end) (-1)) -> ?H_N = ?H_S
    1,2: exact b.
H: Univalence
P: Type
b: P
p: b = b
Susp
  ((fix Sphere (n : trunc_index) : Type :=
      match n with
      | (_.+1 as n').+1 => Susp (Sphere n')
      | _ => Empty
      end) (-1)) -> b = b
    simpl.
H: Univalence
P: Type
b: P
p: b = b
Susp Empty -> b = b
    srapply Susp_rec.
H: Univalence
P: Type
b: P
p: b = b
b = b
H: Univalence
P: Type
b: P
p: b = b
b = b
H: Univalence
P: Type
b: P
p: b = b
Empty -> ?H_N = ?H_S
    1: exact p.
H: Univalence
P: Type
b: P
p: b = b
b = b
H: Univalence
P: Type
b: P
p: b = b
Empty -> p = ?H_S
    1: reflexivity.
H: Univalence
P: Type
b: P
p: b = b
Empty -> p = 1%path
    exact Empty_rec.
  Defined.

  Definition Sph1_rec_beta_loop (P : Type) (b : P) (p : b = b)
    : ap (Sph1_rec P b p) (merid North @ (merid South)^) = p.
H: Univalence
P: Type
b: P
p: b = b
ap (Sph1_rec P b p) (merid North @ (merid South)^) = p
  Proof.
H: Univalence
P: Type
b: P
p: b = b
ap (Sph1_rec P b p) (merid North @ (merid South)^) = p
    rewrite ap_pp.
H: Univalence
P: Type
b: P
p: b = b
ap (Sph1_rec P b p) (merid North) @
ap (Sph1_rec P b p) (merid South)^ = p
    rewrite ap_V.
H: Univalence
P: Type
b: P
p: b = b
ap (Sph1_rec P b p) (merid North) @
(ap (Sph1_rec P b p) (merid South))^ = p
    rewrite 2 Susp_rec_beta_merid.
H: Univalence
P: Type
b: P
p: b = b
Susp_rec p 1 Empty_rec North @
(Susp_rec p 1 Empty_rec South)^ = p
    apply concat_p1.
  Defined.

  Definition s1_turn : forall x : Sphere 1, x = x.
H: Univalence
forall x : Sphere 1, x = x
  Proof.
H: Univalence
forall x : Sphere 1, x = x
    srapply Sph1_ind.
H: Univalence
(fun x : Sphere 1 => x = x) North
H: Univalence
DPath (fun x : Sphere 1 => x = x)
  (merid North @ (merid South)^) ?b ?b
    +
H: Univalence
(fun x : Sphere 1 => x = x) North exact (merid North @ (merid South)^).
    +
H: Univalence
DPath (fun x : Sphere 1 => x = x)
  (merid North @ (merid South)^)
  (merid North @ (merid South)^)
  (merid North @ (merid South)^) apply dp_paths_lr.
H: Univalence
((merid North @ (merid South)^)^ @
 (merid North @ (merid South)^)) @
(merid North @ (merid South)^) =
merid North @ (merid South)^
      by rewrite concat_Vp, concat_1p.
  Defined.

  #[export] Instance sgop_s1 : SgOp (psphere 1)
    := fun x y => Sph1_rec _ y (s1_turn y) x.

  #[export] Instance leftidentity_s1
    : LeftIdentity sgop_s1 (point (psphere 1)).
H: Univalence
LeftIdentity sgop_s1 (point (psphere 1))
  Proof.
H: Univalence
LeftIdentity sgop_s1 (point (psphere 1))
    srapply Sph1_ind.
H: Univalence
(fun x : Sphere 1 => sgop_s1 (point (psphere 1)) x = x)
  North
H: Univalence
DPath
  (fun x : Sphere 1 =>
   sgop_s1 (point (psphere 1)) x = x)
  (merid North @ (merid South)^) ?b ?b
    1: reflexivity.
H: Univalence
DPath
  (fun x : Sphere 1 =>
   sgop_s1 (point (psphere 1)) x = x)
  (merid North @ (merid South)^) 1%path 1%path
    apply dp_paths_lr.
H: Univalence
((merid North @ (merid South)^)^ @ 1) @
(merid North @ (merid South)^) = 1%path
    rewrite concat_p1.
H: Univalence
(merid North @ (merid South)^)^ @
(merid North @ (merid South)^) = 1%path
    apply concat_Vp.
  Defined.

  #[export] Instance rightidentity_s1
    : RightIdentity sgop_s1 (point (psphere 1)).
H: Univalence
RightIdentity sgop_s1 (point (psphere 1))
  Proof.
H: Univalence
RightIdentity sgop_s1 (point (psphere 1))
    srapply Sph1_ind.
H: Univalence
(fun x : Sphere 1 => sgop_s1 x (point (psphere 1)) = x)
  North
H: Univalence
DPath
  (fun x : Sphere 1 =>
   sgop_s1 x (point (psphere 1)) = x)
  (merid North @ (merid South)^) ?b ?b
    1: reflexivity.
H: Univalence
DPath
  (fun x : Sphere 1 =>
   sgop_s1 x (point (psphere 1)) = x)
  (merid North @ (merid South)^) 1%path 1%path
    apply dp_paths_FlFr.
H: Univalence
((ap
    (fun x : Sphere 1 => sgop_s1 x (point (psphere 1)))
    (merid North @ (merid South)^))^ @ 1) @
ap idmap (merid North @ (merid South)^) = 1%path
    rewrite concat_p1.
H: Univalence
(ap
   (fun x : Sphere 1 => sgop_s1 x (point (psphere 1)))
   (merid North @ (merid South)^))^ @
ap idmap (merid North @ (merid South)^) = 1%path
    rewrite ap_idmap.
H: Univalence
(ap
   (fun x : Sphere 1 => sgop_s1 x (point (psphere 1)))
   (merid North @ (merid South)^))^ @
(merid North @ (merid South)^) = 1%path
    rewrite Sph1_rec_beta_loop.
H: Univalence
(s1_turn (point (psphere 1)))^ @
(merid North @ (merid South)^) = 1%path
    apply concat_Vp.
  Defined.

  #[export] Instance hspace_s1 : IsHSpace (psphere 1) := {}.

  #[export] Instance iscoherent_s1 : IsCoherent (psphere 1) := idpath.

  Definition iscohhspace_s1 : IsCohHSpace (psphere 1)
    := Build_IsCohHSpace _ _ _.

  #[export] Instance associative_sgop_s1
    : Associative sgop_s1.
H: Univalence
Associative sgop_s1
  Proof.
H: Univalence
Associative sgop_s1
    intros x y z.
H: Univalence
x, y, z: psphere 1
sgop_s1 x (sgop_s1 y z) = sgop_s1 (sgop_s1 x y) z
    revert x.
H: Univalence
y, z: psphere 1
forall x : psphere 1,
sgop_s1 x (sgop_s1 y z) = sgop_s1 (sgop_s1 x y) z
    srapply Sph1_ind.
H: Univalence
y, z: psphere 1
(fun x : Sphere 1 =>
 sgop_s1 x (sgop_s1 y z) = sgop_s1 (sgop_s1 x y) z)
  North
H: Univalence
y, z: psphere 1
DPath
  (fun x : Sphere 1 =>
   sgop_s1 x (sgop_s1 y z) = sgop_s1 (sgop_s1 x y) z)
  (merid North @ (merid South)^) ?b ?b
    1: reflexivity.
H: Univalence
y, z: psphere 1
DPath
  (fun x : Sphere 1 =>
   sgop_s1 x (sgop_s1 y z) = sgop_s1 (sgop_s1 x y) z)
  (merid North @ (merid South)^) 1%path 1%path
    apply sq_dp^-1.
H: Univalence
y, z: psphere 1
PathSquare 1 1
  (ap (fun x : Sphere 1 => sgop_s1 x (sgop_s1 y z))
     (merid North @ (merid South)^))
  (ap (fun x : Sphere 1 => sgop_s1 (sgop_s1 x y) z)
     (merid North @ (merid South)^))
    revert y.
H: Univalence
z: psphere 1
forall y : psphere 1,
PathSquare 1 1
  (ap (fun x : Sphere 1 => sgop_s1 x (sgop_s1 y z))
     (merid North @ (merid South)^))
  (ap (fun x : Sphere 1 => sgop_s1 (sgop_s1 x y) z)
     (merid North @ (merid South)^))
    srapply Sph1_ind.
H: Univalence
z: psphere 1
(fun x : Sphere 1 =>
 PathSquare 1 1
   (ap (fun x0 : Sphere 1 => sgop_s1 x0 (sgop_s1 x z))
      (merid North @ (merid South)^))
   (ap (fun x0 : Sphere 1 => sgop_s1 (sgop_s1 x0 x) z)
      (merid North @ (merid South)^))) North
H: Univalence
z: psphere 1
DPath
  (fun x : Sphere 1 =>
   PathSquare 1 1
     (ap
        (fun x0 : Sphere 1 => sgop_s1 x0 (sgop_s1 x z))
        (merid North @ (merid South)^))
     (ap
        (fun x0 : Sphere 1 => sgop_s1 (sgop_s1 x0 x) z)
        (merid North @ (merid South)^)))
  (merid North @ (merid South)^) ?b ?b
    {
H: Univalence
z: psphere 1
(fun x : Sphere 1 =>
 PathSquare 1 1
   (ap (fun x0 : Sphere 1 => sgop_s1 x0 (sgop_s1 x z))
      (merid North @ (merid South)^))
   (ap (fun x0 : Sphere 1 => sgop_s1 (sgop_s1 x0 x) z)
      (merid North @ (merid South)^))) North apply (sq_flip_v (px0:=1) (px1:=1)).
H: Univalence
z: psphere 1
PathSquare 1 1
  (ap
     (fun x : Sphere 1 => sgop_s1 (sgop_s1 x North) z)
     (merid North @ (merid South)^))
  (ap
     (fun x : Sphere 1 => sgop_s1 x (sgop_s1 North z))
     (merid North @ (merid South)^))
      exact (ap_nat' (fun a => ap (fun b => sgop_s1 b z)
        (rightidentity_s1 a)) (merid North @ (merid South)^)). }
H: Univalence
z: psphere 1
DPath
  (fun x : Sphere 1 =>
   PathSquare 1 1
     (ap
        (fun x0 : Sphere 1 => sgop_s1 x0 (sgop_s1 x z))
        (merid North @ (merid South)^))
     (ap
        (fun x0 : Sphere 1 => sgop_s1 (sgop_s1 x0 x) z)
        (merid North @ (merid South)^)))
  (merid North @ (merid South)^)
  (let X := equiv_fun sq_flip_v in
   X
     (ap_nat'
        (fun a : psphere 1 =>
         ap (fun b : psphere 1 => sgop_s1 b z)
           (rightidentity_s1 a))
        (merid North @ (merid South)^)))
  (let X := equiv_fun sq_flip_v in
   X
     (ap_nat'
        (fun a : psphere 1 =>
         ap (fun b : psphere 1 => sgop_s1 b z)
           (rightidentity_s1 a))
        (merid North @ (merid South)^)))
    apply path_ishprop.
  Defined.

  #[export] Instance commutative_sgop_s1
    : Commutative sgop_s1.
H: Univalence
Commutative sgop_s1
  Proof.
H: Univalence
Commutative sgop_s1
    intros x y.
H: Univalence
x, y: psphere 1
sgop_s1 x y = sgop_s1 y x
    revert x.
H: Univalence
y: psphere 1
forall x : psphere 1, sgop_s1 x y = sgop_s1 y x
    srapply Sph1_ind.
H: Univalence
y: psphere 1
(fun x : Sphere 1 => sgop_s1 x y = sgop_s1 y x) North
H: Univalence
y: psphere 1
DPath (fun x : Sphere 1 => sgop_s1 x y = sgop_s1 y x)
  (merid North @ (merid South)^) ?b ?b
    1: cbn; symmetry; apply right_identity.
H: Univalence
y: psphere 1
DPath (fun x : Sphere 1 => sgop_s1 x y = sgop_s1 y x)
  (merid North @ (merid South)^)
  ((right_identity (sgop_s1 North y))^
   :
   (fun x : Sphere 1 => sgop_s1 x y = sgop_s1 y x)
     North)
  ((right_identity (sgop_s1 North y))^
   :
   (fun x : Sphere 1 => sgop_s1 x y = sgop_s1 y x)
     North)
    apply sq_dp^-1.
H: Univalence
y: psphere 1
PathSquare (right_identity (sgop_s1 North y))^
  (right_identity (sgop_s1 North y))^
  (ap (fun x : Sphere 1 => sgop_s1 x y)
     (merid North @ (merid South)^))
  (ap (sgop_s1 y) (merid North @ (merid South)^))
    revert y.
H: Univalence
forall y : psphere 1,
PathSquare (right_identity (sgop_s1 North y))^
  (right_identity (sgop_s1 North y))^
  (ap (fun x : Sphere 1 => sgop_s1 x y)
     (merid North @ (merid South)^))
  (ap (sgop_s1 y) (merid North @ (merid South)^))
    srapply Sph1_ind.
H: Univalence
(fun x : Sphere 1 =>
 PathSquare (right_identity (sgop_s1 North x))^
   (right_identity (sgop_s1 North x))^
   (ap (fun x0 : Sphere 1 => sgop_s1 x0 x)
      (merid North @ (merid South)^))
   (ap (sgop_s1 x) (merid North @ (merid South)^)))
  North
H: Univalence
DPath
  (fun x : Sphere 1 =>
   PathSquare (right_identity (sgop_s1 North x))^
     (right_identity (sgop_s1 North x))^
     (ap (fun x0 : Sphere 1 => sgop_s1 x0 x)
        (merid North @ (merid South)^))
     (ap (sgop_s1 x) (merid North @ (merid South)^)))
  (merid North @ (merid South)^) ?b ?b
    1: exact (ap_nat' rightidentity_s1 _).
H: Univalence
DPath
  (fun x : Sphere 1 =>
   PathSquare (right_identity (sgop_s1 North x))^
     (right_identity (sgop_s1 North x))^
     (ap (fun x0 : Sphere 1 => sgop_s1 x0 x)
        (merid North @ (merid South)^))
     (ap (sgop_s1 x) (merid North @ (merid South)^)))
  (merid North @ (merid South)^)
  (ap_nat' rightidentity_s1
     (merid North @ (merid South)^))
  (ap_nat' rightidentity_s1
     (merid North @ (merid South)^))
    srapply dp_ishprop.
  Defined.

End HSpace_S1.