Library HoTT.Homotopy.HSpaceS1

Require Import Classes.interfaces.canonical_names.
Require Import Cubical.DPath Cubical.PathSquare.
Require Import Homotopy.Suspension.
Require Import Homotopy.HSpace.Core.
Require Import Homotopy.HSpace.Coherent.
Require Import Spaces.Spheres.

Section HSpace_S1.

  Context `{Univalence}.

  Definition Sph1_ind (P : Sphere 1 → Type) (b : P North)
    (p : DPath P (merid North @ (merid South)^) b b)
    : ∀ x : Sphere 1, P x.
  Proof.
    srapply Susp_ind.
    1: exact b.
    1: exact (merid South # b).
    srapply Susp_ind; hnf.
    { apply moveL_transport_p.
      refine ((transport_pp _ _ _ _)^ @ _).
      apply p. }
    1: reflexivity.
    apply Empty_ind.
  Defined.

  Definition Sph1_rec (P : Type) (b : P) (p : b = b)
    : Sphere 1 → P.
  Proof.
    srapply Susp_rec.
    1,2: exact b.
    simpl.
    srapply Susp_rec.
    1: exact p.
    1: reflexivity.
    apply 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.
  Proof.
    rewrite ap_pp.
    rewrite ap_V.
    rewrite 2 Susp_rec_beta_merid.
    apply concat_p1.
  Defined.

  Definition s1_turn : ∀ x : Sphere 1, x = x.
  Proof.
    srapply Sph1_ind.
    + exact (merid North @ (merid South)^).
    + apply dp_paths_lr.
      by rewrite concat_Vp, concat_1p.
  Defined.

  Global Instance sgop_s1 : SgOp (psphere 1)
    := fun x y ⇒ Sph1_rec _ y (s1_turn y) x.

  Global Instance leftidentity_s1
    : LeftIdentity sgop_s1 (point (psphere 1)).
  Proof.
    srapply Sph1_ind.
    1: reflexivity.
    apply dp_paths_lr.
    rewrite concat_p1.
    apply concat_Vp.
  Defined.

  Global Instance rightidentity_s1
    : RightIdentity sgop_s1 (point (psphere 1)).
  Proof.
    srapply Sph1_ind.
    1: reflexivity.
    apply dp_paths_FlFr.
    rewrite concat_p1.
    rewrite ap_idmap.
    rewrite Sph1_rec_beta_loop.
    apply concat_Vp.
  Defined.

  Global Instance hspace_s1 : IsHSpace (psphere 1) := {}.

  Global Instance iscoherent_s1 : IsCoherent (psphere 1) := idpath.

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

  Global Instance associative_sgop_s1
    : Associative sgop_s1.
  Proof.
    intros x y z.
    revert x.
    srapply Sph1_ind.
    1: reflexivity.
    apply sq_dp^-1.
    revert y.
    srapply Sph1_ind.
    { apply (sq_flip_v (px0:=1) (px1:=1)).
      exact (ap_nat' (fun a ⇒ ap (fun b ⇒ sgop_s1 b z)
        (rightidentity_s1 a)) (merid North @ (merid South)^)). }
    apply path_ishprop.
  Defined.

  Global Instance commutative_sgop_s1
    : Commutative sgop_s1.
  Proof.
    intros x y.
    revert x.
    srapply Sph1_ind.
    1: cbn; symmetry; apply right_identity.
    apply sq_dp^-1.
    revert y.
    srapply Sph1_ind.
    1: exact (ap_nat' rightidentity_s1 _).
    srapply dp_ishprop.
  Defined.

End HSpace_S1.