#матлог #учёба #спецсеминар

13 мая 2026 г. состоится заседание Рабочего семинара по математической логике под руководством С.Л. Кузнецова и С.О. Сперанского, в рамках НОЦ МИАН.

Время начала: 16:00
Место: МИАН (ул. Губкина, 8), ауд. 303 + Контур.Толк
Всех слушателей просим зарегистрироваться на странице семинара: www.mathnet.ru/conf2533

Павел Турянский, Александр Грызлов

Гетерогенные колчаны и (ко)пределы, полиморфные по предикативному уровню

Аннотация:
На докладе покажем практические применения теории категорий для программирования с зависимыми типами. В языках без кумулятивности вселенных типов часто приходится явно поднимать типы до необходимого предикативного уровня, это усложняет формализацию, а иногда и не позволяет без изменений переиспользовать уже описанные конструкции. Используя подход G. Allais [1], можно определить категорные структуры, в которых уровни объектов и морфизмов не задаются константно, а вычисляются, что и позволяет избежать лишних поднятий. Рассмотрим, чем такой подход отличается от уже существующих (agda/cubical, Lean mathlib).

Понятия отображаемой структуры [2] и расслоения имеют свои аналоги не только для категорий, но и для рефлексивных графов [3]. Графы обобщаются до гетерогенных колчанов, где начала и концы стрелок лежат потенциально в разных типах, при этом многие конструкции на графах имеют осмысленную версию и на колчанах. В докладе покажем, как можно в гетерогенном стиле сформулировать (ко)пределы.

Литература
[1] G. Allais. (2019). Generic level polymorphic n-ary functions. URL: https://arxiv.org/abs/2110.06107
[2] B. Ahrens, P. Lumsdaine. (2019). Displayed Categories. URL: https://arxiv.org/abs/1705.04296
[3] J. Sterling. (2024). Reflexive graph lenses in univalent foundations. URL: https://arxiv.org/abs/2404.07854

Докладчик — Павел Турянский.