Extension types¶

Extension types $⟨ \prod_{t : I ∣ ψ} A |_{a}^{ϕ} ⟩$ 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 $λ$ -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 ∣ ψ} 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 $λ$ -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 ↩