4
$\begingroup$

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.
  admit.
Admitted.

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?

$\endgroup$
6
  • 2
    $\begingroup$ The HoTT book has a chapter on this and I'm fairly sure that they show how to derive induction types for all the core types that they introduce. $\endgroup$
    – Jake
    Jul 28, 2021 at 18:34
  • $\begingroup$ @Jake, I must say I have never actually read the HoTT book so far. Maybe it's about time I do so. $\endgroup$ Jul 28, 2021 at 20:06
  • 1
    $\begingroup$ You need function extensionality in order to show that two trees are equal if they have the same branching type and equal subtrees. $\endgroup$ Jul 29, 2021 at 13:35
  • 2
    $\begingroup$ 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. $\endgroup$ Jul 29, 2021 at 15:22
  • 1
    $\begingroup$ @AndrásKovács: Ah yes, I forgot about Jasper Hugunin's gem! $\endgroup$ Jul 29, 2021 at 15:43

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.