module DS.SigmaDelta where

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

{- Dybjer-Setzer codes, containerized -}
data DS (D : Set1) (E : Set1) : Set1 where
   ι : E →  DS D E
   σδ : (SP : Cont) -> (cont SP D -> DS D E) -> DS D E

⟦_⟧₀ : {D E : Set1} -> DS D E -> Fam D -> Set
⟦ ι e ⟧₀ X = ⊤
⟦ σδ (S , P)f ⟧₀ (U , T) = Σ[ x ∈ ((S ◃ P) U) ] ⟦ f (◃-map S P T x) ⟧₀ (U , T)

⟦_⟧₁ : {D E : Set1} -> (c : DS D E) -> (F : Fam D) -> ⟦ c ⟧₀ F -> E
⟦ ι e ⟧₁ X _ = e
⟦ σδ (S , P) f ⟧₁ (U , T) (x , g) = ⟦  f (◃-map S P T x) ⟧₁ (U , T) g

⟦_⟧ : {D E : Set1} -> DS D E -> Fam D -> Fam E
⟦ c ⟧ X = ⟦ c ⟧₀ X , ⟦ c ⟧₁ X

-- DS D is functorial
DS-map : {D E E' : Set₁} -> (E -> E') -> DS D E  -> DS D E'
DS-map h (ι e) = ι (h e)
DS-map h (σδ (S , P) f) = σδ (S , P) (λ x → DS-map h (f x))