Typechecking expressions / Translating to foundations #14
Description
Question: Can we typecheck FLaTeX expressions based on weak type annotations directly or do we need to translate them to a foundation?
Obviously, translation to e.g. MitM allows for type checking, but also requires decent alignment coverage.
Additionally/Alternatively: Maybe we can use realms (see #12) for this?
E.g. both a module for set theory and a module for type theory could provide pillars for an interface theory for implication, the former instantiates it with a set of pairs, the latter by a primitive constructor with inference rules. Then an expression containing only symbols for which pillars in type theory (or symbols which have definitions <- recurse) exist could be trivially translated to LF/MitM/LATIN2. "Type theory modules" in FLaTeX/FLOMDoc could be trivially aligned with LF/LATIN2/MitM concepts.
Similarly, a module for natural numbers could have a pillar for the Von Neumann construction, indicating how to translate it to ZF (or a weaker set theory - we only need infinity, extensionality and restricted comprehension, I think?), whereas the peano-axiomatic face-theory naturally yields a "type theoretic" pillar.