{-# OPTIONS --without-K #-}

open import lib.Basics
open import lib.types.Span
open import lib.types.Pointed
open import lib.types.Pushout
open import lib.types.PushoutFlattening
open import lib.types.Unit
open import lib.types.Paths
open import lib.cubical.Square

-- Suspension is defined as a particular case of pushout

module lib.types.Suspension where

module _ {i} (A : Type i) where

  suspension-span : Span
  suspension-span = span Unit Unit A  _  tt)  _  tt)

  Suspension : Type i
  Suspension = Pushout suspension-span

  north : Suspension
  north = left tt

  south : Suspension
  south = right tt

  merid : A  north == south
  merid x = glue x

  module SuspensionElim {j} {P : Suspension  Type j} (n : P north)
    (s : P south) (p : (x : A)  n == s [ P  merid x ])
    = PushoutElim  _  n)  _  s) p

  open SuspensionElim public using () renaming (f to Suspension-elim)

  module SuspensionRec {j} {C : Type j} (n s : C) (p : A  n == s)
    = PushoutRec {d = suspension-span}  _  n)  _  s) p

  module SuspensionRecType {j} (n s : Type j) (p : A  n  s)
    = PushoutRecType {d = suspension-span}  _  n)  _  s) p

suspension-⊙span :  {i}  Ptd i  ⊙Span
suspension-⊙span X =
  ⊙span ⊙Unit ⊙Unit X (⊙cst {X = X}) (⊙cst {X = X})

⊙Susp :  {i}  Ptd i  Ptd i
⊙Susp (A , _) = ⊙[ Suspension A , north A ]


σloop :  {i} (X : Ptd i)  fst X  north (fst X) == north (fst X)
σloop (_ , x₀) x = merid _ x  ! (merid _ x₀)

σloop-pt :  {i} {X : Ptd i}  σloop X (snd X) == idp
σloop-pt {X = (_ , x₀)} = !-inv-r (merid _ x₀)


module FlipSusp {i} {A : Type i} = SuspensionRec A
  (south A) (north A) (!  merid A)

flip-susp :  {i} {A : Type i}  Suspension A  Suspension A
flip-susp = FlipSusp.f

⊙flip-susp :  {i} (X : Ptd i)  fst (⊙Susp X ⊙→ ⊙Susp X)
⊙flip-susp X = (flip-susp , ! (merid _ (snd X)))

module _ {i j} where

  module SuspFmap {A : Type i} {B : Type j} (f : A  B) =
    SuspensionRec A (north B) (south B) (merid B  f)

  susp-fmap : {A : Type i} {B : Type j} (f : A  B)
     (Suspension A  Suspension B)
  susp-fmap = SuspFmap.f

  ⊙susp-fmap : {X : Ptd i} {Y : Ptd j} (f : fst (X ⊙→ Y))
     fst (⊙Susp X ⊙→ ⊙Susp Y)
  ⊙susp-fmap (f , fpt) = (susp-fmap f , idp)

module _ {i} where

  susp-fmap-idf : (A : Type i)   a  susp-fmap (idf A) a == a
  susp-fmap-idf A = Suspension-elim _ idp idp $ λ a 
    ↓-='-in (ap-idf (merid _ a)  ! (SuspFmap.glue-β (idf A) a))

  ⊙susp-fmap-idf : (X : Ptd i)
     ⊙susp-fmap (⊙idf X) == ⊙idf (⊙Susp X)
  ⊙susp-fmap-idf X = ⊙λ= (susp-fmap-idf (fst X)) idp

module _ {i j} where

  susp-fmap-cst : {A : Type i} {B : Type j} (b : B)
    (a : Suspension A)  susp-fmap (cst b) a == north _
  susp-fmap-cst b = Suspension-elim _ idp (! (merid _ b)) $  a 
    ↓-app=cst-from-square $ SuspFmap.glue-β (cst b) a ∙v⊡ tr-square _)

  ⊙susp-fmap-cst : {X : Ptd i} {Y : Ptd j}
     ⊙susp-fmap (⊙cst {X = X} {Y = Y}) == ⊙cst
  ⊙susp-fmap-cst = ⊙λ= (susp-fmap-cst _) idp

module _ {i j k} where

  susp-fmap-∘ : {A : Type i} {B : Type j} {C : Type k} (g : B  C) (f : A  B)
    (σ : Suspension A)  susp-fmap (g  f) σ == susp-fmap g (susp-fmap f σ)
  susp-fmap-∘ g f = Suspension-elim _
    idp
    idp
     a  ↓-='-in $
      ap-∘ (susp-fmap g) (susp-fmap f) (merid _ a)
       ap (ap (susp-fmap g)) (SuspFmap.glue-β f a)
       SuspFmap.glue-β g (f a)
       ! (SuspFmap.glue-β (g  f) a))

  ⊙susp-fmap-∘ : {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
    (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
     ⊙susp-fmap (g ⊙∘ f) == ⊙susp-fmap g ⊙∘ ⊙susp-fmap f
  ⊙susp-fmap-∘ g f = ⊙λ= (susp-fmap-∘ (fst g) (fst f)) idp


{- Extract the 'glue component' of a pushout -}
module _ {i j k} {s : Span {i} {j} {k}} where

  module ExtGlue = PushoutRec {d = s} {D = Suspension (Span.C s)}
     _  north _)  _  south _) (merid _)

  ext-glue = ExtGlue.f

module _ {i j k} {s : Span {i} {j} {k}} {x₀ : Span.A s} where

  ⊙ext-glue :
    fst ((Pushout s , left x₀) ⊙→ (Suspension (Span.C s) , north _))
  ⊙ext-glue = (ext-glue , idp)