open import Chapter5.Container

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

open import Function

open import Data.Product 

open import Relation.Binary.PropositionalEquality

record Contornament  
         (φ : I ▸ J)
         (u : K → I)(v : L → J) : Set₁ where
  field
    -- We can give more precise shapes:
    extend : (l : L)(sh : S φ (v l)) → Set

    -- We can be more restrictive for the next index:
    refine : {l : L}{sh : S φ (v l)}(e : extend l sh) → P φ sh → K
    coherence⊢ : {l : L}(sh : S φ (v l))(e : extend l sh)(p : P φ sh) →
                    u (refine e p) ≡ n φ p 


module Interpretation 
         {φ : I ▸ J}{u : K → I}{v : L → J} 
       where

  ⟦_⟧corn : Contornament φ u v → K ▸ L
  ⟦ υ ⟧corn = 
     record { S = λ l → Σ[ sh ∈ S φ (v l) ] extend υ l sh
            ; P = P φ ∘ proj₁
            ; n = λ {l}{sh} → refine υ (proj₂ sh) }
    where open Contornament

open Interpretation public