A.1 Relations

Definition A.1

Let \( R : \sigma \to \tau \to \mathsf{Prop}\). We define

the image of \( R \) to be the set \( \operatorname {\mathsf{im}}R = \{ y : \tau \mid \exists x : \sigma ,\, x \mathrel {R} y \} \);
the coimage of \( R \) to be the set \( \operatorname {\mathsf{coim}}R = \{ x : \sigma \mid \exists y : \tau ,\, x \mathrel {R} y \} \) (note that this is not the same as the category-theoretic coimage of a morphism);
the field of \( R \) to be the set \( \operatorname {\mathsf{field}}R = \operatorname {\mathsf{coim}}R \cup \operatorname {\mathsf{im}}R \);
the image of \( R \) on \( s : \operatorname {\mathsf{Set}}\sigma \) to be the set \( \operatorname {\mathsf{im}}R|_s = \{ y : \tau \mid \exists x \in s,\, x \mathrel {R} y \} \);
the coimage of \( R \) on \( t : \operatorname {\mathsf{Set}}\tau \) to be the set \( \operatorname {\mathsf{coim}}R|_t = \{ x : \sigma \mid \exists y \in t,\, x \mathrel {R} y \} \);
the converse of \( R \) to be the relation \( R^{-1} : \tau \to \sigma \to \mathsf{Prop}\) such that \( y \mathrel {R^{-1}} x \) if and only if \( x \mathrel {R} y \);
if \( S : \tau \to \upsilon \to \mathsf{Prop}\), the composition \( S \circ R : \sigma \to \upsilon \to \mathsf{Prop}\) is the relation given by \( x \mathrel {(S\circ R)} z \) if and only if there is \( y : \tau \) such that \( x \mathrel {R} y \) and \( y \mathrel {S} z \);
for a natural number \( n \), the \( n \)th power of \( R : \tau \to \tau \to \mathsf{Prop}\) is defined by \( R^{n+1} = R \circ R^n \) and \( R^0 \) is the identity relation on \( \operatorname {\mathsf{coim}}R \);
for an integer \( n \), the \( n \)th power of \( R : \tau \to \tau \to \mathsf{Prop}\) is defined by \( R^{(n : \mathbb Z)} = R^n \) and \( R^{-(n : \mathbb Z)} = (R^n)^{-1} \) for \( n : \mathbb N \). ¹

We say that \( R \) is

injective, if \( s_1 \mathrel {R} t, s_2 \mathrel {R} t \) imply \( s_1 = s_2 \);
surjective, if for every \( t : \tau \), there is some \( s : \sigma \) such that \( s \mathrel {R} t \);
coinjective, if \( s \mathrel {R} t_1, s \mathrel {R} t_2 \) imply \( t_1 = t_2 \);
cosurjective, if for every \( s : \sigma \), there is some \( t : \tau \) such that \( s \mathrel {R} t \);
functional, if \( R \) is coinjective and cosurjective, or equivalently, for every \( s : \sigma \) there is exactly one \( t : \tau \) such that \( s \mathrel {R} t \);
cofunctional, if \( R \) is injective and surjective, or equivalently, for every \( t : \tau \) there is exactly one \( s : \sigma \) such that \( s \mathrel {R} t \);
one-to-one, if \( R \) is injective and coinjective;
bijective, if \( R \) is functional and cofunctional;
permutative, if \( R : \tau \to \tau \to \mathsf{Prop}\) is one-to-one and has equal image and coimage.

We also define the graph of a function \( f : \sigma \to \tau \) to be the functional relation \( R : \sigma \to \tau \to \mathsf{Prop}\) given by \( (x, y) \in R \) if and only if \( f(x) = y \). Most of these definitions are from https://www.kylem.net/math/relations.html, and most of these are in mathlib under Mathlib.Logic.Relator.

Proposition A.2

\( R : \tau \to \tau \to \mathsf{Prop}\) is permutative if and only if it is one-to-one and for all \( x : \tau \), there exists \( y \) such that \( x \mathrel {R} y \) if and only if there exists \( y \) such that \( y \mathrel {R} x \).
If \( R, S : \tau \to \tau \to \mathsf{Prop}\) are permutative and \( \operatorname {\mathsf{coim}}R \cap \operatorname {\mathsf{coim}}S = \emptyset \), then \( R \sqcup S \) is permutative and has coimage \( \operatorname {\mathsf{coim}}R \cup \operatorname {\mathsf{coim}}S \).
If \( R, S : \tau \to \tau \to \mathsf{Prop}\) are permutative and \( \operatorname {\mathsf{coim}}R = \operatorname {\mathsf{coim}}S \), then \( R \circ S \) is permutative and has coimage equal to that of \( R \) and \( S \).
If \( R \) is permutative, then \( \operatorname {\mathsf{coim}}R^n = \operatorname {\mathsf{coim}}R = \operatorname {\mathsf{im}}R = \operatorname {\mathsf{im}}R^n \) for any natural number or integer \( n \).
If \( R \) is permutative and \( s_1, s_2 \subseteq \operatorname {\mathsf{coim}}R \), then the image of \( R \) on \( s_1 \) is equal to \( s_2 \) if and only if the coimage of \( R \) on \( s_2 \) is equal to \( s_1 \).

Definition A.3

✓

Let \( s : \operatorname {\mathsf{Set}}\tau \). An orbit restriction for \( s \) (over some type \( \sigma \)) consists of a set \( t : \operatorname {\mathsf{Set}}\tau \) disjoint from \( s \), a function \( f : \tau \to \sigma \), and a permutation \( \pi : \sigma \simeq \sigma \), such that for each \( u : \sigma \), the set \( t \cap f^{-1}(u) \) has cardinality at least \( \max (\aleph _0, \# s, \# d) \).

An orbit restriction encapsulates information about how orbits should be completed.

\( t \) is the sandbox, the set inside which all added items must reside.
\( f \) is a categorisation function, placing each value \( x : \tau \) into a category \( u : \sigma \).
\( \pi \) is a permutation of categories. If \( x \) has category \( u \), then anything that \( x \) is mapped to should have category \( \pi (u) \).

Proposition A.4 completing restricted orbits

✓

Let \( R : \tau \to \tau \to \mathsf{Prop}\) be a one-to-one relation, and let \( (t, f, \pi ) \) be an orbit restriction for \( \operatorname {\mathsf{field}}R \) over some type \( \sigma \). Then there is a permutative relation \( T \) such that

\( \operatorname {\mathsf{coim}}T \subseteq \operatorname {\mathsf{field}}R \cup t \);
\( \# \operatorname {\mathsf{coim}}T \leq \max (\aleph _0, \# \operatorname {\mathsf{coim}}R) \);
\( R \leq T \); and
if \( (x, y) \in T \), then \( (x, y) \in R \vee f(y) = \pi (f(x)) \).

Proof ▶

For each \( u : \sigma \), define an injection \( i_u : \operatorname {\mathsf{field}}R \times \mathbb N \to \tau \) where \( \operatorname {\mathsf{im}}i_u \subseteq t \cap f^{-1}(u) \). Define a relation \( S \) on \( \tau \) by the following constructors.

\begin{align*} \forall x \in \operatorname {\mathsf{coim}}R \setminus \operatorname {\mathsf{im}}R,\, & (i_{\pi ^{-1}(f(x))}(x, 0), x) \in S \\ \forall n : \mathbb N,\, \forall x \in \operatorname {\mathsf{coim}}R \setminus \operatorname {\mathsf{im}}R,\, & (i_{\pi ^{-n-2}(x)}(x, n+1), i_{\pi ^{-n-1}(x)}(x, n)) \in S \\ \forall x \in \operatorname {\mathsf{im}}R \setminus \operatorname {\mathsf{coim}}R,\, & (x, i_{\pi (f(x))}(x, 0)) \in S \\ \forall n : \mathbb N,\, \forall x \in \operatorname {\mathsf{im}}R \setminus \operatorname {\mathsf{coim}}R,\, & (i_{\pi ^{n+1}(f(x))}(x, n), i_{\pi ^{n+2}(f(x))}(x, n+1)) \in S \end{align*}

Note that \( (x, y) \in S \) implies \( f(y) = \pi (f(x)) \). Finally, as \( R \sqcup S \) is permutative, it satisfies the required conclusion.

Proposition A.5 completing orbits

✓

Let \( R : \tau \to \tau \to \mathsf{Prop}\) be a one-to-one relation. Let \( s : \operatorname {\mathsf{Set}}\tau \) be an infinite set such that \( \# \operatorname {\mathsf{field}}R \leq \# s \), and \( \operatorname {\mathsf{field}}R \) and \( s \) are disjoint. Then there is a permutative relation \( S \) such that \( R \leq S \) and \( \operatorname {\mathsf{coim}}S \subseteq \operatorname {\mathsf{field}}R \cup s \).

Proof ▶

Define the orbit restriction \( (s, f, \pi ) \) for \( \operatorname {\mathsf{field}}R \) over \( \mathsf{Unit}\). Note that for this to be defined, we used the inequality

\[ \# s \geq \max (\aleph _0, \# \operatorname {\mathsf{field}}R) \]

Use proposition A.4 to obtain a permutative relation \( T \) extending \( R \) defined on \( \operatorname {\mathsf{field}}R \cup s \).