Слой топов

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

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

1. Ввести параметр-семейство топов, «функцию» из некоторого куба в TOPE: (psi : I -> TOPE) -> .... Обычно топы зависят от переменных точек из некоторого куба (кубов), и семейство фиксирует эту зависимость; голый параметр-топ (psi : TOPE) -> ... означает то же, что семейство над единичным кубом, (psi : 1 -> TOPE) -> ..., применяемое как psi *_1.

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

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

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

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

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