module Chapter8.Container.CobaseChange
         {I J K L : Set}
       where

open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Chapter5.Container

⟨_,_⟩!_ : (u : I  K)(v : J  L) 
          I  J  K  L
 u , v ⟩! φ = 
  record { S = λ l  Σ[ j  J ] v j  l × S φ j 
         ; P = λ { (_ , q , sh)  P φ sh }
         ; n = λ pos  u (n φ pos) }