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