3 ms·
Does anyone have experience with Coq and Mizar ( http://wiki.mizar.org/bin/view/Mizar http://wiki.mizar.org/bin/view/Mizar ) and could answer the question of th
by whitten 11y ago
Does anyone have experience with Coq and Mizar ( http://wiki.mizar.org/bin/view/Mizar http://wiki.mizar.org/bin/view/Mizar ) and could answer the question of the base for both ?
If Coq can be used with Vladimir Voevodsky's theory of univalent foundations, can Mizar also be based on them as well?
- digama 11y agoI don't believe you could vary Mizar to the extent that it mimics HoTT. Much of the basic properties that follow from the axioms Mizar uses (roughly ZFC + the Tarski-Grothendieck axiom) are built in to the internals of the Mizar prover, in order to increase its proving capability, at the expense of tying it to its axiom set. By contrast I can tell you that Metamath (http://us.metamath.org/mpegif/mmset.html http://us.metamath.org/mpegif/mmset.html), whose main library is also built on ZFC, does not at the most basic level assume any axioms at all (not even first order logic), so it is possible to do type theory or HoTT with no change to the verifier.