# New foundation in homotopy type theory

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}}$.

• The consistency of NF from ZFC is still open. What you linked is the fact that NFU is consistent relative to ZFC. – Asaf Karagila Sep 28 '16 at 10:32
• Open is too strong a word. It's more like "not yet definitively verified". – Emil Jeřábek Sep 28 '16 at 10:50
• @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. – Asaf Karagila Sep 28 '16 at 11:40
• 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. – Andrej Bauer Sep 28 '16 at 13:20
• 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... – Malice Vidrine Sep 28 '16 at 16:54