Extension types¶

Extension types \(\left\langle \prod_{t : I \mid \psi} A \vert ^{\phi} _{a} \right\rangle\) are written as {t : I | psi t} -> A [ phi |-> a ]
- specifying [ phi |-> a ] is optional, semantically defaults to [ BOT |-> recBOT ] (like in RSTT);
- specifying psi in {t : I | psi} is mandatory;
- values of function types are \(\lambda\)-abstractions written in one of the following ways:
  - \t -> <body> — this is usually fine;
  - \{t : I | psi} -> <body> — this sometimes helps the typechecker;
Types of functions from a shape \(\prod_{t : I \mid \psi} A\) are a specialised variant of extension types and are written {t : I | psi} -> A
- specifying the name of the argument is mandatory; i.e. {I | psi} -> A is invalid syntax!
- values of function types are \(\lambda\)-abstractions written in one of the following ways:
  - \t -> <body> — this is usually fine;
  - \{t : I | psi} -> <body> — this sometimes helps the typechecker;

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