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