7.2 Tangled type theory

Definition 7.6 tangled membership

We define the membership relation \( \in ^\alpha _\beta : \mathsf{TSet}_\beta \to \mathsf{TSet}_\alpha \to \mathsf{Prop}\) by

\[ x \in ^\alpha _\beta y \leftrightarrow U_\beta (x) \in U_\alpha (y)(\beta ) \]

Extensionality holds at all proper type indices by proposition 3.8. Also, for every \( \alpha \)-allowable \( \rho \), we have

\[ \rho _\beta (x) \in ^\alpha _\beta \rho (y) \leftrightarrow x \in ^\alpha _\beta y \]

Definition 7.7 symmetric

Let \( \beta {\lt} \alpha \) be proper type indices. A set \( s : \mathsf{TSet}_\beta \) is called \( \alpha \)-symmetric if there is some \( \alpha \)-support \( S \) such that if \( \rho \) is an \( \alpha \)-allowable permutation that fixes \( S \), then \( \rho \) fixes \( s \) setwise. Note that it suffices to prove that for all \( \rho \) that fix \( S \), \( s \subseteq \rho [s] \) (or alternatively, \( \rho [s] \subseteq s \)). Every small set is symmetric, since a support can be obtained by raising the types of chosen supports for elements of the set and then collating the results.

Proposition 7.8

Let \( \beta {\lt} \alpha \) be proper type indices. Let \( s : \mathsf{TSet}_\beta \) be \( \alpha \)-symmetric. Then there is \( x : \mathsf{TSet}_\alpha \) such that

\[ \forall y : \mathsf{TSet}_\beta ,\, y \in _\beta ^\alpha x \leftrightarrow y \in s \]

Moreover, every \( x : \mathsf{TSet}_\alpha \) arises in this way; this is an induction principle for \( \mathsf{TSet}_\alpha \).

Proof ▶

If \( s \) is empty, the result follows directly from the definition of \( \mathsf{TSet}_\alpha \). Otherwise, consider the code \( (\beta , s) \). By definition 3.7, there is exactly one code \( d \) such that \( c \looparrowright (\beta , s) \). Then \( c \) is a new t-set at level \( \alpha \), so is naturally an inhabitant of \( \mathsf{TSet}_\alpha \). Using the membership relation from proposition 3.8, the type-\( \beta \) members of \( c \) are precisely \( s \), as required.

For the induction principle, we apply the above construction to the set

\[ s = \{ y \mid y \in ^\alpha _\beta x \} \]

and use extensionality to deduce that the object constructed is exactly \( x \).

Proposition 7.9 unions of singletons

Let \( \gamma {\lt} \beta {\lt} \alpha \) be proper type indices. Let \( s : \operatorname {\mathsf{Set}}\mathsf{TSet}_\gamma \) be such that \( \operatorname {\mathsf{singleton}}_\beta [s] \) is \( \alpha \)-symmetric. Then \( s \) is \( \beta \)-symmetric.

Proof ▶

Let \( S \) be an \( \alpha \)-support for \( \operatorname {\mathsf{singleton}}_\beta [s] \), which without loss of generality is strong. We claim that the \( \alpha \)-symmetry of \( s \) is witnessed by \( S_\beta \). Let \( \rho \) be a \( \beta \)-allowable permutation such that \( \rho (S_\beta ) = S_\beta \). Let \( x \in s \); it suffices by substituting \( \rho ^{-1} \) to prove that \( \rho _\gamma (x) \in s \). As \( x : \mathsf{TSet}_\gamma \), there is a \( \gamma \)-support \( T \) for \( x \). By proposition 7.5, there is an \( \alpha \)-allowable permutation \( \rho ' \) such that

\[ \rho '(S) = S;\quad (\rho '_\beta )_\gamma (T) = \rho _\gamma (T) \]

Thus,

\[ \rho '_\beta (\operatorname {\mathsf{singleton}}_\beta [s]) = \operatorname {\mathsf{singleton}}_\beta [s];\quad (\rho '_\beta )_\gamma (x) = \rho _\gamma (x) \]

We thus have

\begin{align*} x & \in s \\ \operatorname {\mathsf{singleton}}_\beta (x) & \in \operatorname {\mathsf{singleton}}_\beta [s] \\ \rho ’_\beta (\operatorname {\mathsf{singleton}}_\beta (x)) & \in \rho ’_\beta (\operatorname {\mathsf{singleton}}_\beta [s]) \\ \rho ’_\beta (\operatorname {\mathsf{singleton}}_\beta (x)) & \in \operatorname {\mathsf{singleton}}_\beta [s] \\ \operatorname {\mathsf{singleton}}_\beta ((\rho ’_\beta )_\gamma (x)) & \in \operatorname {\mathsf{singleton}}_\beta [s] \\ \operatorname {\mathsf{singleton}}_\beta (\rho _\gamma (x)) & \in \operatorname {\mathsf{singleton}}_\beta [s] \\ \rho _\gamma (x) & \in s \\ \end{align*}

Theorem 7.10 consistency of tangled type theory

Let \( \{ x \} _\beta \) be an abbreviation for \( \operatorname {\mathsf{singleton}}_\beta (x) \), and let \( \langle x, y \rangle _{\gamma ,\beta } \) be an abbreviation for \( \{ \{ x \} _\gamma , \{ x, y \} _\gamma \} _\beta \). Then, the following axioms hold for our model \( \mathsf{TSet}\) at all sequences of proper type indices \( \zeta {\lt} \varepsilon {\lt} \delta {\lt} \gamma {\lt} \beta {\lt} \alpha \).

\( - \)	extensionality	\( \forall x^\alpha ,\, \forall y^\alpha ,\, (\forall z^\beta ,\, z \in x \leftrightarrow z \in y) \to x = y \)
P1(a)	intersection	\( \forall x^\alpha y^\alpha ,\, \exists z^\alpha ,\, \forall w^\beta ,\, w \in z \leftrightarrow (w \in x \wedge w \in y) \)
P1(b)	complement	\( \forall x^\alpha ,\, \exists z^\alpha ,\, \forall w^\beta ,\, w \in z \leftrightarrow w \notin x \)
\( - \)	singleton	\( \forall x^\beta ,\, \exists y^\alpha ,\, \forall z^\beta ,\, z \in y \leftrightarrow z = x \)
P2	singleton image	\( \forall x^\beta ,\, \exists y^\alpha ,\, \forall z^\varepsilon w^\varepsilon ,\, \langle \{ z \} _\delta , \{ w \} _\delta \rangle _{\gamma ,\beta } \in y \leftrightarrow \langle z, w \rangle _{\delta ,\gamma } \in x \)
P3	insertion two	\( \forall x^\gamma ,\, \exists y^\alpha ,\, \forall z^\zeta w^\zeta t^\zeta ,\, \langle \{ \{ z \} _\varepsilon \} _\delta , \langle w, t \rangle _{\varepsilon , \delta } \rangle _{\gamma ,\beta } \in y \leftrightarrow \langle z, t \rangle _{\varepsilon ,\delta } \in x \)
P4	insertion three	\( \forall x^\gamma ,\, \exists y^\alpha ,\, \forall z^\zeta w^\zeta t^\zeta ,\, \langle \{ \{ z \} _\varepsilon \} _\delta , \langle w, t \rangle _{\varepsilon ,\delta } \rangle _{\gamma ,\beta } \in y \leftrightarrow \langle z, w \rangle _{\varepsilon ,\delta } \in x \)
P5	cross product	\( \forall x^\gamma ,\, \exists y^\alpha ,\, \forall z^\beta ,\, z \in y \leftrightarrow \exists w^\delta t^\delta ,\, z = \langle w, t \rangle _{\gamma ,\beta } \wedge t \in x \)
P6	type lowering	\( \forall x^\alpha ,\, \exists y^\delta ,\, \forall z^\varepsilon ,\, z \in y \leftrightarrow \forall w^\delta ,\, \langle w, \{ z \} _\delta \rangle _{\gamma ,\beta } \in x \)
P7	converse	\( \forall x^\alpha ,\, \exists y^\alpha ,\, \forall z^\delta w^\delta ,\, \langle z, w \rangle _{\gamma ,\beta } \in y \leftrightarrow \langle w, z \rangle _{\gamma ,\beta } \in x \)
P8	cardinal one	\( \exists x^\alpha ,\, \forall y^\beta ,\, y \in x \leftrightarrow \exists z^\gamma ,\, \forall w,\, w \in y \leftrightarrow w = z \)
P9	subset	\( \exists x^\alpha ,\, \forall y^\delta z^\delta ,\, \langle y, z \rangle _{\gamma ,\beta } \in x \leftrightarrow \forall w^\varepsilon ,\, w \in y \to w \in z \)

Proof ▶

The axiom of extensionality was proven in proposition 3.8. All axioms except for the type lowering axiom can be easily proven using proposition 7.8. For type lowering, consider the set

\[ y' = \{ \{ \{ \{ z^\varepsilon \} _\delta \} _\gamma \} _\beta \mid \forall w^\delta ,\, \langle w, \{ z \} _\delta \rangle _{\gamma ,\beta } \in x \} \]

which exists by proposition 7.8, and then apply proposition 7.9 three times.