\[ \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 Exponential object
In a category \(\cC\) with binary products, an exponential object from \(A\) to \(B\) is a universal morphism \((B^A, B^A \times A \xto{\epsilon_A} B)\) from \((-) \times A\) to \(B\).
\[\begin{array}{rlclll} \text{exponential:} & (B^A, B^A \times A \xto{\epsilon_A} B) & \equiv & \forall f: C \times A \to B. & \exists! \hat{f}: C \to B^A. & f = \epsilon_A \compL (\hat{f} \times \id_A). \end{array}\]
- \(\epsilon_A: B^A \times A \to B\) is called evaluation
- \(\hat{f}: C \to B^A\) is called the exponential transpose of \(f: C \times A \to B\)
- \(\bar{g}: C \times A \to B := \epsilon_A \compL (g \times \id_A)\) is the exponential transpose of \(g: C \to B^A\)
\[(-) \times A \adj (-)^A\]
\[\Hom(C \times A, B) \iso \Hom(C, B^A)\]
-- function application
($) :: (a -> b) -> a -> b
-- reverse function application
(&) :: a -> (a -> b) -> bA cartesian closed category has all finite products and exponentials.
In a cartesian closed category, the functor \((-) \times A\) is a left adjoint, which necessarily preserves all colimits, including all coproducts.
\(\Hom(A, B) \iso \Hom(1, B^A) \iso \Hom(0, B^A)\) All objects are isomorphic.
2 Composition
\[A \xto{f} B \xto{g} C \xto{h} D\]
2.1 Composition
\[\compL: C^B \times B^A \to C^A\]
-- function composition
(.) :: (b -> c) -> (a -> b) -> (a -> c)2.2 Postcomposition
\[h^B: C^B \to D^B := h \compL (-)\]
\[\begin{aligned} \begin{array}{cccc} (-)^B: & \cC & \to & \cC \\ & C & \mapsto & C^B \\ & C \xto{h} D & \mapsto & C^B \xto{h^B} D^B \end{array} \end{aligned}\]
2.3 Precomposition
\[C^f: C^B \to C^A := (-) \compL f\]
\[\begin{aligned} \begin{array}{cccc} C^{(-)}: & \cC\op & \to & \cC \\ & B & \mapsto & C^B \\ & B \xto{f\op} A & \mapsto & C^B \xto{C^f} C^A \end{array} \end{aligned}\]
3 Transpose
3.1 Partial application
\[\partf: C^{A \times B} \times A \to C^B\]
3.2 Currying and uncurrying
\[\curry: C^{A \times B} \iso (C^B)^A :\curry\inv\]
\[\Hom(A \times B, C) \iso \Hom(A, C^B)\]
curry :: ((a, b) -> c) -> a -> b -> c
uncurry :: (a -> b -> c) -> (a, b) -> c 4 Product
4.1 Product codomain
\[\angles{p_1^A, p_2^A}: (B \times C)^A \iso B^A \times C^A\]
\[\Hom(A, B \times C) \iso \Hom(A, B) \times \Hom(A, C)\]
4.2 Coproduct domain
\[\angles{C^{i_1}, C^{i_2}}: C^{A + B} \iso C^A \times C^B\]
\[\Hom(A + B, C) \iso \Hom(A, C) \times \Hom(B, C)\]
5 Locally cartesian closed category
A locally cartesian closed category \(\cC\) is a category such that every slice category \(\cC \comma C\) is cartesian closed.
A slice category \(\cC \comma C\) of a locally cartesian closed category \(\cC\) is locally cartesian closed.
A slice of a slice \((\cC \comma C) \comma (A \xto{a} C)\) is isomorphic to a slice \(\cC \comma A\).
A locally cartesian closed category \(\cC\) with a terminal object \(1\) is cartesian closed and finitely complete.
Exponentials in \(\cC \comma 1\) are exponentials in \(\cC\). Products in \(\cC \comma C\) are pullbacks in \(\cC\). Pullbacks and a terminal object imply all finite limits.