Inductive-recursive and infinitary version of https://gist.github.com/larrytheliquid/e2bec348c9fb7d894ff25e61efa0349c

SafeGenerallyIndexedIR.agda

open import Data.Unit
open import Data.Product
module _ where

----------------------------------------------------------------------

data Desc (I : Set) (O : I → Set) : Set₁ where
  `ι : (i : I) (o : O i) → Desc I O
  `δ : (A : Set) (i : A → I) (D : (o : (a : A) → O (i a)) → Desc I O) → Desc I O
  `σ : (A : Set) (D : A → Desc I O) → Desc I O

mutual
  data μ {I O} (R : I → Desc I O) (i : I) : I → Set where
    init : (xs : ⟦ R i ⟧ R) → μ R i (proj₁ (io (R i) R xs))

  ode : ∀ {I O} (R : I → Desc I O) (i j : I) → μ R i j → O j
  ode R i ._ (init xs)  = proj₂ (io (R i) R xs)

  ⟦_⟧ : ∀{I O} (D : Desc I O) (R : I → Desc I O) → Set
  ⟦ `ι i o ⟧ R = ⊤
  ⟦ `δ A i D ⟧ R = Σ ((a : A) → μ R (i a) (i a)) λ f → ⟦ D (λ a → ode R (i a) (i a) (f a)) ⟧ R
  ⟦ `σ A D ⟧ R = Σ A λ a → ⟦ D a ⟧ R
  
  io : ∀{I O} (D : Desc I O) (R : I → Desc I O) (xs : ⟦ D ⟧ R) → Σ I O
  io (`ι i o) R tt = i , o
  io (`δ A i D) R (f , xs) = io (D (λ a → ode R (i a) (i a) (f a))) R xs
  io (`σ A D) R (a , xs) = io (D a) R xs

----------------------------------------------------------------------

Hyps : ∀{I O} (R : I → Desc I O) (P : (i j : I) → μ R i j → Set) (D : Desc I O) (xs : ⟦ D ⟧ R) → Set
Hyps R P (`ι i o) tt = ⊤
Hyps R P (`σ A D) (a , xs) = Hyps R P (D a) xs
Hyps R P (`δ A i D) (f , xs) = ((a : A) → P (i a) (i a) (f a))
  × Hyps R P (D (λ a → ode R (i a) (i a) (f a))) xs

----------------------------------------------------------------------

ind :
  ∀{I O}
  (R : I → Desc I O)
  (P : (i j : I) → μ R i j → Set)
  (pcon : (i : I) (xs : ⟦ R i ⟧ R) → Hyps R P (R i) xs → P i (proj₁ (io (R i) R xs)) (init xs))
  (i j : I)
  (x : μ R i j)
  → P i j x

hyps :
  ∀{I O}
  (R : I → Desc I O)
  (P : (i j : I) → μ R i j → Set)
  (pcon : (i : I) (xs : ⟦ R i ⟧ R) → Hyps R P (R i) xs → P i (proj₁ (io (R i) R xs)) (init xs))
  (D : Desc I O)
  (xs : ⟦ D ⟧ R)
  → Hyps R P D xs

ind R P pcon i j (init xs) = pcon i xs (hyps R P pcon (R i) xs)

hyps R P pcon (`ι i o) tt = tt
hyps R P pcon (`σ A D) (a , xs) = hyps R P pcon (D a) xs
hyps R P pcon (`δ A i D) (f , xs) = (λ a → ind R P pcon (i a) (i a) (f a))
  , hyps R P pcon (D (λ a → ode R (i a) (i a) (f a))) xs

----------------------------------------------------------------------

UnsafeGenerallyIndexedIR.agda

open import Data.Unit
open import Data.Product
module _ where

----------------------------------------------------------------------

data Desc (I : Set) (O : I → Set) : Set₁ where
  `ι : (i : I) (o : O i) → Desc I O
  `δ : (A : Set) (i : A → I) (D : (o : (a : A) → O (i a)) → Desc I O) → Desc I O
  `σ : (A : Set) (D : A → Desc I O) → Desc I O

⟦_⟧ : ∀{I O} (D : Desc I O) (X : I → I → Set) (Y : (i j : I) → X i j → O j) → Set
⟦ `ι i o ⟧ X Y = ⊤
⟦ `δ A i D ⟧ X Y = Σ ((a : A) → X (i a) (i a)) λ f → ⟦ D (λ a → Y (i a) (i a) (f a)) ⟧ X Y
⟦ `σ A D ⟧ X Y = Σ A λ a → ⟦ D a ⟧ X Y

io : ∀{I O} (D : Desc I O) (X : I → I → Set) (Y : (i j : I) → X i j → O j) (xs : ⟦ D ⟧ X Y) → Σ I O
io (`ι i o) X Y tt = i , o
io (`δ A i D) X Y (f , xs) = io (D (λ a → Y (i a) (i a) (f a))) X Y xs
io (`σ A D) X Y (a , xs) = io (D a) X Y xs

{-# TERMINATING #-}
mutual
  data μ {I O} (R : I → Desc I O) (i : I) : I → Set where
    init : (xs : ⟦ R i ⟧ (μ R) (ode R)) → μ R i (proj₁ (io (R i) (μ R) (ode R) xs))

  ode : ∀ {I O} (R : I → Desc I O) (i j : I) → μ R i j → O j
  ode R i ._ (init xs)  = proj₂ (io (R i) (μ R) (ode R) xs)

----------------------------------------------------------------------