jonsterling/agda-effectful-forcing

Agda formalization of the paper, "Higher-Order Functions and Brouwer's Thesis". Deduces a Brouwer ordinal from a function ((nat -> nat) -> nat) in System T.

bar-induction formalization intuitionism system-t type-theory

This is based on Escardó's "effectful forcing" development. See http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.html for the original code and work to which we owe so much!

Languages

Agda99.8%Shell0.2%

Contributors

Created May 9, 2016

Updated November 23, 2025