work in progress... ## Definition ## Given a universe $\mathcal{U}$ with [[excluded middle]], a model of Zermelo-Frankl set theory is a [[set]] $V$ with * a binary relation $(-)\in(-):V \times V \to Prop_\mathcal{U}$ * a dependent function $$\alpha:\prod_{a:V} \prod_{b:V} \left(\prod_{c:V} \prod_{d:V} \mathcal{T}_\mathcal{U}(c \in a) \times \mathcal{T}_\mathcal{U}(d \in b) \times (c = d)\right) \to (a = b)$$ * a term $\emptyset:V$ with a dependent function $$\beta:\prod_{a:V} \mathcal{T}_\mathcal{U}(a \in \emptyset) \to \mathbb{0}$$ * a function $\{(-),(-)\}:V \times V \to V$ with a dependent function $$\gamma: \prod_{a:V} \prod_{b:V} \prod_{c:V} \left[(c = a) + (c = b)\right] \to \mathcal{T}_\mathcal{U}(c \in \{a, b\})$$ * a function $\bigcup:V \to V$ with a dependent function $$\delta: \prod_{a:V} \prod_{b:V} \mathcal{T}_\mathcal{U}(b \in a) \to \mathcal{T}_\mathcal{U}\left(b \in \bigcup a\right)$$ * a function $\{(-) \vert (-)\}:V \times (V \to Prop_\mathcal{U}) \to V$ with a dependent function $$\epsilon: \prod_{a:V} \prod_{P:V \to Prop_\mathcal{U}} \prod_{b:V} ((b \in \{a \vert P\}) \to ((b \in a) \times \mathcal{T}_\mathcal{U}(P(b)))) \times (((b \in a) \times \mathcal{T}_\mathcal{U}(P(b))) \to (b \in \{a \vert P\}))$$ * a function $\mathcal{P}:V \to V$ with a dependent function ## See also ## * [[SEAR]]