Unique paths as formal points

Thierry Coquand and Peter Schuster

The paper mentions Weak König's Lemma.

We (define and) prove:

• WKL (Fin 0) (this is vacuous for any set, not just trees).
• WKL (Fin 1). This is computable and uses a nice exercise in list induction, zerolist.
• An equivalent, using Classical.choice, of WKL (Fin 2) (Marginis link)
• ¬ WKL ℕ.

For Fin 1 the path is indeed (obviously) unique.