Documentation

Marginis.CoquandSchuster2011

Unique paths as formal points #

Thierry Coquand and Peter Schuster

The paper mentions Weak König's Lemma.

We (define and) prove:

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

def tree {α : Type} (T : Set (List α)) :
Equations
def has_a_path {α : Type} (T : Set (List α)) :
Equations
def WKL {α : Type} :
Equations
theorem wklFin0 :
WKL
theorem zerolist (σ : List (Fin 1)) :
σ = List.replicate σ.length 0
theorem wklFin1 :
WKL