Warning: this is an htmlized version! The original is here, and the conversion rules are here.
% (find-LATEX "2020notes-yoneda.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020notes-yoneda.tex" :end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2020notes-yoneda.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020notes-yoneda.pdf"))
% (defun e () (interactive) (find-LATEX "2020notes-yoneda.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020notes-yoneda"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page   "~/LATEX/2020notes-yoneda.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020notes-yoneda.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020notes-yoneda.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020notes-yoneda.pdf
%               file:///tmp/2020notes-yoneda.pdf
%           file:///tmp/pen/2020notes-yoneda.pdf
% http://angg.twu.net/LATEX/2020notes-yoneda.pdf
% (find-LATEX "2019.mk")
%
%   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")
%
% «.the-big-picture»		(to "the-big-picture")
% «.the-big-picture-diag»	(to "the-big-picture-diag")
% «.the-big-picture-UL»		(to "the-big-picture-UL")
%
% «.missing-diagrams»		(to "missing-diagrams")
% «.eilenberg-steenrod»		(to "eilenberg-steenrod")
% «.idarct-mental-space»	(to "idarct-mental-space")
% «.idarct-skeletons»		(to "idarct-skeletons")
% «.missing-diags-elephant»	(to "missing-diags-elephant")
% «.missing-diags-wishlist»	(to "missing-diags-wishlist")
% «.exercise-cwm»		(to "exercise-cwm")
% «.cwm-smaller-diagram»	(to "cwm-smaller-diagram")
% «.yoneda-in-CWM»		(to "yoneda-in-CWM")
%
% «.internal-and-external»	(to "internal-and-external")
% «.blob-sets»			(to "blob-sets")
% «.blob-sets-2»		(to "blob-sets-2")
% «.blob-cats-and-functors»	(to "blob-cats-and-functors")
% «.the»			(to "the")
% «.the-2»			(to "the-2")
% «.the-3»			(to "the-3")
% «.convention-functors»	(to "convention-functors")
% «.meaning-for-Axf»		(to "meaning-for-Axf")
% «.curry-howard»		(to "curry-howard")
% «.proof-search»		(to "proof-search")
% «.proof-search-sets»		(to "proof-search-sets")
% «.sloppiness»			(to "sloppiness")
% «.sloppiness-2»		(to "sloppiness-2")
% «.sloppiness-3»		(to "sloppiness-3")
% «.convention-NTs»		(to "convention-NTs")
% «.convention-NTs-2»		(to "convention-NTs-2")
% «.convention-univs»		(to "convention-univs")
%
% «.that-looks-like-logic»	(to "that-looks-like-logic")
% «.freyd76»	        	(to "freyd76")
% «.freyd76-2»			(to "freyd76-2")
% «.freyd76-3»			(to "freyd76-3")
% «.arrows-between-arrows»	(to "arrows-between-arrows")
% «.arrows-between-arrows-2»	(to "arrows-between-arrows-2")
% «.diagrams-induce-typings»	(to "diagrams-induce-typings")
% «.diagrams-induce-props»	(to "diagrams-induce-props")
% «.diagrams-induce-props-2»	(to "diagrams-induce-props-2")

% «.motivation»			(to "motivation")
% «.three-yoneda-lemmas»	(to "three-yoneda-lemmas")
%
% «.internal-view-to-do»	(to "internal-view-to-do")

% «.back-to-the-yoneda-lemma»	(to "back-to-the-yoneda-lemma")
% «.notational-conventions»	(to "notational-conventions")
% «.three-yoneda-lemmas-2»	(to "three-yoneda-lemmas-2")

% «.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")
%
% «.help-needed»		(to "help-needed")
% «.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[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=violet]{hyperref} % (find-es "tex" "hyperref")
\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 edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
% (find-es "tex" "geometry")
\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=.25cm, left=1cm, right=1cm, includefoot
]{geometry}
%
\usepackage[backend=biber,
style=alphabetic]{biblatex}            % (find-es "tex" "biber")
%\addbibresource{catsem-u.bib}            % (find-LATEX "catsem-u.bib")
%\addbibresource{2019notes-yoneda.bib}    % (find-LATEX "2019notes-yoneda.bib")
\addbibresource{catsem-slides.bib}        % (find-LATEX "catsem-slides.bib")
\begin{document}

\catcode\^^J=10

%L forths["-"] = function () pusharrow("-") end

% «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{SpringGreen4}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#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}}

\def\sfC  {\mathsf{C}}
\def\sfSet{\mathsf{Set}}
\def\nameof#1{\ulcorner#1\urcorner}

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

% «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

%  ____  _               _      _
% | __ )(_) __ _   _ __ (_) ___| |_ _   _ _ __ ___
% |  _ \| |/ _ | | '_ \| |/ __| __| | | | '__/ _ \
% | |_) | | (_| | | |_) | | (__| |_| |_| | | |  __/
% |____/|_|\__, | | .__/|_|\___|\__|\__,_|_|  \___|
%          |___/  |_|
%
% «the-big-picture»  (to ".the-big-picture")
% (nyop 2 "the-big-picture")
% (nyo    "the-big-picture")

\vspace*{40pt}

\begin{center}
\Huge{\bf The Big Picture}   \\[0pt]
%\Large{\bf from several different} \\
%\Large{\bf points of view} \\
\end{center}

\thispagestyle{empty}

\newpage

{\bf The Big Picture}

The rectangles in the next page represent:

lots of text in very small type (several pages of a book), or

a big diagram (a Yoneda Lemma in any of several notations),

or several typings and definitions in Type Theory,

or these typings and definitions converted to code in Idris.

\msk

Following it in this way $\sm{→→→\\↑\phantom{mmm}↓}$ means:

We start with a standard presentation of the YL (\cite{CWM2}),

then we draw its missing diagrams'', then we convert them

to the notation of another book (Emily Riehl's), then we

convert them to a notation that looks more like logic'',

then we complete its the details using term inference,

then we translate our formalization to Idris.

\newpage

% «the-big-picture-diag»  (to ".the-big-picture-diag")
% (nyop 4 "the-big-picture-diag")
% (nyo    "the-big-picture-diag")
%
\def\TL #1{\begin{tabular}{l}#1\end{tabular}}
\def\BTL#1{\fbox{\!\!\!\!\TL{#1}\!\!\!\!}}
\def\MD #1#2{\scalebox{#1}{$\diag{#2}$}}
\def\BMD#1#2{\fbox{\MD{#1}{#2}}}

%D diagram big-picture
%D 2Dx     100  +50  +50  +50
%D 2D  100 A0 - A1 - A2 - A3
%D 2D      |    |  \      |
%D 2D  +70 B0   B1   B2   B3
%D 2D
%D ren A0 ==> \BTL{CWM\\YL}
%D ren B0 ==> \BTL{CWM\\pages\\59--61}
%D ren A1 ==> \BTL{Riehl\\YL}
%D ren B1 ==> \BTL{Riehl\\pages\\57--59}
%D ren A2 ==> \BTL{my\\YL}
%D ren B2 ==> \BTL{Riehl\\example\\2.3.4}
%D ren A3 ==> \BTL{types\\and\\defs}
%D ren B3 ==> \BTL{Impl\\in\\Idris}
%D
%D (( A0 A1 <-> .plabel= a \TL{change\\notation}
%D    A1 A2 <-> .plabel= a \TL{change\\notation}
%D    A2 A3  -> .plabel= a \TL{term\\inference}
%D    A0 B0 <- .plabel= m \TL{missing\\diagram}
%D    A1 B1 <- .plabel= m \TL{missing\\diagram}
%D    A1 B2 -> .plabel= m \phantom{mmmm}\TL{specialize}
%D    A3 B3 ->
%D ))
%D enddiagram
%D
$$\pu \diag{big-picture}$$

\newpage

%  ____  _               _      _                    _   _ _
% | __ )(_) __ _   _ __ (_) ___| |_ _   _ _ __ ___  | | | | |
% |  _ \| |/ _ | | '_ \| |/ __| __| | | | '__/ _ \ | | | | |
% | |_) | | (_| | | |_) | | (__| |_| |_| | | |  __/ | |_| | |___
% |____/|_|\__, | | .__/|_|\___|\__|\__,_|_|  \___|  \___/|_____|
%          |___/  |_|
%
% «the-big-picture-UL»  (to ".the-big-picture-UL")

{\bf The Big Picture: the four diagrams}

%D diagram big-picture-diags
%D 2Dx     100  +50  +50  +50
%D 2D  100 A0 - A1 - A2 - A3
%D 2D      |    |  \      |
%D 2D  +50 B0   B1   B2   B3
%D 2D
%D ren A0 ==> \BTL{CWM\\YL}
%D ren B0 ==> \BTL{CWM\\pages\\59--61}
%D ren A1 ==> \BTL{Riehl\\YL}
%D ren B1 ==> \BTL{Riehl\\pages\\57--59}
%D ren A2 ==> \BTL{my\\YL}
%D ren B2 ==> \BTL{Riehl\\example\\2.3.4}
%D ren A3 ==> \BTL{types\\and\\defs}
%D ren B3 ==> \BTL{Impl\\in\\Idris}
%D
%D (( A0 A1 <-> .plabel= a \TL{change\\notation}
%D    A1 A2 <-> .plabel= a \TL{change\\notation}
%D    A1 B2  -> .plabel= m \phantom{mmmm}\TL{specialize}
%D ))
%D enddiagram
%D
$$\pu \diag{big-picture-diags}$$

\newpage

%D diagram bigpic-yoneda-cwm
%D 2Dx     100    +40
%D 2D  100        D1
%D 2D              |
%D 2D  +20 D2 |-> D3
%D 2D
%D 2D  +10 E0 --> E1
%D 2D
%D 2D  +10 F0 --> F1
%D 2D          \   |
%D 2D  +20        F2
%D 2D
%D ren    D1 ==>      *
%D ren D2 D3 ==>  r  Kr
%D ren E0 E1 ==>  D  \Set
%D ren F0 F1 F2 ==> D(r,-) \Set(*,K-) K
%D
%D (( D1 D3  -> .plabel= r  u
%D    D2 D3 |->
%D    E0 E1  -> .plabel= a K\phantom{mmm}
%D    F0 F1  -> # .plabel= b φ
%D    F0 F2  -> .plabel= l ψ
%D    F1 F2 <->
%D    F0 F1 midpoint D1 D3 midpoint <-> .curve= ^11pt
%D ))
%D enddiagram
%D
%D diagram bigpic-yoneda-riehl
%D 2Dx     100    +40
%D 2D  100        D1
%D 2D              |
%D 2D  +20 D2 |-> D3
%D 2D
%D 2D  +10 E0 --> E1
%D 2D
%D 2D  +10 F0 --> F1
%D 2D          \   |
%D 2D  +20        F2
%D 2D
%D ren    D1    ==>      1
%D ren D2 D3    ==>  c  Fc
%D ren E0 E1    ==> \sfC  \sfSet
%D ren F0 F1 F2 ==> \sfC(c,-) \sfSet(1,F-) F
%D
%D (( D1 D3  -> .plabel= r \nameof{x}
%D    D2 D3 |->
%D    E0 E1  -> .plabel= a F\phantom{mmm}
%D    F0 F1  -> # .plabel= b φ
%D    F0 F2  -> .plabel= l α
%D    F1 F2 <->
%D    F0 F1 midpoint D1 D3 midpoint <-> .curve= ^11pt
%D ))
%D enddiagram
%D
%D diagram bigpic-yoneda-my
%D 2Dx     100    +40
%D 2D  100        D1
%D 2D              |
%D 2D  +20 D2 |-> D3
%D 2D
%D 2D  +10 E0 --> E1
%D 2D
%D 2D  +10 F0 --> F1
%D 2D          \   |
%D 2D  +20        F2
%D 2D
%D ren D1 D2 D3 ==> 1 C RC
%D ren E0 E1    ==> \catC  \Set
%D ren F0 F1 F2 ==> (C{→}\_) (1{→}R\_)) R
%D
%D (( D1 D3  -> .plabel= r \nameof{x}
%D    D2 D3 |->
%D    E0 E1  -> .plabel= a R\phantom{mmm}
%D    F0 F1  -> .plabel= b T
%D    F0 F2  -> .plabel= l T'
%D    F1 F2 <->
%D    F0 F1 midpoint D1 D3 midpoint <-> .curve= ^11pt
%D ))
%D enddiagram

%D diagram riehl-example-2.3.4
%D 2Dx     100 +50
%D 2D  100     A1
%D 2D  +20 A2  A3
%D 2D  +20 A4  A5
%D 2D  +15 B0  B1
%D 2D  +15 C1  C2
%D 2D  +20     C3
%D 2D
%D ren    A1 ==>          1
%D ren A2 A3 ==> \Z[x] U(\Z[x])
%D ren A4 A5 ==>    ∀R UR
%D ren B0 B1 ==> 𝐬{Ring} 𝐬{Set}
%D ren C1 C2 ==> 𝐬{Ring}(\Z[x],-) 𝐬{Set}(1,U-)
%D ren    C3 ==>                           U
%D
%D (( A1 A3  -> .plabel= r \nameof{x}
%D    A2 A3 |->
%D    A2 A4  -> .plabel= l ∃!φ
%D    A3 A5  -> .plabel= r Uφ
%D    A4 A5 |->
%D    A2 A5 harrownodes nil 20 nil |->
%D    A1 A5  -> .slide= 20pt .plabel= r ∀\nameof{φ(x)}
%D    B0 B1 |-> .plabel= a U
%D    C1 C2 <->
%D    C1 C3 <->
%D    C2 C3 <->
%D  # C1 C2 midpoint A1 A3 midpoint xy+= 0 -5 <-> .curve= ^15pt
%D
%D ))
%D enddiagram
%D
\pu

$$\begin{array}{ccc} \BMD{0.65}{bigpic-yoneda-cwm} & \BMD{0.65}{bigpic-yoneda-riehl} \!\!\!\!\!\!\!\!\!\! & \BMD{0.65}{bigpic-yoneda-my} \\ \\ & & \BMD{0.60}{riehl-example-2.3.4} \\ \end{array}$$

% (find-riehlccpage (+ 18 57) "Theorem 2.2.4 (Yoneda lemma)")
% (find-riehlcctext (+ 18 57) "Theorem 2.2.4 (Yoneda lemma)")

\newpage

\noedrxfooter

%  __  __ _         _                   _ _
% |  \/  (_)___ ___(_)_ __   __ _    __| (_) __ _  __ _ ___
% | |\/| | / __/ __| | '_ \ / _ |  / _ | |/ _ |/ _ / __|
% | |  | | \__ \__ \ | | | | (_| | | (_| | | (_| | (_| \__ \
% |_|  |_|_|___/___/_|_| |_|\__, |  \__,_|_|\__,_|\__, |___/
%                           |___/                 |___/
%
% «missing-diagrams»  (to ".missing-diagrams")
% (nyop 2 "the-big-picture")
% (nyo    "the-big-picture")

\vspace*{30pt}

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

\thispagestyle{empty}

\newpage

%  _____ _ _   ____  _                                      _
% | ____(_) | / ___|| |_ ___  ___ _ __     __ _ _   _  ___ | |_ ___
% |  _| | | | \___ \| __/ _ \/ _ \ '_ \   / _ | | | |/ _ \| __/ _ \
% | |___| | |  ___) | ||  __/  __/ | | | | (_| | |_| | (_) | ||  __/
% |_____|_|_| |____/ \__\___|\___|_| |_|  \__, |\__,_|\___/ \__\___|
%                                            |_|
%
% «eilenberg-steenrod»  (to ".eilenberg-steenrod")
% (nyop 5 "eilenberg-steenrod")
% (nyo    "eilenberg-steenrod")
% (find-books "__cats/__cats.el" "eilenberg-steenrod")

{\bf A quote from Eilenberg and Steenrod}

From {\sl Foundations of Algebraic Topology}
(\cite[p.ix]{EilenbergSteenrod}):

\begin{quotation}

The diagrams incorporate a large amount of information. Their use
provides extensive savings in space and in mental effort. In the
case of many theorems, the setting up of the correct diagram is the
major part of the proof. We therefore urge that the reader stop at
the end of each theorem and attempt to construct for himself the
relevant diagram before examining the one which is given in the
text. Once this is done, the subsequent demonstration can be
followed more readily; in fact, {\bf the reader can usually supply
it himself.}

\end{quotation}

\newpage

% «idarct-mental-space»  (to ".idarct-mental-space")
% (nyop 9 "idarct-mental-space")
% (nyo    "idarct-mental-space")
% (find-angg ".emacs" "idarct-preprint")
% (find-idarctpage  1 "1. Mental Space and Diagrams")
% (find-idarcttext  1 "1. Mental Space and Diagrams")

{\bf A quote from \cite{IDARCT}}

\ssk

{\sl 1. Mental Space and Diagrams}

My memory is limited, and not very dependable: I often have to rededuce
results to be sure of them, and I have to make them fit in as little mental
space'' as possible...

Different people have different measures for mental space''; someone
with a good algebraic memory may feel that an expression like
$\mathsf{Frob}: Σ_f(P ∧ f^* Q) ≅ Σ_f P ∧ Q$ is easy to remember, while
I always think diagramatically, and so what I do is that I remember
this diagram,

\begin{center}
\includegraphics[height=40pt]{2020notes-yoneda-frob.pdf}
\end{center}

and I reconstruct the formula from it.

\newpage

% «idarct-skeletons»  (to ".idarct-skeletons")
% (nyop 10 "idarct-skeletons")
% (nyo     "idarct-skeletons")

% (find-angg ".emacs" "idarct-preprint")
% (find-idarctpage 15 "12. Skeletons of proofs")
% (find-idarcttext 15 "12. Skeletons of proofs")
% (find-idarctpage 19 "14. Preservations, Frobenius, Beck-Chevalley")
% (find-idarcttext 19 "14. Preservations, Frobenius, Beck-Chevalley")

{\bf Another quote from \cite{IDARCT}}

{\sl 12. Skeletons of proofs}

Let's call the projected'' version of a mathematical object its
skeleton''. The underlying idea in this paper is that for the right
kinds of projections, and for some kinds of mathetical objects, it
should be possible to reconstruct enough of the original object from
its skeleton and few extra clues --- just like paleontologists can
reconstruct from a fossil skeleton the look of an animal when it was
alive.

\newpage

% «missing-diags-elephant»  (to ".missing-diags-elephant")
% (nyop 11 "missing-diags-elephant")
% (nyo     "missing-diags-elephant")

{\bf A quote from my submission to the ACT2019}

My extended abstract was called On Some Missing

Diagrams in The Elephant'' (\cite{MDE}). It was rejected.

\begin{quotation}

Imagine two category theorists, Aleks and Bob, who both think very
visually and who have exactly the same background. One day Aleks
discovers a theorem, $T_1$, and sends an e-mail, $E_1$, to Bob,
stating and proving $T_1$ in a purely algebraic way; then Bob is
able to reconstruct by himself Aleks's diagrams for $T_1$ exactly as
Aleks has thought them. We say that Bob has reconstructed the
{\it missing diagrams} in Aleks's e-mail.

\end{quotation}

\newpage

(Cont...)

\begin{quotation}

Now suppose that Carol has published a paper, $P_2$, with a theorem
$T_2$. Aleks and Bob both read her paper independently, and both
pretend that she thinks diagrammatically in the same way as them.
They both reconstruct the missing diagrams'' in $P_2$ in the same
way, even though Carol has never used those diagrams herself.

\end{quotation}

The Yoneda Lemma involves three categories.

It's hard to find good conventions for drawing the missing
diagrams'' when there are several categories involved. Here I will use
my \ColorRed{current favorite conventions}.

\newpage

% __        ___     _     _ _     _
% \ \      / (_)___| |__ | (_)___| |_
%  \ \ /\ / /| / __| '_ \| | / __| __|
%   \ V  V / | \__ \ | | | | \__ \ |_
%    \_/\_/  |_|___/_| |_|_|_|___/\__|
%
% «missing-diags-wishlist»  (to ".missing-diags-wishlist")
% (nyop 8 "missing-diags-wishlist")
% (nyo    "missing-diags-wishlist")

{\bf Missing diagrams: wishlist}

% (find-LATEX "2020hyp.tex" "myenumerate")

\newcounter{mycounter}
\long\def\myenumerate#1{%
\begin{list}{\arabic{mycounter}.}%
{\usecounter{mycounter}
\setlength\topsep{0pt}
\setlength\parsep{0pt}
\setlength\itemsep{0pt}
}
#1
\end{list}
}

What are good conventions'' for

drawing missing diagrams?

Some ideas:

\myenumerate{

\item The notation in the diagram should be similar to

the one in the text that we are trying to complement.

\item We should have good {\sl positional conventions} ---

for example, drawing $A \to B$ above $\catC$ could {\sl usually}

mean that the morphism $A \to B$ is {\sl in} the category $\catC$...

so {\sl above} usually means {\sl inside}.

\item It should be possible to infer lots of {\sl typings} and

{\sl definitions} from the diagrams.

\item Each node and arrow in our diagrams should have

a meaning that we know how to formalize.

}

\newpage

{\bf Missing diagrams: wishlist (2)}

Also:

% (find-kopkadaly4page (+ 12 182) "8.1.3   Changing counter values")
% (find-kopkadaly4text            "8.1.3   Changing counter values")

\myenumerate{

\setcounter{mycounter}{4}

\item The diagram should contain \ColorRed{all} entities
mentioned in the text.

}

...or almost all.

\newpage

%  _____                   _             ______        ____  __
% | ____|_  _____ _ __ ___(_)___  ___   / ___\ \      / /  \/  |
% |  _| \ \/ / _ \ '__/ __| / __|/ _ \ | |    \ \ /\ / /| |\/| |
% | |___ >  <  __/ | | (__| \__ \  __/ | |___  \ V  V / | |  | |
% |_____/_/\_\___|_|  \___|_|___/\___|  \____|  \_/\_/  |_|  |_|
%
% «exercise-cwm»  (to ".exercise-cwm")
% (nyop 9 "exercise-cwm")
% (nyo    "exercise-cwm")
% (cwmp 4 "yoneda-lemma")
% (cwm    "yoneda-lemma")
% (find-cwm2page (+ 13  59) "2. The Yoneda Lemma")
% (find-cwm2text (+ 13  59) "2. The Yoneda Lemma")
% (find-cwm2page (+ 13  59) "Proposition 1.")
% (find-cwm2text (+ 13  59) "Proposition 1.")

{\bf An exercise: a missing diagram in CWM}

Read the beginning of section III.2 in \cite{CWM2}.

That section is about the Yoneda Lemma.

{\sl Check that practically all the entities in Proposition 1

and in its proof appear in the diagram below.}
%
%D diagram yoneda-cwm-phi-1
%D 2Dx     100    +35
%D 2D  100        A1
%D 2D              |
%D 2D  +20 A2 |-> A3
%D 2D      |       |
%D 2D  +20 A4 |-> A5
%D 2D      |       |
%D 2D  +20 A6 |-> A7
%D 2D
%D 2D  +15 B0 --> B1
%D 2D
%D 2D  +15 C0 --> C1
%D 2D          \   |
%D 2D  +20        C2
%D 2D
%D ren    A1 ==>      c
%D ren A2 A3 ==>  r  Sr
%D ren A4 A5 ==>  d  Sd
%D ren A6 A7 ==>  d' Sd
%D ren B0 B1 ==>  D   C
%D ren C0 C1 C2 ==> D(r,-) C(c,S-) ?
%D
%D (( A1 A3  -> .plabel= r  u
%D    A2 A3 |->
%D    A2 A4  -> .plabel= l  f'
%D    A3 A5  -> .plabel= r Sf'
%D  # A1 A5  -> .slide= 20pt .plabel= r \sm{K(f')∘u=\\\nameof{K(f')(u(*))}}
%D    A4 A5 |->
%D    A4 A6  -> .plabel= l  g'
%D    A5 A7  -> .plabel= r Sg'
%D    A6 A7 |->
%D
%D    B0 B1  -> .plabel= a S
%D
%D    C0 C1 -> .plabel= a φ
%D  # C0 C2 -> .plabel= l \sm{ψ\\\text{(iso)}}
%D  # C1 C2 <->
%D ))
%D enddiagram
%D
%D diagram yoneda-cwm-phi-NT-1
%D 2Dx     100 +20 +35 +30 +40
%D 2D  100 A0  B0  B1  D0  D1
%D 2D  +17                 D3'
%D 2D   +8 A1  B2  B3  D2  D3
%D 2D
%D 2D  +20     C0  C1
%D 2D
%D ren A0 A1 ==> d d'
%D ren B0 B1 B2 B3 ==> D(r,d) C(c,Sd) D(r,d') C(c,Sd')
%D ren C0 C1 ==> D(r,-) C(c,S-)
%D ren D0 D1 D3' ==> f' Sf'∘u Sg'∘(Sf'∘u)
%D ren    D2 D3  ==> g'∘f' S(g∘f)∘u
%D
%D (( A0 A1 -> .plabel= l f'
%D    B0 B1 -> .plabel= a φ_r
%D    B0 B2 -> .plabel= l D(r,f')
%D    B1 B3 -> .plabel= r C(c,Sf')
%D    B2 B3 -> .plabel= a φ_d
%D    C0 C1 -> .plabel= a φ
%D    D0 D1  |->
%D    D0 D2  |->
%D    D1 D3' |->
%D    D2 D3  |->
%D ))
%D enddiagram
%D
\pu
$$\scalebox{0.8}{ \diag{yoneda-cwm-phi-1} \quad \diag{yoneda-cwm-phi-NT-1} }$$

\newpage

%   ______        ____  __                       _ _
%  / ___\ \      / /  \/  |  ___ _ __ ___   __ _| | | ___ _ __
% | |    \ \ /\ / /| |\/| | / __| '_  _ \ / _ | | |/ _ \ '__|
% | |___  \ V  V / | |  | | \__ \ | | | | | (_| | | |  __/ |
%  \____|  \_/\_/  |_|  |_| |___/_| |_| |_|\__,_|_|_|\___|_|
%
% «cwm-smaller-diagram»  (to ".cwm-smaller-diagram")
% (nyop 10 "cwm-smaller-diagram")
% (nyo     "cwm-smaller-diagram")

{\bf A smaller diagram}

The right side of the diagram of the previous page is

obvious'' in a precise sense: it is just the \ColorRed{internal view}

of the natural transformation $φ$. So we can omit it.

The least obvious, and most important, part of the diagram

is the bijection between $u$'s and $φ$'s. So we will stress it.

%D diagram yoneda-cwm-0-small
%D 2Dx     100    +35
%D 2D  100        A1
%D 2D              |
%D 2D  +20 A2 |-> A3
%D 2D
%D 2D  +10 B0 --> B1
%D 2D
%D 2D  +10 C0 --> C1
%D 2D          \   |
%D 2D  +20        C2
%D 2D
%D ren    A1 ==>      c
%D ren A2 A3 ==>  r  Sr
%D ren B0 B1 ==>  D   C
%D ren C0 C1 C2 ==> D(r,-) C(c,S-) ?
%D
%D (( A1 A3  -> .plabel= r  u
%D    A2 A3 |->
%D
%D    B0 B1  -> .plabel= a S\phantom{mmm}
%D
%D    C0 C1 -> .plabel= b φ
%D  # C0 C2 -> .plabel= l \sm{ψ\\\text{(iso)}}
%D  # C1 C2 <->
%D
%D    C0 C1 midpoint A1 A3 midpoint <-> .curve= ^11pt
%D ))
%D enddiagram

We will sometimes omit the middle part.
%
$$\pu \scalebox{0.65}{ \diag{yoneda-cwm-phi-1} } \qquad \Longrightarrow \qquad \diag{yoneda-cwm-0-small}$$

\newpage

% __   __                   _          ______        ____  __
% \ \ / /__  _ __   ___  __| | __ _   / ___\ \      / /  \/  |
%  \ V / _ \| '_ \ / _ \/ _ |/ _ | | |    \ \ /\ / /| |\/| |
%   | | (_) | | | |  __/ (_| | (_| | | |___  \ V  V / | |  | |
%   |_|\___/|_| |_|\___|\__,_|\__,_|  \____|  \_/\_/  |_|  |_|
%
% «yoneda-in-CWM»  (to ".yoneda-in-CWM")
% (nyop 11 "yoneda-in-CWM")
% (nyo     "yoneda-in-CWM")

{\bf The Yoneda Lemma in CWM}

% (cwmp 4 "yoneda-lemma")
% (cwm    "yoneda-lemma")
% (find-cwm2page (+ 13  59) "2. The Yoneda Lemma")
% (find-cwm2text (+ 13  59) "2. The Yoneda Lemma")
% (find-cwm2page (+ 13  59) "Proposition 1.")
% (find-cwm2text (+ 13  59) "Proposition 1.")
% (find-cwm2page (+ 13 60) "Proposition 2.")
% (find-cwm2text (+ 13 60) "Proposition 2.")

Left: Proposition 1 in \cite[p.59]{CWM2}.

Right: Proposition 2 in \cite[p.60]{CWM2}.

We will see how to obtain functors $D(r,-)$, $C(c,S-)$, and
$\Set(*,K-)$ that deserve these names'', but it will be easier to do
that in another notation first --- and then translate.
%
%D diagram yoneda-cwm-props-1-2
%D 2Dx     100    +35   +35    +40
%D 2D  100        A1           D1
%D 2D              |            |
%D 2D  +20 A2 |-> A3    D2 |-> D3
%D 2D
%D 2D  +10 B0 --> B1    E0 --> E1
%D 2D
%D 2D  +10 C0 --> C1    F0 --> F1
%D 2D          \   |        \   |
%D 2D  +20        C2           F2
%D 2D
%D ren    A1 ==>      c
%D ren A2 A3 ==>  r  Sr
%D ren B0 B1 ==>  D   C
%D ren C0 C1 C2 ==> D(r,-) C(c,S-) ?
%D
%D ren    D1 ==>      *
%D ren D2 D3 ==>  r  Kr
%D ren E0 E1 ==>  D  \Set
%D ren F0 F1 F2 ==> D(r,-) \Set(*,K-) K
%D
%D (( A1 A3  -> .plabel= r  u
%D    A2 A3 |->
%D    B0 B1  -> .plabel= a S\phantom{mmm}
%D    C0 C1  -> .plabel= b φ
%D    C0 C1 midpoint A1 A3 midpoint <-> .curve= ^11pt
%D ))
%D (( D1 D3  -> .plabel= r  u
%D    D2 D3 |->
%D    E0 E1  -> .plabel= a K\phantom{mmm}
%D    F0 F1  -> # .plabel= b φ
%D    F0 F2  -> .plabel= l ψ
%D    F1 F2 <->
%D    F0 F1 midpoint D1 D3 midpoint <-> .curve= ^11pt
%D ))
%D enddiagram
%
$$\pu \diag{yoneda-cwm-props-1-2}$$

\newpage

%  ___       _        __  _____      _
% |_ _|_ __ | |_     / / | ____|_  _| |_
%  | || '_ \| __|   / /  |  _| \ \/ / __|
%  | || | | | |_   / /   | |___ >  <| |_
% |___|_| |_|\__| /_/    |_____/_/\_\\__|
%
% «internal-and-external»  (to ".internal-and-external")
% (nyop 12 "internal-and-external")
% (nyo     "internal-and-external")

\vspace*{20pt}

\begin{center}
\Huge{\bf INTERNAL AND}   \\[0pt]
\Huge{\bf EXTERNAL} \\
\Huge{\bf VIEWS} \\
\end{center}

\thispagestyle{empty}

\newpage

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

{\bf Motivation: blob-sets}

From the introduction of \cite{PH1}, a.k.a.

Planar Heyting Algebras for Children'':

% (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")
% (nyop 20 "blob-sets-2")
% (nyo     "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

%  ____  _       _        __                  _
% | __ )| | ___ | |__    / _|_   _ _ __   ___| |_ ___  _ __ ___
% |  _ \| |/ _ \| '_ \  | |_| | | | '_ \ / __| __/ _ \| '__/ __|
% | |_) | | (_) | |_) | |  _| |_| | | | | (__| || (_) | |  \__ \
% |____/|_|\___/|_.__/  |_|  \__,_|_| |_|\___|\__\___/|_|  |___/
%
% «blob-cats-and-functors»  (to ".blob-cats-and-functors")
% (nyop 21 "blob-cats-and-functors")
% (nyo     "blob-cats-and-functors")

{\bf Blob-categories and functors}

When we draw the internal views of

functors we don't draw the blobs.

In the diagram below the morphism

$g:A→B$ is \ColorRed{above} $\catC$ because it is \ColorRed{in} $\catC$, and

$Fg:FA→FB$ is above $\catD$ because it is in $\catD$.

The $\mto$' arrows above $F$ are actions of $F$

on objects ($F_0$'s) and on morphisms ($F_1$').
%
%D diagram blob-functor
%D 2Dx        100   +25     +30  +30
%D 2D  100    A |-> FA      B0   B1
%D 2D
%D 2D  +25    B |-> FB      B2   B3
%D 2D
%D 2D  +15 \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= a F_0
%D    A FB harrownodes nil 20 nil |-> .plabel= a F_1
%D    \catC \catD -> .plabel= a F
%D ))
%D enddiagram
\pu
$$\scalebox{0.95}{ \diag{blob-functor} }$$

\newpage

%  _____ _
% |_   _| |__   ___
%   | | | '_ \ / _ \
%   | | | | | |  __/
%   |_| |_| |_|\___|
%
% «the»  (to ".the")
% (nyop 22 "the")
% (nyo     "the")
% (nesp 2 "introduction")
% (nes    "introduction")

{\bf The''}

\ssk

Most texts in Category Theory (CT'')

are full of expressions like this:

\msk

Let's write $(A×)$ for \ColorRed{the} functor that takes

each object $B$ to $A×B$''

\msk

I was absolutely fascinated by this \ColorRed{the}''.

A functor --- say, $(A×)$ --- has an action on objects,

an action on morphisms, and guarantees, or proofs,

that it respects identities and compositions.

\msk

That \ColorRed{the} functor'' implies that the reader should be able

to figure out by himself the action on morphisms, i.e.,

the precise meaning for $(A×)f$ when $f:B→C$, and to

check that this $(A×)$ respects identities and compositions.

\newpage

%  _____ _             ________
% |_   _| |__   ___   / /___ \ \
%   | | | '_ \ / _ \ | |  __) | |
%   | | | | | |  __/ | | / __/| |
%   |_| |_| |_|\___| | ||_____| |
%                     \_\    /_/
%
% «the-2»  (to ".the-2")
% (nyop 23 "the-2")
% (nyo     "the-2")

{\bf The'' (2)}

\ssk

Formally, a functor $(A×):\Set→\Set$

is a 4-uple:

\msk

\phantom{mmm}
$(A×) = ((A×)_0, (A×)_1, \respids_{(A×)}, \respcomp_{(A×)})$

\bsk

The \ColorRed{the}'' in

\msk

\phantom{m}
$(A×)$ is \ColorRed{the} functor that takes each object $B$ to $A{×}B$''

\msk

suggests that learning CT transforms you in a certain way...

you become a person who can infer $(A×)_1$, $\respids_{(A×)}$,

and $\respcomp_{(A×)}$ from just $(A×)_0$...

\msk

...you become a person who can define functors in a very

compact way, and the other CT people will understand you.

\msk

\ColorRed{(I wanted to become like that when I'd grow up)}

\newpage

%  _____ _             _________
% |_   _| |__   ___   / /___ /\ \
%   | | | '_ \ / _ \ | |  |_ \ | |
%   | | | | | |  __/ | | ___) || |
%   |_| |_| |_|\___| | ||____/ | |
%                     \_\     /_/
%
% «the-3»  (to ".the-3")
% (nyop 24 "the-3")
% (nyo     "the-3")

{\bf The'' (3)}

\ssk

...you become a person who can define functors in a very

compact way, and the other CT people will understand you.

\msk

I wanted to become like that when I'd grow up, \ColorRed{but}

I also wanted to be able to \ColorRed{explain my tricks!!!}

\msk

In short: the trick for \ColorRed{inferring} the meaning for $(A×)f$

is slightly related to \ColorRed{Type Inference}...

it is a (sloppy kind of) \ColorRed{Term Inference}, composed by a

\ColorRed{Proof Search} followed by \ColorRed{Curry-Howard}.

\msk

I will explain that with lots of diagrams, but the

general idea is: we will try to build an object of

\ColorRed{type} $A×B→A×C$ from a hypothesis'' $f:B→C$.

\newpage

%   ____                    __                  _
%  / ___|___  _ ____   __  / _|_   _ _ __   ___| |_ ___  _ __ ___
% | |   / _ \| '_ \ \ / / | |_| | | | '_ \ / __| __/ _ \| '__/ __|
% | |__| (_) | | | \ V /  |  _| |_| | | | | (__| || (_) | |  \__ \
%  \____\___/|_| |_|\_/   |_|  \__,_|_| |_|\___|\__\___/|_|  |___/
%
% «convention-functors»  (to ".convention-functors")
% (nyop 25 "convention-functors")
% (nyo     "convention-functors")

{\bf A diagrammatic convention for functors}

\ssk

Let me introduce a diagrammatic convention.

The obvious way of drawing $(A×):\Set→\Set$

is the diagram at the left.

When I draw it as at the right I am \ColorRed{saying} that

$(A×)_0 B := A×B$,

$(A×)_0 C := A×C$,

%$(A×)_1 f := 〈π,f∘π'〉$.
$(A×)_1 f := λp.(πp,f(π'p))$.
%
%D diagram functor-convention
%D 2Dx     100 +35     +40  +30
%D 2D  100 A0  A1      B0   B1
%D 2D
%D 2D  +30 A2  A3      B2   B3
%D 2D
%D 2D  +15 A4  A5      B4   B5
%D 2D
%D ren A0 A1 ==> B (A{×})_0B
%D ren A2 A3 ==> C (A{×})_0B
%D ren A4 A5 ==> \Set \Set
%D
%D ren B0 B1 ==> B A{×}B
%D ren B2 B3 ==> C A{×}C
%D ren B4 B5 ==> \Set \Set
%D
%D (( A0 A1 |-> .plabel= a (A{×})_0
%D    A0 A2  -> .plabel= l f
%D    A1 A3  -> .plabel= r (A{×})_1f
%D    A2 A3 |-> .plabel= a (A{×})_0
%D    A0 A3 harrownodes nil 20 nil |-> .plabel= a (A{×})_1
%D    A4 A5 -> .plabel= a (A{×})
%D
%D    B0 B1 |->
%D    B0 B2  -> .plabel= l f
%D    B1 B3  -> .plabel= r λp.(πp,f(π'p)) # 〈π,f∘π'〉
%D    B2 B3 |->
%D    B0 B3 harrownodes nil 20 nil |->
%D    B4 B5  -> .plabel= a (A{×})
%D ))
%D enddiagram
\pu
$$\diag{functor-convention}$$

\newpage

%  __  __                  _                __                 _           __
% |  \/  | ___  __ _ _ __ (_)_ __   __ _   / _| ___  _ __     / \   __  __/ _|
% | |\/| |/ _ \/ _ | '_ \| | '_ \ / _ | | |_ / _ \| '__|   / _ \  \ \/ / |_
% | |  | |  __/ (_| | | | | | | | | (_| | |  _| (_) | |     / ___ \  >  <|  _|
% |_|  |_|\___|\__,_|_| |_|_|_| |_|\__, | |_|  \___/|_|    /_/   \_\/_/\_\_|
%                                  |___/
%
% «meaning-for-Axf»  (to ".meaning-for-Axf")
% (nyop 26 "meaning-for-Axf")
% (nyo     "meaning-for-Axf")

{\bf Finding a meaning for $(A×)f$}

\ssk

How did I discover that $(A×)_1f = λp.(πp,f(π'p))$

in the previous slide?

Let's go back one step. Can we find a precise meaning

for the $(A×)f$ at the right below? Or: do we have a

\ColorRed{natural way to construct} a function $(A×)f: A{×}B→A{×}C$?

We are allowed to use $f:B→C$ in the construction.

What are \ColorRed{natural constructions}? Ta-daaa: \ColorRed{$λ$-terms}!
%
%D diagram functor-convention-2
%D 2Dx     100 +35     +40  +30
%D 2D  100 A0  A1      B0   B1
%D 2D
%D 2D  +30 A2  A3      B2   B3
%D 2D
%D 2D  +15 A4  A5      B4   B5
%D 2D
%D ren A0 A1 ==> B (A{×})_0B
%D ren A2 A3 ==> C (A{×})_0B
%D ren A4 A5 ==> \Set \Set
%D
%D ren B0 B1 ==> B A{×}B
%D ren B2 B3 ==> C A{×}C
%D ren B4 B5 ==> \Set \Set
%D
%D (( A0 A1 |-> .plabel= a (A{×})_0
%D    A0 A2  -> .plabel= l f
%D    A1 A3  -> .plabel= r (A{×})_1f
%D    A2 A3 |-> .plabel= a (A{×})_0
%D    A0 A3 harrownodes nil 20 nil |-> .plabel= a (A{×})_1
%D    A4 A5 -> .plabel= a (A{×})
%D
%D    B0 B1 |->
%D    B0 B2  -> .plabel= l f
%D    B1 B3  -> .plabel= r \ColorRed{(A×)f}
%D    B2 B3 |->
%D    B0 B3 harrownodes nil 20 nil |->
%D    B4 B5  -> .plabel= a (A{×})
%D ))
%D enddiagram
\pu
$$\diag{functor-convention-2}$$

\newpage

%   ____                            _   _                            _
%  / ___|   _ _ __ _ __ _   _      | | | | _____      ____ _ _ __ __| |
% | |  | | | | '__| '__| | | |_____| |_| |/ _ \ \ /\ / / _ | '__/ _ |
% | |__| |_| | |  | |  | |_| |_____|  _  | (_) \ V  V / (_| | | | (_| |
%  \____\__,_|_|  |_|   \__, |     |_| |_|\___/ \_/\_/ \__,_|_|  \__,_|
%                       |___/
%
% «curry-howard»  (to ".curry-howard")
% (nyop 27 "curry-howard")
% (nyo     "curry-howard")

{\bf Curry-Howard in one slide}

Compare:
%:
%:
%:           [P∧Q]^1                        [p:A×B]^1
%:           -------                        ---------
%:  [P∧Q]^1      Q     Q→R      [p:A×B]^1     π'p:B    f:B→C
%:  -------      --------       ---------     --------------
%:     P            R             πp:A            f(π'p):C
%:     --------------             ------------------------
%:           P∧R                        (πp,f(π'p)):A×C
%:        -------1               ----------------------------1
%:        P∧Q→P∧R                (λp⠆A×B.(πp,f(π'p))):A×B→A×C
%:
%:        ^curry-h-logic         ^curry-h-func
%:
%:
\pu
$$\def×{{\times}} \begin{array}{c} \ded{curry-h-logic} \\ \\ \ded{curry-h-func} \end{array}$$

% (nesp 23 "term-search-2")
% (nes     "term-search-2")

\newpage

%  ____                   __                           _
% |  _ \ _ __ ___   ___  / _|  ___  ___  __ _ _ __ ___| |__
% | |_) | '__/ _ \ / _ \| |_  / __|/ _ \/ _ | '__/ __| '_ \
% |  __/| | | (_) | (_) |  _| \__ \  __/ (_| | | | (__| | | |
% |_|   |_|  \___/ \___/|_|   |___/\___|\__,_|_|  \___|_| |_|
%
% «proof-search»  (to ".proof-search")
% (nyop 28 "proof-search")
% (nyo     "proof-search")

{\bf Proof search}

A double bar in a proof means

several steps here, details omitted'', or

several steps here, the details are obvious''...

\msk

%:
%:
%:     Q→R                         f:B→C
%:   =======                   =============
%:   P∧Q→P∧R                   (A×)f:A×B→A×C
%:
%:   ^curry-h-logic-folded     ^curry-h-func-folded
%:
\pu
$$\ded{curry-h-logic-folded} \quad ⇒ \ded{curry-h-logic}$$

\newpage

%  ____        __                _                _
% |  _ \ _ __ / _|  ___ _ __ ___| |__    ___  ___| |_ ___
% | |_) | '__| |_  / __| '__/ __| '_ \  / __|/ _ \ __/ __|
% |  __/| |  |  _| \__ \ | | (__| | | | \__ \  __/ |_\__ \
% |_|   |_|  |_|   |___/_|  \___|_| |_| |___/\___|\__|___/
%
% «proof-search-sets»  (to ".proof-search-sets")
% (nyop 29 "proof-search-sets")
% (nyo     "proof-search-sets")

{\bf Proof search, translated to sets (term inference)}

\bsk

$$\begin{array}{l} \ded{curry-h-func-folded} \quad ⇒ \\ \\ \ded{curry-h-func} \\ \end{array}$$

\bsk

Alternative names:

term search, term inference...

\newpage

%  ____  _
% / ___|| | ___  _ __
% \___ \| |/ _ \| '_ \
%  ___) | | (_) | |_) |
% |____/|_|\___/| .__/
%               |_|
%
% «sloppiness»  (to ".sloppiness")
% (nyop 30 "sloppiness")
% (nyo     "sloppiness")

{\bf Two kinds of sloppiness}

We can pronounce'' the trees below as:

$$\ded{curry-h-logic-folded} \qquad \ded{curry-h-func-folded}$$

If I know that $P→Q$ is true

then I know that $P∧Q→P∧R$ is true.

\msk

If I know an element of type $B→C$ (call it $f$')

then I know an element of type $A×B→A×C$

(call it $(A×)f$').

\msk

I can ignore the $f:$' and $(A×)f:$' and think/say just this:

if I know \ColorRed{an} element of type $B→C$

then I know \ColorRed{an} element of type $A×B→A×C$.

\newpage

%  ____  _               ____
% / ___|| | ___  _ __   |___ \
% \___ \| |/ _ \| '_ \    __) |
%  ___) | | (_) | |_) |  / __/
% |____/|_|\___/| .__/  |_____|
%               |_|
%
% «sloppiness-2»  (to ".sloppiness-2")
% (nyop 31 "sloppiness-2")
% (nyo     "sloppiness-2")

{\bf Two kinds of sloppiness (2)}

\msk

If I know \ColorRed{an} element of type $B→C$

then I know \ColorRed{an} element of type $A×B→A×C$.

\msk

The diagrams that I will show for the Yoneda Lemma(s)

permit the kind of thinking above as a first step.

In it we \ColorRed{don't care} if there are several different,

non-equivalent ways of building a result of the

desired output type from the inputs.

\msk

We can \ColorRed{start} by playing just with the types ---

and \ColorRed{then} we introduce the terms, as if they were

obvious'', or a trivial exercise''.

\msk

(I can do this playing with types'' visually very quickly

by looking at the diagrams without writing anything down).

% (\ColorRed{I} can do that \ColorRed{visually} on the diagrams very quickly ---

\newpage

%  ____  _               _____
% / ___|| | ___  _ __   |___ /
% \___ \| |/ _ \| '_ \    |_ \
%  ___) | | (_) | |_) |  ___) |
% |____/|_|\___/| .__/  |____/
%               |_|
%
% «sloppiness-3»  (to ".sloppiness-3")
% (nyop 32 "sloppiness-3")
% (nyo     "sloppiness-3")

{\bf Two kinds of sloppiness (3)}

\msk

Our diagrams for the Yoneda Lemmas also \ColorRed{permit} a

second kind of sloppiness: the Syntactical World'' of

\cite[section 19]{IDARCT}, in which we do all \ColorRed{constructions}

first, and all the parts that involve \ColorRed{checking equations}

are left to a second moment.

\msk

But this is just a curiosity!

The details are not relevant now.

I will explain this very briefly in the last slides.

\newpage

%   ____                   _   _ _____
%  / ___|___  _ ____   __ | \ | |_   _|__
% | |   / _ \| '_ \ \ / / |  \| | | |/ __|
% | |__| (_) | | | \ V /  | |\  | | |\__ \
%  \____\___/|_| |_|\_/   |_| \_| |_||___/
%
% «convention-NTs»  (to ".convention-NTs")
% (nyop 33 "convention-NTs")
% (nyo     "convention-NTs")

{\bf A diagrammatic convention on NTs}

\ssk

If $F,G:\catC→\catD$ are functors and

$T:F→G$ is a natural transformation between them,

we will \ColorRed{usually} draw the internal view of $T:F→G$

as a square above its external view, and at the right

of the input morphism'' $f:A→B$ in $\catC$:
%
%D diagram NT-0
%D 2Dx     100 +20 +30
%D 2D  100 A0
%D 2D  +15     B0  B1
%D 2D  +15 A1
%D 2D  +15     B2  B3
%D 2D
%D 2D  +15     C0  C1
%D 2D
%D ren A0 A1 ==> A B
%D ren B0 B1 B2 B3 ==> FA GA FB GB
%D ren C0 C1 ==> F G
%D
%D (( A0 B0 |->
%D    A0 B1 |->
%D    A1 B2 |->
%D    A1 B3 |->
%D
%D    A0 A1 -> .plabel= l f
%D    B0 B1 -> .plabel= b TA
%D    B0 B2 -> .plabel= r Ff
%D    B1 B3 -> .plabel= r Gf
%D    B2 B3 -> .plabel= b TB
%D    C0 C1 -> .plabel= b T
%D ))
%D enddiagram
%D
%D diagram NT-1
%D 2Dx     100 +20 +30
%D 2D  100 A0  B0  B1
%D 2D
%D 2D  +30 A1  B2  B3
%D 2D
%D 2D  +15     C0  C1
%D 2D
%D ren A0 A1 ==> A B
%D ren B0 B1 B2 B3 ==> FA GA FB GB
%D ren C0 C1 ==> F G
%D
%D (( A0 A1 -> .plabel= l f
%D    B0 B1 -> .plabel= a TA
%D    B0 B2 -> .plabel= l Ff
%D    B1 B3 -> .plabel= r Gf
%D    B2 B3 -> .plabel= a TB
%D    C0 C1 -> .plabel= a T
%D ))
%D enddiagram
%D
$$\pu \diag{NT-0} \quad \Longrightarrow \quad \diag{NT-1}$$

\newpage

%   ____                   _   _ _          ________
%  / ___|___  _ ____   __ | \ | | |_ ___   / /___ \ \
% | |   / _ \| '_ \ \ / / |  \| | __/ __| | |  __) | |
% | |__| (_) | | | \ V /  | |\  | |_\__ \ | | / __/| |
%  \____\___/|_| |_|\_/   |_| \_|\__|___/ | ||_____| |
%                                          \_\    /_/
%
% «convention-NTs-2»  (to ".convention-NTs-2")
% (nyop 34 "convention-NTs-2")
% (nyo     "convention-NTs-2")

{\bf Another diagrammatic convention on NTs}

If $F,G:\catC→\Set$ are functors going \ColorRed{to $\Set$} and

$T:F→G$ is a natural transformation between them,

we draw everything as before, but we add

at the right \ColorRed{an internal view of the internal view}.

% The square commutes when $∀x∈FA.((Gf∘TA)(x) = (TB∘Ff)(x))$.

%D diagram NT-2
%D 2Dx     100 +20 +30 +25 +45
%D 2D  100 A0  B0  B1  D0  D1
%D 2D  +22                 D3'
%D 2D  +8  A1  B2  B3  D2  D3
%D 2D
%D 2D  +15     C0  C1
%D 2D
%D ren A0 A1       ==> A B
%D ren B0 B1 B2 B3 ==> FA GA FB GB
%D ren C0 C1       ==> F G
%D ren D0 D1 D3'   ==> x (TA)(x) (Gf∘TA)(x)
%D ren    D2 D3    ==>   (Ff)(x) (TB∘Ff)(x)
%D
%D (( A0 A1 -> .plabel= l f
%D    B0 B1 -> .plabel= a TA
%D    B0 B2 -> .plabel= l Ff
%D    B1 B3 -> .plabel= r Gf
%D    B2 B3 -> .plabel= a TB
%D    C0 C1 -> .plabel= a T
%D    D0 D1 |-> D1 D3' |-> D0 D2 |-> D2 D3 |->
%D ))
%D enddiagram
%D
$$\pu \diag{NT-2}$$

% Tom Leinster has a diagram like my internal view of
% the internal view...
% (find-leinsterbasicpage (+ 8  86)   "Lemma 4.1.10")
% (find-leinsterbasictext (+ 8  86)   "Lemma 4.1.10")

\newpage

% (nyop 35 "convention-adjs")

{\bf A diagrammatic convention on adjunctions}

I draw adjunctions like this --- see \cite{IDARCT}.

%D 2Dx     100  +30    +25  +25
%D 2D  100      LA <-| A
%D 2D           |      |
%D 2D           v      v
%D 2D  +20 G    LB <-| B    I
%D 2D      |    |      |    |
%D 2D      v    v      v    v
%D 2D  +20 H    C |--> RC   J
%D 2D           |      |
%D 2D           v      v
%D 2D  +20      D |--> RD
%D 2D
%D 2D  +20      E <==> F
%D 2D
%D ren LA A ==> LA' A'
%D ren LB B ==> LA  A
%D ren C RC ==> B  RB
%D ren D RD ==> B' RB'
%D ren E F  ==> \catB \catA
%D ren G H  ==> LRB B
%D ren I J  ==> A RLA
%D
%D (( LA A <-| # .plabel= a L_0
%D    LB B <-| # .plabel= a L_0
%D    C RC |-> # .plabel= b R_0
%D    D RD |-> # .plabel= b R_0
%D
%D    LA  B harrownodes nil 20 nil <-| # sl^ .plabel= a L_1
%D    LB RC harrownodes nil 20 nil <-| sl^ # .plabel= a ♭
%D    LB RC harrownodes nil 20 nil |-> sl_ # .plabel= b ♯
%D    C  RD harrownodes nil 20 nil |-> # sl^ .plabel= b R_1
%D
%D    LA LB -> # .plabel= l Lα
%D     A  B -> # .plabel= r  α
%D    LB  C -> # .plabel= l \sm{g^♭\\f}
%D     B RC -> # .plabel= r \sm{g\\f^♯}
%D     C  D -> # .plabel= l β
%D    RC RD -> # .plabel= r Rβ
%D    E F <- sl^ .plabel= a L
%D    E F -> sl_ .plabel= b R
%D  # G H -> .plabel= l εB
%D  # I J -> .plabel= r ηA
%D ))
%D enddiagram
%D
%D diagram (xB)-|(B->)
%D 2Dx     100  +45    +25  +40
%D 2D  100      LA <-| A
%D 2D           |      |
%D 2D           v      v
%D 2D  +20 G    LB <-| B    I
%D 2D      |    |      |    |
%D 2D      v    v      v    v
%D 2D  +20 H    C |--> RC   J
%D 2D           |      |
%D 2D           v      v
%D 2D  +20      D |--> RD
%D 2D
%D 2D  +20      E <==> F
%D 2D
%D ren LA A ==> A{×}C A
%D ren LB B ==> B{×}C B
%D ren C RC ==> D (C{→}D)
%D ren D RD ==> E (C{→}E)
%D ren E F  ==> \Set \Set
%D ren G H  ==> (C{→}D){×C} D
%D ren I J  ==> B (C→B{×}C)
%D ren I J  ==> B (C{→}(B{×}C))
%D
%D (( LA A <-| # .plabel= a ({×}B)_0
%D    LB B <-| # .plabel= a ({×}B)_0
%D    C RC |-> # .plabel= b (B{→})_0
%D    D RD |-> # .plabel= b (B{→})_0
%D
%D    LA  B harrownodes nil 20 nil <-| # sl^ .plabel= a L_1
%D    LB RC harrownodes nil 20 nil <-| sl^ # .plabel= a ♭
%D    LB RC harrownodes nil 20 nil |-> sl_ # .plabel= b ♯
%D    C  RD harrownodes nil 20 nil |-> # sl^ .plabel= b R_1
%D
%D    LA LB -> # .plabel= l λp.(f(πp),π'p)
%D     A  B -> # .plabel= r f
%D    LB  C -> # .plabel= l \sm{λp.g(πp)(π'p)\\\phantom{mmmmmm}h}
%D     B RC -> # .plabel= r \sm{g\phantom{mmmmm}\\λb.λc.h(b,c)}
%D     C  D -> # .plabel= l k
%D    RC RD -> # .plabel= r λf.λc.k(fc)
%D    E F <- sl^ .plabel= a ({×}C)
%D    E F -> sl_ .plabel= b (C{→})
%D  # G H -> .plabel= l λp.(πp)(π'p)
%D  # I J -> .plabel= r λb.λc.(b,c)
%D ))
%D enddiagram
%D
$$\pu \diag{generic-adjunction} \qquad \diag{(xB)-|(B->)}$$

Left: general case. Right: my favorite particular case.

% When I explain CT to beginners I start by $({×}B)⊣(B{→})$.

\newpage

% «convention-univs»  (to ".convention-univs")
% (nyop 36 "convention-NTs-2")
% (nyo     "convention-NTs-2")

{\bf A diagrammatic convention on universals}

I draw universals like this.

Left: general case. Right: my favorite particular case.

%D diagram convention-univs
%D 2Dx     100 +25 +45 +35
%D 2D  100     A3      C3
%D 2D
%D 2D  +20 A4  A5  C4  C5
%D 2D
%D 2D  +20 A6  A7  C6  C7
%D 2D
%D 2D  +20 B0  B1  D0  D1
%D 2D
%D ren    A3    C3 ==>      A            B
%D ren A4 A5 C4 C5 ==>  B  RB  B{×}C (C{→}B{×}C)
%D ren A6 A7 C6 C7 ==>  B' RB'     D (C{→}D)
%D ren B0 B1 D0 D1 ==> \catB \catA \Set \Set
%D
%D (( A3 A5  ->             .plabel= r η
%D    A4 A5 |->
%D    A4 A6  ->             .plabel= l ∃!g
%D    A5 A7  ->             .plabel= r Rg
%D    A6 A7 |->
%D    A3 A7 -> .slide= 20pt .plabel= r ∀f
%D    A4 A7 harrownodes nil 20 nil |->
%D    B0 B1 -> .plabel= a R
%D
%D    C3 C5  ->             .plabel= r η
%D    C4 C5 |->
%D    C4 C6  ->             .plabel= l ∃!g
%D    C5 C7  ->             .plabel= r Rg
%D    C6 C7 |->
%D    C3 C7 -> .slide= 30pt .plabel= r ∀f
%D    C4 C7 harrownodes nil 20 nil |->
%D    D0 D1 -> .plabel= a (C{→}\_)
%D ))
%D enddiagram
%D
$$\pu \diag{convention-univs}$$

\bsk

My convention on how to draw the Yoneda Lemma

is based on that shape.

\newpage

% «that-looks-like-logic»  (to ".that-looks-like-logic")
% (nyop 37 "that-looks-like-logic")
% (nyo     "that-looks-like-logic")

\vspace*{20pt}

\begin{center}
\Huge{\bf A notation} \\[0pt]
\Huge{\bf that looks} \\[0pt]
\Huge{\bf like Logic}    \\[0pt]
\end{center}

\thispagestyle{empty}

\newpage

%  _____                   _ _____ __
% |  ___| __ ___ _   _  __| |___  / /_
% | |_ | '__/ _ \ | | |/ _ |  / / '_ \
% |  _|| | |  __/ |_| | (_| | / /| (_) |
% |_|  |_|  \___|\__, |\__,_|/_/  \___/
%                |___/
%
% «freyd76»  (to ".freyd76")
% (nyop 38 "freyd76")
% (nyo    "freyd76")

{\bf Origins: Freyd76}

The diagrams here are \ColorRed{based} on the ones

from \cite{Freyd76}, but with several changes.

\ssk

\cite{Freyd76} uses bars with quantifiers,

that mean, for example,

for all extensions of the previous diagram to this
one''...

% (dnop 2 "freyd")
% (dno    "freyd")
% (dno    "freyd" "cat-has-equalizers-2")
%
%D diagram freyd76-1
%D 2Dx     100 +00   +15   +20 +15 +15   +20   +20 +15 +15   +20   +20 +15 +15   +20   +20
%D 2D  100 U0                  U1                  U2                  U3
%D 2D       |                   |                   |                   |
%D 2D  +10  |  A0               |  B0               |  C0               |  D0
%D 2D       |  |  \             |  |  \             |  |  \             |  |  \
%D 2D  +20  |  A1 -- A2 == A3   |  B1 -- B2 == B3   |  C1 -- C2 == C3   |  D1 -- D2 == D3
%D 2D       |                   |                   |                   |
%D 2D  +20 L0                  L1                  L2                  L3
%D 2D
%D ren U0 L0 A0 A1 A2 A3 ==> ∀  {}
%D ren U1 L1 B0 B1 B2 B3 ==> ∃  {}
%D ren U2 L2 C0 C1 C2 C3 ==> ∀  {}
%D ren U3 L3 D0 D1 D2 D3 ==> ∃! {}
%D # ren U2              ==> \ColorRed{∀}
%D
%D (( B2 B3 -> sl^^ # .plabel= a f
%D    B2 B3 -> sl__ # .plabel= b g
%D    B2 B3 midpoint .TeX= * place
%D    B1 B2 -> # .plabel= b e
%D ))
%D (( U2 L2 -
%D    C2 C3 -> sl^^ # .plabel= a f
%D    C2 C3 -> sl__ # .plabel= b g
%D    C2 C3 midpoint .TeX= * place
%D    C1 C2 -> # .plabel= b e
%D    C0 C2 -> # .plabel= r h
%D ))
%D (( U3 L3 -
%D    D2 D3 -> sl^^ # .plabel= a f
%D    D2 D3 -> sl__ # .plabel= b g
%D    D2 D3 midpoint .TeX= * place
%D    D1 D2 -> # .plabel= b e
%D    D0 D2 -> # .plabel= r h
%D    D0 D1 -> # .plabel= l k
%D ))
%D enddiagram
%D
$$\pu \scalebox{0.8}{ \diag{freyd76-1} }$$

\newpage

%  _____                   _ _____ __      ________
% |  ___| __ ___ _   _  __| |___  / /_    / /___ \ \
% | |_ | '__/ _ \ | | |/ _ |  / / '_ \  | |  __) | |
% |  _|| | |  __/ |_| | (_| | / /| (_) | | | / __/| |
% |_|  |_|  \___|\__, |\__,_|/_/  \___/  | ||_____| |
%                |___/                    \_\    /_/
%
% «freyd76-2»  (to ".freyd76-2")
% (nyop 39 "freyd76")
% (nyo    "freyd76")

{\bf Origins: Freyd76 (2)}

We can draw them more compactly

if we use numbered quantifiers.

A category {\sl has equalizers} iff:

%D diagram equalizer-big-1
%D 2Dx     100   +20   +20
%D 2D  100 A0
%D 2D      |  \
%D 2D  +20 A1 -- A2 == A3
%D 2D
%D ren A0 A1 A2 A3 ==> X E A B
%D ren A0 A1 A2 A3 ==>
%D
%D (( A2 A3 -> sl^^ .plabel= a ∀_1
%D    A2 A3 -> sl__ .plabel= b ∀_1
%D    A2 A3 midpoint .TeX= * place
%D    A1 A2 -> .plabel= b ∃_2
%D    A0 A2 -> .plabel= r ∀_3
%D    A0 A1 -> .plabel= l ∃!_4
%D ))
%D enddiagram
%D
$$\pu \scalebox{2}{ \diag{equalizer-big-1} }$$

\newpage

% «freyd76-3»  (to ".freyd76-3")
% (nyop 40 "freyd76-3")
% (nyo     "freyd76-3")

{\bf Origins: Freyd76 (3)}

At some point I started to draw

the $∀∃!$''s as functions and

this gave me arrows between arrows...

%D diagram equalizer-big-2
%D 2Dx     100 +15 +15   +30
%D 2D  100 A0
%D 2D      |  \
%D 2D  +15 M0  M1
%D 2D      |     \
%D 2D  +15 A1 ---- A2 == A3
%D 2D
%D ren A0 A1 A2 A3 ==> X E A B
%D ren A0 A1 A2 A3 ==>
%D ren M0 M1 ==> {} {}
%D
%D (( A2 A3 -> sl^^ .plabel= a f
%D    A2 A3 -> sl__ .plabel= b g
%D    A2 A3 midpoint .TeX= * place
%D    A1 A2 -> .plabel= b e
%D    A0 A2 -> .plabel= r h
%D    A0 A1 -> .plabel= l k
%D
%D    M0 M1 harrownodes nil 17 nil <- .plabel= b φ
%D ))
%D enddiagram
%D
$$\pu \scalebox{1.5}{ \diag{equalizer-big-2} }$$

The equalizerness'' of the lower
%
$\diagxyto/->/ \two/->->/$
%

is the small horizontal arrow inside the triangle.

\newpage

% «arrows-between-arrows»  (to ".arrows-between-arrows")
% (nyop 41 "arrows-between-arrows")
% (nyo     "arrows-between-arrows")

{\bf Arrows between arrows}

\ColorRed{Some} of my diagrams with

arrows between arrows

\ColorRed{look like Logic}.

For example:

%D diagram arrows-between-arrows
%D 2Dx     100 +35 +50 +35
%D 2D  100 A0  A1  B0  B1
%D 2D
%D 2D  +35 A2  A3  B2  B3
%D 2D
%D ren A0 A1 ==> X \Hom_\catC(A,X)
%D ren A2 A3 ==> Y \Hom_\catC(A,Y)
%D ren B0 B1 ==> X (A{→}X)
%D ren B2 B3 ==> Y (A{→}Y)
%D
%D (( A0 A1 |->
%D    A2 A3 |->
%D    A0 A2 -> .plabel= l f
%D    A1 A3 -> .plabel= r \Hom_\catC(A,f)
%D    A0 A3 harrownodes nil 20 nil |->
%D
%D    B0 B2 ->
%D    B1 B3 ->
%D    B0 B3 harrownodes nil 35 nil ->
%D ))
%D enddiagram
%D
$$\pu \diag{arrows-between-arrows}$$

\bsk

$$\phantom{mmmmmm}(X→Y) → ((A→X)→(A→Y))$$

\newpage

% «arrows-between-arrows-2»  (to ".arrows-between-arrows-2")
% (nyop 42 "arrows-between-arrows-2")
% (nyo     "arrows-between-arrows-2")

{\bf Arrows between arrows (2)}

\ColorRed{Some} of my diagrams with

arrows between arrows

\ColorRed{look like Logic}.

\msk

This motivated me to try to define

a certain (incomplete!) system of

Natural Deduction for Categories...

\msk

\ColorRed{More on this in the last slides.}

\newpage

% «diagrams-induce-typings»  (to ".diagrams-induce-typings")
% (nyop 43 "diagrams-induce-typings")
% (nyo     "diagrams-induce-typings")

{\bf Diagrams induce typings}

...and this lets us omit some typings! An example:

%D diagram diagrams-induce-typings
%D 2Dx     100 +25
%D 2D  100     A3
%D 2D
%D 2D  +20 A4  A5
%D 2D
%D 2D  +20 A6  A7
%D 2D
%D 2D  +20 B0  B1
%D 2D
%D ren    A3 ==>      A
%D ren A4 A5 ==>  B  RB
%D ren A6 A7 ==> ∀B' RB'
%D ren B0 B1 ==> \catB \catA
%D
%D (( A3 A5  ->             .plabel= r η
%D    A4 A5 |->
%D    A4 A6  ->             .plabel= l ∃!g
%D    A5 A7  ->             .plabel= r Rg
%D    A6 A7 |->
%D    A3 A7 -> .slide= 20pt .plabel= r ∀f
%D    A4 A7 harrownodes nil 20 nil |->
%D    B0 B1 -> .plabel= a R
%D ))
%D enddiagram
%D
\pu
$$\diag{diagrams-induce-typings} \qquad \begin{array}[c]{l} ∀B':\Objs(\catB). \\ ∀f:A→RB'. \\ ∃!g:B→B'. \\ f = Rg∘η \\ \\ \phantom{mmm}\Downarrow \\ \\ ∀B'. \; \\ ∀f. \; \\ ∃!g. \\ f = Rg∘η \end{array}$$

\newpage

% «diagrams-induce-props»  (to ".diagrams-induce-props")
% (nyop 44 "diagrams-induce-props")
% (nyo     "diagrams-induce-props")

{\bf Diagrams with quantifiers induce propositions}

In \cite{Freyd76} every extension of a diagram to the next one

commutes by default, and non-commuting cells have to be

indicated... if we follow this convention,

$∃!g.\;f=Rg∘η$'' can be rewritten as:

$∃!g$ (such that everything commutes)''.

Another convention: $∀$''s come before $∃!$''s. So:

$$\diag{diagrams-induce-typings} \qquad \begin{array}[c]{l} ∀B'. \; ∀f. \; ∃!g. \\ f = Rg∘η \\ \phantom{mmm}\Downarrow \\ ∀B'. \; ∀f. \; ∃!g \\ \phantom{mmm}\Downarrow \\ ∀\_\_.∃\_ \\ \phantom{mmm}\Downarrow \\ \text{(nothing!)} \end{array}$$

\newpage

% «diagrams-induce-props-2»  (to ".diagrams-induce-props-2")
% (nyop 45 "diagrams-induce-props-2")
% (nyo     "diagrams-induce-props-2")

{\bf Diagrams with quantifiers induce propositions (2)}

With these conventions the default proposition associated

to the diagram at the left is the one at the right.

We don't need to write down the proposition ---

it can be extracted from the diagram.

Note that the $∀B'$'' must come before the $∀f$''.

$$\diag{diagrams-induce-typings} \qquad \Longrightarrow \qquad \begin{array}[c]{l} ∀B':\Objs(\catB). \\ ∀f:A→RB'. \\ ∃!g:B→B'. \\ f = Rg∘η \\ \end{array}$$

\newpage

%  _         _           _              ____
% | |    ___(_)_ __  ___| |_ ___ _ __  |  _ \ ___ _ __ _ __ ___  _ __   ___
% | |   / _ \ | '_ \/ __| __/ _ \ '__| | |_) / _ \ '__| '__/ _ \| '_ \ / _ \
% | |__|  __/ | | | \__ \ ||  __/ |    |  __/  __/ |  | | | (_) | | | |  __/
% |_____\___|_|_| |_|___/\__\___|_|    |_|   \___|_|  |_|  \___/|_| |_|\___|
%
% (nyop 46 "ask-leinster-and-perrone")

{\bf TODO: Ask Tom Leinster and Paolo Perrone}

They both have books on basic CT that are available online

and that use some of these diagrammatic conventions...

See: \cite[Introduction]{Leinster}

and \cite[Chapter 4]{Perrone}.

\msk

Are these conventions common?

Where are they formalized?

(I don't know!!! I'm an outsider!!!)

${=}($

% (find-books "__cats/__cats.el" "leinster-basic")
% (find-leinsterbasicpage (+ 8 3) "This diagram means")
% (find-leinsterbasictext (+ 8 3) "This diagram means")
% (find-books "__cats/__cats.el" "perrone")
% (find-perronenctpage 116   "precisely the universal property of a basis")
% (find-perronencttext 116   "precisely the universal property of a basis")

\newpage

%  __  __       _   _            _   _
% |  \/  | ___ | |_(_)_   ____ _| |_(_) ___  _ __
% | |\/| |/ _ \| __| \ \ / / _ | __| |/ _ \| '_ \
% | |  | | (_) | |_| |\ V / (_| | |_| | (_) | | | |
% |_|  |_|\___/ \__|_| \_/ \__,_|\__|_|\___/|_| |_|
%
% «motivation»  (to ".motivation")
% (nyop 47 "motivation")
% (nyo     "motivation")

{\bf Motivation}

People who are very visual often remember statements, constructions
and proofs via shapes and movement (\cite{IDARCT}). For them the
diagrams are the skeletons'' of formal proofs
(\cite[sec.12]{IDARCT}).

\ssk

The shape'' of the Yoneda Lemma that I will present in these slides
is my favorite way for remembering \ColorRed{both} the
\ColorRed{statement} and the \ColorRed{proof} of the YL --- and its
variants!!!

\ssk

In order to work with diagrams {\sl formally} we need to be able to
translate our diagrams to languages that are {\sl precise} and {\sl
well-known}. One way to do that is to treat our diagrams as
skeletons for their formalizations in Type Theory.

% \ssk
%
% I'm currently \ColorRed{trying} to implement/program this in Idris.

\ssk

For an introduction to using TT as foundations, see \cite[introduction
and chapter 1]{HOTT}.

\ssk

\ColorGreen{I'm currently trying to implement/program this in Idris.}

% (find-angg ".emacs" "idarct-preprint")
% (find-books "__logic/__logic.el" "hott")

% In \cite{IDARCT} I sketched, in a {\sl very} incomplete way, how a system
% of Natural Deduction for Categories could work (with a kind of
% Curry-Howard, even!); I will use some its ideas here, but not
% explicitly.
%
% The introduction of [PH1] mentions some
%
% Once we have fixed a shape for a

\newpage

% «back-to-the-yoneda-lemma»  (to ".back-to-the-yoneda-lemma")
% (nyop 48 "back-to-the-yoneda-lemma")
% (nyo     "back-to-the-yoneda-lemma")

\vspace*{20pt}

\begin{center}
\Huge{\bf BACK TO THE}   \\[0pt]
\Huge{\bf YONEDA} \\
\Huge{\bf LEMMA} \\
\end{center}

\thispagestyle{empty}

\newpage

%  _____  __   ___
% |___ /  \ \ / / |    ___
%   |_ \   \ V /| |   / __|
%  ___) |   | | | |___\__ \
% |____/    |_| |_____|___/
%
% «three-yoneda-lemmas» (to ".three-yoneda-lemmas")
% (nyop 49 "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 /| |   / __| | |  __) | |
%  ___) |   | | | |___\__ \ | | / __/| |
% |____/    |_| |_____|___/ | ||_____| |
%                            \_\    /_/
%
% «three-yoneda-lemmas-2»  (to ".three-yoneda-lemmas-2")
% (nyop 4 "three-yoneda-lemmas-2")
% (nyo    "three-yoneda-lemmas-2")

{\bf Three Yoneda Lemmas (and their names)}

\msk

%D diagram three-yonedas-0
%D 2Dx     100    +40  +35    +40  +35    +45
%D 2D  100        L0          M0          R0
%D 2D              |           |           |
%D 2D              v           v           v
%D 2D  +25 L1 |-> L2   M1 |-> M2   R1 |-> R2
%D 2D
%D 2D   +0 L3 --> L4   M3 --> M4   R3 --> R4
%D 2D
%D 2D  +20 L5 --> L6   M5 --> M6   R5 --> R6
%D 2D              |           |           |
%D 2D              v           v           v
%D 2D  +25        L7          M7          R7
%D 2D
%D ren L0 L1 L2 ==> A C RC
%D ren L5 L6 L7 ==> (C{→}\_) (A{→}R\_) \phantom{R}
%D
%D (( L1 L2 |-> L0 L2 -> .plabel= r γ
%D    L5 L6 -> .plabel= a T
%D    L7 place
%D ))
%D
%D ren M0 M1 M2 ==> 1 C RC
%D ren M5 M6 M7 ==> (C{→}\_) (1{→}R\_) R
%D
%D (( M1 M2 |-> M0 M2 -> .plabel= r γ
%D    M5 M6 -> .plabel= a T
%D    M6 M7 <->
%D    M5 M7 -> .plabel= l T'
%D ))
%D
%D ren R0 R1 R2 ==> 1 C (B{→C})
%D ren R5 R6 R7 ==> (C{→}\_) (1{→}(B{→}\_)) (B{→}\_)
%D
%D (( R1 R2 |-> R0 R2 -> .plabel= r γ
%D    R5 R6 -> .plabel= a T
%D    R6 R7 <->
%D    R5 R7 -> .plabel= l T'
%D ))
%D enddiagram
%
\pu

$\resizebox{0.98\textwidth}{!}{%$\diag{three-yonedas-0}
$}$

\msk

Left: an (obscure?) lemma from adjunctions.

Middle: the \ColorRed{Yoneda Lemma.}

Right: the \ColorRed{Yoneda Embedding.}

\msk

Left: $\Hom(A,RC) ≅ \Nat(\Hom(C,-),\Hom(A,R-))$

Middle: \phantom{mmm} $RC ≅ \Nat(\Hom(C,-),R)$

Right: $\Hom(B,C) ≅ \Nat(\Hom(C,-),\Hom(B,-))$

\newpage

\newpage

%   ____                           _   _
%  / ___|___  _ ____   _____ _ __ | |_(_) ___  _ __  ___
% | |   / _ \| '_ \ \ / / _ \ '_ \| __| |/ _ \| '_ \/ __|
% | |__| (_) | | | \ V /  __/ | | | |_| | (_) | | | \__ \
%  \____\___/|_| |_|\_/ \___|_| |_|\__|_|\___/|_| |_|___/
%
% «notational-conventions»  (to ".notational-conventions")
% (nyop 4 "notational-conventions")
% (nyo    "notational-conventions")

{\bf Some notational conventions}

We will follow the conventions for internal and external diagrams from
\cite[introduction]{PH1}, with some slight changes.

\ssk

In the diagram below we have the external view of the functor
$F:\catC→\catA$ below and its internal view above.

\ssk

The object $C$ over $\catC$ is in the category $\catC$.

\ssk

The morphism $γ:A→FC$ above $\catA$ is in the category $\catA$.

\ssk

The arrow $C ↦ FC$ shows the functor $F$ acting on an object.

Note the difference between $→$' and $↦$'!
%
%D diagram notation-1
%D 2Dx     100    +40
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> FC
%D 2D
%D 2D  +15 catC catA
%D 2D
%D ren catC catA ==> \catC \catA
%D
%D (( C FC |->
%D    A FC  -> .plabel= r γ
%D    catC catA -> .plabel= a F
%D ))
%D enddiagram
$$\pu \diag{notation-1}$$

\newpage

{\bf Some notational conventions (2)}

We will sometimes omit the external view.

\ssk

1 is an object of $\Set$ --- the singleton set.

In this diagram there's a morphism $\nameof{x}: 1 → FC$,

so $1$ and $FC$ are in the same category, so $FC$ is in $\Set$.

\ssk

$\nameof{x}$ is pronounced the name of $x$''.

The image of a map $\nameof{α}: 1→A$ is the element $α∈A$.

%D diagram notation-2
%D 2Dx     100    +40
%D 2D  100        1
%D 2D             |
%D 2D             v
%D 2D  +25 C |-> FC
%D 2D
%D 2D  +15 catC catA
%D 2D
%D ren catC catA ==> \catC \Set
%D
%D (( C FC |->
%D    1 FC  -> .plabel= r \nameof{x}
%D    catC catA -> .plabel= a F
%D ))
%D enddiagram
%
$$\pu \diag{notation-2}$$

\newpage

{\bf Some notational conventions (3)}

The lower triangle is made of three objects

in another category. What category is that?

\ssk

$R:\catC→\Set$, so $R$ is an object of $\Set^\catC$,

and $(C{→}\_)$ and $(1{→}R\_)$ are objects of $\Set^\catC$ too.

\ssk

$R$, $(C{→}\_)$, and $(1{→}R\_)$ are functors, so $T$ and $T'$ are NTs.
%
%D diagram notation-3
%D 2Dx     100    +40
%D 2D  100        M0
%D 2D              |
%D 2D              v
%D 2D  +20 M1 |-> M2
%D 2D
%D 2D  +10 M3 --> M4
%D 2D
%D 2D  +15 M5 --> M6
%D 2D              |
%D 2D              v
%D 2D  +20        M7
%D 2D
%D ren M0 M1 M2 ==> 1 C RC
%D ren M3 M4    ==> \catC \Set
%D ren M5 M6 M7 ==> (C{→}\_) (1{→}R\_) R
%D
%D (( M1 M2 |-> M0 M2 -> .plabel= r γ
%D    M3 M4 -> .plabel= a R
%D    M5 M6 -> .plabel= a T
%D    M6 M7 <->
%D    M5 M7 -> .plabel= l T'
%D ))
%D enddiagram
%
\pu
$$\scalebox{0.9}{ \diag{notation-3} }$$

\newpage

{\bf Some notational conventions (4)}

We can use parallel diagrams to compare notations.

At the left: our notation for the Yoneda Lemma.

At the right: the same diagram in the notation of \cite{Riehl}.

She states the Yoneda Lemma as $\Hom(\sfC(c,-),F) ≅ Fc$.

It's her theorem 2.2.4, in page 57.
%
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 57)      "Theorem 2.2.4 (Yoneda lemma).")
% (find-riehlcctext (+ 18 57)      "Theorem 2.2.4 (Yoneda lemma).")
%
%
%D diagram notation-3
%D 2Dx     100    +40 +40    +40
%D 2D  100        M0         R0
%D 2D              |          |
%D 2D              v          v
%D 2D  +20 M1 |-> M2  R1 |-> R2
%D 2D
%D 2D  +10 M3 --> M4  R3 --> R4
%D 2D
%D 2D  +15 M5 --> M6  R5 --> R6
%D 2D              |          |
%D 2D              v          v
%D 2D  +20        M7         R7
%D 2D
%D ren M0 M1 M2 ==> 1 C RC
%D ren M3 M4    ==> \catC \Set
%D ren M5 M6 M7 ==> (C{→}\_) (1{→}R\_) R
%D
%D (( M1 M2 |-> M0 M2 -> .plabel= r γ
%D    M3 M4 -> .plabel= a R
%D    M5 M6 -> .plabel= a T
%D    M6 M7 <->
%D    M5 M7 -> .plabel= l T'
%D ))
%D
%D ren R0 R1 R2 ==> 1 c Fc
%D ren R3 R4    ==> \sfC \sfSet
%D ren R5 R6 R7 ==> \sfC(c,-) \sfSet(1,F(-)) F
%D
%D (( R1 R2 |-> R0 R2 -> .plabel= r \nameof{x}
%D    R3 R4 -> .plabel= a F
%D    R5 R6 ->
%D    R6 R7 <->
%D    R5 R7 -> .plabel= l α
%D ))
%D enddiagram
%
\pu
$$\scalebox{1.0}{ \diag{notation-3} }$$

% \end{document}

% (find-es "tex" "minipage")

\newpage

\newpage

\vspace*{30pt}

\begin{center}
\Huge{\bf The details}   \\[0pt]
\huge{\bf (as types and terms)}   \\[0pt]
\end{center}

\thispagestyle{empty}

\newpage

%  _____ _          _    __   ___
% |  ___(_)_ __ ___| |_  \ \ / / |
% | |_  | | '__/ __| __|  \ V /| |
% |  _| | | |  \__ \ |_    | | | |___
% |_|   |_|_|  |___/\__|   |_| |_____|
%
% «first-yoneda-lemma» (to ".first-yoneda-lemma")
% (nyop 20 "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 21 "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 22 "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 23 "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 24 "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 25 "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 26 "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 63 "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 28 "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 29 "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 30 "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")
% (nyop 31 "changing-A-to-Set")
% (nyo     "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 32 "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 33 "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 34 "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 35 "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 36 "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 37 "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 38 "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 39 "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 40 "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 41 "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

%  _   _ _____ _     ____    _   _ _____ _____ ____  _____ ____
% | | | | ____| |   |  _ \  | \ | | ____| ____|  _ \| ____|  _ \
% | |_| |  _| | |   | |_) | |  \| |  _| |  _| | | | |  _| | | | |
% |  _  | |___| |___|  __/  | |\  | |___| |___| |_| | |___| |_| |
% |_| |_|_____|_____|_|     |_| \_|_____|_____|____/|_____|____/
%
% «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

%  ____  _      _   _                        _
% |  _ \(_) ___| |_(_) ___  _ __   __ _ _ __(_) ___  ___
% | | | | |/ __| __| |/ _ \| '_ \ / _ | '__| |/ _ \/ __|
% | |_| | | (__| |_| | (_) | | | | (_| | |  | |  __/\__ \
% |____/|_|\___|\__|_|\___/|_| |_|\__,_|_|  |_|\___||___/
%
% «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

\newpage

\noedrxfooter

\vspace*{30pt}

\begin{center}
\Huge{\bf ND for}   \\[0pt]
\Huge{\bf Cats}   \\[0pt]
\end{center}

\thispagestyle{empty}

\newpage

\def\ren{\text{ren}}
\def→{{\to}}

%:
%:
%:                           [:C→D]^2  [:D→E]^3
%:                           ------------------
%:                              :C→E
%:                          ------------2
%:                          :(C→D)→(C→E)
%:                       -------------------3
%:   C:  [D:]^1          :(D→E)→((C→D)→(C→E))
%:   ----------        -----------------------
%:     C→D:            :ΠD.(D→E)→((C→D)→(C→E))
%:   -------         --------------------------
%:   λD.C→D:         :ΠD.ΠE.(D→E)→((C→D)→(C→E))
%:   -------\ren     --------------------------\ren
%:   (C→\_)_0:              (C→\_)_1:
%:   --------------------------------
%:            (C→\_):
%:
%:            ^C->_
%:
%:
$$\pu \ded{C->_}$$

%:
%:
%:                                  [:D→E]^3
%:                                  ------
%:                       [:A→RD]^2  :RD→RE
%:                       -----------------
%:                               :A→RE
%:                          --------------2
%:   [D:]^1                 :(A→RD)→(A→RE)
%:   ------             ----------------------3
%:    RD:               :(D→E)→((A→RD)→(A→RE))
%:   -----             -------------------------
%:   A→RD:             :ΠE.(D→E)→((A→RD)→(A→RE))
%:   --------        ----------------------------
%:   ∧D.A→RD:        :ΠD.ΠE.(D→E)→((A→RD)→(A→RE))
%:   --------\ren    ---------------------------\ren
%:   (A→R\_)_0:            (A→R\_)_1:
%:   --------------------------------
%:              (A→R\_):
%:
%:              ^A->R_
%:
%:
$$\pu \ded{A->R_}$$

%:
%:                [:C→D]^1
%:                --------
%:    [:A→RC]^2    :RC→RD
%:    -------------------
%:            :A→RD
%:       -------------1
%:       :(C→D)→(A→RD)
%:     ----------------
%:     :ΠD.(C→D)→(A→RD)           C:    C:   [:(C→\_)→(A→R\_)]^2
%:     ------------------\ren    ----   ----------------------
%:     ((C→\_)→(A→R\_))_0:       :C→C   :(C→C)→(A→RC)
%:     -------------------       ------------
%:     :(C→\_)→(A→R\_)             :A→RC
%:     ---------------------------------2
%:        :(A→RC)↔((C→\_)→(A→R\_))
%:
%:        ^yoneda0-bij
%:
$$\pu \ded{yoneda0-bij}$$

\newpage

\printbibliography

\end{document}

%  __  __       _
% |  \/  | __ _| | _____
% | |\/| |/ _ | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%
% <make>

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020notes-yoneda veryclean
make -f 2019.mk STEM=2020notes-yoneda pdf

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