My question is basically, what approaches have been made to make computer proof assistants which can handle the internal logic of a topos ?
To explain: while learning topos theory I was struck by the elegance of Mitchell-Bénabou language (the internal language of a topos). I was more delighted when I read Toposes and local set theories, by Bell, and found out that it is possible to build up the topos logic axiomatically, and use it to describe topos theory. Although I have not read it yet, I gather Lambek and Scott have a similar approach towards describing toposes (this time ones with natural number objects), using what they call intuitionistic type theories (but I am not sure about this). I have also heard there is dependent type theory, and homotopy type theory, but I do not really know about them.
Before I set off trying to build a proof assistant for local set theory independently, I wanted to understand what has been done before. So I have the following questions:
(1) Are dependent type theory, and/or homotopy type theory descriptive enough to handle the internal logic of a topos ? Are they at least as general as intuitionistic type theory / local set theory, in the sense that they can handle non-binary truth values etc. ?
(2) What is the state of the art type theory approach to handling topos logic ?
(3) What practical software exists for doing proofs in such type theories ? Should I be looking to agda, Coq, idris ? Do I have to write my own ?
I hope my lack of type theory knowledge does not make my questions sound too silly. I am just trying to find out which theory I should learn, for my goal of automating proofs in topos theory in a way which is acceptable by the communities of people doing computer assisted proofs, and type theory.
from Hot Weekly Questions - Mathematics Stack Exchange
Richard Southwell
Post a Comment