module Chapter8.Ornament where
open import Level
renaming ( zero to zeroL
; suc to sucL )
open import Function
open import Data.Nat hiding (_⊔_)
open import Data.Fin
open import Chapter2.Logic
open import Chapter5.IDesc
data Orn {ℓ k}{I K : Set k}(u : I → K) : IDesc ℓ K → Set (sucL ℓ ⊔ k) where
insert : ∀{D} → (S : Set ℓ)(D⁺ : S → Orn u D) → Orn u D
`var : ∀{i} → (i⁻¹ : u ⁻¹ i) → Orn u (`var i)
`1 : Orn u `1
_`×_ : ∀{D D'} → (D⁺ : Orn u D)(D'⁺ : Orn u D') → Orn u (D `× D')
`σ : ∀{n T} → (T⁺ : (k : Fin n) → Orn u (T k)) → Orn u (`σ n T)
`Σ : ∀{S T} → (T⁺ : (s : S) → Orn u (T s)) → Orn u (`Σ S T)
`Π : ∀{S T} → (T⁺ : (s : S) → Orn u (T s)) → Orn u (`Π S T)
deleteΣ : ∀{S T} → (s : S)
(T⁺ : Orn u (T s)) →
Orn u (`Σ S T)
deleteσ : ∀{n T} → (k : Fin n)
(T⁺ : Orn u (T k)) →
Orn u (`σ n T)
⟦_⟧Orn : ∀{ℓ k}{I K : Set k}{u}{D : IDesc ℓ I} → Orn u D → IDesc ℓ K
⟦ `1 ⟧Orn = `1
⟦ T⁺ `× T'⁺ ⟧Orn = ⟦ T⁺ ⟧Orn `× ⟦ T'⁺ ⟧Orn
⟦ `σ {n} T⁺ ⟧Orn = `σ n ((λ D → ⟦ D ⟧Orn) ∘ T⁺)
⟦ `Σ {S} T⁺ ⟧Orn = `Σ S ((λ D → ⟦ D ⟧Orn) ∘ T⁺)
⟦ `Π {S} T⁺ ⟧Orn = `Π S ((λ D → ⟦ D ⟧Orn) ∘ T⁺)
⟦ `var (inv i⁺) ⟧Orn = `var i⁺
⟦ insert S D⁺ ⟧Orn = `Σ S (λ s → ⟦ D⁺ s ⟧Orn)
⟦ deleteΣ s T⁺ ⟧Orn = ⟦ T⁺ ⟧Orn
⟦ deleteσ k T⁺ ⟧Orn = ⟦ T⁺ ⟧Orn
record orn {ℓ k : Level}{I J K L : Set k}(D : func ℓ K L)(u : I → K)(v : J → L) : Set (k ⊔ sucL ℓ) where
constructor mk
field
out : (j : J) → Orn u (func.out D (v j))
⟦_⟧orn : ∀{ℓ k}{I J K L : Set k}{D : func ℓ K L}{u : I → K}{v : J → L} →
orn D u v → func ℓ I J
⟦ o ⟧orn = func.mk λ j → ⟦ orn.out o j ⟧Orn