Binary W-types

Content created by Egbert Rijke.

Created on 2024-04-17.
Last modified on 2024-04-17.

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

Idea

Consider a type A and two type families B and C over A. Then we obtain the polynomial functor

  X Y ↦ Σ (a : A), (B a → X) × (C a → Y)

in two variables X and Y. By diagonalising, we obtain the polynomial endofunctor

  X ↦ Σ (a : A), (B a → X) × (C a → X).

which may be brought to the exact form of a polynomial endofunctor if one wishes to do so:

  X ↦ Σ (a : A), (B a + C a → X).

The binary W-type is the W-type binary-𝕎 associated to this polynomial endofunctor. In other words, it is the inductive type generated by

  make-binary-𝕎 : (a : A) → (B a → binary-𝕎) → (C a → binary-𝕎) → binary-𝕎.

The binary W-type is equivalent to the hereditary W-types via an equivalence that generalizes the equivalence of plane trees and full binary plane trees, which is a well known equivalence used in the study of the Catalan numbers.

Definitions

Binary W-types

module _
  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
  where

  data binary-𝕎 : UU (l1 ⊔ l2 ⊔ l3) where
    make-binary-𝕎 :
      (a : A) → (B a → binary-𝕎) → (C a → binary-𝕎) → binary-𝕎

Recent changes