Gödel's Dialectica in Coq Various existing developments updated and ported to Coq+SSreflect / Cubical Agda. http://math.andrej.com/2011/01/03/the-dialectica-interpertation-in-coq/ https://github.com/ppedrot/vitef/tree/master/dialectica Pedrot, [2014] "A Functional Functional Interpretation" https://cj-xu.github.io/agda/Dialectica/Dialectica.html https://github.com/jeremie-koenig/diagames/