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