Homotopy Type Theory ZF > history (Rev #1)

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

Revision on May 19, 2022 at 17:20:05 by Anonymous?. See the history of this page for a list of all contributions to it.