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)