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 ]

    • 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;

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

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