Skip to content

Tope disjunction 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)\).

Removed syntax

Older versions of rzk also accepted the form recOR(psi, phi, a_psi, a_phi). This syntax has been removed, since it is easy to confuse which tope relates to which term. Use recOR(psi |-> a_psi, phi |-> a_phi) instead.

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