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

Recent changes