# Indexed W-types

Content created by Jonathan Prieto-Cubides, Egbert Rijke and Fredrik Bakke.

Created on 2023-01-26.
Last modified on 2024-04-17.

module trees.indexed-w-types where

Imports
open import foundation.universe-levels


## Idea

The concept of indexed W-types is a generalization of ordinary W-types using a dependently typed variant of polynomial endofunctors. The main idea is that indexed W-types are initial algebras for the polynomial endofunctor

  (X : I → UU) ↦ (λ (j : I) → Σ (a : A j), Π (i : I), B i j a → X i),


where B : (i j : I) → A j → 𝒰 is a type family. In other words, given the data

  A : I → 𝒰
B : (i j : I) → A j → 𝒰


of an indexed container we obtain for each j : I a multivariable polynomial

  Σ (a : A j), Π (i : I), B i j a → X i


Since the functorial operation

  (X : I → UU) ↦ (λ (j : I) → Σ (a : A j), Π (i : I), B i j a → X i),


takes an I-indexed family of inputs and returns an I-indexed family of outputs, it is endofunctorial, meaning that it can be iterated and we can consider initial algebras for this endofunctor.

We will formally define the indexed W-type associated to the data of an indexed container as the inductive type generated by

  tree-indexed-𝕎 :
(x : A j) (α : (i : I) (y : B i j x) → indexed-𝕎 i) → indexed-𝕎 j.


Note. In the usual definition of indexed container, the type family B is directly given as a type family over A

  B : (i : I) → A i → 𝒰,


and furthermore there is a reindexing function

  j : (i : I) (a : A i) → B i a → I.


The pair (B , j) of such a type family and a reindexing function is via type duality equivalent to a single type family

  (j i : I) → A i → 𝒰.


## Definitions

### The indexed W-type associated to an indexed container

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