{-# 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)