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

boththe 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