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