Errata to "On the logical structure of choice and bar induction principles", N. Brede, H. Herbelin
--------------------------------------------------------------------------------------------------
(July 2022)

While the definition of sequential alignment in Table XII is enough
for Theorem 4 to hold, the definitions of alignment in Table XV miss
stability by downwards (resp. upwards) inclusion for Theorem 7 to
work. They have to be changed into:
positive alignment of R (R⊤) : λu. ∀(a, b) ∈ u (R(a, b))
negative alignment of R (R⊥) : λu. ∃(a, b) ∈ u (R(a, b))

Page 3, column 2, definition of u ≺ₛ α: "is an initial prefix of f"
should be "is an initial prefix of α" (thanks to Jad Koleilat).

Proof of Proposition 6: the given more general lemma needed in the
proof is not general enough. It should state: "for u∈↓⁻T, T is
productive from u iff T has unbounded paths from u" (thanks to Étienne
Miquey).