Login
You're viewing the discuss.systems public feed.
  • Martin EscardoMartinEscardo@mathstodon.xyz
    Aug 22, 2024, 7:05 PM

    Is ℕ∞ an oddity among the zoo of types, by having these outrageously nice constructive properties?

    Perhaps.

    But there are as many such outrageously nice types as there are ordinals for which you can define "codes".

    (I) Given any such ordinal α, we can find a well-ordered type X(α) whose order type is ≥ α and X(α) has such outrageously nice constructive properties.

    This is in TypeTopology, but, unfortunately, I didn't get to write a paper about this yet, although I've given many talks with different angles about this situation.

    (II) And what are the ordinals α for which we can define codes in type theory in practice?

    They e.g. go well above the Feferman–Schütte ordinal

    en.wikipedia.org/wiki/Feferman

    as shown by Anton Setzer.

    So we have an outrageously large zoo of outrageously nice types, by combining (I) and (II).

    3/

    💬 1🔄 0⭐ 0

Replies

  • Martin EscardoMartinEscardo@mathstodon.xyz
    Aug 22, 2024, 7:37 PM

    Why invoke ordinals to explain that?

    Actually we don't need to.

    What I did, in practice, was to show that such outrageously nice types are closed under a number of type-theoretic constructions, so that we can get more and more of them.

    Then I saw, after the fact, that these constructions preserve not only outrageous-nicety but also well-orderedness (constructively).

    So we can use ordinals to measure how far we can get with outrageous nicety.

    4/

    💬 2🔄 0⭐ 0
  • Martin EscardoMartinEscardo@mathstodon.xyz
    Aug 23, 2024, 6:06 PM

    Let me add that the use of HoTT/UF is not essential for the above claims.

    We could equally work in the setoid model, to get the same results, where everything invoked above is also available, including propositional truncations and function extensionality.

    5/

    💬 0🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0