Jun 30, 2026
A notation for computing with types.
Types are sets with operations that determine the type. For example, the set of integers defines commutative and associative addition and multiplication that satisfy the distributive law, and have an additive identity 0 and multiplicative identity 1.
We assume the reader is familiar with basic operations involving sets. Given sets A and B the union {A\cup B = \{c\mid c\in A\text{ or }c\in B\}}, intersection A\cap B = {\{c\mid c\in A\text{ and }c\in B\}}, product {A\times B = \{(a,b)\mid a\in A, b\in B}, and exponential {B^A = \{f\colon A\to B\}} consisting of all functions from A to B.
Exercise. Show if A and B are finite then the number of elements in the exponetial {\#B^A = \#B^{\# A}}.
Functions are typically thought of as an algorithm for taking an element a\in A and producing an element f(a)\in B. The graph of a function from A to B is \{(a,b)\mid f(a) = b\}\subseteq A\times B. If A is finite then this is a map, dictionary, or set of key-value pairs. If A is infinite the graph hides the algorithm for computing f(a) given a\in A. Suppose an oracle could tell you whether or not a given pair (a,b) belongs to the graph, or even tell you b = f(a) given a\in A. There is no known way to convert this to an algorithmic formula for f.
Injective, surjective, bijective.
Two sets a equal if they have the same elements. Two sets are equivalent if there is a bijection from one to the other.
Exercise. (reflexive) Show every set A is equivalent to A.
Exercise. (symmetric) Show if A is equivalent to B then B is equivalent to A.
Exercise. (transitive) Show if A is equivalent to B and B is equivalent to C then A is equivalent to C.
A relation is a subset R\subseteq A\times B. We write aRb for {(a,b)\in R}. Define the left coset {Rb = \{a\in A\mid aRb\}\subseteq A} for b\in B and the right coset {aR = \{b\in B\mid aRb\}\subseteq B} for a\in A. The domain of a relation is {\operatorname{dom}R = RB = \{Rb\mid b\in B\}\subseteq A}. The codomain of a relation is {\operatorname{cod}R = AR = \{aR\mid a\in A\}\subseteq B}.
Exercise. Show \operatorname{dom}R = \cup_{b\in B}Rb and \operatorname{cod}R = \cup_{a\in A} aR.
Exercise. Show R is a function if and only if \operatorname{dom}R = A and aR has exactly one element for {a\in A}.
A partial function drops the requirement {\operatorname{dom}f = A}. Every partial function can be turned into a function by selecting an element \bot\not\in B and defining f(a) = \bot for a\not\in\operatorname{dom}f. Partial functions are quite common. For instance f\colon\boldsymbol{{R}}\to\boldsymbol{{R}} by f(x) = 1/x is not defined at x = 0.
Given relations R\subseteq A\times B and S\subseteq B\times C their composition {SR = \{(a,c)\mid aRb\text{ and }bRc\text{ for some }b\in B\}}.
This is closely related to the join operation in relational databases which provides (a,b,c).
Exercise. Show if R\subseteq A\times B, S\subseteq B\times C, and T\subseteq C\times D then $T(RS) = (TR)S.
This shows we can write TRS unambiguously.
Given a set A define the diagonal 1_A = \{(a,a)\mid a\in A\}\subseteq A\times A.
Exercise Show if R\subseteq A\times B then R1_A = R = 1_BR.
This shows every relation has a left and a right identity relation.
The transpose of a relation R\subseteq A\times B is {R' = \{(b,a)\mid aRb\}\subseteq B\times A}
Exercise. Show (SR)' = R'S' if R\subseteq A\times B and S\subseteq B\times C.
Relations on R = A\times A are classified by various properties. A relation is reflexive if aRa for all a\in A.
Exercise. Show R is reflexive if and only if 1_A\subseteq R.
We can make any relation reflexive by taking its union with 1_A.
A relation is symmetric if aRb implies bRa for a,b\in A.
Exercise. Show R is symmetric if and only if R = R'.
We can make any relation symmetric by taking the union with its transpose.
A relation is transitive if aRb and bRc imply aRc.
Exercise. Show R is transitive if and only if RR = R^2\subseteq R.
We can make any relation transitive by taking the union of all powers of R. Define R^+ = \cup_{n > 0} R^n.
Exercise. Show R^+ is transitive.
An equivalence relation is reflexive, symmetric, and transitive.
R+ cup R+’ is still transitive.
They provide a weaker but more powerful abstraction than equality. Equality is also an equivalence relation so it is stronger, but equivalence relations are more powerful because they provide an abstraction of equality useful for simplifying mathematics.
A prime example comes from set theory. Two sets are equal if and only if they have the same elements. Two sets are equivalent if and only if they have the same number of elements. The number 3 is a succinct way of discussing all 3 element sets.
The set diagonal 1_A represents equality. An equivalence relation fattens the skinny diagonal to blocks along the diagonal.
If \sigma\colon I\to J we can define f^\sigma\colon X^J\to X^I by (f^\sigma g)(i) = g(\sigma(i)).