Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

HoTT foundational status update

Yesterday I read the article “Proof Theory of Constructive Systems: Inductive Types and Univalence” by Michael Rathjen and reviewed “From Multisets to Sets in Homotopy Type Theory” by Håkon Robbestad Gylterud.

Let CZF denote the constructive Zermel-Fraenkel set theory, a weak set theory which turns into full-blown ZF/ZFC iff Law of Excluded Middle/Axiom of Choice are respectively added. Let CZF(n) denote CZF + REA + Inacc(n), i.e. CZF augmented by Regular Extension Axiom and axioms about existence of `n` universes (`ω` is allowed, meaning Inacc(n) for each positive `n`).
Now let HoTT(n) be the univalent dependent intuitionistic type theory with higher inductive types and `n` universes (`ω` allowed) and HoTT(n++) the same theory augmented by existence of one additional universe U(n + 1) and type V of Un-small Aczel-Gylterud hereditary sets. Note that HoTT(n++) includes HoTT(n + 1) and is included in HoTT(n + 2).

Now, if I understand it correctly, the following holds:
1) For all `n`, CZF(n + 1) models HoTT(n++) which in turn models CZF(n). The whole sequence of theories shares same proof theoretic ordinal as long as `n` is finite. Moreover, CZF(n) proves the same arithmetical statements as HoTT(n + 1) and HoTT(n++).
2) CZF(ω) and HoTT(ω) are bi-interpretable, prove the same arithmetical statements and share the same proof theoretical ordinal (equal or slightly above Bachmann-Howard ordinal, yet way below KPM-ordinal).
3) In HoTT(ω) + LEM/AC the same construction models ZF(C)

Is it true that HoTT(n++) + LEM/AC would model ZF(C) + Inacc(n) and be modelled by ZF(C) + Inacc(n + 1)? If so, can we show conservativity regarding set-theoretic statements?

The results mentioned above can be shown to hold in a roundabout way, but could be straightforwardly if it turns out that Aczel-Gylterud iterated set construction in HoTT satisfies CZF + REA + ΠΣW-AC + RDC + PAx in strong enough sense.

Would adding propositional resizing (i.e. impredicative Prop) and/or inductive-recursive definitions to HoTT ruin something in this idyllic picture?
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.
  • 0 comments