Questions tagged [internal-language]
The internal-language tag has no usage guidance.
1
question
25
votes
2
answers
346
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 ...