open import Level module Chapter8.Ornament.Identity {ℓ k : Level} {I : Set k} where open import Function open import Chapter2.Logic open import Chapter5.IDesc open import Chapter8.Ornament idO : (D : func ℓ I I) → orn D id id idO D = orn.mk (λ i → help (func.out D i)) where help : (D : IDesc ℓ I) → Orn id D help (`var i) = `var (inv i) help `1 = `1 help (D₁ `× D₂) = help D₁ `× help D₂ help (`σ n T) = `σ λ k → help (T k) help (`Σ S T) = `Σ λ s → help (T s) help (`Π S T) = `Π λ s → help (T s)