Is there any model of NF (New Foundations) on HoTT (homotopy type theory)?

Because there is a model of ZF(C) on HoTT (The HoTT book, Section 10.5) and NF on ZFC (by this Wikipedia articile), I think anyway we have a model of NF in that way. I am looking for easier ways to define one.

I tried to define a model by assigning $\mathsf{Set}_{\mathcal{U}_n}$ to the collection of sets of type $n$, but I got stuck when I tried to define the membership relation between $x: \mathsf{Set}_{\mathcal{U}_{n}}$ and $y: \mathsf{Set}_{\mathcal{U}_{n+1}}$.

  • 2
    $\begingroup$ The consistency of NF from ZFC is still open. What you linked is the fact that NFU is consistent relative to ZFC. $\endgroup$ – Asaf Karagila Sep 28 '16 at 10:32
  • 1
    $\begingroup$ Open is too strong a word. It's more like "not yet definitively verified". $\endgroup$ – Emil Jeřábek Sep 28 '16 at 10:50
  • $\begingroup$ @Emil: Sure. I met Randall at some point and he gave me a full account of the proof he had at the time. It's been three months or so, which is forever in new developments as far as his manuscript goes. $\endgroup$ – Asaf Karagila Sep 28 '16 at 11:40
  • 1
    $\begingroup$ Types do not have a global membership relation. Since in NF you need such a relation, it is best to think of a model of NF as something that builds both the universe of sets and the membership relation simultaneously. I would try to define the type $\mathsf{NF}$ of NF-sets and the membership relation $\in_\mathsf{NF}$ simultaneously as an inductive-inductive definition. $\endgroup$ – Andrej Bauer Sep 28 '16 at 13:20
  • 1
    $\begingroup$ It would certainly be interesting if there were such a model, though it's very far from clear how you'd do it. I'm not sure Holmes' proof would translate well into a typed context, but Holmes has expressed suspicion that any inductive construction of $\in_{NF}$ would be at least as ugly as his proof... $\endgroup$ – Malice Vidrine Sep 28 '16 at 16:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.