module Chapter9.FunOrnament where

open import Level
  renaming ( suc to sucL )

open import Data.Unit
open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Chapter2.Logic

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint

open import Chapter8.Ornament
open import Chapter8.Ornament.Algebra 

open import Chapter9.Functions

data FunctionOrn {k ℓ : Level} : Type {k} ℓ → Set (sucL (k ⊔ ℓ)) where
  μ⁺_[_]→_ : ∀{I I⁺ : Set k}{D : func ℓ I I}{i}{T : Type {k} ℓ}
              {u : I⁺ → I} → 
                 (o : orn D u u)(i⁻¹ : u ⁻¹ i)
                 (T⁺ : FunctionOrn T) → FunctionOrn (μ D [ i ]→ T)
  μ⁺_[_]×_ : ∀{I I⁺ : Set k}{D : func ℓ I I}{i}{T : Type {k} ℓ}
              {u : I⁺ → I} →
                 (o : orn D u u)(i⁻¹ : u ⁻¹ i)
                 (T⁺ : FunctionOrn T) → FunctionOrn (μ D [ i ]× T)
  `⊤ : FunctionOrn `⊤

-- * Projections

-- ** Lifted function

⟦_⟧FunctionOrn : ∀{k ℓ T} → FunctionOrn {k}{ℓ} T → Set ℓ
⟦ μ⁺ o [ inv i⁺ ]→ T⁺ ⟧FunctionOrn = μ ⟦ o ⟧orn i⁺ → ⟦ T⁺ ⟧FunctionOrn
⟦ μ⁺ o [ inv i⁺ ]× T⁺ ⟧FunctionOrn = μ ⟦ o ⟧orn i⁺ × ⟦ T⁺ ⟧FunctionOrn
⟦ `⊤ ⟧FunctionOrn = Lift ⊤

-- ** Coherence proof

⟦_⟧Coherence : ∀{k ℓ T} → (fo : FunctionOrn {k}{ℓ} T) → ⟦ T ⟧Type → ⟦ fo ⟧FunctionOrn → Set ℓ
⟦ μ⁺ o [ inv i⁺ ]→ T⁺ ⟧Coherence f f⁺ = 
  (x⁺ : μ ⟦ o ⟧orn i⁺) → ⟦ T⁺ ⟧Coherence (f (forgetOrnament o x⁺)) (f⁺ x⁺)
⟦ μ⁺ o [ inv i⁺ ]× T⁺ ⟧Coherence (x , xs) (x⁺ , xs⁺) = 
  x ≡ forgetOrnament o x⁺ × ⟦ T⁺ ⟧Coherence xs xs⁺ 
⟦ `⊤ ⟧Coherence (lift tt) (lift tt) = Lift ⊤