Martin Escardo.

W-types.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module W.Type where

open import MLTT.Spartan

data W {๐“ค ๐“ฅ : Universe} (X : ๐“ค ฬ‡ ) (A : X โ†’ ๐“ฅ ฬ‡ ) : ๐“ค โŠ” ๐“ฅ ฬ‡ where
 ssup : (x : X) (ฯ† : A x โ†’ W X A) โ†’ W X A

module _ {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } where

 private
  ๐•Ž = W X A

 W-root : ๐•Ž โ†’ X
 W-root (ssup x ฯ†) = x

 W-forest : (w : ๐•Ž) โ†’ A (W-root w) โ†’ ๐•Ž
 W-forest (ssup x ฯ†) = ฯ†

 W-ssup-root : (x : X) (ฯ† : A x โ†’ ๐•Ž)
             โ†’ W-root (ssup x ฯ†) ๏ผ x
 W-ssup-root x ฯ† = refl

 W-ssup-forest : (x : X) (ฯ† : A x โ†’ ๐•Ž)
               โ†’ W-forest (ssup x ฯ†) ๏ผ ฯ†
 W-ssup-forest x ฯ† = refl

 W-ฮท : (w : ๐•Ž) โ†’ ssup (W-root w) (W-forest w) ๏ผ w
 W-ฮท (ssup x ฯ†) = refl

 W-induction : (P : ๐•Ž โ†’ ๐“ฆ ฬ‡ )
             โ†’ ((x : X) (ฯ† : A x โ†’ ๐•Ž)
                   โ†’ ((a : A x) โ†’ P (ฯ† a)) โ†’ P (ssup x ฯ†))
             โ†’ (w : ๐•Ž) โ†’ P w
 W-induction P IH = h
  where
   h : (w : ๐•Ž) โ†’ P w
   h (ssup x ฯ†) = IH x ฯ† (ฮป x โ†’ h (ฯ† x))

 W-induction' : (P : ๐•Ž โ†’ ๐“ฆ ฬ‡ )
             โ†’ ((w : ๐•Ž)
                   โ†’ ((a : A (W-root w)) โ†’ P (W-forest w a))
                   โ†’ P w)
             โ†’ (w : ๐•Ž) โ†’ P w
 W-induction' P IH = W-induction P (ฮป x ฯ† IH' โ†’ IH (ssup x ฯ†) IH')

 W-recursion : (P : ๐“ฆ ฬ‡ )
             โ†’ ((x : X) โ†’ (A x โ†’ ๐•Ž)
                        โ†’ (A x โ†’ P) โ†’ P)
             โ†’ ๐•Ž โ†’ P
 W-recursion P = W-induction (ฮป _ โ†’ P)

 W-iteration : (P : ๐“ฆ ฬ‡ )
             โ†’ ((x : X) โ†’ (A x โ†’ P) โ†’ P)
             โ†’ ๐•Ž โ†’ P
 W-iteration P g = W-recursion P (ฮป X _ โ†’ g X)

\end{code}

The record version of W:

\begin{code}

record W' {๐“ค ๐“ฅ : Universe} (X : ๐“ค ฬ‡ ) (A : X โ†’ ๐“ฅ ฬ‡ ) : ๐“ค โŠ” ๐“ฅ ฬ‡ where
 inductive
 constructor
  ssup
 field
  prโ‚ : X
  prโ‚‚ : A prโ‚ โ†’ W' X A

\end{code}

Indexed version of W:

\begin{code}

data Wแตข {๐“ค ๐“ฅ ๐“ฆ : Universe}
        (I : ๐“ฆ ฬ‡ )
        (A : ๐“ค ฬ‡ )
        (t : A โ†’ I)
        (B : A โ†’ ๐“ฅ ฬ‡ )
        (s : (a : A) โ†’ B a โ†’ I)
      : I โ†’ ๐“ค โŠ” ๐“ฅ โŠ” ๐“ฆ ฬ‡
 where
  ssup : (a : A) โ†’ ((b : B a) โ†’ Wแตข I A t B s (s a b)) โ†’ Wแตข I A t B s (t a)

\end{code}

E.g. for typed terms:

  I    type of "types"
  A    type of operations
  t    type of the result
  B    arity assignment
  s    type of arguments