Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% (find-angg "LATEX/2019notes-yoneda.tex")
% (defun c  () (interactive) (find-LATEXsh "lualatex -record 2019notes-yoneda.tex" 1 ee-end))
% (defun c0 () (interactive) (find-LATEXsh "pdflatex -record 2019notes-yoneda.tex" 1 ee-end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2019notes-yoneda.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019notes-yoneda.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2019notes-yoneda; makeindex 2019notes-yoneda"))
% (defun e () (interactive) (find-LATEX "2019notes-yoneda.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019notes-yoneda"))
% (find-xpdfpage "~/LATEX/2019notes-yoneda.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019notes-yoneda.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019notes-yoneda.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019notes-yoneda.pdf
%               file:///tmp/2019notes-yoneda.pdf
%           file:///tmp/pen/2019notes-yoneda.pdf
% http://angg.twu.net/LATEX/2019notes-yoneda.pdf
%
%   A diagram for the Yoneda Lemma
%   (In which each node and arrow can be
%   interpreted precisely as a lambda-term,
%   and most of the interpretations are
%   "obvious"; plus dictionaries!!!)
%
% (find-TH "math-b" "notes-yoneda")
% (find-es "dednat" "arxiv-yoneda")

% «.colors»			(to "colors")
% «.yoneda-R-5»			(to "yoneda-R-5")
% «.yoneda-R-5+»		(to "yoneda-R-5+")
% «.yoneda-R-6»			(to "yoneda-R-6")
% «.yoneda-B->-6»		(to "yoneda-B->-6")
% «.yoneda-R-ACDE»		(to "yoneda-R-ACDE")
% «.yoneda-F1»			(to "yoneda-F1")
% «.yoneda-F2»			(to "yoneda-F2")
% «.yoneda-Tobjs»		(to "yoneda-Tobjs")
% «.yoneda-Tsqcond»		(to "yoneda-Tsqcond")
% «.yoneda-bij»			(to "yoneda-bij")
% «.yoneda-curve-with-terms»	(to "yoneda-curve-with-terms")

% «.title-page»			(to "title-page")
% «.three-yoneda-lemmas»	(to "three-yoneda-lemmas")
% «.first-yoneda-lemma»		(to "first-yoneda-lemma")
% «.first-yoneda-F1-F2»		(to "first-yoneda-F1-F2")
% «.first-yoneda-Tobjs»		(to "first-yoneda-Tobjs")
% «.first-yoneda-Tsqcond»	(to "first-yoneda-Tsqcond")
% «.first-yoneda-diagram»	(to "first-yoneda-diagram")
% «.first-yoneda-diagram-2»	(to "first-yoneda-diagram-2")
% «.first-yoneda-bijection»	(to "first-yoneda-bijection")
% «.first-yoneda-bijection-2»	(to "first-yoneda-bijection-2")
% «.first-yoneda-bijection-3»	(to "first-yoneda-bijection-3")
% «.first-yoneda-bijection-4»	(to "first-yoneda-bijection-4")
% «.drawing-the-bijection»	(to "drawing-the-bijection")
% «.changing-A-to-Set»		(to "changing-A-to-Set")
% «.getting-rid-of-1»		(to "getting-rid-of-1")
% «.bijs-and-isos»		(to "bijs-and-isos")
% «.bijs-and-isos-2»		(to "bijs-and-isos-2")
% «.getting-rid-of-1-2»		(to "getting-rid-of-1-2")
% «.getting-rid-of-1-3»		(to "getting-rid-of-1-3")
% «.getting-rid-of-1-4»		(to "getting-rid-of-1-4")
% «.getting-rid-of-1-5»		(to "getting-rid-of-1-5")
% «.changing-A-to-Set-2»	(to "changing-A-to-Set-2")
% «.changing-R-to-Bto»		(to "changing-R-to-Bto")
% «.changing-R-to-Bto-2»	(to "changing-R-to-Bto-2")
%
% «.reading»			(to "reading")
% «.blob-sets»			(to "blob-sets")
% «.blob-sets-2»		(to "blob-sets-2")
% «.internal-view-functor»	(to "internal-view-functor")
% «.internal-view-functor-2»	(to "internal-view-functor-2")
% «.internal-view-to-do»	(to "internal-view-to-do")

% «.help-needed»		(to "help-needed")
% «.limpberg»			(to "limpberg")
% «.dictionaries»		(to "dictionaries")
% «.same-shape»			(to "same-shape")
% «.CWM»			(to "CWM")
% «.CWM-2»			(to "CWM-2")
% «.CWM-3»			(to "CWM-3")
% «.CWM-4»			(to "CWM-4")
% «.CWM-p61»			(to "CWM-p61")
% «.awodey»			(to "awodey")
% «.riehl»			(to "riehl")


\documentclass[oneside]{book}
\usepackage{ifluatex}
\ifluatex
  \input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
  \input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\else
  \usepackage[utf8]{inputenc}
  \input 2019oxford-chars.tex       % (find-LATEX "2019oxford-chars.tex")
\fi

\usepackage[colorlinks,urlcolor=violet]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{color}                % (find-LATEX "edrx15.sty" "colors")
%\usepackage{colorweb}             % (find-es "tex" "colorweb")
%\usepackage{tikz}
\usepackage{stmaryrd}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15}               % (find-LATEX "edrx15.sty")
%\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
%\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
% (find-angg ".emacs.papers" "latexgeom")
% (find-LATEXfile "2016-2-GA-VR.tex" "{geometry}")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[paperwidth=11.5cm, paperheight=9.5cm,
            %total={6.5in,4in},
            %textwidth=4in,  paperwidth=4.5in,
            %textheight=5in, paperheight=4.5in,
            %a4paper,
            top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
           ]{geometry}
%
\begin{document}

% \catcode`\^^J=10
% \directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

% (find-dednat6 "demo-write-dnt.tex")
%
\ifluatex
  \catcode`\^^J=10
  \directlua{dofile "dednat6load.lua"}
\else
  % \input\jobname.dnt
  \input 2019notes-yoneda.dnt
  \def\pu{}
\fi



% «colors» (to ".colors")
% (find-angg ".emacs.papers" "xcolor")
\long\def\ColorRed   #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray  #1{{\color{GrayLight}#1}}
\long\def\ColorGray  #1{{\color{black!30!white}#1}}

\def\setofst#1#2{\{\,#1\;|\;#2\,\}}
\def\setofsc#1#2{\{\,#1\;;\;#2\,\}}

\setlength{\parindent}{0em}

\def\O{\mathcal{O}}
\def\T{\mathbf{T}}
\def\F{\mathbf{F}}

\def\Nat{\operatorname{Nat}}

% (find-LATEXfile "2017idarct.tex" "\\def\\sqcond")
\def\respcomp{\mathsf{respcomp}}
\def\respids {\mathsf{respids}}
\def\sqcond  {\mathsf{sqcond}}





%  ____  _                                     
% |  _ \(_) __ _  __ _ _ __ __ _ _ __ ___  ___ 
% | | | | |/ _` |/ _` | '__/ _` | '_ ` _ \/ __|
% | |_| | | (_| | (_| | | | (_| | | | | | \__ \
% |____/|_|\__,_|\__, |_|  \__,_|_| |_| |_|___/
%                |___/                         

% «yoneda-R-5» (to ".yoneda-R-5")
%D diagram yoneda-R-5
%D 2Dx     100    +40
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> RC
%D 2D
%D 2D  +20 F1 -> F2
%D 2D             |
%D 2D             v
%D 2D  +25       F3
%D 2D
%D ren F1 F2 F3 ==> (C{→}\_) (A{→}R\_) \phantom{R}
%D
%D (( C RC |-> A RC -> .plabel= r Ξ³
%D    F1 F2 -> .plabel= a T
%D    # F3 place
%D ))
%D enddiagram

% «yoneda-R-5+» (to ".yoneda-R-5+")
%D diagram yoneda-R-5+
%D 2Dx     100    +40
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> RC
%D 2D
%D 2D  +20 F1 -> F2
%D 2D             |
%D 2D             v
%D 2D  +25       F3
%D 2D
%D ren F1 F2 F3 ==> (C{→}\_) (A{→}R\_) \phantom{R}
%D
%D (( C RC |-> A RC -> .plabel= r Ξ³
%D    F1 F2 -> .plabel= a T
%D    F3 place
%D ))
%D enddiagram

% «yoneda-R-6» (to ".yoneda-R-6")
%D diagram yoneda-R-6
%D 2Dx     100    +40
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> RC
%D 2D
%D 2D  +20 F1 -> F2
%D 2D             |
%D 2D             v
%D 2D  +25       F3
%D 2D
%D ren A ==> 1
%D ren F1 F2 F3 ==> (C{→}\_) (1{→}R\_) R
%D
%D (( C RC |-> A RC -> .plabel= r Ξ³
%D    F1 F2 -> .plabel= a T
%D    F2 F3 <->
%D    F1 F3 -> .plabel= l T'
%D ))
%D enddiagram

% «yoneda-B->-6» (to ".yoneda-B->-6")
%D diagram yoneda-B->-6
%D 2Dx     100    +45
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> RC
%D 2D
%D 2D  +20 F1 -> F2
%D 2D             |
%D 2D             v
%D 2D  +25       F3
%D 2D
%D ren A RC ==> 1 (B{→C})
%D ren F1 F2 F3 ==> (C{→}\_) (1{→}(B{→}\_)) (B{→}\_)
%D
%D (( C RC |-> A RC -> .plabel= r Ξ³
%D    F1 F2 -> .plabel= a T
%D    F2 F3 <->
%D    F1 F3 -> .plabel= l T'
%D ))
%D enddiagram

% «yoneda-R-ACDE» (to ".yoneda-R-ACDE")
%D diagram yoneda-R-ACDE
%D 2Dx     100    +30
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +20 C |-> RC
%D 2D      |      |
%D 2D      v      v
%D 2D  +20 D |-> RD
%D 2D      |      |
%D 2D      v      v
%D 2D  +20 E |-> RE
%D 2D
%D 2D  +20 \catC \catA
%D 2D
%D # ren ==>
%D
%D ((                       A RC -> .plabel= r Ξ³
%D    C D -> .plabel= l g  RC RD -> .plabel= r Rg
%D    D E -> .plabel= l h  RD RE -> .plabel= r Rh
%D    A RD -> .slide= 20pt .plabel= r Ξ∧
%D    C RC |->
%D    D RD |->
%D    E RE |->
%D    \catC \catA -> .plabel= a R
%D ))
%D enddiagram
%D

% «yoneda-F1» (to ".yoneda-F1")
%D diagram (C->_)
%D 2Dx     100    +35 +25
%D 2D  100 A1 |-> A2  C1
%D 2D      |       |   |
%D 2D      v       v   v
%D 2D  +20 A3 |-> A4  C2
%D 2D
%D 2D  +20 B1 --> B2
%D 2D
%D ren A1 A2 A3 A4 ==> D (C{→}D) E (C{→}E)
%D ren B1 B2 ==> \catC \Set
%D ren C1 C2 ==> g g;h
%D
%D (( A1 A2 |->
%D    A1 A3 -> .plabel= l h
%D    A2 A4 -> .plabel= r Ξ»g.(g;h)
%D    A3 A4 |->
%D    B1 B2 -> .plabel= a (C{→}\_)
%D    C1 C2 |->
%D ))
%D enddiagram

% «yoneda-F2» (to ".yoneda-F2")
%D diagram (A->R_)
%D 2Dx     100    +35 +30
%D 2D  100 A1 |-> A2  C1
%D 2D      |       |   |
%D 2D      v       v   v
%D 2D  +20 A3 |-> A4  C2
%D 2D
%D 2D  +20 B1 --> B2
%D 2D
%D ren A1 A2 A3 A4 ==> D (A{→}RD) E (A{→}RE)
%D ren B1 B2 ==> \catC \Set
%D ren C1 C2 ==> Ξ∧ Ξ∧;Rh
%D
%D (( A1 A2 |->
%D    A1 A3 -> .plabel= l h
%D    A2 A4 -> .plabel= r Ξ»Ξ∧.(Ξ∧;Rh)
%D    A3 A4 |->
%D    B1 B2 -> .plabel= a (A{→}R\_)
%D    C1 C2 |->
%D ))
%D enddiagram

% «yoneda-Tobjs» (to ".yoneda-Tobjs")
%D diagram yoneda-Tobjs
%D 2Dx     100 +25     +40   +30     +40
%D 2D  100 D   F1D |-> F2D   f1d |-> f2d
%D 2D
%D 2D  +20 E   F1E |-> F2E   f1e |-> f2e
%D 2D
%D 2D  +20     F1 ---> F2
%D 2D
%D ren F1D F2D ==> (C{→}D) (A{→}RD)
%D ren F1E F2E ==> (C{→}E) (A{→}RE)
%D ren f1d f2d ==> g   Ξ³;Rg
%D ren f1e f2e ==> g;h Ξ³;R(g;h)
%D ren F1  F2  ==> (C{→}\_) (A{→}R\_)
%D
%D (( D place E place
%D    F1D F2D -> .plabel= a TD
%D    F1E F2E -> .plabel= a TE
%D    F1  F2  -> .plabel= a T
%D    f1d f2d |->
%D    f1e f2e |->
%D ))
%D enddiagram

% «yoneda-Tsqcond» (to ".yoneda-Tsqcond")
%D diagram yoneda-Tsqcond
%D 2Dx     100 +30     +40   +30     +40   +30
%D 2D  100 D   F1D |-> F2D   f1d |-> f2d   f2d2
%D 2D      |   |         |   -        -     -
%D 2D      |   |         |   |        |     |
%D 2D      |   |         |   |        v     v
%D 2D  +25 v   v         v   v       f2e1  f2e3
%D 2D   +8 E   F1E |-> F2E   f1e |-> f2e2
%D 2D
%D 2D  +20     F1 ---> F2
%D 2D
%D ren F1D F2D ==> (C{→}D) (A{→}RD)
%D ren F1E F2E ==> (C{→}E) (A{→}RE)
%D ren f1d f2d ==> g   Ξ³;Rg
%D ren f1e f2e1 f2e2 ==> g;h (Ξ³;Rg);Rh Ξ³;R(g;h)
%D ren     f2d2 f2e3 ==> Ξ∧ Ξ∧;Rh
%D ren F1  F2  ==> (C{→}\_) (A{→}R\_)
%D
%D (( D E -> .plabel= l h
%D    F1D F2D -> .plabel= a TD
%D    F1D F1E -> .plabel= l (C{→}\_)h
%D    F2D F2E -> .plabel= l (A{→}R\_)h
%D    F1E F2E -> .plabel= a TE
%D    F1  F2  -> .plabel= a T
%D    f1d f2d |-> f2d f2e1 |->
%D    f1d f1e |-> f1e f2e2 |->
%D   f2d2 f2e3 |->
%D ))
%D enddiagram

% «yoneda-bij» (to ".yoneda-bij")
%D diagram yoneda-bij
%D 2Dx     100 +30     +40   +30     +40 
%D 2D  100 C   F1C --> F2C   f1c |-> f2c 
%D 2D      |   |         |   -        -  
%D 2D      |   |         |   |        |  
%D 2D      |   |         |   |        v  
%D 2D  +25 v   v         v   v       f2d1
%D 2D   +8 D   F1D --> F2D   f1d |-> f2d2
%D 2D
%D 2D  +20     F1 ---> F2
%D 2D
%D ren F1C F2C ==> (C{→}C) (A{→}RC)
%D ren F1D F2D ==> (C{→}D) (A{→}RD)
%D ren f1c f2c f2d1 ==> \id_C TC(\id_C) TC(\id_C);Rg
%D ren f1d f2d2 ==> g TD(g)
%D ren F1  F2  ==> (C{→}\_) (A{→}R\_)
%D
%D (( C D -> .plabel= l g
%D    F1C F2C -> .plabel= a TC
%D    F1C F1D -> .plabel= l (C{→}\_)g
%D    F2C F2D -> .plabel= l (A{→}R\_)g
%D    F1D F2D -> .plabel= a TD
%D    F1  F2  -> .plabel= a T
%D    f1c f2c |-> f2c f2d1 |->
%D    f1c f1d |-> f1d f2d2 |->
%D ))
%D enddiagram

% «yoneda-curve-with-terms»  (to ".yoneda-curve-with-terms")
%D diagram yoneda-curve-with-terms
%D 2Dx     100    +40
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> RC
%D 2D
%D 2D  +20 F1 -> F2
%D 2D             |
%D 2D             v
%D 2D  +25       F3
%D 2D
%D ren F1 F2 F3 ==> (C{→}\_) (A{→}R\_) \phantom{R}
%D
%D (( C RC |->
%D    A RC  -> .plabel= r Ξ³
%D    F1 F2 -> .plabel= l T
%D    F1 F2 midpoint A RC midpoint <-> .curve= ^14pt
%D ))
%D enddiagram

\pu



%  _____ _ _   _                               
% |_   _(_) |_| | ___   _ __   __ _  __ _  ___ 
%   | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
%   | | | | |_| |  __/ | |_) | (_| | (_| |  __/
%   |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
%                      |_|          |___/      
%
% «title-page» (to ".title-page")
% (nyop 1 "title-page")
% (nyo    "title-page")

% (cl1p 1 "title-page")
% (cl1    "title-page")

\begin{tabular}[b]{c}
{\Large {\bf A diagram for the Yoneda Lemma       }}\\
{\Large { (In which each node and arrow can be    }}\\
{\Large { interpreted precisely as a ``term'',    }}\\
{\Large { and most of the interpretations are     }}\\
{\Large { ``obvious''; plus dictionaries!!!)  }}\\[2.5pt]
\scriptsize \ColorRed{Eduardo Ochs (UFF, Rio das Ostras, Brazil)} \\[-4pt]
\scriptsize \url{http://angg.twu.net/\#intro-tys-lfc} \\
\\
%
$\begin{array}{ccc}
   \resizebox{!}{30pt}{$\diag{yoneda-curve-with-terms}$} &
   % &
   \begin{array}[c]{l}
     T_0 := Ξ»D.Ξ»g.(Ξ³;Rg) \\
     Ξ³ := TC(\id_C) \\
   \end{array}
 \end{array}
$ \\
%
\end{tabular}

\newpage

\noedrxfooter

%  _____  __   ___         
% |___ /  \ \ / / |    ___ 
%   |_ \   \ V /| |   / __|
%  ___) |   | | | |___\__ \
% |____/    |_| |_____|___/
%                          
% «three-yoneda-lemmas» (to ".three-yoneda-lemmas")
% (nyop 2 "three-yoneda-lemmas")
% (nyo    "three-yoneda-lemmas")

{\bf Three Yoneda Lemmas}

These are \ColorRed{our} diagrams for three ``Yoneda Lemmas''.

\msk

\resizebox{1.0\textwidth}{!}{%
$\diag{yoneda-R-5+}
  \quad
  \diag{yoneda-R-6}
  \quad
  \diag{yoneda-B->-6}
$}

\msk

In all cases we have bijections between `$Ξ³$'s and `$T$'s.

The `$Ξ³$'s are morphisms, the `$T$'s are natural transformations.

Right: the most concrete and familiar YL, a bijection

$\Hom(B,C) ↔ \Nat((C{→}\_), (B{→}\_))$.

Left: the most abstract YL.

\newpage

%  _____ _          _    __   ___     
% |  ___(_)_ __ ___| |_  \ \ / / |    
% | |_  | | '__/ __| __|  \ V /| |    
% |  _| | | |  \__ \ |_    | | | |___ 
% |_|   |_|_|  |___/\__|   |_| |_____|
%                                     
% «first-yoneda-lemma» (to ".first-yoneda-lemma")
% (nyop 3 "first-yoneda-lemma")
% (nyo    "first-yoneda-lemma")

{\bf The first (most abstract) Yoneda Lemma}

Choose (locally small) categories $\catA$ and $\catC$,

objects $A∈\catA$ and $C∈\catC$, a functor $R:\catC→\catA$,

and a morphism $Ξ³:A→RC$.
%
$$\diag{yoneda-R-5}$$
%
We need to understand the functors $(C→\_):\catC→\Set$

and $(A→R\_):\catC→\Set$ and see how the morphism

$Ξ³:A→RC$ induces a natural transformation $T$...

\newpage

%  _____ _          _    __   ___         _____ _     _____ ____  
% |  ___(_)_ __ ___| |_  \ \ / / |    _  |  ___/ |   |  ___|___ \ 
% | |_  | | '__/ __| __|  \ V /| |   (_) | |_  | |   | |_    __) |
% |  _| | | |  \__ \ |_    | | | |___ _  |  _| | |_  |  _|  / __/ 
% |_|   |_|_|  |___/\__|   |_| |_____(_) |_|   |_( ) |_|   |_____|
%                                                |/               
%
% «first-yoneda-F1-F2» (to ".first-yoneda-F1-F2")
% (nyop 4 "first-yoneda-F1-F2")
% (nyo    "first-yoneda-F1-F2")

{\bf The two functors: internal views}

To understand the functors $(C{→}\_)$ and $(A{→}R\_)$ we

1) draw an auxiliar diagram (left),

2) draw their internal views (middle, right).

\msk

\resizebox{1.0\textwidth}{!}{%
$
  \diag{yoneda-R-ACDE}
  \quad
  \diag{(C->_)}
  \quad
  \diag{(A->R_)}
$}

\msk

$(C{→}\_)_0(D) = \Hom_\catC(C,D)$, $(C{→}\_)_1(h) = Ξ»g.(g;h)$,

$(A{→}R\_)_0(D) = \Hom_\catA(A,RD)$, $(A{→}R\_)_1(h) = Ξ»Ξ∧.(Ξ∧;Rh)$.

\newpage

%  _____ _          _    __   ___         _____ 
% |  ___(_)_ __ ___| |_  \ \ / / |    _  |_   _|
% | |_  | | '__/ __| __|  \ V /| |   (_)   | |  
% |  _| | | |  \__ \ |_    | | | |___ _    | |  
% |_|   |_|_|  |___/\__|   |_| |_____(_)   |_|  
%                                               
% «first-yoneda-Tobjs» (to ".first-yoneda-Tobjs")
% (nyop 5 "first-yoneda-Tobjs")
% (nyo    "first-yoneda-Tobjs")

{\bf The natural transformation: internal view}

To understand the NT $T: (C{→}\_) → (A{→}R\_)$

we start by seeing how it produces, for objects $D,E∈\catC$,

morphisms $TD$ and $TE$...

\msk

\resizebox{0.95\textwidth}{!}{%
$
  \diag{yoneda-R-ACDE}
  \quad
  \diag{yoneda-Tobjs}
$}

\bsk

So $TD = Ξ»g.(R;g)$,

$T_0 = Ξ»D.Ξ»g.(R;g)$.


\newpage


%  _____ _          _    __   ___         _____                              _ 
% |  ___(_)_ __ ___| |_  \ \ / / |    _  |_   _|__  __ _  ___ ___  _ __   __| |
% | |_  | | '__/ __| __|  \ V /| |   (_)   | |/ __|/ _` |/ __/ _ \| '_ \ / _` |
% |  _| | | |  \__ \ |_    | | | |___ _    | |\__ \ (_| | (_| (_) | | | | (_| |
% |_|   |_|_|  |___/\__|   |_| |_____(_)   |_||___/\__, |\___\___/|_| |_|\__,_|
%                                                     |_|                      
%
% «first-yoneda-Tsqcond» (to ".first-yoneda-Tsqcond")
% (nyop 6 "first-yoneda-Tsqcond")
% (nyo    "first-yoneda-Tsqcond")

{\bf The natural transformation: internal view (2)}

Now we want to check that this $T$ obeys $\sqcond_T$,

i.e. that for every morphism $h:D→E$ the

``obvious'' induced square commutes.

\msk

\resizebox{0.95\textwidth}{!}{%
$
  \diag{yoneda-R-ACDE}
  \quad
  \diag{yoneda-Tsqcond}
$}

\bsk

It commutes because we have

$∀g.((Ξ³;Rg);Rh = Ξ³;R(g;h))$.




\newpage

%  _____ _          _    __   ___             _ _             
% |  ___(_)_ __ ___| |_  \ \ / / |    _    __| (_) __ _  __ _ 
% | |_  | | '__/ __| __|  \ V /| |   (_)  / _` | |/ _` |/ _` |
% |  _| | | |  \__ \ |_    | | | |___ _  | (_| | | (_| | (_| |
% |_|   |_|_|  |___/\__|   |_| |_____(_)  \__,_|_|\__,_|\__, |
%                                                       |___/ 
%
% «first-yoneda-diagram» (to ".first-yoneda-diagram")
% (nyop 7 "first-yoneda-diagram")
% (nyo    "first-yoneda-diagram")

{\bf The diagram of the first Yoneda Lemma}

We now understand all nodes and arrows in this diagram...

Remember that $Ξ³$ \ColorRed{induced} $T$.

\msk

\resizebox{0.85\textwidth}{!}{%
$\cdiag{yoneda-R-5+}
 \quad
 \begin{array}[c]{l}
 A∈\catA \\
 C∈\catC \\
 R:\catA→\catC \\
 Ξ³:A→RC \\[5pt]
 %
 (C{→}\_): \catC→\Set \\
 (C{→}\_)_0(D) = \Hom_\catC(C,D) \\
 (C{→}\_)_1(h) = Ξ»g.(g;h) \\[5pt]
 %
 (A{→}R\_): \catC→\Set \\
 (A{→}R\_)_0(D) = \Hom_\catA(A,RD) \\
 (A{→}R\_)_1(h) = Ξ»Ξ∧.(Ξ∧;Rh) \\[5pt]
 %
 T: (C{→}\_) → (A{→}R\_) \\
 \ColorRed{T_0(D) := Ξ»g.(Ξ³;Rg)} \\
 \end{array}
$}


\newpage

%  _____ _          _    __   ___             _ _               ____  
% |  ___(_)_ __ ___| |_  \ \ / / |    _    __| (_) __ _  __ _  |___ \ 
% | |_  | | '__/ __| __|  \ V /| |   (_)  / _` | |/ _` |/ _` |   __) |
% |  _| | | |  \__ \ |_    | | | |___ _  | (_| | | (_| | (_| |  / __/ 
% |_|   |_|_|  |___/\__|   |_| |_____(_)  \__,_|_|\__,_|\__, | |_____|
%                                                       |___/         
%
% «first-yoneda-diagram-2» (to ".first-yoneda-diagram-2")
% (nyop 8 "first-yoneda-diagram-2")
% (nyo    "first-yoneda-diagram-2")

{\bf The diagram of the first Yoneda Lemma (2)}

We started with a morphism $Ξ³$ and defined $T$ from it.

We can also do the inverse!

\msk

\resizebox{0.85\textwidth}{!}{%
$\cdiag{yoneda-R-5+}
 \quad
 \begin{array}[c]{l}
 A∈\catA \\
 C∈\catC \\
 R:\catA→\catC \\
 Ξ³:A→RC \\
 \ColorRed{Ξ³ := TC(\id_C)} \\[5pt]
 %
 (C{→}\_): \catC→\Set \\
 (C{→}\_)_0(D) = \Hom_\catC(C,D) \\
 (C{→}\_)_1(h) = Ξ»g.(g;h) \\[5pt]
 %
 (A{→}R\_): \catC→\Set \\
 (A{→}R\_)_0(D) = \Hom_\catA(A,RD) \\
 (A{→}R\_)_1(h) = Ξ»Ξ∧.(Ξ∧;Rh) \\[5pt]
 %
 T: (C{→}\_) → (A{→}R\_) \\
 % \ColorRed{T_0(D) := Ξ»g.(Ξ³;Rg)} \\
 \end{array}
$}


\newpage

%  _____ _          _    __   ___         _     _  _ 
% |  ___(_)_ __ ___| |_  \ \ / / |    _  | |__ (_)(_)
% | |_  | | '__/ __| __|  \ V /| |   (_) | '_ \| || |
% |  _| | | |  \__ \ |_    | | | |___ _  | |_) | || |
% |_|   |_|_|  |___/\__|   |_| |_____(_) |_.__/|_|/ |
%                                               |__/ 
%
% «first-yoneda-bijection» (to ".first-yoneda-bijection")
% (nyop 9 "first-yoneda-bijection")
% (nyo    "first-yoneda-bijection")

{\bf The bijection}

Fact: the operations

$T := Ξ»D.Ξ»g.(Ξ³;Rg)$ and

$Ξ³ := TC(\id_C)$

are inverses to one another.

Let's rewrite them as ``$T_Ξ³$'' and ``$Ξ³_T$''...

\msk

$T_Ξ³ = Ξ»D.Ξ»g.(Ξ³;Rg)$

$Ξ³_T = TC(\id_C)$

$T_{(Ξ³_T)} = Ξ»D.Ξ»g.(Ξ³_T;Rg) = Ξ»D.Ξ»g.((TC(\id_C));Rg)$

$Ξ³_{(T_Ξ³)} = T_Ξ³C(\id_C) = (Ξ»D.Ξ»g.(Ξ³;Rg)) C(\id_C)$

\msk

We want to check that $Ξ³_{(T_Ξ³)} = Ξ³$ (easy)

and that $T_{(Ξ³_T)} = T$ (harder).

\newpage

%  _____ _          _    __   ___         _     _  _   ____  
% |  ___(_)_ __ ___| |_  \ \ / / |    _  | |__ (_)(_) |___ \ 
% | |_  | | '__/ __| __|  \ V /| |   (_) | '_ \| || |   __) |
% |  _| | | |  \__ \ |_    | | | |___ _  | |_) | || |  / __/ 
% |_|   |_|_|  |___/\__|   |_| |_____(_) |_.__/|_|/ | |_____|
%                                               |__/         
%
% «first-yoneda-bijection-2» (to ".first-yoneda-bijection-2")
% (nyop 10 "first-yoneda-bijection-2")
% (nyo     "first-yoneda-bijection-2")

{\bf The bijection (2)}

It's easy to check that $Ξ³_{(T_Ξ³)} = Ξ³$:

$\begin{array}{rcl}
 Ξ³_{(T_Ξ³)} &=& T_Ξ³C(\id_C) \\
           &=& (Ξ»D.Ξ»g.(Ξ³;Rg)) C(\id_C) \\
           &=& (Ξ»g.(Ξ³;Rg)) (\id_C) \\
           &=& Ξ³;R(\id_C) \\
           &=& Ξ³;\id_{RC} \\
           &=& Ξ³ \\
 \end{array}
$

\newpage

%  _____ _          _    __   ___         _     _  _   _____ 
% |  ___(_)_ __ ___| |_  \ \ / / |    _  | |__ (_)(_) |___ / 
% | |_  | | '__/ __| __|  \ V /| |   (_) | '_ \| || |   |_ \ 
% |  _| | | |  \__ \ |_    | | | |___ _  | |_) | || |  ___) |
% |_|   |_|_|  |___/\__|   |_| |_____(_) |_.__/|_|/ | |____/ 
%                                               |__/         
%
% «first-yoneda-bijection-3» (to ".first-yoneda-bijection-3")
% (nyop 11 "first-yoneda-bijection-3")
% (nyo     "first-yoneda-bijection-3")

{\bf The bijection (3)}

Remember that

$T_{(Ξ³_T)} = Ξ»D.Ξ»g.((TC(\id_C));Rg)$, and so

$T_{(Ξ³_T)}D(g) = TC(\id_C);Rg$.

\msk

We want to check this:

$∀D.∀g.(T_{(Ξ³_T)}D(g) = TD(g))$, i.e.,

$∀D.∀g.(TC(\id_C);Rg = TD(g))$...

\msk

This is a consequence of $\sqcond_T$!

\newpage

%  _____ _          _    __   ___         _     _  _   _  _   
% |  ___(_)_ __ ___| |_  \ \ / / |    _  | |__ (_)(_) | || |  
% | |_  | | '__/ __| __|  \ V /| |   (_) | '_ \| || | | || |_ 
% |  _| | | |  \__ \ |_    | | | |___ _  | |_) | || | |__   _|
% |_|   |_|_|  |___/\__|   |_| |_____(_) |_.__/|_|/ |    |_|  
%                                               |__/          
%
% «first-yoneda-bijection-4» (to ".first-yoneda-bijection-4")
% (nyop 12 "first-yoneda-bijection-4")
% (nyo     "first-yoneda-bijection-4")

{\bf The bijection (4)}

We want to check this:

$∀D.∀g.(TC(\id_C);Rg = TD(g))$...

\msk

This is a consequence of $\sqcond_T$!

Look:

\msk

$\diag{yoneda-bij}$


\newpage


%  ____                     _               _   _            _     _  _ 
% |  _ \ _ __ __ ___      _(_)_ __   __ _  | |_| |__   ___  | |__ (_)(_)
% | | | | '__/ _` \ \ /\ / / | '_ \ / _` | | __| '_ \ / _ \ | '_ \| || |
% | |_| | | | (_| |\ V  V /| | | | | (_| | | |_| | | |  __/ | |_) | || |
% |____/|_|  \__,_| \_/\_/ |_|_| |_|\__, |  \__|_| |_|\___| |_.__/|_|/ |
%                                   |___/                          |__/ 
%
% «drawing-the-bijection» (to ".drawing-the-bijection")
% (nyop 13 "drawing-the-bijection")
% (nyo     "drawing-the-bijection")

{\bf Drawing the bijection}

A honest way to draw the bijection between `$Ξ³$'s and `$T$'s

would be diagram with the curved arrow in the middle...

But we will commit an abuse of (diagrammatical) language

and use a vertical arrow, as in the diagram at the right.

\msk

%D diagram yoneda-curve
%D 2Dx     100    +40
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> RC
%D 2D
%D 2D  +20 F1 -> F2
%D 2D             |
%D 2D             v
%D 2D  +25       F3
%D 2D
%D ren F1 F2 F3 ==> (C{→}\_) (A{→}R\_) \phantom{R}
%D
%D (( C RC |->
%D    A RC  -> .plabel= r Ξ³
%D    F1 F2 -> .plabel= b T
%D    F1 F2 midpoint A RC midpoint <-> .curve= ^14pt
%D ))
%D enddiagram

%D diagram yoneda-bij-vert
%D 2Dx     100    +40
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> RC
%D 2D
%D 2D  +20 F1 -> F2
%D 2D             |
%D 2D             v
%D 2D  +25       F3
%D 2D
%D ren F1 F2 F3 ==> (C{→}\_) (A{→}R\_) \phantom{R}
%D
%D (( A RC  -> .plabel= r Ξ³
%D    C RC |->
%D    F1 F2 -> .plabel= r T
%D    C F2 varrownodes nil 18 nil <->
%D ))
%D enddiagram

\pu

\resizebox{1.0\textwidth}{!}{%
$\diag{yoneda-R-5}
 \quad
 \diag{yoneda-curve}
 \quad
 \diag{yoneda-bij-vert}
$}

\msk

Now we have a \ColorRed{shape} for the (first) Yoneda Lemma

and we can use it to \ColorRed{compare several notations}...

But it's better to do that with the tree YLs at once,

so let's prove the other two.


\newpage

%            _      _                ____       _   
%   ___ __ _| |_   / \     _ _____  / ___|  ___| |_ 
%  / __/ _` | __| / _ \   (_)_____| \___ \ / _ \ __|
% | (_| (_| | |_ / ___ \   _|_____|  ___) |  __/ |_ 
%  \___\__,_|\__/_/   \_\ (_)       |____/ \___|\__|
%                                                   
% «changing-A-to-Set»  (to ".changing-A-to-Set")

{\bf Changing the category $\catA$ to $\Set$}

Remember that $A,RC∈\catA$ and $C∈\catC$...

This is not shown in the diagram, but it appears

in the terms and types in lots of places.

Let's take a particular case: $\catA$ becomes $\Set$...

In the notation of (simultaneous) substitution: $[\catA:=\Set]$.

The \ColorRed{diagram} does not change, but we can now

take a particular case of $A$ too: $[A:=1]$. We get:
%
%D diagram yoneda-curve
%D 2Dx     100    +40
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> RC
%D 2D
%D 2D  +20 F1 -> F2
%D 2D             |
%D 2D             v
%D 2D  +25       F3
%D 2D
%D ren F1 F2 F3 ==> (C{→}\_) (A{→}R\_) \phantom{R}
%D
%D (( C RC |->
%D    A RC  -> .plabel= r Ξ³
%D    F1 F2 -> .plabel= b T
%D    F1 F2 midpoint A RC midpoint <-> .curve= ^14pt
%D ))
%D enddiagram
%
%D diagram yoneda-curve-A:=1
%D 2Dx     100    +40
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> RC
%D 2D
%D 2D  +20 F1 -> F2
%D 2D             |
%D 2D             v
%D 2D  +25       F3
%D 2D
%D ren A ==> 1
%D ren F1 F2 F3 ==> (C{→}\_) (1{→}R\_) \phantom{R}
%D
%D (( C RC |->
%D    A RC  -> .plabel= r Ξ³
%D    F1 F2 -> .plabel= b T
%D    F1 F2 midpoint A RC midpoint <-> .curve= ^14pt
%D ))
%D enddiagram
%
\pu
$$
  \resizebox{!}{35pt}{$
  \left(\diag{yoneda-curve}\right)
  \bmat{\catA:=\Set \\ A:=1}
  \quad
  =
  \quad
  \left(
  \diag{yoneda-curve-A:=1}
  \right)
  $}
$$


\newpage

%   ____      _          _     _          __   _ 
%  / ___| ___| |_   _ __(_) __| |   ___  / _| / |
% | |  _ / _ \ __| | '__| |/ _` |  / _ \| |_  | |
% | |_| |  __/ |_  | |  | | (_| | | (_) |  _| | |
%  \____|\___|\__| |_|  |_|\__,_|  \___/|_|   |_|
%                                                
% «getting-rid-of-1»  (to ".getting-rid-of-1")
% (nyop 15 "getting-rid-of-1")
% (nyo     "getting-rid-of-1")

{\bf Getting rid of the `1's}

Convention: $1$ is the singleton set,

with single element $*$: $*∈1∈\Set$, $1=\{*\}$.

If $B∈\Set$ then an arrow $Ξ²:1→B$

``selects'' an element $b∈B$...

We have a bijection between elements of $b∈B$

and arrows $Ξ²:1→B$,

that we write as $B \bij (1{→}B)$,

or as two operations as $b:=Ξ²(*)$, $Ξ²:=Ξ»{*}.b$ ...

\msk

My favourite way to represent a bijection
$A \two/->`<-/<200>^f_g B$

\ColorRed{in a type system} is as a 6-uple $(A,B,f,g,𝐬{wdl},𝐬{wdr})$,

where $f:A→B$, $g:B→A$, and $𝐬{wdl}$ and $𝐬{wdr}$ \ColorRed{assure}

that $∀a∈A.(g∘f)(a)=a$ and $∀b∈A.(f∘g)(b)=b$

respectively.



\newpage

%  ____  _  _                       _   _               
% | __ )(_)(_)___    __ _ _ __   __| | (_)___  ___  ___ 
% |  _ \| || / __|  / _` | '_ \ / _` | | / __|/ _ \/ __|
% | |_) | || \__ \ | (_| | | | | (_| | | \__ \ (_) \__ \
% |____/|_|/ |___/  \__,_|_| |_|\__,_| |_|___/\___/|___/
%        |__/                                           
%
% «bijs-and-isos»  (to ".bijs-and-isos")
% (nyop 16 "bijs-and-isos")
% (nyo     "bijs-and-isos")

{\bf Bijections and isos in type systems}

One of my reasons for writing these notes was to show how these
diagrams can be interpreted \ColorRed{in a formal way} in type systems
and in proof assistants, so let me be type-ish for a moment...

\msk

% (find-books "__logic/__logic.el" "altenkirch")
% (find-altenkirchnttpage  3   "type of its evidence")
% (find-altenkirchntttext  3   "type of its evidence")

Thorsten Altenkirch --- in his book chapter ``NaÃ―ve Type Theory''
(from 2018(?), available from this home page) --- uses the notation
$⟦P⟧$ for the ``set of evidence'' for the proposition $P$.

\msk

I prefer to call $⟦P⟧$ the ``set of proofs'' of $P$ (which {\sl
  suggests} that we are in the BHK interpretation), or the ``set of
witnesses'' of $P$ (which {\sl suggests} a model with
proof-irrelevance and every $⟦P⟧$ being either empty or a
singleton)...

\msk

So...

\newpage

%  ____  _  _                       _   _                 ____  
% | __ )(_)(_)___    __ _ _ __   __| | (_)___  ___  ___  |___ \ 
% |  _ \| || / __|  / _` | '_ \ / _` | | / __|/ _ \/ __|   __) |
% | |_) | || \__ \ | (_| | | | | (_| | | \__ \ (_) \__ \  / __/ 
% |____/|_|/ |___/  \__,_|_| |_|\__,_| |_|___/\___/|___/ |_____|
%        |__/                                                   
%
% «bijs-and-isos-2»  (to ".bijs-and-isos-2")
% (nyop 17 "bijs-and-isos-2")
% (nyo     "bijs-and-isos-2")

{\bf Bijections and isos in type systems (2)}

So:
%
$$\begin{array}{rcl}
  (A \two/->`<-/<200>^f_g B)
  & = &
  \begin{array}[t]{l}
    (A,B,f,g,𝐬{wdl},𝐬{wdr}) \\
    \text{where:} \\
    A \text{ is a set}, \\
    B \text{ is a set}, \\
    f:A→B, \\
    g:B→A, \\
    𝐬{wdl}:⟦∀a∈A.(g∘f)(a)=a⟧, \\
    𝐬{wdr}:∀b∈B.(f∘g)(b)=b⟧. \\
  \end{array}
  \end{array}
$$

This is easy to adapt to define isos in a category.

$(A \diagxyto/<->/<200>^f B)$ is interpreted as $(A \two/->`<-/<200>^f_{f^{-1}} B)$.

\newpage

%   ____      _          _     _          __   _    ________  
%  / ___| ___| |_   _ __(_) __| |   ___  / _| / |  / /___ \ \ 
% | |  _ / _ \ __| | '__| |/ _` |  / _ \| |_  | | | |  __) | |
% | |_| |  __/ |_  | |  | | (_| | | (_) |  _| | | | | / __/| |
%  \____|\___|\__| |_|  |_|\__,_|  \___/|_|   |_| | ||_____| |
%                                                  \_\    /_/ 
% «getting-rid-of-1-2»  (to ".getting-rid-of-1-2")
% (nyop 18 "getting-rid-of-1-2")
% (nyo     "getting-rid-of-1-2")

{\bf Getting rid of the `1's (2)}

The (nameless) bijection $(1{→}B) \bij B$ can be interpreted as:
%
%D diagram nameless-bij
%D 2Dx     100   +25
%D 2D  100 1->B  Ξ²
%D 2D
%D 2D  +25 B     b
%D 2D
%D ren 1->B ==> (1{→}B)
%D
%D (( B 1->B <->
%D    b Ξ² |-> sl_ # .plabel= l down
%D    Ξ² b |-> sl_ # .plabel= r up
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{nameless-bij}
  \qquad
  \qquad
  \begin{array}[c]{l}
    b∈B \\
    Ξ²âˆˆ(1{→}B) \\
    b:=Ξ²(*) \\
    Ξ²:=Ξ»{*}.b \\
  \end{array}
$$

and written as:

$$B \two/->`<-/<300>^{Ξ»b.Ξ»{*}.b}_{λβ.Ξ²(*)} (1{→}B)
  \qquad
  \text{or}
  \qquad
  (1{→}B) \two/->`<-/<300>^{λβ.Ξ²(*)}_{Ξ»b.Ξ»{*}.b} B
$$

The components $𝐬{wdl}$ and $𝐬{wdr}$ of the 6-uples are treated

as ``obvious'', and are omitted.

\newpage



%   ____      _          _     _          __   _    _________  
%  / ___| ___| |_   _ __(_) __| |   ___  / _| / |  / /___ /\ \ 
% | |  _ / _ \ __| | '__| |/ _` |  / _ \| |_  | | | |  |_ \ | |
% | |_| |  __/ |_  | |  | | (_| | | (_) |  _| | | | | ___) || |
%  \____|\___|\__| |_|  |_|\__,_|  \___/|_|   |_| | ||____/ | |
%                                                  \_\     /_/ 
% «getting-rid-of-1-3»  (to ".getting-rid-of-1-3")
% (nyop 19 "getting-rid-of-1-3")
% (nyo     "getting-rid-of-1-3")

{\bf Getting rid of the `1's (3)}

If $R:\catC→\Set$ then we have a (nameless)

\ColorRed{natural transformation} $(1{→}R▁) \bij R$

between these functors:

%D diagram nameless-NT
%D 2Dx     100    +25   +35    +35
%D 2D  100 D1 |-> RD    D2 |-> FD
%D 2D      |       |    |       |
%D 2D      v       v    v       v
%D 2D  +25 E1 |-> RE    E2 |-> FE
%D 2D
%D 2D  +15 C1 -> Set1   C2 -> Set2
%D 2D
%D ren D1 E2 RD RE C1 Set1 ==> D E      RD       RE  \catC \Set
%D ren D2 E2 FD FE C2 Set2 ==> D E (1{→}RD) (1{→}RE) \catC \Set
%D
%D (( D1 RD |->
%D    D1 E1  -> .plabel= l h
%D    RD RE  -> .plabel= r Rh
%D    E1 RE |->
%D    C1 Set1 -> .plabel= a R
%D    D1 RE harrownodes nil 20 nil |->
%D    
%D    D2 FD |->
%D    D2 E2  -> .plabel= l h
%D    FD FE  -> .plabel= r \sm{(1{→}R▁)(h)\;\;\\:=\;Ξ»Ξ∧.(Ξ∧;Rh)}
%D    E2 FE |->
%D    C2 Set2 -> .plabel= a (1{→}R▁)
%D    D2 FE harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{nameless-NT}
$$

\msk

Note that in type theory $R = (R_0,R_1,\dots)$,

$(1{→}R▁) = ((1{→}R▁)_0, \, (1{→}R▁)_1\, ,\dots)$,

and the diagrams above give us enough information

to let us build $(1{→}R▁)$ as a term.



%   ____      _          _     _          __   _    ___  _ __  
%  / ___| ___| |_   _ __(_) __| |   ___  / _| / |  / / || |\ \ 
% | |  _ / _ \ __| | '__| |/ _` |  / _ \| |_  | | | || || |_| |
% | |_| |  __/ |_  | |  | | (_| | | (_) |  _| | | | ||__   _| |
%  \____|\___|\__| |_|  |_|\__,_|  \___/|_|   |_| | |   |_| | |
%                                                  \_\     /_/ 
%
% «getting-rid-of-1-4»  (to ".getting-rid-of-1-4")
% (nyop 20 "getting-rid-of-1-4")
% (nyo     "getting-rid-of-1-4")

{\bf Getting rid of the `1's (4)}

If $R:\catC→\Set$ then we have a (nameless)

\ColorRed{natural isomorphism} $(1{→}R▁) \bij R$

between the functors defined in the previous page...

If $F,G:\catA→\catB$ then a natural transformation $T:F→G$

is formalized in TT as a pair $(T_0,\sqcond_T)$,

where $T_0$ is its ``action on objects''

and $\sqcond_T$ is its ``square condition''.

The nameless natual iso $(1{→}R▁) \bij R$ can be interpreted as

a \ColorRed{nameless NT} $(1{→}R▁) → R$,

a \ColorRed{nameless NT} $R → (1{→}R▁)$,

and guarantees that their composites are identity functors...



\newpage

%   ____      _          _     _          __   _    ________  
%  / ___| ___| |_   _ __(_) __| |   ___  / _| / |  / / ___\ \ 
% | |  _ / _ \ __| | '__| |/ _` |  / _ \| |_  | | | ||___ \| |
% | |_| |  __/ |_  | |  | | (_| | | (_) |  _| | | | | ___) | |
%  \____|\___|\__| |_|  |_|\__,_|  \___/|_|   |_| | ||____/| |
%                                                  \_\    /_/ 
%
% «getting-rid-of-1-5»  (to ".getting-rid-of-1-5")
% (nyop 21 "getting-rid-of-1-5")
% (nyo     "getting-rid-of-1-5")

{\bf Getting rid of the `1's (5)}

The nameless natual iso $(1{→}R▁) \bij R$ can be interpreted as

a \ColorRed{nameless NT} $(1{→}R▁) → R$,

a \ColorRed{nameless NT} $R → (1{→}R▁)$,

and guarantees that their composites are identity functors...

\msk

Their actions on objects can be defined from this:

$((1{→}R▁) → R)_0(D) : (1{→}RD) → RD)$

$((1{→}R▁) → R)_0(D) = Ξ»Ξ∧.Ξ∧(*)$

$(R → (1{→}R▁))_0(D) : D → (1{→}RD)$

$(R → (1{→}R▁))_0(D) = Ξ»d.Ξ»{*}.d$

\msk

(I will omit the details)

\newpage

%            _      _                ____       _      ________  
%   ___ __ _| |_   / \     _ _____  / ___|  ___| |_   / /___ \ \ 
%  / __/ _` | __| / _ \   (_)_____| \___ \ / _ \ __| | |  __) | |
% | (_| (_| | |_ / ___ \   _|_____|  ___) |  __/ |_  | | / __/| |
%  \___\__,_|\__/_/   \_\ (_)       |____/ \___|\__| | ||_____| |
%                                                     \_\    /_/ 
%
% «changing-A-to-Set-2»  (to ".changing-A-to-Set-2")
% (nyop 22 "changing-A-to-Set-2")
% (nyo     "changing-A-to-Set-2")

{\bf Changing the category $\catA$ to $\Set$ (2)}

With the nameless natural iso $(1{→}R▁) \bij R$

we can add an extra level to the basement our diagram,

and this yields \ColorRed{an ``obvious'' bijection between `$Ξ³$'s and `$T'$'s}.

This new diagram ``is'' our \ColorRed{Second Yoneda Lemma}.

%D diagram yoneda-curve-A:=1-tall
%D 2Dx     100    +40
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> RC
%D 2D
%D 2D  +20 F1 -> F2
%D 2D             |
%D 2D             v
%D 2D  +25       F3
%D 2D
%D ren A ==> 1
%D ren F1 F2 F3 ==> (C{→}\_) (1{→}R\_) \phantom{R}
%D
%D (( C RC |->
%D    A RC  -> .plabel= r Ξ³
%D    F1 F2 -> .plabel= b T
%D    F1 F2 midpoint A RC midpoint <-> .curve= ^14pt
%D    F3 place
%D ))
%D enddiagram
%
%D diagram yoneda-2-curve
%D 2Dx     100    +40
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> RC
%D 2D
%D 2D  +20 F1 -> F2
%D 2D             |
%D 2D             v
%D 2D  +25       F3
%D 2D
%D ren A ==> 1
%D ren F1 F2 F3 ==> (C{→}\_) (1{→}R\_) R
%D
%D (( C RC |->
%D    A RC  -> .plabel= r Ξ³
%D    F1 F2 -> .plabel= b T
%D    F1 F2 midpoint A RC midpoint <-> .curve= ^14pt
%D    F2 F3 <->
%D    F1 F3 -> .plabel= l T'
%D ))
%D enddiagram
%
\pu
$$
  %\resizebox{!}{70pt}{$
  \diag{yoneda-curve-A:=1-tall}
  \qquad
  \diag{yoneda-2-curve}
  %$}
$$

\newpage

%  ____               ______      ____  
% |  _ \   _ _____   / / __ )     \ \ \ 
% | |_) | (_)_____| | ||  _ \ _____\ \ |
% |  _ <   _|_____| | || |_) |_____/ / |
% |_| \_\ (_)       | ||____/     /_/| |
%                    \_\            /_/ 
%
% «changing-R-to-Bto»  (to ".changing-R-to-Bto")
% (nyop 23 "changing-R-to-Bto")
% (nyo     "changing-R-to-Bto")

{\bf Changing $R$ to $(B{→})$}

Choose an object $B∈\catC$.

It induces a functor $(B{→}): \catC→\Set$.

Several slides ago we did this substitution

on the diagram of the first Yoneda Lemma:
%
$$\bmat{\catA \;:=\; \Set \\ A \;:=\; 1}$$
%
Now we will do this substitution

on the diagram of the second Yoneda Lemma:
%
$$\bmat{R \;:=\; (B{→})}$$
%
very little will change \ColorRed{in the diagram},

but a lot will change in the terms and types.


\newpage


%  ____               ______      ____  
% |  _ \   _ _____   / / __ )     \ \ \ 
% | |_) | (_)_____| | ||  _ \ _____\ \ |
% |  _ <   _|_____| | || |_) |_____/ / |
% |_| \_\ (_)       | ||____/     /_/| |
%                    \_\            /_/ 
%
% «changing-R-to-Bto-2»  (to ".changing-R-to-Bto-2")
% (nyop 24 "changing-R-to-Bto-2")
% (nyo     "changing-R-to-Bto-2")

{\bf Changing $R$ to $(B{→})$ (2)}

After the substitution $\bmat{R \;:=\; (B{→})}$

the diagram for the Second Yoneda Lemma (left) becomes

the diagram for the \ColorRed{Third Yoneda Lemma} (right):
%
%D diagram yoneda-3-curve
%D 2Dx     100    +45
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> RC
%D 2D
%D 2D  +20 F1 -> F2
%D 2D             |
%D 2D             v
%D 2D  +25       F3
%D 2D
%D ren A RC ==> 1 (B{→}C)
%D ren F1 F2 F3 ==> (C{→}\_) (1{→}(B{→}\_)) (B{→}▁)
%D
%D (( C RC |->
%D    A RC  -> .plabel= r Ξ³
%D    F1 F2 -> .plabel= b T
%D    F1 F2 midpoint A RC midpoint <-> .curve= ^14pt
%D    F2 F3 <->
%D    F1 F3 -> .plabel= l T'
%D ))
%D enddiagram
%
\pu
$$
  \resizebox{!}{45pt}{$
  \diag{yoneda-2-curve}
  \qquad
  \diag{yoneda-3-curve}
  $}
$$
%
Our Third Yoneda Lemma is usually \ColorRed{stated} as this bijection:

$(B{→}C) \bij ((C{→}▁) → (B{→}▁))$, where the right side is

the \ColorRed{space of natural transformations} from $(C{→}▁)$ to $(B{→}▁))$.

\newpage


%  ____                _ _             
% |  _ \ ___  __ _  __| (_)_ __   __ _ 
% | |_) / _ \/ _` |/ _` | | '_ \ / _` |
% |  _ <  __/ (_| | (_| | | | | | (_| |
% |_| \_\___|\__,_|\__,_|_|_| |_|\__, |
%                                |___/ 
%
% «reading»  (to ".reading")
% (nyop 25 "reading")
% (nyo     "reading")

\vspace*{20pt}

\begin{center}
\Huge{\bf READING}   \\[0pt]
\Huge{\bf INTERNAL} \\
\Huge{\bf DIAGRAMS} \\
\end{center}

\thispagestyle{empty}

\newpage

%  ____  _       _                    _       
% | __ )| | ___ | |__        ___  ___| |_ ___ 
% |  _ \| |/ _ \| '_ \ _____/ __|/ _ \ __/ __|
% | |_) | | (_) | |_) |_____\__ \  __/ |_\__ \
% |____/|_|\___/|_.__/      |___/\___|\__|___/
%                                             
% «blob-sets»  (to ".blob-sets")

{\bf Motivation: blob-sets}

% (oxap 3 "internal-diagrams")
% (oxa    "internal-diagrams")
% (oxap 4 "fig:internal-1")
% (oxa    "fig:internal-1")

\def\ooo(#1,#2){\begin{picture}(0,0)\put(0,0){\oval(#1,#2)}\end{picture}}
\def\oooo(#1,#2){{\setlength{\unitlength}{1ex}\ooo(#1,#2)}}
%
%D diagram second-blob-function
%D 2Dx     100 +20   +20   
%D 2D  100 a-1 |-->  b-1    
%D 2D  +08 a0  |-->  b0    
%D 2D  +08 a1  |-->  b1    
%D 2D  +08 a2  |-->  b2    
%D 2D  +08 a3  |-->  b3    
%D 2D  +08 a4  |-->  b4    
%D 2D  +14 a5  |-->  b5    
%D 2D  +25 \N  --->  \R
%D 2D
%D ren a-1 a0 a1 a2 a3 a4 a5 ==> -1 0 1 2 3 4 n
%D ren b-1 b0 b1 b2 b3 b4 b5 ==> -1 0 1 \sqrt{2} \sqrt{3} 2 \sqrt{n}
%D ((  a0 a5 midpoint .TeX= \oooo(7,23) y+= -2 place
%D    b-1 b5 midpoint .TeX= \oooo(7,25) y+= -2 place
%D       b-1 place
%D    a0 b0 |->
%D    a1 b1 |->
%D    a2 b2 |->
%D    a3 b3 |->
%D    a4 b4 |->
%D    a5 b5 |->
%D    \N \R -> .plabel= a \sqrt{\phantom{a}}
%D    a-1 relplace -7 -7 \phantom{foo}
%D    b5  relplace  7  7 \phantom{bar}
%D ))
%D enddiagram
%D
\pu
$$\begin{array}{rrcl}
   \sqrt{\;\;}: & \N &→& \R \\
                &  n &↦& \sqrt{n} \\
   \end{array}
   \qquad
   \diag{second-blob-function}
$$

\newpage

%  ____  _       _                _         ____  
% | __ )| | ___ | |__    ___  ___| |_ ___  |___ \ 
% |  _ \| |/ _ \| '_ \  / __|/ _ \ __/ __|   __) |
% | |_) | | (_) | |_) | \__ \  __/ |_\__ \  / __/ 
% |____/|_|\___/|_.__/  |___/\___|\__|___/ |_____|
%                                                 
% «blob-sets-2»  (to ".blob-sets-2")

{\bf Motivation: blob-sets (2)}

\msk

``Internal diagrams are a tool that lets us \ColorRed{lower the level
  of abstraction}. (...) Look at the figure at the left in the
previous slide and compare its `$\N→\R$' in the upper line (the
external view), with the `$n↦\sqrt{n}$' in the lower line (the
internal view); the \ColorRed{$n↦\sqrt{n}$} shows a (generic) element
and its image.

\msk

The figure at the right shows the external view at the bottom and an
internal view at the top; note that all elements in the blobs for $\N$
and $\R$ are named, but only a few of the elements are shown (...) the
arrows like \ColorRed{$3↦\sqrt3$} and \ColorRed{$4↦2$}, that show
elements and their images, are \ColorRed{substitution instances of the
  generic $n↦\sqrt{n}$, maybe after some calculations (or
  ``reductions'' in $Ξ»$-calculus terminology)}.''

\newpage

% «internal-view-functor»  (to ".internal-view-functor")

{\bf The internal view of a functor}

We \ColorRed{usually} draw internal views above external views,

general cases at the left, particular cases at the right.

Remember that a functor $F:\catC→\catD$

is a 4-uple: $(F0,F1,\respids_F,\respcomp_F)$.

The diagram at the right below \ColorRed{defines} $(X{×})$. How?


%D diagram functor
%D 2Dx        100   +30     +30  +30
%D 2D  100    A |-> FA      B0   B1
%D 2D
%D 2D  +30    B |-> FB      B2   B3
%D 2D
%D 2D  +20 \catC -> \catD   C1   C2
%D ren B0 B1 ==> Y X{×}Y
%D ren B2 B3 ==> Z X{×}Z
%D ren C1 C2 ==> \Set \Set
%D 
%D (( A FA |-> .plabel= a F_0
%D    A B   -> .plabel= l g
%D    FA FB -> .plabel= r Fg
%D    B FB |-> .plabel= b F_0
%D    A FB harrownodes nil 20 nil |-> .plabel= a F_1
%D    \catC \catD -> .plabel= a F
%D
%D    B0 B1 |->
%D    B0 B2  -> .plabel= l f
%D    B1 B3  -> .plabel= r 〈π,f∘π'〉
%D    B2 B3 |->
%D    B0 B3 harrownodes nil 20 nil |->
%D    C1 C2  -> .plabel= a (X{×})
%D ))
%D enddiagram
\pu
$$
  \diag{functor}
$$

\newpage

% «internal-view-functor-2»  (to ".internal-view-functor-2")

{\bf The internal view of a functor (2)}

%D diagram functor-2
%D 2Dx        100   +30     +30  +30   +35  +35
%D 2D  100    A |-> FA      B0   B1    D0   D1
%D 2D
%D 2D  +30    B |-> FB      B2   B3    D2   D3
%D 2D
%D 2D  +20 \catC -> \catD   C1   C2    E1   E2
%D ren B0 B1 ==> Y X{×}Y
%D ren B2 B3 ==> Z X{×}Z
%D ren C1 C2 ==> \Set \Set
%D 
%D ren D0 D1 ==> Y (X{×})_0(Y)
%D ren D2 D3 ==> Z (X{×})_0(Z)
%D ren E1 E2 ==> \Set \Set
%D 
%D (( A FA |-> .plabel= a F_0
%D    A B   -> .plabel= l g
%D    FA FB -> .plabel= r Fg
%D    B FB |-> .plabel= b F_0
%D    A FB harrownodes nil 20 nil |-> .plabel= a F_1
%D    \catC \catD -> .plabel= a F
%D
%D    B0 B1 |-> .plabel= a (X{×})_0
%D    B0 B2  -> .plabel= l f
%D    B1 B3  -> .plabel= r 〈π,f∘π'〉
%D    B2 B3 |-> .plabel= a (X{×})_0
%D    B0 B3 harrownodes nil 20 nil |-> .plabel= a (X{×})_1
%D    C1 C2  -> .plabel= a (X{×})
%D
%D    D0 D1 |-> .plabel= a (X{×})_0
%D    D0 D2  -> .plabel= l f
%D    D1 D3  -> .plabel= r (X{×})_1(f)
%D    D2 D3 |-> .plabel= a (X{×})_0
%D    D0 D3 harrownodes nil 20 nil |-> .plabel= a (X{×})_1
%D    E1 E2  -> .plabel= a (X{×})
%D ))
%D enddiagram
\pu

Compare:

\msk

$
  \resizebox{!}{30pt}{$
  \diag{functor}
  $}
$

\bsk

$
  \resizebox{!}{30pt}{$
  \diag{functor-2}
  $}
$

\bsk

So $(X{×})_0 = Ξ»Y.(X×Y)$,

and $(X{×})_1 = Ξ»f.〈π,f∘π'〉$.


\newpage

% «internal-view-to-do»  (to ".internal-view-to-do")

{\bf TO DO: internal diagrams of NTs and adjunctions}

(I have lots of those diagrams --- plus monads, etc ---

but I never explained the conventions in them very clearly...)

\msk

This is an adjunction:

\bsk

%D
%D diagram adjunction
%D 2Dx     100 +20    +30 +20
%D 2D  100 A1  B1 <-| B2  C1
%D 2D      |   |       |   |
%D 2D      |   |  <->  |   |
%D 2D      v   v       v   v
%D 2D  +30 A2  B3 |-> B4  C2
%D 2D
%D 2D  +20     D1 <=> D2
%D 2D
%D ren A1 A2 ==> LRB B
%D ren B1 B2 B3 B4 ==> LA A B RB
%D ren C1 C2 ==> A RLA
%D ren D1 D2 ==> \catB \catA
%D
%D (( A1 A2 -> .plabel= l Ξ΅B
%D    C1 C2 -> .plabel= r Ξ·A
%D
%D    B1 B2 <-| .plabel= a L_0
%D    B1 B3 ->  .plabel= l f
%D    B2 B4 ->  .plabel= r g
%D    B3 B4 |-> .plabel= b R_0
%D    B1 B4 harrownodes nil 20 nil <-| sl^ .plabel= a ♭_{AB}
%D    B1 B4 harrownodes nil 20 nil |-> sl_ .plabel= b â™―_{AB}
%D
%D    D1 D2 <- sl^ .plabel= a L
%D    D1 D2 -> sl_ .plabel= b R
%D    
%D ))
%D enddiagram
\pu
$$
   \diag{adjunction}
$$


\newpage



%  _   _ _____ _     ____    _   _ _____ _____ ____  _____ ____  
% | | | | ____| |   |  _ \  | \ | | ____| ____|  _ \| ____|  _ \ 
% | |_| |  _| | |   | |_) | |  \| |  _| |  _| | | | |  _| | | | |
% |  _  | |___| |___|  __/  | |\  | |___| |___| |_| | |___| |_| |
% |_| |_|_____|_____|_|     |_| \_|_____|_____|____/|_____|____/ 
%                                                                
% «help-needed»  (to ".help-needed")
% (nyop 25 "help-needed")
% (nyo     "help-needed")

\vspace*{30pt}

\begin{center}
\Huge{\bf HELP}   \\[0pt]
\Huge{\bf NEEDED} \\
\end{center}

\thispagestyle{empty}

\newpage

{\bf Help needed: proof assistants}

I was never able to learn enough Coq or Agda...

I \ColorRed{guess} that it would be easy to formalize the figure with
the three Yoneda Lemmas in Coq or Agda. We can number its objects as
%
$$\begin{tabular}{cccccccc}
      & o11  &&      & o21  &&     & o31 \\
  o12 & o13  &&  o22 & o23  && o32 & o33 \\
  \\
  o14 & o15  &&  o24 & o25  && o34 & o35 \\
      &      &&      & o26  &&     & o36 \\
  \end{tabular}
$$
%
and choose some convention for the ascii names for arrows, and for the
ascii names for arrows between arrows.

\newpage

{\bf Help needed: proof assistants (2)}

Smart proof assistants should be able to find by themselves the proofs
that we said that were ``obvious''. Besides the obvious
\ColorRed{proofs} I've said that some \ColorRed{constructions} are
``obvious''. Finding obvious ``constructions'' needs term inference
instead of proof inference, and implementation of term inference are
rare.


\newpage

{\bf Help needed: Agda}

There are several implementation of CT in Agda.

There is even a ``Big list of formalizations of Category Theory in
proof assistants'' in MathOverflow!

I'm trying to read --- with Juan Meleiro --- a big blog post by Jannis
Limpberg called ``Yoneda's Lemma in Excruciating Detail'', that has an
implementation in Agda.

\msk

We will try to:

1. draw its diagrams in our favourite shapes,

2. assign coordinates to some of his terms,

3. sketch a way to read our 2D diagrams directly in Agda...


\newpage


%  _     _                 _                    
% | |   (_)_ __ ___  _ __ | |__   ___ _ __ __ _ 
% | |   | | '_ ` _ \| '_ \| '_ \ / _ \ '__/ _` |
% | |___| | | | | | | |_) | |_) |  __/ | | (_| |
% |_____|_|_| |_| |_| .__/|_.__/ \___|_|  \__, |
%                   |_|                   |___/ 
%
% «limpberg»  (to ".limpberg")
% (nyop 1 "title-page")
% (nyo    "title-page")

\def\Ap{\mathrm{Ap}}
\def\Sets{\mathbf{Sets}}


{\bf Jannis Limpberg}

``Yoneda's Lemma in Excruciating Detail'' (blog post):

\url{https://limperg.de/posts/2018-07-27-yoneda.html}

The functor $\Ap$:

%D diagram Ap
%D 2Dx     100    +35      +40 +20   +30
%D 2D  100 A0 |-> A1       C1  D0 -> D1
%D 2D      |       |       |   |      |
%D 2D      |  |->  |       |   |      |
%D 2D      v       v       v   v      v
%D 2D  +25 A2 |-> A3       C2  D2 -> D3
%D 2D
%D 2D  +20 B1 --> B2           E1 -> E2
%D 2D
%D ren A0 A1 ==> (F,C) FC
%D ren A2 A3 ==> (G,D) GD
%D ren B1 B2 ==> (\catC{→}\catD){×}\catC \catD
%D
%D ren C1 C2 ==> C D
%D ren D0 D1 D2 D3 ==> FC GC FD GD
%D ren E1 E2 ==> F G
%D
%D (( A0 A1 |->
%D    A0 A2  -> .plabel= l (ΞΈ,f)
%D    A1 A3  -> .plabel= r Gfâˆ˜ΞΈ_C
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |->
%D    B1 B2  -> .plabel= a \Ap
%D
%D    C1 C2  -> .plabel= l f
%D    D0 D1  -> .plabel= a ΞΈ_C
%D    D0 D2  -> .plabel= l Ff
%D    D1 D3  -> .plabel= r Gf
%D    D2 D3  -> .plabel= a ΞΈ_D
%D    E1 E2  -> .plabel= a ΞΈ
%D ))
%D enddiagram
%D
$$\pu
  \diag{Ap}
$$

\newpage

{\bf Jannis Lindberg (2)}

The functor $\Hom$:


%D diagram Hom
%D 2Dx     100 +10   +30    +45   +45   
%D 2D  100 C1  D1    A0 |-> A1    H1    
%D 2D      ^   |     |       |    -     
%D 2D      |   |     |  |->  |    |     
%D 2D      |   v     v       v    v     
%D 2D  +25 C2  D2    A2 |-> A3    H2    
%D 2D                                   
%D 2D  +20           B1 --> B2          
%D 2D
%D ren A0 A1 ==> (C,D)   \Hom(C,D)
%D ren A2 A3 ==> (C',D') \Hom(C',D')
%D ren B1 B2 ==> \catC^\op{×}\catC \Sets
%D ren C1 C2 ==> C C'
%D ren D1 D2 ==> D D'
%D ren H1 H2 ==> h g∘h∘f
%D
%D (( A0 A1 |->
%D    A0 A2  -> .plabel= l (f,g)
%D    A1 A3  -> .plabel= r Ξ»h.(g∘h∘f)
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |->
%D    B1 B2  -> .plabel= a \Ap
%D
%D    C1 C2  <- .plabel= l f
%D    D1 D2  -> .plabel= r g
%D    H1 H2 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{Hom}
$$


\newpage


{\bf Jannis Limpberg (3)}

The functor $y$:



%D diagram y
%D 2Dx     100    +40   +40 +30    +55 +30    +30
%D 2D  100 A0 |-> A1    C1  E0 --> E1  F0 |-> F1
%D 2D      |       |    ^   |       |  -       -
%D 2D      |  |->  |    |   |       |  |       |
%D 2D      v       v    |   v       v  v       v
%D 2D  +25 A2 |-> A3    C2  E2 --> E3  F2 |-> F3
%D 2D                         
%D 2D  +20 B1 --> B2        D1 --> D2 
%D 2D
%D ren A0 A1 ==> D  \Hom(‒,D)
%D ren A2 A3 ==> D' \Hom(‒,D')
%D ren B1 B2 ==> \catC \catC^\op{⇒}\Sets
%D
%D ren C1 C2 ==> C C'
%D ren D1 D2 ==> \Hom(‒,D) \Hom(‒,D')
%D ren E0 E1 ==> \Hom(C,D) \Hom(C,D')
%D ren E2 E3 ==> \Hom(C',D) \Hom(C',D')
%D
%D ren F0 F1 F2 F3 ==> h f∘h h∘g f∘h∘g
%D
%D (( A0 A1 |->
%D    A0 A2  -> .plabel= l f
%D    A1 A3  -> .plabel= r yf
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |->
%D    B1 B2  -> .plabel= a y
%D
%D    C1 C2  <- .plabel= l g
%D    D1 D2  -> .plabel= a yf
%D    E0 E1  -> .plabel= a (yf)_C
%D    E0 E2  -> .plabel= l (yD)(g)
%D    E1 E3  -> .plabel= r (yD')(g)
%D    E2 E3  -> .plabel= a (yf)_{C'}
%D    
%D    F0 F1 |-> F0 F2 |-> F1 F3 |-> F2 F3 |->
%D ))
%D enddiagram
%D
$$\pu
  \resizebox{0.9\textwidth}{!}{$
    \diag{y}
  $}
$$


% (find-es "agda" "limpberg-yoneda")
% (find-limpbergpage)
% (find-limpbergtext)
% (find-limpbergpage 8)
% (find-limpbergtext 8)



\newpage


%  ____  _      _   _                        _           
% |  _ \(_) ___| |_(_) ___  _ __   __ _ _ __(_) ___  ___ 
% | | | | |/ __| __| |/ _ \| '_ \ / _` | '__| |/ _ \/ __|
% | |_| | | (__| |_| | (_) | | | | (_| | |  | |  __/\__ \
% |____/|_|\___|\__|_|\___/|_| |_|\__,_|_|  |_|\___||___/
%                                                        
% «dictionaries»  (to ".dictionaries")
% (nyop 25 "help-needed")
% (nyo     "help-needed")

\vspace*{40pt}

\begin{center}
\Huge{\bf DICTIONARIES}
\end{center}

\thispagestyle{empty}

\newpage

%  ____                             _                      
% / ___|  __ _ _ __ ___   ___   ___| |__   __ _ _ __   ___ 
% \___ \ / _` | '_ ` _ \ / _ \ / __| '_ \ / _` | '_ \ / _ \
%  ___) | (_| | | | | | |  __/ \__ \ | | | (_| | |_) |  __/
% |____/ \__,_|_| |_| |_|\___| |___/_| |_|\__,_| .__/ \___|
%                                              |_|         
% «same-shape»  (to ".same-shape")

{\bf Same shape, several notations}

Now that we have a \ColorRed{shape} for the three Yoneda Lemmas we can
change the \ColorRed{notation} --- i.e., what is written in each of
the nodes that we named o11, o12, $\ldots$, o36 a few slides ago, and
also change what is written in the arrows...

\msk

For typographical reasons --- I don't have good ways to put labels
along curved arrows --- I will have to commit the abuse of
diagrammatical language explained in the slide ``Drawing the
bijection'' (p.13), and draw the curved bijections as just their
vertical-ish lower halves.


\newpage

%   ______        ____  __ 
%  / ___\ \      / /  \/  |
% | |    \ \ /\ / /| |\/| |
% | |___  \ V  V / | |  | |
%  \____|  \_/\_/  |_|  |_|
%                          
% «CWM»  (to ".CWM")
% (nyop 30 "CWM")
% (nyo     "CWM")
% (cwmp 11 "yoneda-L")
% (cwm     "yoneda-L")

{\bf Categories for the Working Mathematician}

Here is how MacLane states our YLs in his CWM.

Our first YL is implicit in his Proposition 1 in p.59:

% (find-cwm2page (+ 13  59) "Proposition 1")
% (find-cwm2text (+ 13  59) "Proposition 1")

  \begin{quote}

  {\bf Proposition 1.} {\sl For a functor $S: D→C$ a pair $〈r,u:
      c→Sr〉$ is universal from $c$ to $S$ if and only if the function
    sending each $f': r → d$ into $Sf'u: c → Sd$ is a bijection of
    hom-sets}

  \msk

  \def\fakeeqn#1#2{\hfill#1\hfill\llap{(#2)}}
  \fakeeqn {$D(r,d) ≅ C(c, Sd).$} {1}

  \msk

  {\sl This bijection is natural in $d$. Conversely, given $r$ and
    $c$, any natural isomorphism (1) is determined in this way by a
    unique arrow $u: c→Sr$ such that $〈r,u〉$ is universal from $c$ to
    $S$.}

  \end{quote}

\newpage

%   ______        ____  __    ________  
%  / ___\ \      / /  \/  |  / /___ \ \ 
% | |    \ \ /\ / /| |\/| | | |  __) | |
% | |___  \ V  V / | |  | | | | / __/| |
%  \____|  \_/\_/  |_|  |_| | ||_____| |
%                            \_\    /_/ 
%
% «CWM-2»  (to ".CWM-2")
% (nyop 31 "CWM-2")
% (nyo     "CWM-2")

{\bf Categories for the Working Mathematician (2)}

Our second YL appears in p.61 of CWM, as this:

% (find-cwm2page (+ 13  61) "Lemma (Yoneda)")
% (find-cwm2text (+ 13  61) "Lemma (Yoneda)")
% (find-es "tex" "eqnarray")

\def\tnto{\ton{\scriptscriptstyle‒}}

  \begin{quote}

  {\bf Lemma} {\sl (Yoneda). If $K:D→\Set$ is a functor from $D$ and
    $r$ an object in $D$ (for $D$ a category with small hom-sets),
    there is a bijection
  %
  $$y: \Nat(D(r, -), K) ≅ Kr$$
  %
  which sends each natural transformation $Ξ±:D(r,-) \tnto K$ to
  $Ξ±_r1_r$, the image of the identity $r→r$.}

  \end{quote}


\newpage

%   ______        ____  __    _________  
%  / ___\ \      / /  \/  |  / /___ /\ \ 
% | |    \ \ /\ / /| |\/| | | |  |_ \ | |
% | |___  \ V  V / | |  | | | | ___) || |
%  \____|  \_/\_/  |_|  |_| | ||____/ | |
%                            \_\     /_/ 
% «CWM-3»  (to ".CWM-3")
% (nyop 32 "CWM-3")
% (nyo     "CWM-3")

{\bf Categories for the Working Mathematician (3)}

Our third YL also appears in p.61 of CWM, as a corollary:

% (find-cwm2page (+ 13  61) "Corollary")
% (find-cwm2text (+ 13  61) "Corollary")

  \begin{quote}

  {\bf Corollary.} {\sl For objects $r, s∈D$, each natural
    transformation $D(r, - ) → D(s, -)$ has the form $D(h, -)$ for a
    unique arrow $h: s→r$.}

  \end{quote}

\newpage

%   ______        ____  __       _  _   
%  / ___\ \      / /  \/  |     | || |  
% | |    \ \ /\ / /| |\/| |_____| || |_ 
% | |___  \ V  V / | |  | |_____|__   _|
%  \____|  \_/\_/  |_|  |_|        |_|  
%                                       
% «CWM-4»  (to ".CWM-4")
% (nyop 33 "CWM-4")
% (nyo     "CWM-4")
% (cwmp 11 "yoneda-L")
% (cwm     "yoneda-L")


{\bf Categories for the Working Mathematician (4)}

%D diagram yonedas-CWM
%D 2Dx     100    +35      +35    +45     +35    +45
%D 2D  100        A1              C1             E1
%D 2D              |               |              |
%D 2D              v               v              v
%D 2D  +30 A2 |-> A3       C2 |-> C3      E2 |-> E3
%D 2D
%D 2D         ^ |             ^ |            ^ |
%D 2D         | |     --->    | |    --->    | |
%D 2D         | v             | v            | v
%D 2D
%D 2D  +30 B1 --> B2       D1 --> D2      F1 --> F2
%D 2D          \   |           \   |          \   |
%D 2D           v  v            v  v           v  v
%D 2D  +30        B3              D3             F3    
%D 2D
%D ren A1 A2 A3 ==> c r Sr
%D ren C1 C2 C3 ==> * r Kr
%D ren E1 E2 E3 ==> * r D(s,r)
%D ren B1 B2    ==> D(r,-) C(c,S-)
%D ren D1 D2 D3 ==> D(r,-) \Set(*,K-) K
%D ren F1 F2 F3 ==> D(r,-) \Set(*,D(s,-)) D(s,-)
%D
%D (( A2 A3 |-> A1 A3 -> .plabel= r u
%D    C2 C3 |-> C1 C3 -> .plabel= r u
%D    E2 E3 |-> E1 E3 -> .plabel= r f
%D    B1 B2 -> .plabel= b T
%D    D1 D2 -> D2 D3 <-> D1 D3 -> .plabel= b T'
%D    F1 F2 -> F2 F3 <-> F1 F3 -> .plabel= b D(f,-)
%D
%D    A2 B2 varrownodes nil 17 nil |-> sl_
%D    A2 B2 varrownodes nil 17 nil <-| sl^
%D    C2 D2 varrownodes nil 17 nil |-> sl_
%D    C2 D2 varrownodes nil 17 nil <-| sl^ .plabel= r y
%D    E2 F2 varrownodes nil 17 nil |-> sl_ .plabel= l Y
%D    E2 F2 varrownodes nil 17 nil <-| sl^
%D ))
%D enddiagram
%D
$$\pu
  \resizebox{275pt}{!}{$
  \diag{yonedas-CWM}
  $}
$$



% «awodey»  (to ".awodey")
% (find-books "__cats/__cats.el" "awodey")
% (find-awodeyctpage (+ 10 160) "8.2 The Yoneda embedding")
% (find-awodeycttext          "\n8.2 The Yoneda embedding")

% «riehl»  (to ".riehl")
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 49) "2. Universal Properties, Representability, and the Yoneda Lemma")
% (find-riehlccpage (+ 18 50) "2.1. Representable functors")
% (find-riehlccpage (+ 18 55) "2.2. The Yoneda lemma")
% (find-riehlccpage (+ 18 60)      "Corollary 2.2.8 (Yoneda embedding)")
% (find-riehlcctext (+ 18 60)      "Corollary 2.2.8 (Yoneda embedding)")

%L write_dnt_file()
\pu




\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-tla: "nyo"
% End: