\[ \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} % |/= \]
A category is a collection of morphisms between objects with the concepts of identity and composition.
1 Category
A category \(\cC = (\Obj, \Hom, \compL, \id)\) consists of
- a collection of objects \(\Obj\)
- a collection of morphisms \(\Hom(A, B)\) between objects
- a composition function \(\compL: \Hom(B, C) \times \Hom(A, B) \to \Hom(A, C)\)
- an identity morphism \(\id_A \in \Hom(A, A)\) for each object
subject to
- associativity: \((h \compL g) \compL f = h \compL (g \compL f)\)
- identity: \(\id_B \compL f = f = f \compL \id_A\)
-- function composition
(.) :: (b -> c) -> (a -> b) -> (a -> c)1.1 Isomorphism
An inverse of a morphism \(f: A \to B\) is a morphism \(f\inv: B \to A\) such that \(f\inv \compL f = \id_A\) and \(f \compL f\inv = \id_B\).
\(A\) and \(B\) are isomorphic, denoted by \(A \iso B\).
- skeletal category: isomorphic objects are equal
- groupoid: all morphisms are isomorphisms
1.2 Size
- thin: \(\Hom(A, B)\) contains at most one morphism
- finite: \(\Obj\) is a finite set and \(\Hom(A, B)\) is a finite set
- small: \(\Obj\) is a set and \(\Hom(A, B)\) is a set
- locally small: \(\Hom(A, B)\) is a set
- essentially small: equivalent to a small category
- large: otherwise
1.3 Construction
- opposite category \(\cC\op\): the same objects and reversed morphisms
- product category \(\cC \times \cD\): ordered pairs of objects and morphisms
1.4 Examples
\[2:= \set{\varnothing, \singleton} \iso \set{\lfal, \ltru}\]
1.4.1 Monoid
A monoid \((M, \otimes, e)\) (a set with a unital and associative binary operation) is a single-object category, where \(\Hom(*, *) = M\).
- \((\Hom(X, X), \compL, \id_X)\) endomorphism monoid
- \((LX, \concat, [])\) free monoid
- \((2, \lcon, \ltru)\), \((2, \leqv, \ltru)\)
- \((2, \ldis, \lfal)\), \((2, \lneqv, \lfal)\)
- \((\N, +, 0)\)
- \((\N, \times, 1)\)
- \((PX, \cap, X)\)
- \((PX, \cup, \varnothing)\)
1.4.2 Poset
A preordered set (proset) \((A, \leq)\) (a set with a reflexive and transitive binary relation) is a thin category, where \(\Hom(a, b) \in 2\).
A partially ordered set (poset) is a skeleton of a proset.
- \((PA, \subseteq)\)
- \((\N, \leq)\)
- \((\N, \mid)\)
Any poset \((A, \leq)\) is isomorphic to an inclusion order \((\set{A_{\leq c}}_{c \in A}, \subseteq)\) where \(A_{\leq c} := \set{a \in A \mid a \leq c}\).
\[a \leq b \leqv A_{\leq a} \subseteq A_{\leq b}\]
1.4.3 Finite category
- empty/initial category \(\cZero\): no objects
- trivial/terminal category \(\cOne\): one object \(*\) and one morphism \(\id_*\)
- interval category \(\cTwo\): two objects and one non-identity morphism
1.4.4 Concrete category
- \(\cSet\): sets and functions
- \(\cRel\): sets and relations
- \(\cPos\): posets and monotones
- \(\cMon\): monoids and monoid homomorphisms
- \(\cGrp\): groups and group homomorphisms
- \(\cAb\): abelian groups and group homomorphisms
- \(\cVect\): vector spaces and linear functions
- \(\cMet\): metric spaces and metric maps
2 Functor
For categories \(\cC\) and \(\cD\), a functor \(F: \cC \to \cD\) is a mapping, which sends
\(\cC\)-objects to \(\cD\)-objects
\[\begin{aligned} F: \Obj_\cC & \to \Obj_\cD \\ A & \mapsto FA \end{aligned}\]
\(\cC\)-morphisms to \(\cD\)-morphisms
\[\begin{aligned} F_{A, B}: \Hom_\cC(A, B) & \to \Hom_\cD(FA, FB) \\ (A \xto{f} B) & \mapsto (FA \xto{Ff} FB) \end{aligned}\]
in such a way that \(F\) preserves
- composition: \(F(g \compL_\cC f) = Fg \compL_\cD Ff\)
- identity: \(F\id_{\cC: A} = \id_{\cD: FA}\)
-- application operator
($) :: (a -> b) -> a -> b
-- fmap
(<$>) :: Functor f => (a -> b) -> f a -> f b(<$) :: Functor f => a -> f b -> f a
(<$) = fmap . const
($>) :: Functor f => f a -> b -> f b
($>) = flip (<$)2.1 Composition
For \(\cA \xto{F} \cB \xto{G} \cC\):
\[\begin{aligned} \begin{array}{cccc} GF: & \cA & \to & \cC \\ & A & \mapsto & G(FA) \\ & f & \mapsto & G(Ff) \end{array} \end{aligned}\]
The identity functor \(\id_\cC: \cC \to \cC\) sends each object and morphism to itself.
\(\cCat\): category of small categories and functors
2.2 Isomorphism
A functor between groupoids preserves the inverse:
\[Ff\inv \compL_\cD Ff = F(f\inv \compL_\cC f) = F\id_{\cC:A} = \id_{\cD:FA}\]
\[Ff \compL_\cD Ff\inv = F(f \compL_\cC f\inv) = F\id_{\cC:B} = \id_{\cD:FB}\]
An inverse of a functor \(F: \cC \to \cD\) is a functor \(F\inv: \cD \to \cC\) such that \(\id_\cC = GF\) and \(FG = \id_\cD\).
2.3 Construction
- covariant functor from \(\cC\) to \(\cD\): \(\cC \to \cD\)
- contravariant functor from \(\cC\) to \(\cD\): \(\cC\op \to \cD\)
- presheaf on \(\cC\): \(\cC\op \to \cSet\)
- copresheaf on \(\cC\): \(\cC \to \cSet\)
- bifunctor from \(\cC\) and \(\cD\) to \(\cE\): \(\cC \times \cD \to \cE\)
- profunctor from \(\cC\) to \(\cD\): \(\cD\op \times \cC \to \cSet\)
2.4 Properties
- faithful: \(\Hom_\cC(A, B) \to \Hom_\cD(FA, FB)\) is injective
- full: \(\Hom_\cC(A, B) \to \Hom_\cD(FA, FB)\) is surjective
- injective-on-objects: \(\Obj_\cC \to \Obj_\cD\) is injective
- surjective-on-objects: \(\Obj_\cC \to \Obj_\cD\) is surjective
- bijective-on-objects: \(\Obj_\cC \to \Obj_\cD\) is bijective
- essentially surjective: \(\Obj_\cC \to \Obj_\cD\) is surjective up to isomorphism
forgetful functor:
- a fully faithful and essentially surjective functor forgets nothing.
- a fully faithful functor forgets only properties.
- a faithful functor forgets at most structure.
- a functor may forget everything.
2.5 Subcategory
Given a category \(\cC\), a subcategory \(\cS\) is a category consisting of subcollections of \(\cC\)-objects and \(\cC\)-morphisms with the same identity morphisms and composition.
The inclusion functor \(I: \cS \incl \cC\) sends objects and morphisms to themselves.
- full subcategory: some objects, all morphisms (full inclusion functor)
- wide subcategory: all objects, some morphisms (bijective-on-objects inclusion functor)
- essentially wide subcategory: all objects up to isomorphism, some morphisms (essentially surjective inclusion functor)
3 Natural transformation
For functors \(F, G: \cC \to \cD\), a natural transformation \(\alpha: F \nat G\) is a collection of \(\cD\)-morphisms indexed by \(\cC\)-objects \(\alpha_A: FA \to GA\) that satisfies
- naturality: \(\alpha_B \compL Ff = Gf \compL \alpha_A\)
3.1 Composition
3.1.1 Vertical composition
\[F, G, H: \cC \to \cD\]
\[\beta \compL \alpha : F \xnat{\alpha} G \xnat{\beta} H\]
\[(\beta \compL \alpha)_A := \beta_A \compL_\cD \alpha_A\]
The identity natural transformation \(\id_F: F \nat F\) sends each \(\cC\)-object \(A\) to the identity \(\cD\)-morphism \(\id_{FA}\).
functor category \([\cC, \cD]\) or \(\cD^\cC\): category of functors from \(\cC\) to \(\cD\) and natural transformations
3.1.2 Horizontal composition
\[\begin{aligned} \begin{array}{ccccc} [\cB, \cC] & \times & [\cA, \cB] & \to & [\cA, \cC] \\ G && F & \mapsto & GF \\ \beta: G_1 \nat G_2 && \alpha: F_1 \nat F_2 & \mapsto & \beta\alpha: G_1F_1 \nat G_2F_2 \end{array} \end{aligned}\]
\[(\beta\alpha)_A := \beta_{F_2 A} \compL_\cC G_1 \alpha_A = G_2 \alpha_A \compL_\cC \beta_{F_1 A}\]
3.1.3 Whiskering
\[G \alpha: GF_1 \nat GF_2 := \id_G \alpha\]
\[(G \alpha)_A := G \alpha_A\]
\[\beta F: G_1F \nat G_2F := \beta \id_F\]
\[(\beta F)_A := \beta_{FA}\]
\[\beta\alpha = \beta F_2 \compL G_1 \alpha = G_2 \alpha \compL \beta F_1\]
3.2 Isomorphism
A natural isomorphism \(\alpha: F \nat G\) is a natural transformation whose components \(\alpha_A: FA \to GA\) are isomorphisms.
\(F\) and \(G\) are naturally isomorphic, denoted by \(F \iso G\).
A natural isomorphism is an isomorphism in the functor category \([\cC, \cD]\).
An equivalence between categories \(\cC\) and \(\cD\) consists of a pair of functors \(F: \cC \toot \cD: G\) such that \(\id_\cC \iso GF\) and \(FG \iso \id_\cD\).
A fully faithful and essentially surjective functor realizes an equivalence of categories.
4 Construction
4.1 Comma category
comma category \((F: \cA \to \cC) \comma (G: \cB \to \cC)\)
- objects are triplets \((\cA\text{-object } A, \cB\text{-object } B, \cC\text{-morphism } h: FA \to GB)\)
- morphisms are pairs \((\cA\text{-morphism } f: A_1 \to A_2, \cB\text{-morphism } g: B_1 \to B_2)\) such that \(h_2 \compL Ff = Gg \compL h_1\)
For functors \(F, G: \cC \to \cD\), a natural transformation \(\alpha: F \nat G\) is isomorphic to a functor to the comma category:
\[\begin{aligned} \alpha: \cC & \to F \comma G \\ A & \mapsto (A, A, \alpha_A) \\ f & \mapsto (f, f) \end{aligned}\]
4.1.1 Arrow category
arrow category \(\cArr(\cC) \iso (\id_\cC: \cC \to \cC) \comma (\id_\cC: \cC \to \cC) \iso [\cTwo, \cC]\)
- objects are morphisms: \(h: A \to B\)
- morphisms are commutative squares: \((f: A_1 \to A_2, g: B_1 \to B_2): h_1 \to h_2\) such that \(h_2 \compL f = g \compL h_1\)
4.1.2 Slice category
slice category \(\cC \comma C \iso (\id_\cC: \cC \to \cC) \comma (C: \cOne \to \cC)\)
- objects are morphisms to \(C\): \(h: A \to C\)
- morphisms are commutative triangles: \((f: A_1 \to A_2): h_1 \to h_2\) such that \(h_2 \compL f = h_1\)
For a monoid \(\cM: (*, M)\), the Green’s preorder \(\leq_R\) is the slice category \(\cM \comma *: (M, a \xto{c: a = b \compL c} b)\).
4.1.3 Coslice category
coslice category \(C \comma \cC \iso (C: \cOne \to \cC) \comma (\id_\cC: \cC \to \cC)\)
- objects are morphisms from \(C\): \(h: C \to B\)
- morphisms are commutative triangles: \((g: B_1 \to B_2): h_1 \to h_2\) such that \(h_2 = g \compL h_1\)
4.2 Functor category
\[\cA \xto{F} \cB \xto{G} \cC \xto{H} \cD\]
A functor \(H: \cC \to \cD\) induces a postcomposition functor \(H^\cB: \cC^\cB \to \cD^\cB\) between functor categories:
\[\begin{aligned} \begin{array}{cccc} H^\cB: & \cC^\cB & \to & \cD^\cB \\ & G & \mapsto & HG \\ & G_1 \xnat{\beta} G_2 & \mapsto & H G_1 \xnat{H \beta} H G_2 \end{array} \end{aligned}\]
A functor \(F: \cA \to \cB\) induces a precomposition functor \(\cC^F: \cC^\cB \to \cC^\cA\) between functor categories:
\[\begin{aligned} \begin{array}{cccc} \cC^F: & \cC^\cB & \to & \cC^\cA \\ & G & \mapsto & GF \\ & G_1 \xnat{\beta} G_2 & \mapsto & G_1 F \xnat{\beta F} G_2 F \end{array} \end{aligned}\]
A constant functor \(\Delta C: \cD \to \cC\) sends all \(\cD\)-objects to \(C\) and all \(\cD\)-morphisms to \(\id_C\).
A diagonal functor \(\Delta: \cC \to \cC^\cD\) is isomorphic to a precomposition functor induced by the unique functor \(\cD \to \cOne\):
\[\begin{aligned} \begin{array}{cccc} \Delta: & \cC & \to & \cC^\cD \\ & C & \mapsto & \Delta C \\ & A \xto{f} B & \mapsto & \Delta A \xnat{\Delta f} \Delta B \end{array} \end{aligned}\]
binary diagonal functor \(\Delta_\cTwo: \cC \to \cC \times \cC\):
\[\begin{aligned} \begin{array}{cccc} \Delta_\cTwo: & \cC & \to & \cC \times \cC \\ & C & \mapsto & (C, C) \\ & A \xto{f} B & \mapsto & (A, A) \xto{(f, f)} (B, B) \end{array} \end{aligned}\]
4.3 Hom-functor
\[A \xto{f} B \xto{g} C \xto{h} D\]
The hom-functor \(\Hom: \cC\op \times \cC \to \cSet\) is an endoprofunctor:
\[\begin{aligned} \begin{array}{cccccc} \Hom: & \cC\op & \times & \cC & \to & \cSet \\ & A && B & \mapsto & \Hom(A, B) \\ & B \xto{f\op} A && C \xto{h} D & \mapsto & \Hom(B, C) \xto{h \compL (-) \compL f} \Hom(A, D) \end{array} \end{aligned}\]
The postcomposition \(\Hom(B, -): \cC \to \cSet\) is a copresheaf:
\[\begin{aligned} \begin{array}{cccc} \Hom(B, -): & \cC & \to & \cSet \\ & C & \mapsto & \Hom(B, C) \\ & C \xto{h} D & \mapsto & \Hom(B, C) \xto{h \compL (-)} \Hom(B, D) \end{array} \end{aligned}\]
The precomposition \(\Hom(-, C): \cC\op \to \cSet\) is a presheaf:
\[\begin{aligned} \begin{array}{cccc} \Hom(-, C): & \cC\op & \to & \cSet \\ & B & \mapsto & \Hom(B, C) \\ & B \xto{f\op} A & \mapsto & \Hom(B, C) \xto{(-) \compL f} \Hom(A, C) \end{array} \end{aligned}\]
A representable functor is a presheaf naturally isomorphic to a hom-functor \(\Hom(-, C): \cC\op \to \cSet\).
4.3.1 Naturality
\[\begin{aligned} \Hom(f, -) &: \Hom(B, -) \nat \Hom(A, -) \\ \Hom(-, h) &: \Hom(-, C) \nat \Hom(-, D) \end{aligned}\]
A functor on morphisms \(F_{B, C}: \Hom(B, C) \to \Hom(FB, FC)\) is natural in the domain \(B\) and codomain \(C\).
4.3.2 Yoneda lemma
Yoneda embedding:
\[\begin{aligned} \begin{array}{cccc} よ: & \cC & \to & [\cC\op, \cSet] \\ & C & \mapsto & \Hom(-, C) \\ & A \xto{f} B & \mapsto & \Hom(-, A) \xto{\Hom(-, f)} \Hom(-, B) \end{array} \end{aligned}\]
The Yoneda embedding is full and faithful.
\[\begin{aligned} \begin{array}{ccc} \Hom_\cCat(\cC\op \times \cC, \cSet) & \iso & \Hom_\cCat(\cC, [\cC\op, \cSet]) \\ \Hom & \leqv & よ \end{array} \end{aligned}\]
\[\Hom_{[\cC, \cSet]}(\Hom_\cC(A, -), F) \iso FA \iso \Hom_{[\cC\op, \cSet]}(\Hom_\cC(-, A), F)\]
Any natural transformation between covariant hom-functors is of the form \(\Hom_\cC(f, -)\).
\[\Hom_{[\cC, \cSet]}(\Hom_\cC(B, -), \Hom_\cC(A, -)) \iso \Hom_\cC(A, B)\]
Any natural transformation between contravariant hom-functors is of the form \(\Hom_\cC(-, f)\).
\[\Hom_{[\cC\op, \cSet]}(\Hom_\cC(-, A), \Hom_\cC(-, B)) \iso \Hom_\cC(A, B)\]
\[\begin{aligned} \begin{array}{rccc} \Hom_{(X, \leq)}: & (X, \leq)\op \times (X, \leq) & \to & \cSet \\ & (a, b) & \mapsto & a \leq b \\ & (a' \leq a), (b \leq b') & \mapsto & (a \leq b) \lproves (a' \leq b') \\ \\ よ_{(X, \leq)}: & (X, \leq) & \to & [(X, \leq)\op, \cSet] \\ & c & \mapsto & X_{\leq c} \\ & a \leq b & \mapsto & X_{\leq a} \subseteq X_{\leq b} \end{array} \end{aligned}\]