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)