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

open import Function

open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Sum

open import Relation.Binary.PropositionalEquality

open import Chapter2.Logic

open import Chapter5.Container



record _⇒[_∣_]_ (φ' : I ▸ J)
                (u : I → K)(v : J → L)
                (φ : K ▸ L) : Set where
  field
    σ : ∀{j} → S φ' j → S φ (v j)
    ρ : ∀{j : J}{sh' : S φ' j} → P φ (σ sh') → P φ' sh'
    q : ∀{j : J}{sh' : S φ' j} → 
        (p : P φ (σ sh')) → u (n φ' (ρ p)) ≡ n φ p
--open _⇒[_∣_]_ public

{-
_⇒[_]_ : (φ' : I ▸ I)(u : I → K)(φ : K ▸ K) → Set
φ' ⇒[ u ] φ = φ' ⇒[ u ∣ u ] φ

_⇒_ : {O : Set}(φ : O ▸ O)(φ' : O ▸ O) → Set
φ ⇒ φ' = φ ⇒[ id ] φ'
-}

⟦_⟧⇒ : {φ' : I ▸ J}{φ : K ▸ L}{u : I → K}{v : J → L} →
       (τ : φ' ⇒[ u ∣ v ] φ) → 
       ∀ (X : Pow K) → ⟦ φ' ⟧ (X ∘ u) ⇒ ⟦ φ ⟧ X ∘ v
⟦ τ ⟧⇒ X (sh , Xs) = σ sh , λ pos → subst X (q pos) (Xs (ρ pos))
  where open _⇒[_∣_]_ τ