# W-types

```agda
module trees.w-types where
```

<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.postcomposition-functions
open import foundation.propositional-truncations
open import foundation.sets
open import foundation.torsorial-type-families
open import foundation.transport-along-identifications
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.type-theoretic-principle-of-choice
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import trees.algebras-polynomial-endofunctors
open import trees.coalgebras-polynomial-endofunctors
open import trees.morphisms-algebras-polynomial-endofunctors
open import trees.polynomial-endofunctors
```

</details>

## Idea

Consider a type `A` equipped with a type family `B` over `A`. The type `W`
generated inductively by a constructor `B x โ†’ W` for each `x : A` is called the
**W-type** `W A B` of `B`. The elements of `A` can be thought of as symbols for
the constructors of `W A B`, and the functions `B x โ†’ W A B` are the
constructors. The elements of `W A B` can be thought of as well-founded trees.

## Definition

```agda
data ๐•Ž {l1 l2 : Level} (A : UU l1) (B : A โ†’ UU l2) : UU (l1 โŠ” l2) where
  tree-๐•Ž : (x : A) (ฮฑ : B x โ†’ ๐•Ž A B) โ†’ ๐•Ž A B

module _
  {l1 l2 : Level} {A : UU l1} {B : A โ†’ UU l2}
  where

  shape-๐•Ž : ๐•Ž A B โ†’ A
  shape-๐•Ž (tree-๐•Ž x ฮฑ) = x

  component-๐•Ž : (x : ๐•Ž A B) โ†’ B (shape-๐•Ž x) โ†’ ๐•Ž A B
  component-๐•Ž (tree-๐•Ž x ฮฑ) = ฮฑ

  ฮท-๐•Ž : (x : ๐•Ž A B) โ†’ tree-๐•Ž (shape-๐•Ž x) (component-๐•Ž x) ๏ผ x
  ฮท-๐•Ž (tree-๐•Ž x ฮฑ) = refl
```

### W-types as algebras for a polynomial endofunctor

```agda
structure-๐•Ž-Alg :
  {l1 l2 : Level} {A : UU l1} {B : A โ†’ UU l2} โ†’
  type-polynomial-endofunctor A B (๐•Ž A B) โ†’ ๐•Ž A B
structure-๐•Ž-Alg (pair x ฮฑ) = tree-๐•Ž x ฮฑ

๐•Ž-Alg :
  {l1 l2 : Level} (A : UU l1) (B : A โ†’ UU l2) โ†’
  algebra-polynomial-endofunctor (l1 โŠ” l2) A B
๐•Ž-Alg A B = pair (๐•Ž A B) structure-๐•Ž-Alg
```

### W-types as coalgebras for a polynomial endofunctor

```agda
๐•Ž-Coalg :
  {l1 l2 : Level} (A : UU l1) (B : A โ†’ UU l2) โ†’
  coalgebra-polynomial-endofunctor (l1 โŠ” l2) A B
pr1 (๐•Ž-Coalg A B) = ๐•Ž A B
pr1 (pr2 (๐•Ž-Coalg A B) x) = shape-๐•Ž x
pr2 (pr2 (๐•Ž-Coalg A B) x) = component-๐•Ž x
```

## Properties

### The elements of the form `tree-๐•Ž x ฮฑ` where `B x` is an empty type are called the constants of `W A B`

```agda
module _
  {l1 l2 : Level} {A : UU l1} {B : A โ†’ UU l2}
  where

  constant-๐•Ž : (x : A) โ†’ is-empty (B x) โ†’ ๐•Ž A B
  constant-๐•Ž x h = tree-๐•Ž x (ex-falso โˆ˜ h)

  is-constant-๐•Ž : ๐•Ž A B โ†’ UU l2
  is-constant-๐•Ž x = is-empty (B (shape-๐•Ž x))
```

### If each `B x` is inhabited, then the type `W A B` is empty

```agda
module _
  {l1 l2 : Level} {A : UU l1} {B : A โ†’ UU l2}
  where

  is-empty-๐•Ž : ((x : A) โ†’ type-trunc-Prop (B x)) โ†’ is-empty (๐•Ž A B)
  is-empty-๐•Ž H (tree-๐•Ž x ฮฑ) =
    apply-universal-property-trunc-Prop
      ( H x)
      ( empty-Prop)
      ( ฮป y โ†’ is-empty-๐•Ž H (ฮฑ y))
```

### Equality of W-types

```agda
module _
  {l1 l2 : Level} {A : UU l1} {B : A โ†’ UU l2}
  where

  Eq-๐•Ž : ๐•Ž A B โ†’ ๐•Ž A B โ†’ UU (l1 โŠ” l2)
  Eq-๐•Ž (tree-๐•Ž x ฮฑ) (tree-๐•Ž y ฮฒ) =
    ฮฃ (x ๏ผ y) (ฮป p โ†’ (z : B x) โ†’ Eq-๐•Ž (ฮฑ z) (ฮฒ (tr B p z)))

  refl-Eq-๐•Ž : (w : ๐•Ž A B) โ†’ Eq-๐•Ž w w
  refl-Eq-๐•Ž (tree-๐•Ž x ฮฑ) = pair refl (ฮป z โ†’ refl-Eq-๐•Ž (ฮฑ z))

  center-total-Eq-๐•Ž : (w : ๐•Ž A B) โ†’ ฮฃ (๐•Ž A B) (Eq-๐•Ž w)
  center-total-Eq-๐•Ž w = pair w (refl-Eq-๐•Ž w)

  aux-total-Eq-๐•Ž :
    (x : A) (ฮฑ : B x โ†’ ๐•Ž A B) โ†’
    ฮฃ (B x โ†’ ๐•Ž A B) (ฮป ฮฒ โ†’ (y : B x) โ†’ Eq-๐•Ž (ฮฑ y) (ฮฒ y)) โ†’
    ฮฃ (๐•Ž A B) (Eq-๐•Ž (tree-๐•Ž x ฮฑ))
  aux-total-Eq-๐•Ž x ฮฑ (pair ฮฒ e) = pair (tree-๐•Ž x ฮฒ) (pair refl e)

  contraction-total-Eq-๐•Ž :
    (w : ๐•Ž A B) (t : ฮฃ (๐•Ž A B) (Eq-๐•Ž w)) โ†’ center-total-Eq-๐•Ž w ๏ผ t
  contraction-total-Eq-๐•Ž
    ( tree-๐•Ž x ฮฑ) (pair (tree-๐•Ž .x ฮฒ) (pair refl e)) =
    ap
      ( ( aux-total-Eq-๐•Ž x ฮฑ) โˆ˜
        ( map-distributive-ฮ -ฮฃ
          { A = B x}
          { B = ฮป y โ†’ ๐•Ž A B}
          { C = ฮป y โ†’ Eq-๐•Ž (ฮฑ y)}))
      { x = ฮป y โ†’ pair (ฮฑ y) (refl-Eq-๐•Ž (ฮฑ y))}
      { y = ฮป y โ†’ pair (ฮฒ y) (e y)}
      ( eq-htpy (ฮป y โ†’ contraction-total-Eq-๐•Ž (ฮฑ y) (pair (ฮฒ y) (e y))))

  is-torsorial-Eq-๐•Ž : (w : ๐•Ž A B) โ†’ is-torsorial (Eq-๐•Ž w)
  is-torsorial-Eq-๐•Ž w =
    pair (center-total-Eq-๐•Ž w) (contraction-total-Eq-๐•Ž w)

  Eq-๐•Ž-eq : (v w : ๐•Ž A B) โ†’ v ๏ผ w โ†’ Eq-๐•Ž v w
  Eq-๐•Ž-eq v .v refl = refl-Eq-๐•Ž v

  is-equiv-Eq-๐•Ž-eq : (v w : ๐•Ž A B) โ†’ is-equiv (Eq-๐•Ž-eq v w)
  is-equiv-Eq-๐•Ž-eq v =
    fundamental-theorem-id
      ( is-torsorial-Eq-๐•Ž v)
      ( Eq-๐•Ž-eq v)

  eq-Eq-๐•Ž : (v w : ๐•Ž A B) โ†’ Eq-๐•Ž v w โ†’ v ๏ผ w
  eq-Eq-๐•Ž v w = map-inv-is-equiv (is-equiv-Eq-๐•Ž-eq v w)

  equiv-Eq-๐•Ž-eq : (v w : ๐•Ž A B) โ†’ (v ๏ผ w) โ‰ƒ Eq-๐•Ž v w
  equiv-Eq-๐•Ž-eq v w = pair (Eq-๐•Ž-eq v w) (is-equiv-Eq-๐•Ž-eq v w)

  is-trunc-๐•Ž : (k : ๐•‹) โ†’ is-trunc (succ-๐•‹ k) A โ†’ is-trunc (succ-๐•‹ k) (๐•Ž A B)
  is-trunc-๐•Ž k is-trunc-A (tree-๐•Ž x ฮฑ) (tree-๐•Ž y ฮฒ) =
    is-trunc-is-equiv k
      ( Eq-๐•Ž (tree-๐•Ž x ฮฑ) (tree-๐•Ž y ฮฒ))
      ( Eq-๐•Ž-eq (tree-๐•Ž x ฮฑ) (tree-๐•Ž y ฮฒ))
      ( is-equiv-Eq-๐•Ž-eq (tree-๐•Ž x ฮฑ) (tree-๐•Ž y ฮฒ))
      ( is-trunc-ฮฃ
        ( is-trunc-A x y)
        ( ฮป p โ†’ is-trunc-ฮ  k
          ( ฮป z โ†’
            is-trunc-is-equiv' k
            ( ฮฑ z ๏ผ ฮฒ (tr B p z))
            ( Eq-๐•Ž-eq (ฮฑ z) (ฮฒ (tr B p z)))
            ( is-equiv-Eq-๐•Ž-eq (ฮฑ z) (ฮฒ (tr B p z)))
            ( is-trunc-๐•Ž k is-trunc-A (ฮฑ z) (ฮฒ (tr B p z))))))

  is-set-๐•Ž : is-set A โ†’ is-set (๐•Ž A B)
  is-set-๐•Ž = is-trunc-๐•Ž neg-one-๐•‹
```

### The structure map of the algebra `๐•Ž A B` is an equivalence

```agda
map-inv-structure-๐•Ž-Alg :
  {l1 l2 : Level} {A : UU l1} {B : A โ†’ UU l2} โ†’
  ๐•Ž A B โ†’ type-polynomial-endofunctor A B (๐•Ž A B)
map-inv-structure-๐•Ž-Alg (tree-๐•Ž x ฮฑ) = pair x ฮฑ

is-section-map-inv-structure-๐•Ž-Alg :
  {l1 l2 : Level} {A : UU l1} {B : A โ†’ UU l2} โ†’
  (structure-๐•Ž-Alg {B = B} โˆ˜ map-inv-structure-๐•Ž-Alg {B = B}) ~ id
is-section-map-inv-structure-๐•Ž-Alg (tree-๐•Ž x ฮฑ) = refl

is-retraction-map-inv-structure-๐•Ž-Alg :
  {l1 l2 : Level} {A : UU l1} {B : A โ†’ UU l2} โ†’
  (map-inv-structure-๐•Ž-Alg {B = B} โˆ˜ structure-๐•Ž-Alg {B = B}) ~ id
is-retraction-map-inv-structure-๐•Ž-Alg (pair x ฮฑ) = refl

is-equiv-structure-๐•Ž-Alg :
  {l1 l2 : Level} {A : UU l1} {B : A โ†’ UU l2} โ†’
  is-equiv (structure-๐•Ž-Alg {B = B})
is-equiv-structure-๐•Ž-Alg =
  is-equiv-is-invertible
    map-inv-structure-๐•Ž-Alg
    is-section-map-inv-structure-๐•Ž-Alg
    is-retraction-map-inv-structure-๐•Ž-Alg

equiv-structure-๐•Ž-Alg :
  {l1 l2 : Level} {A : UU l1} {B : A โ†’ UU l2} โ†’
  type-polynomial-endofunctor A B (๐•Ž A B) โ‰ƒ ๐•Ž A B
equiv-structure-๐•Ž-Alg =
  pair structure-๐•Ž-Alg is-equiv-structure-๐•Ž-Alg

is-equiv-map-inv-structure-๐•Ž-Alg :
  {l1 l2 : Level} {A : UU l1} {B : A โ†’ UU l2} โ†’
  is-equiv (map-inv-structure-๐•Ž-Alg {B = B})
is-equiv-map-inv-structure-๐•Ž-Alg =
  is-equiv-is-invertible
    structure-๐•Ž-Alg
    is-retraction-map-inv-structure-๐•Ž-Alg
    is-section-map-inv-structure-๐•Ž-Alg

inv-equiv-structure-๐•Ž-Alg :
  {l1 l2 : Level} {A : UU l1} {B : A โ†’ UU l2} โ†’
  ๐•Ž A B โ‰ƒ type-polynomial-endofunctor A B (๐•Ž A B)
inv-equiv-structure-๐•Ž-Alg =
  pair map-inv-structure-๐•Ž-Alg is-equiv-map-inv-structure-๐•Ž-Alg
```

### W-types are initial algebras for polynomial endofunctors

```agda
map-hom-๐•Ž-Alg :
  {l1 l2 l3 : Level} {A : UU l1} {B : A โ†’ UU l2}
  (X : algebra-polynomial-endofunctor l3 A B) โ†’
  ๐•Ž A B โ†’ type-algebra-polynomial-endofunctor X
map-hom-๐•Ž-Alg X (tree-๐•Ž x ฮฑ) =
  structure-algebra-polynomial-endofunctor X
    ( pair x (ฮป y โ†’ map-hom-๐•Ž-Alg X (ฮฑ y)))

structure-hom-๐•Ž-Alg :
  {l1 l2 l3 : Level} {A : UU l1} {B : A โ†’ UU l2}
  (X : algebra-polynomial-endofunctor l3 A B) โ†’
  ( (map-hom-๐•Ž-Alg X) โˆ˜ structure-๐•Ž-Alg) ~
  ( ( structure-algebra-polynomial-endofunctor X) โˆ˜
    ( map-polynomial-endofunctor A B (map-hom-๐•Ž-Alg X)))
structure-hom-๐•Ž-Alg X (pair x ฮฑ) = refl

hom-๐•Ž-Alg :
  {l1 l2 l3 : Level} {A : UU l1} {B : A โ†’ UU l2}
  (X : algebra-polynomial-endofunctor l3 A B) โ†’
  hom-algebra-polynomial-endofunctor (๐•Ž-Alg A B) X
hom-๐•Ž-Alg X = pair (map-hom-๐•Ž-Alg X) (structure-hom-๐•Ž-Alg X)

htpy-htpy-hom-๐•Ž-Alg :
  {l1 l2 l3 : Level} {A : UU l1} {B : A โ†’ UU l2}
  (X : algebra-polynomial-endofunctor l3 A B) โ†’
  (f : hom-algebra-polynomial-endofunctor (๐•Ž-Alg A B) X) โ†’
  map-hom-๐•Ž-Alg X ~
  map-hom-algebra-polynomial-endofunctor (๐•Ž-Alg A B) X f
htpy-htpy-hom-๐•Ž-Alg {A = A} {B} X f (tree-๐•Ž x ฮฑ) =
  ( ap
    ( ฮป t โ†’ structure-algebra-polynomial-endofunctor X (pair x t))
    ( eq-htpy (ฮป z โ†’ htpy-htpy-hom-๐•Ž-Alg X f (ฮฑ z)))) โˆ™
  ( inv
    ( structure-hom-algebra-polynomial-endofunctor (๐•Ž-Alg A B) X f
      ( pair x ฮฑ)))

compute-structure-htpy-hom-๐•Ž-Alg :
  {l1 l2 l3 : Level} {A : UU l1} {B : A โ†’ UU l2}
  (X : algebra-polynomial-endofunctor l3 A B) (x : A) (ฮฑ : B x โ†’ ๐•Ž A B)
  {f : ๐•Ž A B โ†’ type-algebra-polynomial-endofunctor X} โ†’
  (H : map-hom-๐•Ž-Alg X ~ f) โ†’
  ( ap
    ( structure-algebra-polynomial-endofunctor X)
    ( htpy-polynomial-endofunctor A B H (pair x ฮฑ))) ๏ผ
  ( ap
    ( ฮป t โ†’ structure-algebra-polynomial-endofunctor X (pair x t))
    ( htpy-postcomp (B x) H ฮฑ))
compute-structure-htpy-hom-๐•Ž-Alg {A = A} {B} X x ฮฑ =
  ind-htpy
    ( map-hom-๐•Ž-Alg X)
    ( ฮป f H โ†’
      ( ap
        ( structure-algebra-polynomial-endofunctor X)
        ( htpy-polynomial-endofunctor A B H (pair x ฮฑ))) ๏ผ
      ( ap
        ( ฮป t โ†’ structure-algebra-polynomial-endofunctor X (pair x t))
        ( htpy-postcomp (B x) H ฮฑ)))
    ( ap
      ( ap (pr2 X))
      ( coh-refl-htpy-polynomial-endofunctor A B
        ( map-hom-๐•Ž-Alg X)
        ( pair x ฮฑ)) โˆ™
    ( inv
      ( ap
        ( ap (ฮป t โ†’ pr2 X (pair x t)))
        ( eq-htpy-refl-htpy (map-hom-๐•Ž-Alg X โˆ˜ ฮฑ)))))

structure-htpy-hom-๐•Ž-Alg :
  {l1 l2 l3 : Level} {A : UU l1} {B : A โ†’ UU l2}
  (X : algebra-polynomial-endofunctor l3 A B) โ†’
  (f : hom-algebra-polynomial-endofunctor (๐•Ž-Alg A B) X) โ†’
  ( structure-hom-๐•Ž-Alg X โˆ™h
    ( ( structure-algebra-polynomial-endofunctor X) ยทl
      ( htpy-polynomial-endofunctor A B (htpy-htpy-hom-๐•Ž-Alg X f)))) ~
  ( ( (htpy-htpy-hom-๐•Ž-Alg X f) ยทr structure-๐•Ž-Alg {B = B}) โˆ™h
    ( structure-hom-algebra-polynomial-endofunctor (๐•Ž-Alg A B) X f))
structure-htpy-hom-๐•Ž-Alg {A = A} {B} X (pair f ฮผ-f) (pair x ฮฑ) =
  ( ( ( compute-structure-htpy-hom-๐•Ž-Alg X x ฮฑ
        ( htpy-htpy-hom-๐•Ž-Alg X (pair f ฮผ-f))) โˆ™
      ( inv right-unit)) โˆ™
    ( ap
      ( concat
        ( ap
          ( ฮป t โ†’ pr2 X (pair x t))
          ( eq-htpy (htpy-htpy-hom-๐•Ž-Alg X (pair f ฮผ-f) ยทr ฮฑ)))
        ( pr2 X (map-polynomial-endofunctor A B f (pair x ฮฑ))))
      ( inv (left-inv ( ฮผ-f (pair x ฮฑ)))))) โˆ™
  ( inv
    ( assoc
      ( ap
        ( ฮป t โ†’ pr2 X (pair x t))
        ( eq-htpy (htpy-htpy-hom-๐•Ž-Alg X (pair f ฮผ-f) ยทr ฮฑ)))
      ( inv (ฮผ-f (pair x ฮฑ)))
      ( ฮผ-f (pair x ฮฑ))))

htpy-hom-๐•Ž-Alg :
  {l1 l2 l3 : Level} {A : UU l1} {B : A โ†’ UU l2}
  (X : algebra-polynomial-endofunctor l3 A B) โ†’
  (f : hom-algebra-polynomial-endofunctor (๐•Ž-Alg A B) X) โ†’
  htpy-hom-algebra-polynomial-endofunctor (๐•Ž-Alg A B) X (hom-๐•Ž-Alg X) f
htpy-hom-๐•Ž-Alg X f =
  pair (htpy-htpy-hom-๐•Ž-Alg X f) (structure-htpy-hom-๐•Ž-Alg X f)

is-initial-๐•Ž-Alg :
  {l1 l2 l3 : Level} {A : UU l1} {B : A โ†’ UU l2}
  (X : algebra-polynomial-endofunctor l3 A B) โ†’
  is-contr (hom-algebra-polynomial-endofunctor (๐•Ž-Alg A B) X)
is-initial-๐•Ž-Alg {A = A} {B} X =
  pair
    ( hom-๐•Ž-Alg X)
    ( ฮป f โ†’
      eq-htpy-hom-algebra-polynomial-endofunctor (๐•Ž-Alg A B) X (hom-๐•Ž-Alg X) f
        ( htpy-hom-๐•Ž-Alg X f))
```