Indexed W-types

module trees.indexed-w-types where
Imports
open import foundation.universe-levels

Idea

Indexed W-types are a generalization of ordinary W-types using indexed containers. The main idea is that indexed W-types are initial algebras for the polynomial endofunctor

  (X : I → UU) ↦ Σ (a : A i), Π (b : B i a), X (f i a b),

where f : Π (i : I), Π (a : A i), B i a → I is a reindexing function.

data
  i𝕎
    {l1 l2 l3 : Level} (I : UU l1) (A : I  UU l2) (B : (i : I)  A i  UU l3)
    (f : (i : I) (x : A i)  B i x  I) (i : I) :
    UU (l2  l3) where
  tree-i𝕎 : (x : A i) (α : (y : B i x)  i𝕎 I A B f (f i x y))  i𝕎 I A B f i