module Orn.AlgebraicOrnament.Examples.Lifting {K : Set } {X : K → Set } where open import Function open import Data.Unit open import Data.Nat open import Data.Fin open import Data.Product open import Relation.Binary.PropositionalEquality open import IDesc.IDesc open import IDesc.Fixpoint open import IDesc.InitialAlgebra open import IDesc.Examples.Nat open import Orn.Ornament import Orn.AlgebraicOrnament [_]^ : (D : func K K) → orn D proj₁ proj₁ [ D ]^ = algOrn where open Orn.AlgebraicOrnament.Func {K}{μ D} D ⟨_⟩