# Importing (translating) Mizar into Coq (Axiomatic set theory into constructive type theory)

There are 3 basic formalisms of the mathematical knowledge (and their respective theorem provers/libraries):

1. Axiomatic set theory (Mizar)
2. Higher order logic (Isabelle/HOL)
3. Constructive Type Theory (Coq)

The translations among formalisms is big open problem according to https://jfr.unibo.it/article/view/4570. There are translations from HOL to Set theory and Type Theory (see resp. https://link.springer.com/chapter/10.1007%2F978-3-642-14052-5_22 and https://link.springer.com/chapter/10.1007/978-3-642-14052-5_23), but I have not managed to find translation from Set theory to Type Theory (importing Mizar into Coq). There is one work about Mizar mode in Coq, but it explicitly states, that such mode is not importing Mizar into Coq.

So - I am asking for references and ideas - how to import Mizar in Coq or how to express (translate into) axiomatic set theory into constructive type theory?

First, I'll say what is easy relatively speaking. You can formalize Tarski-Grothendieck set theory (TG) in Coq. Jonas Kaiser axiomatizes TG in Formal Construction of a Set Theory in Coq mentioned in the mailing list post. Another paper mentioned in the same mailing list post, Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families by Bruno Barras, formalizes the closely related ZFC+U but does so in a somewhat different way. Kaiser simply postulates a type $\mathsf{set}$ and a relation ${\in} :\mathsf{set}\to\mathsf{set}\to\mathsf{Prop}$ and the TG axioms. This approach is basically just using Coq as a logical framework and doesn't "reduce" TG to CIC at all. Barras, on the other hand, while also introducing a type $\mathsf{set}$, does so by definition rather than postulation in which case some of the axioms and notions of set theory can be derived, though some axioms still need to be postulated to go all the way. This provides a more proper reduction of ZFC+U to CIC plus some axioms which aren't doing all of the work as they are in Kaiser's case.
With either approach, the key thing for us is that anything you might talk about in either of these systems is a value of type $\mathsf{set}$. If all you cared about is verifying Mizar proofs with Coq, then this would be relatively straightforward. Certainly, as far as the TG axioms, you'd be able to translate those one-to-one. The Mizar meta-language is actually not that different from a dependent type theory and should be able to be translated without too much trouble. The hardest part is likely to be some of the built-in reasoning of Mizar's proof language. With sufficiently fancy Ltac programming, you should be able to produce tactics that mimic these proof rules, allowing a simple translation.
The issues and solutions to programming language interoperability have direct parallels. First, we need a way to embed values of arbitrary types into $\mathsf{set}$ and to project them out. But for a type $T$, there is not a unique or canonical embedding $T\to\mathsf{set}$. We'd likely more prefer something like $T\cong\Sigma s\!:\!\mathsf{set}.\varphi(s)$ where $\varphi(s)$ states that $s$ is a set-theoretic representation of $T$. This isomorphism is not unique and neither $\varphi$ nor the isomorphism can be automatically, let alone uniformly, derived. However, you could derive a $\varphi$ and isomorphism of this form in a type-directed manner (using meta-programming techniques or possibly "type classes"), but the problem there is that the set-theoretic representation, i.e. $\varphi$, quite likely won't be the representation the Mizar proofs were written against. You could resolve this by proving in Mizar (or in Coq) that the two set-theoretic representations were isomorphic. This can't be automated. You then need to insert these conversions all over the place. This can be partially automated. However, you can only prove things using the Mizar proofs with respect to a representation, and you have no way of verifying that you've used the correct representation. If I define $<$ on naturals as $\in$, from Coq that's just a $\mathsf{set}\to\mathsf{set}\to\mathsf{Prop}$ predicate. If I use the wrong representation, I just get seemingly false theorems. Adding proofs to validate the representations and wrapping things to produce a more idiomatic interface can't be automated. Finally, the proof checking of the translated Mizar proofs is likely to be far less efficient than a more idiomatic direct encoding. (Yes, mathematicians in the not distant future [it's already happening now] will have to care about performance just like us programmers.)