# Binary W-types

Content created by Egbert Rijke.

Created 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-𝕎