module Cartesian.Translation where open import Stdlib open import Signature open import Ornament open import Cartesian open import Inverse module ToOrnament {I⁺ I}{Σ⁺ : Sig I⁺}{Σ : Sig I}{v : I⁺ → I} where toOrnament : Cartesian Σ⁺ Σ v → COrn Σ I⁺ v toOrnament τ = record { extend = λ i⁺ op → (σ i⁺) ⁻¹ op ; refine = λ { i⁺ op (op⁺ , q) ar → Ty (subst id (ρ i⁺ op⁺) (subst (Sig.Ar Σ) (sym q) ar)) } ; coh = λ { i⁺ .(σ i⁺ op⁺) (op⁺ , refl) ar → coh i⁺ op⁺ (subst (Sig.Ar Σ) (sym refl) ar) } } where open Cartesian.Cartesian τ open Sig Σ⁺ module ToCartesian {I}{Σ : Sig I}{I⁺}{v : I⁺ → I} where toCartesian : (τ : COrn Σ I⁺ v) → Cartesian ⟦ τ ⟧COrn Σ v toCartesian τ = record { σ = λ { i⁺ (op , ext) → op } ; ρ = λ { i⁺ (op , ext) → refl } ; coh = λ { i⁺ (op , ext) ar → coh i⁺ op ext ar } } where open COrn τ