# 1 Subobject

In a category $$\cC$$, a subobject of an object $$C$$ is a monomorphism $$a: A \mono C$$.

For a category $$\cC$$, the category of subobjects and inclusions $$\Sub_\cC(C)$$ of an object $$C$$ is the full subcategory of the slice category $$\cC \comma C$$ whose objects are monomorphisms.

preorder of subobjects: $$a \leq b := \exists f: A \to B. a = b \compL f$$.

$$\id_C$$ is a terminal object (top) in the subobject category $$\Sub_\cC(C)$$.

## 1.1 Subobject functor

A $$\cC$$-morphism $$f: C' \to C$$ induces a base change functor $$f^*: \cC \comma C \to \cC \comma C'$$ via pullback along $$f$$:

\begin{aligned} \begin{array}{cccc} f^*: & \cC \comma C & \to & \cC \comma C' \\ & A \xto{a} C & \mapsto & \Pull(f, a) \xto{f^*a} C' \\ & A \xto{m} B & \mapsto & \Pull(f, a) \xto{f^*m} \Pull(f, b) \end{array} \end{aligned}

slice functor $$\cC \comma (-): \cC\op \to \cCat$$:

\begin{aligned} \begin{array}{cccc} \cC \comma (-): & \cC\op & \to & \cCat \\ & C & \mapsto & \cC \comma C \\ & C \xto{f\op} C' & \mapsto & f^*: \cC \comma C \to \cC \comma C' \end{array} \end{aligned}

subobject functor $$\Sub_\cC: \cC\op \to \cCat$$:

\begin{aligned} \begin{array}{cccc} \Sub_\cC: & \cC\op & \to & \cCat \\ & C & \mapsto & \Sub_\cC(C) \\ & C \xto{f\op} C' & \mapsto & f^*: \Sub_\cC(C) \to \Sub_\cC(C') \end{array} \end{aligned}

For a category $$\cC$$, the category of subobjects and pullbacks is the subcategory of the arrow category $$\cArr(\cC)$$ whose objects are monomorphisms and morphisms are pullbacks.

## 1.2 Subobject classifier

In a finitely complete category $$\cC$$, a subobject classifier is a terminal object $$\ltru: 1 \mono \Omega$$ of the category of subobjects and pullbacks.

The domain of a subobject classifier $$\ltru: 1 \mono \Omega$$ is a terminal object $$1$$ in $$\cC$$.

For any object $$C$$ in $$\cC$$, the identity morphism $$\id_C$$ is a monomorphism. If $$t: T \mono S$$ is a subobject classifier, then for any object $$C$$, there exists a morphism $$e_C: C \to T$$, which is unique because it forms a pullback with $$\id_C$$. Thus, $$T$$ is a terminal object in $$\cC$$.

The composition $$\ltru \compL e_C$$ is abbreviated as $$\ltru_C$$.

In a finitely complete category $$\cC$$, a subobject classifier is a universal subobject $$\ltru: 1 \mono \Omega$$: for every subobject $$a: A \mono C$$, there exists a unique morphism $$\chi_a: C \to \Omega$$ such that $$a$$ is a pullback of $$\ltru$$ along $$\chi_a$$.

$$\chi_a$$ is called the classifying morphism of the subobject $$a$$.

An elementary topos is a finitely complete and cartesian closed category with a subobject classifier.

In an elementary topos, all monomorphisms are regular: $$a: A \mono C$$ is an equalizer of $$\ltru_C, \chi_a: C \to \Omega$$.

\begin{aligned} \begin{array}{cccc} \Hom_\cC(-, \Omega): & \cC\op & \to & \cSet \\ & C & \mapsto & \Hom_\cC(C, \Omega) \\ & C \xto{f\op} C' & \mapsto & \Hom_\cC(f, \Omega): \Hom_\cC(C, \Omega) \xto{(-) \compL f} \Hom_\cC(C', \Omega) \end{array} \end{aligned}

$\Hom_\cC(-, \Omega) \iso \Sub_\cC$

## 1.3 Dependent sum

A $$\cC$$-morphism $$f: C' \to C$$ induces a dependent sum functor $$\Sigma_f: \cC \comma C' \to \cC \comma C$$ via postcomposition with $$f$$:

\begin{aligned} \begin{array}{cccc} \Sigma_f: & \cC \comma C' & \to & \cC \comma C \\ & A \xto{a} C' & \mapsto & A \xto{f \compL a} C \\ & A \xto{m} B & \mapsto & A \xto{m} B \end{array} \end{aligned}

$\Sigma_f \adj f^*$

\begin{aligned} \begin{array}{ccc} \Hom_{\cC \comma C}(\Sigma_f a, b) & \iso & \Hom_{\cC \comma C'}(a, f^*b) \\ m: A \to B & & n: A \to B^* \end{array} \end{aligned}

$f \times_C (-): \cC \comma C \xto{f^*} \cC \comma C' \xto{\Sigma_f} \cC \comma C$

## 1.4 Dependent product

For a $$\cC$$-morphism $$f: C' \to C$$, the dependent product functor $$\Pi_f: \cC \comma C' \to \cC \comma C$$ is the right adjoint functor to $$f^*$$.

$f^* \adj \Pi_f$

$\Hom_{\cC \comma C'}(f^*a, b) \iso \Hom_{\cC \comma C}(a, \Pi_f b)$

$[f, -]_C: \cC \comma C \xto{f^*} \cC \comma C' \xto{\Pi_f} \cC \comma C$

# 2 Connective

## 2.1 Conjunction

The conjunction $$\lcon: \Omega \times \Omega \to \Omega$$ is the classifying morphism of the paring $$\angles{\ltru, \ltru}: 1 \mono \Omega \times \Omega$$.

The conjunction $$\lcon \compL \angles{\chi_1, \chi_2}$$ is also written as $$\chi_1 \lcon \chi_2$$.

If $$\cC$$ is finitely complete, $$\Sub_\cC(C)$$ is a meet-semilattice.

Let $$a_1: A_1 \mono C$$, $$a_2: A_2 \mono C$$, and $$a: A \mono C$$ be the subobjects of $$C$$ classified by $$\chi_1$$, $$\chi_2$$, and $$\chi_1 \lcon \chi_2: C \to \Omega$$.

\begin{aligned} & b \leq_C a \\ \equiv& \lcon \compL \angles{\chi_1, \chi_2} \compL b = \ltru_B \\ \equiv& \lcon \compL \angles{\chi_1 \compL b, \chi_2 \compL b} = \ltru_B \\ \equiv& \angles{\chi_1 \compL b, \chi_2 \compL b} = \angles{\ltru, \ltru} \compL e_B \\ \equiv& \angles{\chi_1 \compL b, \chi_2 \compL b} = \angles{\ltru_B, \ltru_B} \\ \equiv& \chi_1 \compL b = \ltru_B, \chi_2 \compL b = \ltru_B \\ \equiv& b \leq_C a_1, b \leq_C a_2 \end{aligned}

## 2.2 Equality

The equality predicate $$=_C: C \times C \to \Omega$$ is the classifying morphism of the diagonal $$\Delta_C: C \to C \times C$$.

equality $$\leqv: \Omega \times \Omega \to \Omega := =_\Omega$$

## 2.3 Implication

implication $$\limp: \Omega \times \Omega \to \Omega := \leqv \compL \angles{\lcon, p_1}$$

# 3 Power object

In a category $$\cC$$, a relation over objects $$A$$ and $$B$$ is a monomorphism $$r: R \mono A \times B$$.

In a finitely complete category $$\cC$$, a power object of an object $$A$$ is a universal relation $$\epsilon: \in_A \mono A \times PA$$: for every relation $$r: R \mono A \times B$$, there exists a unique morphism $$\chi_r: B \to PA$$ such that $$r$$ is a pullback of $$\epsilon$$ along $$\id_A \times \chi_r$$.

$$\chi_r$$ is called the classifying morphism of the relation $$r$$.

$P1 \iso \Omega$

$PA \iso \Omega^A$

$\Sub_\cC(A \times -) \iso \Hom_\cC(-, \Omega^A) \iso \Hom_\cC(A \times -, \Omega)$

## 3.1 Power object functor

contravariant power object functor $$P: \cC\op \to \cC$$:

\begin{aligned} \begin{array}{cccc} P: & \cC\op & \to & \cC \\ & A & \mapsto & PA \\ & B \xto{f\op} A & \mapsto & PB \xto{f\inv} PA \end{array} \end{aligned}

inverse image

covariant power object functor $$P: \cC \to \cC$$:

\begin{aligned} \begin{array}{cccc} P: & \cC & \to & \cC \\ & A & \mapsto & PA \\ & A \xto{f} B & \mapsto & PA \xto{Pf} PB \end{array} \end{aligned}

direct image

# 4 Quantifier

## 4.1 Universal quantifier

$$\forall_A: \Omega^A \to \Omega$$

$$\Hom_\cC(-, \forall_A): \Hom(-, \Omega^A) \iso \Hom(A \times -, \Omega) \nat \Hom(-, \Omega)$$

$$\forall_A: \Sub_\cC(A \times -) \nat \Sub_\cC$$

$$\forall_A: \Sub_\cC(A \times B) \to \Sub_\cC(B)$$ right adjoint to $${p_B}^*: \Sub_\cC(B) \to \Sub_\cC(A \times B)$$

$$\Pi_{p_B}: \cC \comma (A \times B) \to \cC \comma B$$

## 4.2 Existential quantifier

$$\exists_A: \Omega^A \to \Omega$$

$$\Hom_\cC(-, \exists_A): \Hom(-, \Omega^A) \iso \Hom(A \times -, \Omega) \nat \Hom(-, \Omega)$$

$$\exists_A: \Sub_\cC(A \times -) \nat \Sub_\cC$$

$$\exists_A: \Sub_\cC(A \times B) \to \Sub_\cC(B)$$ left adjoint to $${p_B}^*: \Sub_\cC(B) \to \Sub_\cC(A \times B)$$

$$\Sigma_{p_B}: \cC \comma (A \times B) \to \cC \comma B$$