Martin Escardo. W-types. \begin{code} {-# OPTIONS --safe --without-K #-} module W.index where import W.Type import W.Properties import W.Numbers import W.Paths \end{code}