# Is it possible to recover induction for nat from W-types?

W-types generalize the type of well-founded trees, i.e., possibly infinetely branching trees. I understand that inductive types may be encoded as such in dependent type theory (CIC, MLTT, etc), this answer being particularly helpful in that, but is it possible to derive the usual induction principles from those? E.g., consider the following code in Coq:

Inductive W (A: Type) (B: A -> Type): Type :=
| sup:
forall a: A, (B a -> W A B) -> W A B.

Definition nat: Type :=
W bool (fun b =>
if b then
(* Zero recursive arguments *)
False
else
(* One recursive argument. *)
unit).

Definition O: nat :=
sup _ _ true (False_rect _).

Definition S (n: nat): nat :=
sup _ _ false (fun _ => n).

Lemma nat_rect:
forall P: nat -> Type,
forall H1: P O,
forall H2: (forall n, P n -> P (S n)),
forall n, P n.
Proof.

It seems that I can't show that, e.g., the function for O is $$\bot$$-elimination, even though (I believe) it's the only possible function to write at that point. If it's not possible to do that in Coq, would it be possible in HoTT/CTT?
• If Coq had eta rule for the unit type, it would be possible to define nat from W without funext, with exactly the same computational behavior as expected: jashug.github.io/papers/whynotw.pdf. Agda has the required eta, but not Coq. Jul 29, 2021 at 15:22