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