Hereditary W-types

Content created by Egbert Rijke.

Created on 2024-04-17.
Last modified 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-𝕎

Recent changes

2024-04-17. Egbert Rijke. Hereditary W-types (#1112).