5
$\begingroup$

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

Improve this question
$\endgroup$
5
  • 3
    $\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 ♦
    Commented Sep 28, 2016 at 10:32
  • 3
    $\begingroup$ Open is too strong a word. It's more like "not yet definitively verified". $\endgroup$
    – Emil Jeřábek
    Commented Sep 28, 2016 at 10:50
  • 1
    $\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 ♦
    Commented Sep 28, 2016 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
    Commented Sep 28, 2016 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
    Commented Sep 28, 2016 at 16:54

1 Answer 1

Reset to default
1
$\begingroup$

It is not difficult to build models of Constructive NF on type theory, but if you want to get models of standard NF I don't think you can avoid the various sufferings that have been endured by previous generations.[1][2]

Equality and membership can be obtained from Coq's IZF implementation, and the only unimplemented part is stratified formula checker, which is also not difficult. However in general you can only go so far, you do not simply get NF consistency from CNF. (for example it is not clear if CNF implies axiom of infinity)

If [2] is correct, then we don't need a stronger type theory than Calculus of Constructions (CC), let alone HoTT.

If works in intensional NF (= just membership + stratified formula checker) and considers the setoid, groupoid structure on intensional NF, then the HoTT is useful for the extra design over CC. intensional NF is purer constructivism than the NF(U), but it will also be more different from the standard NF(U).

[1] https://arxiv.org/abs/1503.01406

[2] https://arxiv.org/abs/1406.4060

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ I would be a bit wary of [2], the Gabbay preprint. Earlier versions of the paper had significant gaps/errors in them (though certainly also promising ideas); I haven’t read the latest versions carefully, but as far as I know they’ve not generally been accepted by other experts in the field. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Jun 25, 2023 at 10:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .