Chapter5.Container

module Chapter5.Container where 

open import Function

open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Sum

open import Chapter2.Logic


infixl 60 _▸_
record _▸_ (I J : Set) : Set1 where
  field
    S : J → Set
    P : {j : J} → S j → Set
    n : {j : J}{sh : S j} → P sh → I
open _▸_ public


⟦_⟧ : {I J : Set} → I ▸ J → Pow I → Pow J
⟦ φ ⟧ X j = Σ[ sh ∈ S φ j ] ((p : P φ sh) → X (n φ p))


⟦_⟧map : {I J : Set}{X Y : Pow I} → (φ : I ▸ J) → 
           (f : X ⇒ Y) → ⟦ φ ⟧ X ⇒ ⟦ φ ⟧ Y
⟦ φ ⟧map f (sh , pos) = (sh , f ∘ pos)