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)