Induction for descriptions with fixpoints

Desc.agda

open import Level using (Level) renaming (suc to lsuc ; zero to lzero)
open import Function
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)

variable ℓ : Level

data Desc (I : Set) : Set₁ where
  var : I → Desc I
  σ π : (A : Set) (D : A → Desc I) → Desc I
  _×D_ : Desc I → Desc I → Desc I
  κ : Set → Desc I
  μ : (J : Set) → (J → Desc (I ⊎ J)) → J → Desc I

indDesc : (P : (I : Set) → Desc I → Set ℓ)
  → ((I : Set) (i : I) → P I (var i))
  → ((I : Set) (A : Set) (D : A → Desc I) → ((x : A) → P I (D x)) → P I (σ A D))
  → ((I : Set) (A : Set) (D : A → Desc I) → ((x : A) → P I (D x)) → P I (π A D))
  → ((I : Set) (x y : Desc I) → P I x → P I y → P I (x ×D y))
  → ((I : Set) (A : Set) → P I (κ A))
  → ((I J : Set) (f : J → Desc (I ⊎ J)) → (j : J) → ((j : J) → P (I ⊎ J) (f j)) → P I (μ J f j))
  → (I : Set) (x : Desc I) → P I x
indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I (var i) = x₀ I i
indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I (σ A D) = x₁ I A D (indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I ∘ D)
indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I (π A D) = x₂ I A D (indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I ∘ D)
indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I (x ×D y) = x₃ I x y (indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I x) (indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I y)
indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I (κ A) = x₄ I A
indDesc P x₀ x₁ x₂ x₃ x₄ x₅ I (μ J f j) = x₅ I J f j (indDesc P x₀ x₁ x₂ x₃ x₄ x₅ (I ⊎ J) ∘ f)

-- sanity check
idDesc : (I : Set) → Desc I → Desc I
idDesc = indDesc (λ I _ → Desc I) (λ _ → var) (λ _ A _ f → σ A f) (λ _ A _ f → π A f) (λ _ _ _ x y → x ×D y) (λ _ A → κ A) (λ _ J _ j f → μ J f j)