open import Data.Nat
open import Data.Fin
open import Data.Product
open import Data.Sum
open import Data.Unit
open import Relation.Binary.PropositionalEquality
open import Logic.Logic
open import IDesc.IDesc
open import IDesc.Fixpoint
open import IDesc.InitialAlgebra
open import IDesc.Induction
open import Orn.Ornament.Examples.Lifting
open import Orn.Ornament
module Orn.AlgebraicOrnament
{K : Set }
{X : K → Set } where
I : Set
I = Σ K X
u : I → K
u = proj₁
module Desc
(k : K)
(x : X k)
(D : IDesc K)
(α : ⟦ D ⟧ X → X k) where
algOrn : Orn u D
algOrn = insert (⟦ D ⟧ X) λ xs →
insert (α xs ≡ x) λ _ →
□h {L = K} D xs
algOrnD : IDesc I
algOrnD = ⟦ algOrn ⟧Orn
module Func
(D : func K K)
(α : Alg D X) where
algOrn : orn D u u
algOrn = orn.mk λ { (k , xs) → Desc.algOrn k xs (func.out D k) (α {k}) }
algOrnD : func I I
algOrnD = ⟦ algOrn ⟧orn
open Func public