open import Chapter5.Container

module Chapter8.Container.Morphism.Contornament.Identity 
         {I J : Set}{φ : I ▸ J}
       where

open import Function

open import Data.Unit

open import Relation.Binary.PropositionalEquality

open import Chapter5.Container

open import Chapter8.Container.Morphism.Contornament

idO : Contornament φ id id
idO =
  record { extend = λ _ _ → ⊤
         ; refine = λ _ p → n φ p
         ; coherence⊢ = λ sh e p → refl }