Skip to content

Tope disjuction elimination

Following Riehl and Shulman's type theory1, rzk-1 introduces two primitive terms for disjunction elimination:

  1. recBOT corresponds to \(\mathsf{rec}_\bot\), has any type, and is valid whenever tope context is included in BOT;

  2. recOR(«tope_1» |-> «term_1», ..., «tope_n» |-> «term_n») defines a term for a disjunction of topes «tope_1» \/ ... \/ «tope_n». This is well-typed when for an intersection of any two topes «tope_i» /\ «tope_j» the corresponding terms «term_i» and «term_j» are judgementally equal. In particular, recOR(psi |-> a_psi, phi |-> a_phi) corresponds to \(\mathsf{rec}_\lor^{\psi, \phi}(a_\psi, a_\phi)\).

Deprecated syntax

recOR(psi, phi, a_psi, a_phi) corresponds to \(\mathsf{rec}_\lor^{\psi, \phi}(a_\psi, a_\phi)\), is well-typed when a_psi is definitionally equal to a_phi under psi /\ phi. However, this syntax is deprecated since it is easy to confuse which tope relates to which term.

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