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

open import Function

open import Relation.Binary.PropositionalEquality

open import Data.Product

open import Chapter5.Container
open import Chapter5.Container.Morphism

-- * Definition

record _⇒c[_∣_]_ (φ' : 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 φ' (subst id ρ p)) ≡ n φ p
-- open _⇒c[_∣_]_ public

{-
_⇒c[_]_ : {O+ O : Set}(φ+ : O+ ▸ O+)(forgetO+ : O+ → O)(φ : O ▸ O) → Set₁
φ+ ⇒c[ forgetO+ ] φ = φ+ ⇒c[ forgetO+ ∣ forgetO+ ] φ
-}

-- * Sub-category of Containers:

to⇒ : {φ' : I ▸ J}{φ : K ▸ L}{u : I → K}{v : J → L} →
       φ' ⇒c[ u ∣ v ] φ → φ' ⇒[ u ∣ v ] φ
to⇒ τ = record { σ = σ τ
               ; ρ = subst id (ρ τ)
               ; q = q τ }
    where open _⇒c[_∣_]_ public