Перейти к содержанию

Типы-расширения

  1. Типы-расширения \(\left\langle \prod_{t : I \mid \psi} A \vert ^{\phi} _{a} \right\rangle\) записываются как (t : I | psi t) -> A [ phi |-> a ]
  2. указание [ phi |-> a ] необязательно, семантически по умолчанию равно [ BOT |-> recBOT ] (как в RSTT);
  3. указание psi в (t : I | psi t) обязательно;

  4. значения типов функций — это \(\lambda\)-абстракции, записанные одним из следующих способов:

    • \t -> <body> — это обычно подходит;
    • \(t : I | psi t) -> <body> — это иногда помогает проверщику типов;

  5. Типы функций из формы \(\prod_{t : I \mid \psi} A\) — это специализированный вариант типов-расширений и записываются как (t : I | psi t) -> A

  6. указание имени аргумента обязательно; т.е. (I | psi t) -> A — это невалидный синтаксис!
  7. значения типов функций — это \(\lambda\)-абстракции, записанные одним из следующих способов:
    • \t -> <body> — это обычно подходит;
    • \(t : I | psi t) -> <body> — это иногда помогает проверщику типов;

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