module DS.Arg where

-- Dybjer-Setzer codes like it's 1999 (TLCA paper), i.e. with ι not
-- carrying a D, but a separate Arg type. This version is also
-- containerised up.

open import Prelude.Basic
open import Prelude.Equality
open import Prelude.Fam
open import Prelude.Container

data SP (D : Set₁) : Set₁ where
  ι  : (X : Cont) → SP D
  σδ : LCFam D (SP D) → SP D

Arg : {D : Set₁} → (SP D) → Set₁
Arg {D = D} (ι X) = cont X D
Arg {D = D} (σδ (Q , h)) = Σ[ x ∈ cont Q D ] (Arg (h x))

DS' : (D E : Set₁) → Set₁
DS' D E = Σ[ Q ∈ SP D ] (Arg Q -> E)

-- The decoding

mutual
  arg : {D : Set1} -> SP D -> Fam D -> Set
  arg (ι X) (U , T) = cont X U
  arg (σδ (Q , h)) Z@(U , T)
    = Σ[ x ∈ cont Q U ] arg (h (cont-map Q T x)) Z

  ⟦_⟧map : ∀ {D} -> (c : SP D)(Z : Fam D) -> arg c Z -> Arg c
  ⟦ ι X ⟧map (U , T) (x , g) = x , T ∘ g
  ⟦ σδ (Q , h) ⟧map Z@(U , T) (x , y)
    = cont-map Q T x , ⟦ h _ ⟧map Z y

⟦_⟧ : {D E : Set1} -> DS' D E -> Fam D -> Fam E
⟦ c , α ⟧ Z = arg c Z , α ∘ ⟦ c ⟧map Z

-- DS' D is functorial

DS-map : {D E E' : Set₁} → (E -> E') -> DS' D E -> DS' D E'
DS-map f (c , α) = (c , (f ∘ α))

-- ... and it is monadic

η : {D E : Set1} -> E -> DS' D E
η e = ι K1-Cont , (λ _ → e)

μ0 : {D E : Set1} -> (c : SP D) -> (α : Arg c -> DS' D E) -> SP D
μ0 (ι X) α = σδ (X , (proj₁ ∘ α))
μ0 (σδ (Q , h)) α =  σδ (Q , (λ x → μ0 (h x) (λ y → α (x , y))))

μ1 : ∀ {D E} c α -> Arg (μ0 {D} {E} c α) -> E
μ1 (ι X) α (x , y) = proj₂ (α x) y
μ1 (σδ (Q , h)) α (x , y) = μ1 (h x) (α ∘ (λ z → x , z)) y

-- Note: μ0 can be defined in terms of proj₁ ∘ α only, but μ1 then
-- mentions proj₁ ∘ α in its type, and uses proj₂ ∘ α, so cannot be
-- defined in terms of proj₂ ∘ α only (whatever that would mean)

μ : {D E : Set1} -> DS' D (DS' D E) -> DS' D E
μ (c , α) = (μ0 c α , μ1 c α)

-- Note: it seems impossible to define μ if we add a π constructor to
-- SP D. IRish IR gets away with it because it has a proper
-- sigma, which makes μ easy.

open _Fam⇒_

-- triangle laws up to trivial differences in decoding (I only give
-- maps back and forth, but they are very simple)

triangleL : {D E : Set1} -> (c : DS' D E) -> ∀ {Z} ->
            ⟦ μ (DS-map η c) ⟧ Z Fam⇒ ⟦ c ⟧ Z
triangleL (c , α) = triangleL0 c α , triangleL1 c α
  where
    triangleL0 : {D E : Set1} -> (c : SP D)(α : Arg c -> E) ->
                 ∀ {Z} -> arg (μ0 c (η ∘ α)) Z -> arg c Z
    triangleL0 (ι X) α (x , _) = x
    triangleL0 (σδ (Q , h)) α {(U , T)} (x , y)
      = x , triangleL0 (h _) (λ z → α  _) y

    triangleL1 : {D E : Set1} -> (c : SP D)(α : Arg c -> E) ->
                 ∀ {Z} → (x : arg (μ0 c (η ∘ α)) Z) ->
                 μ1 c (η ∘ α) (⟦ μ0 c (η ∘ α) ⟧map Z x)
                                      ≡ α (⟦ c ⟧map Z (triangleL0 c α x))
    triangleL1 (ι X) α (x , _) = refl
    triangleL1 (σδ (Q , h)) α {U , T} (x , y)
      = triangleL1 (h _) (λ z → α  _) y

triangleR : {D E : Set1} -> (c : DS' D E) -> ∀ {Z} ->
            ⟦ c ⟧ Z Fam⇒ ⟦ μ (DS-map η c) ⟧ Z
triangleR (c , α) = triangleR0 c α , triangleR1 c α
  where
    triangleR0 : {D E : Set1} -> (c : SP D)(α : Arg c -> E) ->
                 ∀ {Z} -> arg c Z -> arg (μ0 c (η ∘ α)) Z
    triangleR0 (ι X) α x = x , _ , λ ()
    triangleR0 (σδ (Q , h)) α {(U , T)} (x , y) = x , triangleR0 (h _) (λ z → α _) y

    triangleR1 : {D E : Set1} -> (c : SP D)(α : Arg c -> E) ->
                 ∀ {Z} → (x : arg c Z) ->
                 α (⟦ c  ⟧map Z x) ≡ μ1 c (η ∘ α)
                                      (⟦ μ0 c (η ∘ α) ⟧map Z (triangleR0 c α x))
    triangleR1 (ι X) α x = refl
    triangleR1 (σδ (Q , h)) α (x , y) = triangleR1 (h _) (λ z → α _) y

triangleLL : {D E : Set1} -> (c : DS' D (DS' D E)) -> ∀ {Z} ->
            ⟦ μ (η c) ⟧ Z Fam⇒ ⟦ c ⟧ Z
triangleLL (c , α) = proj₂ , (λ x → refl)

triangleRR : {D E : Set1} -> (c : DS' D (DS' D E)) -> ∀ {Z} ->
             ⟦ c ⟧ Z Fam⇒ ⟦ μ (η c) ⟧ Z
triangleRR c = (λ x → (_ , (λ ())) , x) , (λ x → refl)

-- associtivity (on the nose!)

assocL : {D E : Set1} -> (c : DS' D (DS' D (DS' D E))) -> ∀ {Z} ->
            ⟦ μ (DS-map μ c) ⟧ Z Fam⇒ ⟦ μ (μ c) ⟧ Z
assocL (c , α) = assocL0 c α , assocL1 c α
  where
    assocL0 : {D E : Set1} -> (c : SP D) ->
              (α : Arg c -> DS' D (DS' D E)) -> ∀ {Z} ->
              arg (μ0 c (μ ∘ α)) Z -> arg (μ0 (μ0 c α) (μ1 c α)) Z
    assocL0 (ι X) α x              = x
    assocL0 (σδ (Q , h)) α (x , y) = x , assocL0 (h _) (λ z → α _) y

    assocL1 : {D E : Set1} -> (c : SP D) ->
              (α : Arg c -> DS' D (DS' D E)) -> ∀ {Z} ->
              (x : arg (μ0 c (μ ∘ α)) Z) ->
              μ1 c (μ ∘ α) (⟦ μ0 c (μ ∘ α) ⟧map Z x)
                ≡ μ1 (μ0 c α) (μ1 c α)
                     (⟦ μ0 (μ0 c α) (μ1 c α) ⟧map Z (assocL0 c α x) )
    assocL1 (ι X) α x              = refl
    assocL1 (σδ (Q , h)) α (x , y) = assocL1 (h _) (λ z → α _) y

assocR : {D E : Set1} -> (c : DS' D (DS' D (DS' D E))) -> ∀ {Z} ->
         ⟦ μ (μ c) ⟧ Z Fam⇒ ⟦ μ (DS-map μ c) ⟧ Z
assocR (c , α) = assocR0 c α , assocR1 c α
  where
    assocR0 : {D E : Set1} -> (c : SP D) ->
              (α : Arg c -> DS' D (DS' D E)) -> ∀ {Z} ->
              arg (μ0 (μ0 c α) (μ1 c α)) Z -> arg (μ0 c (μ ∘ α)) Z
    assocR0 (ι X) α x              = x
    assocR0 (σδ (Q , h)) α (x , y) = x , assocR0 (h _) (λ z → α _) y

    assocR1 : {D E : Set1} -> (c : SP D) ->
              (α : Arg c -> DS' D (DS' D E)) -> ∀ {Z} ->
              (x : arg (μ0 (μ0 c α) (μ1 c α)) Z) ->
              μ1 (μ0 c α) (μ1 c α) (⟦ μ0 (μ0 c α) (μ1 c α) ⟧map Z x)
                ≡ μ1 c (μ ∘ α) (⟦ μ0 c (μ ∘ α) ⟧map Z (assocR0 c α x))
    assocR1 (ι X) α x              = refl
    assocR1 (σδ (Q , h)) α (x , y) = assocR1 (h _) (λ z → α _) y