Где R — это модель вещественной прямой. Еще его называют фунда | Формальна Філософія

Где R — это модель вещественной прямой. Еще его называют фундаментальный инфинити групоид. Обратный оператор (бемоль или флэт модалити) соотвественно переводит из гомотопического определения (для чего HoTT и была придумана) в теоретико-множественное определение, наделяя это множество топологией, заданной покрытием, сформированным из гомотопической информации по HIT типу (или другими словами на основе его гомогенной структуры композиции). Если представить бемоль в теории типов, то ничего интересного не получится, так как это будет просто коиндуктивный процесс ретопологизации:

data flat (A: U)
= con (x: flat A)

flatInd (A: U) (C: flat A -> U)
(f: (u: flat A) -> C (con u))
: (x: flat A) -> C x
= split con x -> f x

Один из примеров связующих топосов — это категории рефлексивных графов, как предпучок над категорией множеств. Если G — такой граф, то shape(G) — это граф компонентной связности G, flat(G) — это граф с теми же вершинами, что G, но только лишь с рефлексивными стрелками, sharp(G) — это полная сеть на множестве вершин графа G.

Теперь перейдем к дифференциальной геометории и тройке сопряженным модальных операторов связующего дифференциального топоса:

re (coerflection) ⊣ im (reflection) ⊣ etale.

Средний модальный оператор — это коредукция, стек де Рама, или инфинитезимальная форма, она позволяет моделироват бесконечно-малые окресности вокруг точек, скрывая комонадические вычисления за 5 аксиомами теории типов: формация, интро, элиминатор, бета и эта правила. С ее помощью мы будем моделировать картановую геометрию в HoTT в следующих выпусках.

Im : U -> U
ImUnit (A: U) : A -> Im A
isCoreduced (A:U): U = isEquiv A (Im A) (ImUnit A)
ImCoreduced (A:U): isCoreduced (Im A)
ImRecursion (A B: U) (c: isCoreduced B) (f: A -> B) : Im A -> B

Про связующие топосы вы можете почитать в работах Уильяма Ловера, Майкла Шульмана, Урса Шрайбера, Феликса Веллена, Дэна Ликаты. Последние два также есть на youtube.