Skip to content

Extension types

  1. 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 ]
  2. specifying [ phi |-> a ] is optional, semantically defaults to [ BOT |-> recBOT ] (like in RSTT);
  3. specifying psi in (t : I | psi t) is mandatory;

  4. 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;

  5. 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 t) -> A

  6. specifying the name of the argument is mandatory; i.e. (I | psi t) -> A is invalid syntax!
  7. values of function types are \(\lambda\)-abstractions written in one of the following ways:
    • \t -> <body> — this is usually fine;
    • \(t : I | psi t) -> <body> — this sometimes helps the typechecker;

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