open import Chapter5.Container

module Chapter8.Container.Morphism.Cartesian.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.Cartesian


idO : φ ⇒c[ id ∣ id ] φ
idO = record { σ = id
             ; ρ = refl
             ; q = λ p → refl }