Elimination theorem for the theory of binary choice sequences

We define the theory of binary choice sequence BCS. The BCS contains choice sequences other than constructive functions on the natural numbers, and has axioms of analytic data and continuity for binary choice sequences. We show that BCS is a conservative extension of the theory of elementary analysis EL (which is a conservative extension of HA) by adapting the method of elimination of choice sequences by Kreisel and Troelstra to the binary choice sequences. As an application, we show that EL + (Fan theorem) admits a constructive interpretation in EL. Moreover, we relate our elimination translation to a sheaf semantics of BCS in the category of sheaves on the site whose underlying category is the monoid of uniformly continuous functions on Cantor space equipped with the open cover topology.  Specifically, our translation is a formalization of the sheaf semantics in EL.