\[ \require{mathtools} \let\DeclarePairedDelimiter\DeclarePairedDelimiters % MathJax typo %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % symbol %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % sets \newcommand{\N}{\mathbb{N}} % natural numbers \newcommand{\Z}{\mathbb{Z}} % integers \newcommand{\Q}{\mathbb{Q}} % rational numbers \newcommand{\R}{\mathbb{R}} % real numbers \newcommand{\C}{\mathbb{C}} % complex numbers % category \newcommand{\catf}[1]{{\mathbf{#1}}} \newcommand{\cA}{\catf{A}} \newcommand{\cB}{\catf{B}} \newcommand{\cC}{\catf{C}} \newcommand{\cD}{\catf{D}} \newcommand{\cE}{\catf{E}} \newcommand{\cF}{\catf{F}} \newcommand{\cG}{\catf{G}} \newcommand{\cH}{\catf{H}} \newcommand{\cI}{\catf{I}} \newcommand{\cJ}{\catf{J}} \newcommand{\cK}{\catf{K}} \newcommand{\cL}{\catf{L}} \newcommand{\cM}{\catf{M}} \newcommand{\cN}{\catf{N}} \newcommand{\cO}{\catf{O}} \newcommand{\cP}{\catf{P}} \newcommand{\cQ}{\catf{Q}} \newcommand{\cR}{\catf{R}} \newcommand{\cS}{\catf{S}} \newcommand{\cT}{\catf{T}} \newcommand{\cU}{\catf{U}} \newcommand{\cV}{\catf{V}} \newcommand{\cW}{\catf{W}} \newcommand{\cX}{\catf{X}} \newcommand{\cY}{\catf{Y}} \newcommand{\cZ}{\catf{Z}} \newcommand{\cZero}{\catf{0}} \newcommand{\cOne}{\catf{1}} \newcommand{\cTwo}{\catf{2}} \newcommand{\cArr}{\catf{Arr}} % arrow \newcommand{\cPSh}{\catf{PSh}} % presheaf \newcommand{\cCone}{\catf{Cone}} % cone \newcommand{\cCocone}{\catf{Cocone}} % cocone \newcommand{\cFin}{\catf{Fin}} % finite prefix \newcommand{\cSet}{\catf{Set}} % functions \newcommand{\cRel}{\catf{Rel}} % relations \newcommand{\cPos}{\catf{Pos}} % posets \newcommand{\cMon}{\catf{Mon}} % monoids \newcommand{\cCMon}{\catf{CMon}} % commutative monoids \newcommand{\cGrp}{\catf{Grp}} % groups \newcommand{\cAb}{\catf{Ab}} % abelian groups \newcommand{\cCat}{\catf{Cat}} % categories \newcommand{\cGrpd}{\catf{Grpd}} % groupoids \newcommand{\cVect}{\catf{Vect}} % vector spaces \newcommand{\cMat}{\catf{Mat}} % matrices \newcommand{\cTop}{\catf{Top}} % topological spaces and continuous maps \newcommand{\cMet}{\catf{Met}} % metric spaces and metric maps \newcommand{\cMeas}{\catf{Meas}} % measurable spaces and measurable functions \newcommand{\cStoch}{\catf{Stoch}} % measurable spaces and stochastic maps \newcommand{\cProb}{\catf{Prob}} % probability measures and measure-preserving functions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % supscript %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\op}{^\mathrm{op}} \newcommand{\inv}{^{-1}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % function %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \DeclareMathOperator{\lcm}{lcm} \DeclareMathOperator{\logsumexp}{log-sum-exp} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % arrow %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % morphism \newcommand{\xto}{\xrightarrow} % -> \newcommand{\xot}{\xleftarrow} % <- \newcommand{\toot}{\rightleftarrows} % <=> \newcommand{\xtoot}[2]{\xrightleftharpoons[#2]{#1}} \newcommand{\iso}{\cong} % ~= \newcommand{\klto}{\rightsquigarrow} % ~> \newcommand{\mono}{\rightarrowtail} % >-> \newcommand{\epi}{\twoheadrightarrow} % ->> \newcommand{\ihom}{\multimap} % -o % category \newcommand{\incl}{\hookrightarrow} \newcommand{\adjto}[2]{\overset{{}\xto[]{#1}{}}{\underset{{}\xot[#2]{}{}}{\bot}}} % functor \newcommand{\nat}{\Rightarrow} % => \newcommand{\xnat}{\xRightarrow} % => \newcommand{\comma}{\downarrow} \newcommand{\adj}{\dashv} % -| %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % delimiter %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \DeclarePairedDelimiter{\parens}{(}{)} % parentheses ( ) \DeclarePairedDelimiter{\bracks}{[}{]} % brackets [ ] \DeclarePairedDelimiter{\braces}{\{}{\}} % braces { } \DeclarePairedDelimiter{\angles}{\langle}{\rangle} % angles \DeclarePairedDelimiter{\floor}{\lfloor}{\rfloor} \DeclarePairedDelimiter{\ceil}{\lceil}{\rceil} \newcommand{\set}{\braces} \newcommand{\singleton}{{\set{*}}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % operator %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\compL}{\mathbin{\circ}} \newcommand{\compR}{\mathbin{;}} \newcommand{\Kl}{\mathrm{Kl}} \DeclareMathOperator{\Obj}{Obj} \DeclareMathOperator{\Hom}{Hom} \DeclareMathOperator{\Sub}{Sub} \DeclareMathOperator{\Eq}{Eq} \DeclareMathOperator{\Coeq}{Coeq} \DeclareMathOperator{\Pull}{Pull} \DeclareMathOperator{\Push}{Push} \DeclareMathOperator{\Lan}{Lan} \DeclareMathOperator{\Ran}{Ran} \DeclareMathOperator{\Lift}{Lift} \DeclareMathOperator{\Rift}{Rift} \DeclareMathOperator{\id}{id} \DeclareMathOperator{\act}{act} \DeclareMathOperator{\colim}{colim} % exponential \DeclareMathOperator{\partf}{partial} \DeclareMathOperator{\curry}{curry} % natural number \DeclareMathOperator{\zero}{zero} \DeclareMathOperator{\successor}{succ} % list \DeclareMathOperator{\nil}{nil} \DeclareMathOperator{\cons}{cons} \newcommand{\concat}{\mathbin{{+}\mspace{-8mu}{+}}} % fold \DeclareMathOperator{\fold}{fold} \DeclareMathOperator{\map}{map} \DeclareMathOperator{\filter}{filter} % bool \DeclareMathOperator{\cond}{cond} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % order %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\meet}{\wedge} \newcommand{\join}{\vee} \newcommand{\bigmeet}{\bigwedge} \newcommand{\bigjoin}{\bigvee} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % logic %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\lfal}{\bot} \newcommand{\ltru}{\top} \newcommand{\lcon}{\wedge} \newcommand{\lncon}{\uparrow} \newcommand{\ldis}{\vee} \newcommand{\lndis}{\downarrow} \newcommand{\limp}{\rightarrow} \newcommand{\lnimp}{\nrightarrow} \newcommand{\lcim}{\leftarrow} \newcommand{\lncim}{\nleftarrow} \newcommand{\leqv}{\leftrightarrow} \newcommand{\lneqv}{\nleftrightarrow} \newcommand{\lproves}{\vdash} % |- \newcommand{\lmodels}{\vDash} % |= \newcommand{\lnproves}{\nvdash} % |/- \newcommand{\lnmodels}{\nvDash} % |/= \]
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\)