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
, ofWKL (Fin 2)
(Marginis link) ¬ WKL ℕ
.
For Fin 1
the path is indeed (obviously) unique.