module Prelude.Container where

open import Prelude.Basic
open import Prelude.Equality

-- Containers

Cont :  {a b} -> Set (lsuc (a  b))
Cont {a} {b} = Σ (Set a)  S -> (S  Set b))

-- The functor Set -> Set the container represents

-- action on sets

_◃_ :  {a b c}  (S : Set a) -> (P : S -> Set b) -> Set c  Set (a  b  c)
(S  P) X = Σ S  s -> (P s  X))

cont :  {a b c}  Cont {a}{b} -> Set c -> Set (a  b  c)
cont (S , P) = (S  P)

-- action on functions

◃-map :  {a b c d} -> (S : Set a) -> (P : S -> Set b) ->
       {X : Set c}{Y : Set d} -> (X -> Y) ->
      (S  P) X -> (S  P) Y
◃-map S P f (s , g) = (s , f  g)

cont-map :  {a b c d} -> (H : Cont {a}{b}) ->
          {X : Set c}{Y : Set d} -> (X -> Y) ->
          cont H X -> cont H Y
cont-map (S , P) = ◃-map S P

-- The container representing the functor X ↦ 1

K1-Cont :  {a} {b} -> Cont {a} {b}
K1-Cont = Lift  ,  _  )

-- All predicate transformer

All :  {a b x p} -> {S : Set a} -> {P : S -> Set b} ->
      {X : Set x}(T : X -> Set p) -> (S  P) X -> Set (p  b)
All {P = P} T (s , f) = (x : P s) -> T (f x)

-- Large containers

LC :  {a b c}  {D : Set c} -> Cont {lsuc (a  b)} {a  b  c}
LC {a} {b} {D = D} = (Cont {a} {b} , λ H  cont H D)

LCFam :  {a b}   Set (lsuc a) -> Set (lsuc b) -> Set (lsuc (a  b))
LCFam {a} {b} D E = cont (LC {a} {b} {lsuc a} {D = D}) E

LCFam-map :  {a b}  {I : Set (lsuc a)}{X Y : Set (lsuc b)} -> (X -> Y) ->
            LCFam I X -> LCFam I Y
LCFam-map f P = cont-map LC f P