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) }