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