Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Open induction for h-truncations

Высшие индуктивные типы это такие типы, у которых не только set level представляет из себя well-ordering type, но и все другие высшие типы. Индукция по обычным W-типам это обычная трансфинитная индукция, а индукция по высшим индуктивным типам должны быть её известным обобщением: открытой индукцией.

Как же будет выглядеть открытая рекурсия?
* * *

Mike Shulman recently succeed in constructing HITs H with paths in all dimensions. Is there a way to define a type $H of all sequences of the elements e: H, together with their automorphisms e1: Id H e e, their equivalences e2: Id (Id H e e) e1 e1, etc? It seems to be a very natural way to define separable second-countable T0 spaces with semidecidable apartness relation.

Has anyone already thought about connections between such types and open induction? In appears that some such induction would provide the only generic way to prove stuff for elements of $H.

Open induction is a generalization of transfinite induction:
Let U: Seq T → Prop be an open property on infinite sequences of T, _<_: (T, T) → Prop a decidable wellfounded relation on T. The relation _<_ can be lexicographically extended to sequences of T, the resulting relation is not necessarily wellfounded anymore, but still

[∀(a: Seq T, b: Seq T) a < b → U b → U a] → ∀(s: Seq T) U(s)

What's the recursion counterpart to the open induction?
Subscribe

  • Прогресс

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

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

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

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)

  • 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.
  • 17 comments

  • Прогресс

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

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

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

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)