Слой топов

Все топы находятся во вселенной TOPE.

Вот все способы построения топа:

1. Ввести переменную, например (psi : TOPE) -> ...;

2. Обычно топы зависят от переменных точек из некоторого куба (кубов). Чтобы указать это, мы обычно вводим топы как "функции" из некоторого куба в TOPE. Например, (psi : I -> TOPE) -> ....

3. Использовать константу:

4. верхний топ \(\top\) записывается как TOP

5. нижний топ \(\bot\) записывается как BOT

6. Использовать соединительный оператор:

7. конъюнкция топов \(\psi \land \phi\) записывается как psi /\ phi
8. дизъюнкция топов \(\psi \lor \phi\) записывается как psi \/ phi
9. топ равенства \(t \equiv s\) записывается как t === s, когда t и s являются точками одного и того же куба
10. топ неравенства \(t \leq s\) записывается как t <= s, когда t : 2 и s : 2