Устранение дизъюнкции топов

Следуя теории типов Рил и Шульмана¹, rzk-1 вводит два примитивных терма для исключения дизъюнкции:

1. recBOT соответствует \(\mathsf{rec}_\bot\), имеет любой тип и валиден, когда контекст топов включён в BOT;

2. recOR(«tope_1» |-> «term_1», ..., «tope_n» |-> «term_n») определяет терм для дизъюнкции топов «tope_1» \/ ... \/ «tope_n». Это хорошо типизировано, когда для пересечения любых двух топов «tope_i» /\ «tope_j» соответствующие термы «term_i» и «term_j» сужденчески равны. В частности, recOR(psi |-> a_psi, phi |-> a_phi) соответствует \(\mathsf{rec}_\lor^{\psi, \phi}(a_\psi, a_\phi)\).

Устаревший синтаксис

recOR(psi, phi, a_psi, a_phi) соответствует \(\mathsf{rec}_\lor^{\psi, \phi}(a_\psi, a_\phi)\), хорошо типизирован, когда a_psi определительно равен a_phi при psi /\ phi. Однако этот синтаксис устарел, так как легко перепутать, какой топ относится к какому терму.

---

1. Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures 1(1), 147-224. 2017. https://arxiv.org/abs/1705.07442 ↩