https://proofassistants.stackexchange.com/questions/1981/what-are-the-complex-induction-patterns-supported-by-agda/2002#2002

DoubleIndRec.aya

open import Paths
open data Nat | zero | suc Nat
open data Unit | unit
open data Empty

open data U
| ℕ'
| Π' (A : U) (B : El A → U) (resp~ B)

def resp~ {A : U} (B : El A → U) : Type
=> ∀ {a a' : El A} → (El~ reflU a a') → U~ (B a) (B a')

def U~ (A B : U) : Type
| ℕ', ℕ'               => Unit
| ℕ', Π' _ _ _         => Empty
| Π' _ _ _, ℕ'         => Empty
| Π' A B _, Π' A' B' _ => Σ (A~ : U~ A A') ** ∀ {a : El A} {a' : El A'} → (El~ A~ a a') → U~ (B a) (B' a')

def reflU {A : U} : U~ A A
| {ℕ'}        => unit
| {Π' A B Br} => (reflU, fn a~ => Br a~)

def El (A : U) : Type
| ℕ'        => Nat
| Π' A B Br => ∀ (a : El A) → El (B a)

def El~ {A A' : U} (U~ A A') (El A) (El A') : Type
| {ℕ'}, {ℕ'}, A~, x, y                     => x = y
| {Π' A B _}, {Π' A' B' _}, (A~, B~), f, g => ∀ {a : El A} {a' : El A'} (a~ : El~ A~ a a') → El~ (B~ a~) (f a) (g a')

Endo-Rec.aya

open import Paths
open data Nat | zero | suc Nat
open data Unit | unit
open data Empty

open data U
| Nat'
| Π (A : U) (B : El A → U) (∀ (dom : PiDom reflU) → IdU (B dom.1) (B dom.2))

def PiDom {A A' : U} (IdA : IdU A A') =>
  Sig (a : El A) (a' : El A') ** (IdEl IdA a a')

def IdU (A B : U) : Type
| Nat', Nat'         => Unit
| Π A B _, Π A' B' _ => Σ (IdA : IdU A A') ** ∀ (dom : PiDom IdA) → IdU (B dom.1) (B' dom.2)
| _, _         => Empty

def reflU {A : U} : IdU A A
| {Nat'}     => unit
| {Π A B Br} => (reflU, Br)

def El (A : U) : Type
| Nat'    => Nat
| Π A B _ => ∀ (a : El A) → El (B a)

def IdEl {A A' : U} (IdU A A') (El A) (El A') : Type
| {Nat'}, {Nat'}, IdA, x, y                => x = y
| {Π A B _}, {Π A' B' _}, (IdA, IdB), f, g =>
   ∀ (dom : PiDom IdA) → IdEl (IdB dom.3) (f dom.1) (g dom.2)