module Chapter5.Equivalence.ToDesc
         {I J : Set}
       where

open import Level

open import Chapter5.IDesc
open import Chapter5.Container

⟨_⟩⁻¹ : I  J  func zero I J
 φ ⟩⁻¹ = func.mk λ j   (S φ j)  sh  
                         (P φ sh)  ps  
                        `var (n φ ps)))