[TYPES] Representing inductive types with W-types

[roconnor at theorem.ca]

Does anyone have a reference on how to encode (non-mutually recursive) 
inductive data type declarations of a language similar to CiC using 
W-Types?

I was playing around with this by hand, and I can make ad-hoc encodings 
for the types I've tried; but I haven't quite figured out what the 
systematic translation is.  For example, I find

Inductive Tree (A:Type) : Type :=
node : A -> list (Tree A) -> Tree A

quite difficult to translate.  I can only manage because I happen to know 
that list X ~ Sigma n:nat. Fin n -> X

where Fin

Fin 0 = Void
Fin (S n) = Unit + Fin n

By my ad hoc method I get

nat ~ W : Bool. if b then Void else Unit
list A ~ W x : Unit + A. [const Void | const Unit] x
Tree A ~ W (a,n):A*nat. Fin n

But of course nat and Fin do not directly appear in the Inductive 
definition of Tree, so I'm not entirely sure how to deduce them (or 
something isomorphic) systematically.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''