Просто не нужно путать тот язык, в котором мы работаем в теоркате, и internal язык топоса

До алгебры Гейтинга, если конкретнее. Истинностные значения в топосе её образуют

Ну вот я говорил про Omega в Effective топосе. Она соответствует истинностным значениям конструктивизма Маркова, классам вычислимости подмножеств натуральных

Соответственно к Хотту это всё непосредственно не относится.
Т.к. все местные определения требуют равенства между морфизмами в определениях лимитов.
Есть обобщение, где равенство заменяется на изоморфизм  более высокого порядка, их равенство - на изоморфизм ещё более высокого и т.п.
Это соответствует  (∞, 1) топосам, т.е. (∞, 1) - категориям с (∞, 1) - лимитами
Вот это уже, как я понимаю имеет отношение к HoTT

Топос, это категория, достаточно похожая на категорию предпучков (т.е., контрвариантных функторов F^op -> Set).

subobject

В каждом топосе своё Omega.

Да правильно всё.

В любой категории Omega уникален, если существует (как и большинство категорных конструкций)

Добрый день! Можете на примере показать разницу между G->1->G и айдишкой?

пример: отображение в одноэлементное множество и потом его вложение, а айдишка сохраняет все множество

Спасибо! Примерно также хотел

О, приветствую! Как-то слишком много людей тут из вашего чата...

А "ваш" это что за чат, если не секрет?

Чат канала "Жизнь с другими". Он не про математику, так что едва ли Вам будет интересно.

Понял, спасибо!

И вам привет. Почему же 'слишком'? У меня тоже люди, любящие foundations дисциплин

Добрый день! Посоветуйте, пожалуйста, книги (хоть на англ), где разобраны задачи по функциональному анализу. Интересуют метрические пространства, непрерывность, равномерная непрерывность, условие Липшица. Очень много задачников знаю, 99% из них даже без ответов в конце, но не знаю книг, где разобраны хотя бы типичные примеры. А на примерах эти темы намного легче понимать, чем через абстрактную теорию. Заранее спасибо!

Вы, скорее всего, ошиблись чатом.