On: Gödel's Incompleteness Theorems (2015)

[ratmice]

> If anyone has looked into this more, would be interesting to hear about it!

I would have a look at e.g. Bob Harper's homotopy type theory lectures. In the 2nd lecture on Judgements, he goes through it at about 50 minutes in.

http://www.cs.cmu.edu/~rwh/courses/hott/

And Andrej Bauer's paper/lecture on "5 stages of accepting constructive mathematics"

[wfn → ratmice]

Thanks, will look at both! (I've been interested in HoTT but never looked closer.) Paper looks good, too (for future reference / interested folks, full version available at http://www.ams.org/journals/bull/0000-000-00/S0273-0979-2016... )