All Questions
Tagged with topos internal-language
1
question
25
votes
2
answers
390
views
How to use a proof assistant to reason in a topos?
I would like to use a proof assistant to reason in the internal language of a topos. More specifically, I would like to (be able to) formalise informal arguments such as in Ingo Blechschmidt's PhD ...
- 722