Фундированные (∞,1)-категории

Подход к формализации предпучков над категориями при помощи чрезвычайно зависимых типов (very dependent types) проработан (в диссертации Николая Крауса) для обратных категорий, но похоже, допускает обобщение на категории более широкого класса — что-то вроде элегантных обобщённо-Риди (∞,1)-категорий, не до конца определённого пока очень общего класса категорий, включающий в себя все интересные используемые на данный момент категории форм. Это такое сильное обобщение симплициальной категории в том смысле, что все это наиболее общего вида класс категорий, где отображения факторизуются через отображения трёх особых классов: face maps, shape symmetries и degeneracy maps, причём первые задают на объектах фундированный порядок I, а вторые и третьи не мешают тому, чтобы строить категории предпучков пошагово по индукции вдоль порядка I.

С другой стороны, всё идёт к тому (см. последний абзац http://homotopytypetheory.org/2015/08/10/a-new-class-of-models-for-the-univalence-axiom/), что самый общий класс явных моделей HoTT — предпучки на этих самых элегантных обобщённых элегантных обобщённо-Риди (∞,1)-категорий.

Видимо это совпадение не случайно. А эти самые обобщённо элегантные, видимо, следует окрестить фундированными (∞,1)-категориями.