open import Level 
  hiding (suc)
  renaming (zero to zeroL)

open import Chapter5.IDesc

module Chapter8.Equivalence.ToContornament
          {I J K L : Set}{u : K → I}{v : L → J}
          {D : func zeroL I J}
       where

open import Function

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.Contornament


toCorn : (o : orn D u v) → 
         Contornament (⟨ D ⟩) u v
toCorn o = 
  record { extend = λ l sh → extendO (orn.out o l) sh
         ; refine = λ {l} e p → refineO (orn.out o l) e p
         ; coherence⊢ = λ {l} sh e p → cohO (orn.out o l) e p }
  where extendO : ∀{D} → Orn u D → Shape D → Set
        extendO (insert S D⁺) sh = Σ[ s ∈ S ] extendO (D⁺ s) sh 
        extendO (`var i⁻¹) sh = ⊤
        extendO `1 sh = ⊤
        extendO (o₁ `× o₂) (sh₁ , sh₂) = extendO o₁ sh₁ × extendO o₂ sh₂
        extendO (`σ T⁺) (k , sh) = extendO (T⁺ k) sh
        extendO (`Σ T⁺) (s , sh) = extendO (T⁺ s) sh
        extendO (`Π T⁺) sh = (s : _) → extendO (T⁺ s) (sh s)
        extendO (deleteΣ {T = T} s o₁) (s' , sh) = 
                Σ[ q ∈ s' ≡ s ] 
                  extendO o₁ (subst (λ s → Shape (T s)) q sh)
        extendO (deleteσ {T = T} k o₁) (k' , sh) = 
                Σ[ q ∈ k' ≡ k ]
                  extendO o₁ (subst (λ k → Shape (T k)) q sh)

        refineO : ∀{D sh} → (O : Orn u D) → extendO O sh → Pos D sh → K
        refineO (insert S D⁺) (s , e) p = refineO (D⁺ s) e p
        refineO (`var (inv k)) e p = k
        refineO `1 e ()
        refineO (o₁ `× o₂) (e₁ , _) (inj₁ x) = refineO o₁ e₁ x
        refineO (o₁ `× o₂) (_ , e₂) (inj₂ y) = refineO o₂ e₂ y
        refineO (`σ T⁺) e p = refineO (T⁺ _) e p
        refineO (`Σ T⁺) e p = refineO (T⁺ _) e p
        refineO (`Π T⁺) e (s , p) = refineO (T⁺ s) (e s) p
        refineO {sh = s , sh} (deleteΣ .s o₁) (refl , e) p = refineO o₁ e p
        refineO {sh = k , sh} (deleteσ .k o₁) (refl , e) p = refineO o₁ e p

        cohO : ∀{D sh} → (O : Orn u D)(e : extendO O sh)(p : Pos D sh) → 
               u (refineO O e p) ≡ Next D sh p
        cohO (insert S D⁺) (s , e) p = cohO (D⁺ s) e p
        cohO (`var (inv k)) e p = refl
        cohO `1 e ()
        cohO (o₁ `× o₂) (e₁ , _) (inj₁ x) = cohO o₁ e₁ x
        cohO (o₁ `× o₂) (_ , e₂) (inj₂ y) = cohO o₂ e₂ y
        cohO (`σ T⁺) e p = cohO (T⁺ _) e p
        cohO (`Σ T⁺) e p = cohO (T⁺ _) e p
        cohO (`Π T⁺) e (s , p) = cohO (T⁺ s) (e s) p
        cohO {sh = s , sh} (deleteΣ .s o) (refl , e) p = cohO o e p
        cohO {sh = k , sh} (deleteσ .k o) (refl , e) p = cohO o e p