Tope layer

All topes live in TOPE universe.

Here are all the ways to build a tope:

1. Introduce a variable, e.g. (psi : TOPE) -> ...;

   • Usually, topes depend on point variables from some cube(s). To indicate that, we usually introduce topes as "functions" from some cube to TOPE. For example, (psi : I -> TOPE) -> ....

2. Use a constant:

   • top tope \(\top\) is written TOP
   • bottom tope \(\bot\) is written BOT

3. Usa a tope connective:

   • tope conjunction \(\psi \land \phi\) is written psi /\ phi
   • tope disjunction \(\psi \lor \phi\) is written psi \/ phi
   • equality tope \(t \equiv s\) is written t === s, whenever t and s are points of the same cube
   • inequality tope \(t \leq s\) is written t <= s whenever t : 2 and s : 2