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