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