```module FunOrn.FunOrnament where

open import Data.Unit
open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Logic.Logic
open import Logic.IProp

open import IDesc.IDesc
open import IDesc.Fixpoint

open import Orn.Ornament
open import Orn.Ornament.Algebra

open import FunOrn.Functions

-- Paper: Definition 5.5
data FunctionOrn : Type  → Set₁ where
μ⁺_[_]→_ : ∀{I I⁺ : Set}{D : func  I I}{i}{T : Type}
{u : I⁺ → I} →
(o : orn D u u)(i⁻¹ : u ⁻¹ i)
(T⁺ : FunctionOrn T) → FunctionOrn (μ D [ i ]→ T)
μ⁺_[_]×_ : ∀{I I⁺ : Set}{D : func  I I}{i}{T : Type}
{u : I⁺ → I} →
(o : orn D u u)(i⁻¹ : u ⁻¹ i)
(T⁺ : FunctionOrn T) → FunctionOrn (μ D [ i ]× T)
`⊤ : FunctionOrn `⊤

-- * Projections

-- ** Lifted function

-- Paper: Definition 5.6
⟦_⟧FunctionOrn : ∀{T} → FunctionOrn T → Set
⟦ μ⁺ o [ inv i⁺ ]→ T⁺ ⟧FunctionOrn = μ ⟦ o ⟧orn i⁺ → ⟦ T⁺ ⟧FunctionOrn
⟦ μ⁺ o [ inv i⁺ ]× T⁺ ⟧FunctionOrn = μ ⟦ o ⟧orn i⁺ × ⟦ T⁺ ⟧FunctionOrn
⟦ `⊤ ⟧FunctionOrn = ⊤

-- ** Coherence proof

-- Paper: Definition 5.7
⟦_⟧Coherence : ∀{T} → (fo : FunctionOrn T) → ⟦ T ⟧Type → ⟦ fo ⟧FunctionOrn → Set
⟦ μ⁺ o [ inv i⁺ ]→ T⁺ ⟧Coherence f f⁺ =
(x⁺ : μ ⟦ o ⟧orn i⁺) → ⟦ T⁺ ⟧Coherence (f (forget o x⁺)) (f⁺ x⁺)
⟦ μ⁺ o [ inv i⁺ ]× T⁺ ⟧Coherence (x , xs) (x⁺ , xs⁺) =
(⊢ x ≡ forget o x⁺) × ⟦ T⁺ ⟧Coherence xs xs⁺
⟦ `⊤ ⟧Coherence tt tt = ⊤
```