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)))