(By request from a comment: UF stands for [Univalent Foundations](https://en.wikipedia.org/wiki/Univalent_foundations))


Correct me if I'm wrong, but in a model $M$ of ZF each element $x$ of $M$ should produce a directed-graph-with-a-marked-sink $G\_x$ having $x$ as marked sink, as follows: to $\varnothing$, i. e. the element with no $y$ satisfying $y\in\varnothing$, assign the graph with the single node $\varnothing$ which is marked, and no arrows. If the graphs $G\_y$ for each $y\in x$ are known, then let $G\_x$ be the disjoint union of all $G\_y$, one more node $x$, and new arrows $y\to x$ for each $y$, with $x$ marked.


Something like univalence would tell us that if there is an isomorphism between $G\_x$ and $G\_{x'}$ under which isomorphism $x$ and $x'$ correspond to each other, then it must be the case that $x=x'$.


Does every model of ZF satisfy this? If yes, is it trivial? If no, are there some additional axioms known that would ensure it?


On the other side, does this construction allow to construct a model of ZF from every univalent universe? If yes, is it trivial? If no, are there some additional axioms known that would ensure it?


Last question - are these matters addressed somewhere? Where can I read about it?



What do UF and ZF do to each other?
This is a standard way of building a model of "material" / membership-based set theory (such as ZFC) from a "structural" / categorical set theory (such as ETCS or the sets in HoTT/UF). In the context of comparing membership-based set theories to category theory and topos theory, it goes back at least to the work of Mitchell, Cole, and Osius in the 70s. There are various different versions of it that use rigid trees (which I think is what you describe) or extensional graphs (a quotient of the tree). A more recent sketch of one using trees can be found in Mac Lane and Moerdijk's *Sheaves in Geometry and Logic*. I recently wrote a [detailed exposition](https://arxiv.org/abs/1808.05204v2) [1] of the extensional-graph version that compares the strength of various axioms on both sides of the translation. The construction in the HoTT Book that Andrej mentioned was inspired by these older versions, and I believe is essentially equivalent, though it is formulated in terms of an inductive construction of the entire universe of sets (related is Joyal-Moerdijk's book *Algebraic set theory*, LMS Lecture Note Series **220** (1995) doi:[10.1017/CBO9780511752483](https://doi.org/10.1017/CBO9780511752483)).


In particular, if you start from a model of ZFC, take its category of sets, then rebuild a model of ZFC, you get something isomorphic to the model you started from (because of Mostowski's collapsing principle, as mentioned in the comments). Thus, every model of ZFC can be obtained in this way. (However, for weaker set theories less can be said.)


[1] *Comparing material and structural set theories*, Annals of Pure and Applied Logic **170** Issue 4 (2019) 465–504, doi:[10.1016/j.apal.2018.11.002](https://doi.org/10.1016/j.apal.2018.11.002), arXiv:[1808.05204](https://arxiv.org/abs/1808.05204)


