module Chapter5.Container.Composition
         {I J K : Set}
       where

open import Data.Product

open import Chapter5.Container


_∘_ : J ▸ K → I ▸ J → I ▸ K
ψ ∘ φ = 
  record { S = λ k → ⟦ ψ ⟧ (λ j → S φ j) k
         ; P = λ { {k} (sh , pos) → Σ[ p ∈ P ψ sh ] P φ (pos p) }
         ; n = λ { {k}{sh , pos} (pψ , pφ) → n φ pφ } }