open import Chapter5.Container

module Chapter8.Equivalence.ToCartesian 
          {I J K L : Set}{u : K  I}{v : L  J}
          {φ : I  J}
       where

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

open import Relation.Binary.PropositionalEquality

open import Chapter2.Logic

open import Chapter5.Equivalence.ToContainer

open import Chapter8.Ornament
open import Chapter8.Container.Morphism.Cartesian
open import Chapter8.Container.Morphism.Contornament


toCartesian : (υ : Contornament φ u v)  
               υ ⟧corn ⇒c[ u  v ] φ
toCartesian υ =  
  record { σ = proj₁
         ; ρ = refl
         ; q = λ p  coherence⊢ υ _ _ p }
  where open Contornament