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
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 `⊤
⟦_⟧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 : ∀{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 = ⊤