open import Data.Unit open import Data.Product open import Logic.Logic open import IDesc.IDesc open import Orn.Ornament module Orn.Ornament.Examples.Lifting {K L : Set} {X : K → Set} where private u : Σ K X → K u = proj₁ □h : (D : IDesc K) → ⟦ D ⟧ X → Orn u D □h `1 tt = `1 □h (`var k) x = `var (inv (k , x)) □h (T `× T') (t , t') = □h T t `× □h T' t' □h (`σ n T) (k , xs) = deleteσ k (□h (T k) xs) □h (`Σ S T) (s , xs) = deleteΣ s (□h (T s) xs) □h (`Π S T) f = `Π λ s → □h (T s) (f s) □ : (D : func K L) → orn D proj₁ proj₁ □ D = orn.mk (λ { (k , x) → □h (func.out D k) x })