Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Categories:

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-правилом, всё меньше и меньше...
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 5 comments