module Chapter8.Container.BaseChange
         {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) →
          K ▸ L → I ▸ J
⟨ u , v ⟩* φ = 
  record { S = λ j → S φ (v j)
         ; P = λ sh → Σ[ pos ∈ P φ sh ] Σ[ i ∈ I ] n φ pos ≡ u i
         ; n =  λ {(pos , i , _) →  i } }