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) -> ...;

2. 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) -> ....

3. Use a constant:

4. top tope \(\top\) is written TOP

5. bottom tope \(\bot\) is written BOT

6. Use a tope connective:

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