Модальности (экспериментально)¶

#lang rzk-1

Модальное расширение Rzk поддерживает рассуждения в стиле Триангулированной теории типов (TTT), введённой Гратцером, Вайнбергером и Бухгольцем¹ как обогащение симплициальной теории типов модальностями \(\flat\), \(\sharp\) и \(op\). Расширение реализовано Исламом Талиповым² с использованием параметризованной теории режимов (композиция и коэрсия режимов), надстроенной над существующими слоями кубов, топов и типов в Rzk. Оно входит в Rzk v0.8 и остаётся экспериментальным.

К формализациям, использующим этот синтаксис, относятся ветка diruniv репозитория sHoTT, в частности примеры модального API и разработка направленной унивалентности (17-diruniv.rzk).

Экспериментально

Модальности — это экспериментальное расширение, вошедшее в Rzk v0.8. Синтаксис и теория режимов могут измениться в будущих релизах.

Модальности в Rzk¶

В настоящее время Rzk поддерживает 3 модальности:

Описание	ASCII-синтаксис	Юникод-синтаксис
Дискретизация	`_b`	`♭`
Кодискретизация	`_#`	`♯`
Обращение направления стрелок	`_op`	`ᵒᵖ`
Тождественная	`_id`	—

Модальности компонуются согласно фиксированной теории режимов (например, _op/_op редуцируется к _id). Не каждая пара модальностей приводится друг к другу; решатель типов отслеживает, какие переменные доступны в текущем модальном контексте.

graph TB
  flat["♭  flat"]
  id["𝑖𝑑  identity"]
  sharp["♯  sharp"]
  op["ᵒᵖ  opposite"]

  flat -->|"coe"| id
  id  -->|"coe"| sharp
  id ~~~ op

♭ идемпотентна и поглощающая

\({\flat} \cdot {\flat} = {\flat}\) \({\flat} \cdot {\sharp} = {\flat}\)

\({op} \cdot {\flat} = {\flat}\) \({\flat} \cdot {op} = {\flat}\)

♯ идемпотентна и поглощающая

\({\sharp} \cdot {\sharp} = {\sharp}\) \({\sharp} \cdot {\flat} = {\sharp}\)

\({\sharp} \cdot {op} = {\sharp}\) \({op} \cdot {\sharp} = {\sharp}\)

op инволютивна

\({op} \cdot {op} = {id}\)

Модальные типы и введение¶

Тип в модальности µ записывается как <| µ | A |>, где A проверяется под µ. Терм этого типа вводится через mod µ t, где t проверяется в контексте «под» модальностью µ:

#def sharp-pure₁ (A : U) (x : A)
  : <| ♯ | A |>
  := mod ♯ x

Это работает для _#, потому что есть коэрсия id → _#, и любая переменная, доступная под id (то есть любая обычная переменная), доступна и под _#. Для _b такой коэрсии нет, поэтому аналогичное определение некорректно типизировано:

-- ошибка типизации
#def bad-flat-pure (A : U) (x : A)
  : <| _b | A |>
  := mod _b x

Модальный `let mod`¶

Модальный let mod — это принцип устранения для модальных типов. Модальные привязки используют форму let mod ext/inn x := value in body, где:

value проверяется на тип <| inn | T |> под ext-замком
body проверяется с x \(:^{ext \cdot inn}\) T в контексте

Если ext опущен, то let mod m x := value in body — это сахар для let mod _id/m x := value in body.

Это можно рассматривать как сопоставление с образцом mod в связке. Например, flat-extract — это противоположность sharp-pure; его можно определить именно потому, что существует коэрсия \(\flat \Rightarrow id\):

#def flat-extract (A : <| ♭ | U |>) (x : let mod ♭ Ab := A in <| ♭ | Ab |>)
  : let mod ♭ Ab := A in Ab
  := let mod ♭ xb := x in xb

С помощью let mod можно определить модальную композицию \(\langle \mu | \langle \nu | A \rangle \rangle \to \langle \mu \cdot \nu | A \rangle\). Конкретный пример — double-op:

#def double-op (A : U) (x : <| ᵒᵖ | <| ᵒᵖ | A |> |>)
  : A
  :=
  let mod ᵒᵖ x_1 := x in
  let mod ᵒᵖ / ᵒᵖ x_2 := x_1 in
  x_2

Модальные связки¶

Модальные аннотации параметров (x : m A) — это синтаксический сахар, который делает определения менее многословными по сравнению с явной формой let mod. Параметр (x : _b A) -> ... разворачивается в (_a : <| _b | A |>) → let mod _b x := _a in …. Этот сахар доступен в λ-абстракциях, Π- и Σ-типах, а также в списках аргументов определений.

Например, b-extract и b-map, записанные с модальными связками, гораздо чище, чем явная форма let mod, показанная выше:

#def b-extract₁ (A : ♭ U) (x : ♭ A)
  : A
  := x

#def b-map₁ (A B : ♭ U) (f : ♭ A → B)
  : <| ♭ | A |> → <| ♭ | B |>
  :=
  \ (x : ♭ A) → mod ♭ (f x)

Комбинаторы в стиле S4¶

Ниже — небольшой самодостаточный пример модального синтаксиса. Комбинаторы следуют структуре в стиле S4: каждая модальность снабжена операциями extract/map/join там, где это допускает теория режимов. Обратите внимание, что ♭ несёт комонадическую структуру (b-extract, b-map, b-dup), тогда как ♯ несёт монадическую структуру (sharp-pure, sharp-map, sharp-join).

#def b-extract (A : ♭ U) (x : ♭ A)
  : A
  := x

#def b-map (A B : ♭ U) (f : ♭ A → B)
  : <| ♭ | A |> → <| ♭ | B |>
  := \ (x : ♭ A) → mod ♭ (f x)

#def b-dup (A : ♭ U) (x : ♭ A)
  : <| ♭ | <| ♭ | A |> |>
  := mod ♭ (mod ♭ x)

#def op-map (A B : ᵒᵖ U) (f : ᵒᵖ A → B)
  : <| ᵒᵖ | A |> → <| ᵒᵖ | B |>
  := \ (x : ᵒᵖ A) → mod ᵒᵖ (f x)

#def sharp-pure (A : U) (x : A)
  : <| ♯ | A |>
  := mod ♯ x

#def sharp-map (A B : U) (f : A → B)
  : <| ♯ | A |> → <| ♯ | B |>
  := \ (x : ♯ A) → mod ♯ (f x)

#def sharp-join (A : U) (a : <| ♯ | <| ♯ | A |> |>)
  : <| ♯ | A |>
  :=
  let mod ♯ x_1 := a in
  let mod ♯ / ♯ x_2 := x_1 in
  mod ♯ x_2

Как решатель типов использует модальности¶

Модальности не только вводят модальные типы, но и накладывают ограничения на то, как переменные можно вводить и использовать.

Каждое выражение mod m … или <| m | … |> ставит m-замок (замок, помеченный модальностью \(m\)) на текущий контекст.
let mod ext/inn x := value in body вводит x как связку, параметризованную модальностью с модальностью \(ext \cdot inn\).
Переменная, связанная под модальностью \(\mu\), может использоваться, только когда накопленный замок \(\hat{m}\) — композиция всех m-замков, поставленных между местом связывания и местом использования, — \(\mu\)-приводим, то есть существует коэрсия из \(\mu\) в \(\hat{m}\).

Если модальность переменной не приводима к текущему накопителю замков, решатель типов сообщает:

unaccessible var with modality … under locks …

Модальности на уровне топов¶

Обращение стрелок с помощью op¶

Модальности также доступны на слоях кубов и топов. Их механика та же, что и у модальных типов на слое зависимых типов. Дополнительно есть операторы для обращения кубов и топов.

Эквивалентность между 2 и <| _op | 2 |> свидетельствуется flipᵒᵖ и unflipᵒᵖ. В частности, flipᵒᵖ 0₂ редуцируется к mod _op 1₂ и наоборот.

Эквивалентность между TOPE и <| _op | TOPE |> свидетельствуется invᵒᵖ и uninvᵒᵖ, которые обращают направление неравенств.

Вот пример функции, обращающей направление морфизма с помощью модальности _op:

#def op-hom-to-hom
  ( B : _op U)
  ( x : _op B)
  ( y : _op B)
  ( h : _op (t : 2) → B [ t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y ])
  : ( ( t : 2) → <| _op | B |> [ t ≡ 0₂ ↦ mod _op y , t ≡ 1₂ ↦ mod _op x ])
  := \ t → let mod _op s := flipᵒᵖ t in mod _op (h s)

Устранение дискретного интервала¶

Дискретный интервал <| _b | 2 |> можно трактовать как булев тип. Чёткая точка типа 2 — это либо 0₂, либо 1₂, поэтому возможен разбор случаев:

#def discrete-2-elim (i : _b 2) (A : U) (x y : A) : A :=
  recOR(
    (i === 0_2) |-> x,
    (i === 1_2) |-> y)

Известная ловушка некорректности: не постулируйте `√` на `2`¶

Не постулируйте √ ("2 крошечный") на кубе 2

При формализации Триангулированной теории типов¹ естественно напрашивающимся следующим шагом после введения модальностей выглядит постулирование удивительной правой сопряжённой √ к функтору пространства путей (2 → −) — что эквивалентно утверждению, что направленный интервал 2 является крошечным (tiny). Это некорректно на стандартной модели RS17.

Причина структурная. В стандартной модели симплициальных множеств PSh(∆) направленный интервал реализуется представимым y([1]), и у функтора (−)^I нет правой сопряжённой — конкретное препятствие в том, что возведение в степень y([1]) не сохраняет кодекартовы квадраты (см. Гратцер–Вайнбергер–Бухгольц §1.3 и §3, сноска 7). Куб 2 в Rzk наследует ровно эту линейно упорядоченную структуру, поэтому постулирование √ на 2 — или любой формулировки is-tiny(2) — противоречит модели.

Планируемый примитив 𝕀 — куб-ограниченная дистрибутивная решётка, согласно GWB §1.3, — будет корректным местом для постулирования √. Пока 𝕀 не реализован, формализации TT⊲ с √-на-2 потенциально могут быть некорректными (если используемый решатель топов когда-либо начнёт опираться на линейный порядок).

Аксиомы и крупные формализации¶

Многие принципы TTT не встроены в Rzk как первичные правила; они вводятся через #postulate в библиотеках. В ветке diruniv репозитория sHoTT примеры включают чёткую индукцию для _b и аксиомы для модальности направленного интервала. Разработка направленной унивалентности в 17-diruniv.rzk — это эталонный корпус того, как модальный синтаксис используется в полном масштабе; эта страница не воспроизводит то доказательство.

Дополнительное чтение¶

Гратцер, Вайнбергер и Бухгольц — Directed univalence in simplicial homotopy type theory (TTT)
Талипов и Кудасов — Towards Formalization of Directed Univalence in Rzk proof assistant — представленный доклад на HoTT/UF 2026 по этому расширению
sHoTT diruniv — формализации, использующие модальности Rzk
Введение — слои кубов, топов и типов
Зависимые типы — функции, суммы и типы тождеств без модальностей

Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz. Directed univalence in simplicial homotopy type theory. arXiv:2407.09146, 2024 (исправл. 2026). https://arxiv.org/abs/2407.09146 ↩↩
Islam Talipov, Nikolai Kudasov. Towards Formalization of Directed Univalence in Rzk proof assistant. Представленный доклад, HoTT/UF 2026. https://hott-uf.github.io/2026/abstracts/HoTTUF_2026_paper_22.pdf ↩