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).