First we define
H : A → H
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
\cl H : \sc A \to \sc H H : A → H . Let
α ∈ A
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
\alpha \in \sc A α ∈ A ; ie, let
α : F ⇒ G
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
\alpha : F \Rightarrow G α : F ⇒ G . We need to give a
functor H : C × 2 → D
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
H : C \times \bf 2 \to D H : C × 2 → D ; this will be the definition for
H ( α )
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
\cl H(\alpha) H ( α ) .
We define
H
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
H H as follows. On
objects we have
H : ( c , n ) ↦ { F ( c ) n = 0 G ( c ) n = 1
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
\begin{align*} H : (c, n) \mapsto \begin{cases}
F(c) & n = 0
\\ G(c) & n = 1
\end{cases}
\end{align*} H : ( c , n ) ↦ { F ( c ) G ( c ) n = 0 n = 1
and on
morphisms we let
H : ( f : x → y , j : n → k ) ↦ { F ( f ) : F ( x ) → F ( y ) j : 0 → 0 α x ; G ( f ) : F ( x ) → G ( y ) j : 0 → 1 G ( f ) : G ( x ) → G ( y ) j : 1 → 1
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
\begin{align*} H : (f : x \to y,\ j : n \to k) \mapsto \begin{cases}
F(f) : F(x) \to F(y) & j : 0 \to 0
\\ \alpha_x \then G(f) : F(x) \to G(y) & j : 0 \to 1
\\ G(f) : G(x) \to G(y) & j : 1 \to 1
\end{cases}
\end{align*} H : ( f : x → y , j : n → k ) ↦ ⎩ ⎨ ⎧ F ( f ) : F ( x ) → F ( y ) α x ; G ( f ) : F ( x ) → G ( y ) G ( f ) : G ( x ) → G ( y ) j : 0 → 0 j : 0 → 1 j : 1 → 1
Then
H
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
H H is a
functor , but for
H ∈ H
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
H \in \sc H H ∈ H to hold we need show that the relevant
diagram commutes. We show that its two inner
diagrams —a left triangle and a right triangle—both commute, as follows:
Left — need that
F = i 0 ; H
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
F = i_0 \then H F = i 0 ; H . On
objects this is true by
F ( x ) = defn of H H ( ( x , 0 ) ) = defn of i 0 H ( i 0 ( x ) )
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
\begin{align*} F(x) \; \underset{\t{defn of } H} = \; H((x, 0)) \; \underset{\t{defn of } i_0} = \; H(i_0(x))
\end{align*} F ( x ) defn of H = H (( x , 0 )) defn of i 0 = H ( i 0 ( x ))
and on
morphisms f ∈ Mor C ( x , y )
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
f \in \text{Mor}_C(x, y) f ∈ Mor C ( x , y ) we have
F ( f ) = defn of H H ( ( f , i d 0 ) ) = defn of i 0 H ( i 0 ( f ) )
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
\newcommand{\apar}{ {-} }
% reverse-order composition
%\newcommand{\then}{ \operatorname{\ ;\ } }
\newcommand{\then}{ {\scriptsize\ \rhd\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\renewcommand{\then}{\operatorname{\, ;\; }}
\begin{align*} F(f) \; \underset{\t{defn of } H} = \; H((f, \mathrm{id}_0)) \; \underset{\t{defn of } i_0} = \; H(i_0(f))
\end{align*} F ( f ) defn of H = H (( f , id 0 )) defn of i 0 = H ( i 0 ( f )) Right — proceeds in essentially the same way
commutes for any choice of in . That is, we need that . And this just holds: