Forcing Bar Induction in System T
Jonathan Sterling · arXiv (Cornell University) · 2016
Using Martin Escardo's effectful forcing technique, we demonstrate the constructive validity of Brouwer's monotone Bar Theorem for any System T-definable bar. We have not assumed any non-constructive (Classical or Brouwerian) principles in this proof, and have carried out the entire development formally in the Agda proof assistant for Martin-Loef's Constructive Type Theory.