# Hereditary W-types

Content created by Egbert Rijke.

Created on 2024-04-17.

module trees.hereditary-w-types where

Imports
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.identity-types
open import foundation.retractions
open import foundation.sections
open import foundation.universe-levels

open import trees.binary-w-types


## 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 fixing either X or Y, we obtain two polynomial endofunctors given by

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


and

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


respectively. The type left-𝕎 is obtained by letting the left argument vary and fixing the right argument, i.e., it is the inductive type generated by

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


Similarly, the type right-𝕎 is obtained by fixing the left argument and varying the right argument, i.e., it is the inductive type generated by

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


Thus we obtain two operations left-𝕎 and right-𝕎. The left and right hereditary W-type are the least fixed points for the operations left-𝕎 and right-𝕎 respectively. That is, we define left-hereditary-𝕎 as the inductive type generated by

  make-left-hereditary-𝕎 : left-𝕎 left-hereditary-𝕎 → left-hereditary-𝕎.


and we define right-hereditary-𝕎 as the inductive type generated by

  make-right-hereditary-𝕎 : right-𝕎 right-hereditary-𝕎 → right-hereditary-𝕎.


We will construct equivalences

  left-hereditary-𝕎 ≃ binary-𝕎


and

  right-hereditary-𝕎 ≃ binary-𝕎,


showing that both the left and right hereditary W-types are equivalent to the binary W-type associated to B and C.

### Motivating example

If we choose A := Fin 2 and

  B 0 := empty        C 0 := empty
B 1 := unit         C 1 := unit,


then the left W-type left-𝕎 B C is equivalent to the inductive type generated by

  nil : left-𝕎
snoc : left-𝕎 → Y → left-𝕎,


which is equivalent to the type list of lists. The left hereditary W-type left-hereditary-𝕎 is then equivalent to the type of plane trees. Furthermore, in this case the binary W-type associated to B and C is equivalent to the inductive type generated by

  leaf : left-hereditary-𝕎
node : left-hereditary-𝕎 → left-hereditary-𝕎 → left-hereditary-𝕎.


Thus we see that the equivalence left-hereditary-𝕎 ≃ binary-𝕎 is a generalization of the well-known equivalence of plane trees and full binary plane trees, which is prominent in the study of the Catalan numbers.

## Definitions

### Left hereditary W-types

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

data left-𝕎 {l4 : Level} (Y : UU l4) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) where
make-left-𝕎 : (a : A) → (B a → left-𝕎 Y) → (C a → Y) → left-𝕎 Y

data left-hereditary-𝕎 : UU (l1 ⊔ l2 ⊔ l3) where
make-left-hereditary-𝕎 : left-𝕎 left-hereditary-𝕎 → left-hereditary-𝕎


### Right hereditary W-types

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

data right-𝕎 {l4 : Level} (X : UU l4) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) where
make-right-𝕎 : (a : A) → (B a → X) → (C a → right-𝕎 X) → right-𝕎 X

data right-hereditary-𝕎 : UU (l1 ⊔ l2 ⊔ l3) where
make-right-hereditary-𝕎 : right-𝕎 right-hereditary-𝕎 → right-hereditary-𝕎


## Properties

### The left hereditary W-type is a fixed point for left-𝕎

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

unpack-left-hereditary-𝕎 :
left-hereditary-𝕎 B C → left-𝕎 B C (left-hereditary-𝕎 B C)
unpack-left-hereditary-𝕎 (make-left-hereditary-𝕎 T) = T

is-section-unpack-left-hereditary-𝕎 :
is-section make-left-hereditary-𝕎 unpack-left-hereditary-𝕎
is-section-unpack-left-hereditary-𝕎 (make-left-hereditary-𝕎 T) = refl

is-retraction-unpack-left-hereditary-𝕎 :
is-retraction make-left-hereditary-𝕎 unpack-left-hereditary-𝕎
is-retraction-unpack-left-hereditary-𝕎 T = refl

is-equiv-make-left-hereditary-𝕎 :
is-equiv make-left-hereditary-𝕎
is-equiv-make-left-hereditary-𝕎 =
is-equiv-is-invertible
( unpack-left-hereditary-𝕎)
( is-section-unpack-left-hereditary-𝕎)
( is-retraction-unpack-left-hereditary-𝕎)

equiv-make-left-hereditary-𝕎 :
left-𝕎 B C (left-hereditary-𝕎 B C) ≃ left-hereditary-𝕎 B C
pr1 equiv-make-left-hereditary-𝕎 = make-left-hereditary-𝕎
pr2 equiv-make-left-hereditary-𝕎 = is-equiv-make-left-hereditary-𝕎


### The right hereditary W-type is a fixed point for right-𝕎

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

unpack-right-hereditary-𝕎 :
right-hereditary-𝕎 B C → right-𝕎 B C (right-hereditary-𝕎 B C)
unpack-right-hereditary-𝕎 (make-right-hereditary-𝕎 T) = T

is-section-unpack-right-hereditary-𝕎 :
is-section make-right-hereditary-𝕎 unpack-right-hereditary-𝕎
is-section-unpack-right-hereditary-𝕎 (make-right-hereditary-𝕎 T) = refl

is-retraction-unpack-right-hereditary-𝕎 :
is-retraction make-right-hereditary-𝕎 unpack-right-hereditary-𝕎
is-retraction-unpack-right-hereditary-𝕎 T = refl

is-equiv-make-right-hereditary-𝕎 :
is-equiv make-right-hereditary-𝕎
is-equiv-make-right-hereditary-𝕎 =
is-equiv-is-invertible
( unpack-right-hereditary-𝕎)
( is-section-unpack-right-hereditary-𝕎)
( is-retraction-unpack-right-hereditary-𝕎)

equiv-make-right-hereditary-𝕎 :
right-𝕎 B C (right-hereditary-𝕎 B C) ≃ right-hereditary-𝕎 B C
pr1 equiv-make-right-hereditary-𝕎 = make-right-hereditary-𝕎
pr2 equiv-make-right-hereditary-𝕎 = is-equiv-make-right-hereditary-𝕎


### Left hereditary W-types are binary W-types

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

binary-left-hereditary-𝕎 : left-hereditary-𝕎 B C → binary-𝕎 B C
binary-left-hereditary-𝕎 (make-left-hereditary-𝕎 (make-left-𝕎 a S T)) =
make-binary-𝕎 a
( λ b → binary-left-hereditary-𝕎 (make-left-hereditary-𝕎 (S b)))
( λ c → binary-left-hereditary-𝕎 (T c))

left-hereditary-binary-𝕎 : binary-𝕎 B C → left-hereditary-𝕎 B C
left-hereditary-binary-𝕎 (make-binary-𝕎 a S T) =
make-left-hereditary-𝕎
( make-left-𝕎 a
( λ b →
unpack-left-hereditary-𝕎 B C (left-hereditary-binary-𝕎 (S b)))
( λ c → left-hereditary-binary-𝕎 (T c)))

is-section-left-hereditary-binary-𝕎 :
is-section binary-left-hereditary-𝕎 left-hereditary-binary-𝕎
is-section-left-hereditary-binary-𝕎 (make-binary-𝕎 a S T) =
ap-binary
( make-binary-𝕎 a)
( eq-htpy
( λ b →
( ap
( binary-left-hereditary-𝕎)
( is-section-unpack-left-hereditary-𝕎 B C
( left-hereditary-binary-𝕎 (S b)))) ∙
( is-section-left-hereditary-binary-𝕎 (S b))))
( eq-htpy (λ c → is-section-left-hereditary-binary-𝕎 (T c)))

is-retraction-left-hereditary-binary-𝕎 :
is-retraction binary-left-hereditary-𝕎 left-hereditary-binary-𝕎
is-retraction-left-hereditary-binary-𝕎
( make-left-hereditary-𝕎 (make-left-𝕎 a S T)) =
ap
( make-left-hereditary-𝕎)
( ap-binary
( make-left-𝕎 a)
( eq-htpy
( λ b →
ap
( unpack-left-hereditary-𝕎 B C)
( is-retraction-left-hereditary-binary-𝕎
( make-left-hereditary-𝕎 (S b)))))
( eq-htpy (λ c → is-retraction-left-hereditary-binary-𝕎 (T c))))

is-equiv-binary-left-hereditary-𝕎 :
is-equiv binary-left-hereditary-𝕎
is-equiv-binary-left-hereditary-𝕎 =
is-equiv-is-invertible
( left-hereditary-binary-𝕎)
( is-section-left-hereditary-binary-𝕎)
( is-retraction-left-hereditary-binary-𝕎)

equiv-binary-left-hereditary-𝕎 :
left-hereditary-𝕎 B C ≃ binary-𝕎 B C
pr1 equiv-binary-left-hereditary-𝕎 = binary-left-hereditary-𝕎
pr2 equiv-binary-left-hereditary-𝕎 = is-equiv-binary-left-hereditary-𝕎


### Right hereditary W-types are binary W-types

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

binary-right-hereditary-𝕎 : right-hereditary-𝕎 B C → binary-𝕎 B C
binary-right-hereditary-𝕎 (make-right-hereditary-𝕎 (make-right-𝕎 a S T)) =
make-binary-𝕎 a
( λ b → binary-right-hereditary-𝕎 (S b))
( λ c → binary-right-hereditary-𝕎 (make-right-hereditary-𝕎 (T c)))

right-hereditary-binary-𝕎 : binary-𝕎 B C → right-hereditary-𝕎 B C
right-hereditary-binary-𝕎 (make-binary-𝕎 a S T) =
make-right-hereditary-𝕎
( make-right-𝕎 a
( λ b → right-hereditary-binary-𝕎 (S b))
( λ c →
unpack-right-hereditary-𝕎 B C (right-hereditary-binary-𝕎 (T c))))

is-section-right-hereditary-binary-𝕎 :
is-section binary-right-hereditary-𝕎 right-hereditary-binary-𝕎
is-section-right-hereditary-binary-𝕎 (make-binary-𝕎 a S T) =
ap-binary
( make-binary-𝕎 a)
( eq-htpy (λ b → is-section-right-hereditary-binary-𝕎 (S b)))
( eq-htpy
( λ c →
( ap
( binary-right-hereditary-𝕎)
( is-section-unpack-right-hereditary-𝕎 B C
( right-hereditary-binary-𝕎 (T c)))) ∙
( is-section-right-hereditary-binary-𝕎 (T c))))

is-retraction-right-hereditary-binary-𝕎 :
is-retraction binary-right-hereditary-𝕎 right-hereditary-binary-𝕎
is-retraction-right-hereditary-binary-𝕎
( make-right-hereditary-𝕎 (make-right-𝕎 a S T)) =
ap
( make-right-hereditary-𝕎)
( ap-binary
( make-right-𝕎 a)
( eq-htpy (λ b → is-retraction-right-hereditary-binary-𝕎 (S b)))
( eq-htpy
( λ c →
ap
( unpack-right-hereditary-𝕎 B C)
( is-retraction-right-hereditary-binary-𝕎
( make-right-hereditary-𝕎 (T c))))))

is-equiv-binary-right-hereditary-𝕎 :
is-equiv binary-right-hereditary-𝕎
is-equiv-binary-right-hereditary-𝕎 =
is-equiv-is-invertible
( right-hereditary-binary-𝕎)
( is-section-right-hereditary-binary-𝕎)
( is-retraction-right-hereditary-binary-𝕎)

equiv-binary-right-hereditary-𝕎 :
right-hereditary-𝕎 B C ≃ binary-𝕎 B C
pr1 equiv-binary-right-hereditary-𝕎 = binary-right-hereditary-𝕎
pr2 equiv-binary-right-hereditary-𝕎 = is-equiv-binary-right-hereditary-𝕎