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)