MMT Syntax/Functionality Problem

[kohlhase]

here is a question about MMT functionality.

I (with a lot of help from Dennis) have started lattice theory in MitM. This has an interesting situation where POSets [2] and SemiLattices [1] form the basis of a realm, i.e. there is a biview between them (see [1]). Now, I would like to say that the two views are inverses.

This should be possible with Florian's new morphism application syntax (which I remember he said is implemented, but I see no documentation about that).

I would like to write something like

  biviewMeet : ⊢ SemilatticeIsPOSet (POSetIsMeetSemiLattice op ) ≐ op |
  biviewJoin : ⊢ SemilatticeIsPOSet (POSetIsJoinSemiLattice op ) ≐ op |

somewhere. Probably in a joint extension of POSetBounds and SemiLattice. But I am not sure about the actual details (see the comment with MiKo in [1])

@Florian, I am sure that you have thought about this, maybe you can help.

[1] https://gl.mathhub.info/MitM/smglom/blob/devel/source/algebra/lattice.mmt [2] https://gl.mathhub.info/MitM/smglom/blob/devel/source/sets/poset.mmt

[florian-rabe]

Have a look at MMT\LATIN\source\math\relations where Stefania (I think) and I worked out all the views in Twelf.

This work is very old and some syntax and design may be outdated by now. But it's quite deep other than that.

I recall we got stuck in one of the morphisms because two expressions had be LF-equal but were only LF/FOL-equal. I think it was the two order-relations (one induced by each algebraic semi-lattice) that are provably equal but not identical.

If we port the development to MMT, we might be able to make use of MMT's more flexible equality to solve this problem.

[florian-rabe]

Regarding your specific question, I suspect you want a module-level theorem that two morphisms are isomorphisms (and inverse to each other).

The main difficulty here is that "isomorphic" is underspecified because we can work in different quotients of the category of theories and morphisms: different equality relations on objects induce different equalities on morphisms and thus different categories:

• MMT: extremely weak, mostly useless
• MMT/LF: better, but still too weak in most cases
• MMT/(LF+proof irrelevance): the usually the minimum to get practically useful isomorphisms; proof irrelevance is needed because mapping an axiom back and forth will almost always yield a complex proof, not the original axiom
• MMT/LF/FOL: usually needed so that provably equal objects can be identified; that's probably what happens in the lattice case; this is also the trickiest case because it's undecidable and may require the user to provide proofs of equality; done correctly, this is a special case of a logical relation-argument