open import Chapter5.Container

open import Chapter8.Container.Morphism.Cartesian

module Chapter8.Equivalence.ToOrn
          {I J K L : Set}{u : K → I}{v : L → J}
          {φ' : K ▸ L}{φ : I ▸ J}
       where

open import Function

open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Chapter2.Logic

open import Chapter5.Equivalence.ToDesc

open import Chapter8.Ornament


toOrn : φ' ⇒c[ u ∣ v ] φ → orn ⟨ φ ⟩⁻¹ u v
toOrn τ = orn.mk λ l → 
          `Σ λ sh → 
          insert (S φ' l) λ ext → 
          insert (σ τ ext ≡ sh) λ invert → 
          `Π λ ps → 
          `var (invView (n φ' (subst id (ρ τ) (subst (P φ) (sym invert) ps)))
               (trans (q τ (subst (P φ) (sym invert) ps))
                      (sym (cong₂' (λ sh ps → n φ {_}{sh} ps) (sym invert) refl))))
      
    where open _⇒c[_∣_]_ public

          invView : ∀{A B : Set}{b}{f : A → B} → 
                    (a : A) → f a ≡ b → f ⁻¹ b
          invView a refl = inv a

          cong₂' : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Set c}
                   (f : (a : A) → B a → C) {x y u v} → (q : x ≡ y) → u ≡ v → f x u ≡ f y (subst B q v)
          cong₂' f refl refl = refl