TWIMC: Поездки

С 13 по 23 сентября я буду в командировке в Бостоне. Кто желает развиртуализоваться/познакомиться — буду очень рад. Я в Бостоне ничего и почти никого не знаю, так что буду рад в нерабочее время узнать город с кем-нибудь знающим.


P.S. В анкете на американскую визу меня попросили перечислить страны, в которых я был за последние 10 лет. Я посчитал и впечатлился: 16 стран: все граничащие с Германией (кроме Люксембурга), плюс Италия, Израиль, Финляндия, Белоруссия и Россия, плюс Монако и Ватикан впридачу. Притом всего в жизни я был в 18, за последние десять лет я не был в Казахстане и Украине. Из непосещённых западных стран, в ближайшие годы кроме США ещё хочется посмотреть Испанию, Португалию, Канаду, Норвегию и Исландию. Из полузападных, возможно, ещё что-нибудь из Балканских стран, Грецию и Турцию.

OTT + QITs?..

Пока змий-искуситель Воеводский не соблазнил нас яблоком унивалентности, мы пару лет жили в славном мире, где кроме неразрешимой extensional MLTT и противоестественно слабой intensional MLTT существовала Observational Type Theory МакБрайда-Альтенкирха, которая как будто решала все проблемы, кроме разве только проблемы определения фактортипов и тесно связанной с нею проблемы определения вещественных чисел и занятий анализом.

Из лагеря “змия-искусителя” пришла новая концепция: HITs — высшие индуктивные типы данных, их обрезанный до уровня просто множеств вариант, называемый Альтенкирхом QITs достаточен и для определения вещественных чисел, и для создания модели теории множеств, и, главное, для метапрограммирования и создания модели зависимой теории типов в самой себе, см. http://www.cs.nott.ac.uk/~txa/publ/tt-in-tt.pdf. Может быть можно пропатчить OTT так, чтобы она содержала QITs, и всё ещё имела вычислимое J-правило?.. Ведь в сущности, зачем простому смертному более мощные HITs? – только для занятий алгебраической топологией и высшими категориями, это ведь не всем нужно.

Но увы, простой смертный уже искушён змием, и знает что наличие унивалентных вселенных позволяет синтаксически идентифицировать изоморфные структуры, т.е. фактически, без всяких маханий руками, без тактик обёртывания в ватные слои синтаксического сахара делать то, без чего слабопредставимы почти все нетривиальные доказательства в математике. А наличие унивалентный вселенных, как показал Николай Краус, означает существование высших типов любого конечного уровня как минимум, значит даже терм имеющий тип Nat где-то внутри себя может нуждаться в применении J-правила к типам устроенным произвольно сложно, и надежды, что найдётся вычислительная модель с унивалентностю и вычислимым J-правилом, всё меньше и меньше...