Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Попытка ответить на свой вопрос #HoTT

Несколько постов назад я задал вопрос, как бы нам так определить для высших индуктивных типов T тип $T, зависимых бесконечных последовательностей, где первым элементом e: T, вторым e1: Id(e, e), третьим e2: Id(e1, e1) и так далее. Понятно что это можно рассматривать как тип коданных заданный деструктором

d: $[T] -> (head: T, tail: $[Id(head, head)]),

но хочется же не этого. Если нам нужен только первый элемент этой последовательности, то этот тип изоморфен Unit -> T. Если первые два, то Interval -> T, где Interval это тип, заданный через
s: Interval
t: Interval
line: s = t,
также определимый как ||Boolean||. Любая функция их него, должна сказать, куда будет отображаться s и t (это один и тот же элемент по условию line), и куда line. Тут line не обязана отображаться в refl, в отличие от отображения из Unit.

Для случая первых трёх элементов, нам уже нужно, чтобы в исходном типе было три размерности, то есть надо сперва вместо одной line сделать две, а потом поставить в качестве условия их равенство. Это получается кружочек:
Kreis:
s: Kreis
t: Kreis
s1: s = t
t1: s = t
filler: s1 = s2

В трёхмерном случае это уже будет шарик. Давайте сразу для общего случая определим тип Ball: Nat -> Type.
Ball n:
s: Ball n
t: Ball n
s1: s = t
t1: s = t
s2: s1 = t1
t2: s1 = t1
...
filler: s_n = t_n.

Несложно заметить, что эти типы получаются индуктивно по следующей схеме:
Ball 0: Unit
Ball n:
s: Ball n
t: Ball n
filler: Ball (n - 1) -> (s = t)

Конечные варианты типа $[T] получаются как отображения (Ball n) -> T, но нам-то нужен полный тип, для чего нам нужен тип SuperBall, бесконечномерный мячик. Как бы его получить? Возможно есть какое-то универсальное свойство, возможно все отображения какого-то естественного типа между двумя высшими индуктивными типами факторизуются через SuperBall? Может быть функции ||X|| -> T это такие функции X -> T, которые можно записать как композицию X -> SuperBall -> T?, и SuperBall минимален в этом смысле?

* * *

На тип SuperBall -> SuperBall, очень похожий на булеан Серпиньского: пространство из двух точек, одна из которых замкнутая, а другая открытая. Как задаётся отображение f: SuperBall -> SuperBall?
На первом уровне возможны четыре варианта:
f(s) = f(t) = s, тогда на следующих уровнях все конструкторы refl.
f(s) = f(t) = t, тогда на следующих уровнях все конструкторы refl.
f(s) = s, f(t) = t, на следующих уровнях снова четыре варианта.
f(s) = t, f(t) = s, на следующих уровнях снова четыре варианта.

Итого, последовательность может на каждом уровне либо обрываться двумя способами, либо продолжаться двумя способами. С экстенциональной точки зрения ситуация много проще: все f, которые рано или поздно оканчиваются бесконечной последовательностью refl'ов между собой равны (то есть определяют одну точку p), причём если равенство имеет место, то оно дефиниционально, стало быть с точки зрения вычислительной топологии они определяют во множестве (SuperBall -> SuperBall) открытую точку: принадлежность к множеству {p} определяется за (заранее неизвестное, но) конечное число шагов, а отдельность от него не может быть определена за конечное время.
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