|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2019notes-yoneda.tex")
% (find-angg "LATEX/2019notes-yoneda.bib")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019notes-yoneda.tex" :end))
% (defun c0 () (interactive) (find-LATEXsh "pdflatex -record 2019notes-yoneda.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019notes-yoneda.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019notes-yoneda.pdf"))
% (defun e () (interactive) (find-LATEX "2019notes-yoneda.tex"))
% (defun b () (interactive) (find-LATEX "2019notes-yoneda.bib"))
% (defun u () (interactive) (find-latex-upload-links "2019notes-yoneda"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page "~/LATEX/2019notes-yoneda.pdf")
% (find-pdf-text "~/LATEX/2019notes-yoneda.pdf")
% (find-sh0 "cp -v ~/LATEX/2019notes-yoneda.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019notes-yoneda.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019notes-yoneda.pdf
% file:///tmp/2019notes-yoneda.pdf
% file:///tmp/pen/2019notes-yoneda.pdf
% http://angg.twu.net/LATEX/2019notes-yoneda.pdf
%
% A diagram for the Yoneda Lemma
% (In which each node and arrow can be
% interpreted precisely as a lambda-term,
% and most of the interpretations are
% "obvious"; plus dictionaries!!!)
%
% (find-TH "math-b" "notes-yoneda")
% (find-es "dednat" "arxiv-yoneda")
% «.colors» (to "colors")
% «.yoneda-R-5» (to "yoneda-R-5")
% «.yoneda-R-5+» (to "yoneda-R-5+")
% «.yoneda-R-6» (to "yoneda-R-6")
% «.yoneda-B->-6» (to "yoneda-B->-6")
% «.yoneda-R-ACDE» (to "yoneda-R-ACDE")
% «.yoneda-F1» (to "yoneda-F1")
% «.yoneda-F2» (to "yoneda-F2")
% «.yoneda-Tobjs» (to "yoneda-Tobjs")
% «.yoneda-Tsqcond» (to "yoneda-Tsqcond")
% «.yoneda-bij» (to "yoneda-bij")
% «.yoneda-curve-with-terms» (to "yoneda-curve-with-terms")
% «.title-page» (to "title-page")
%
% «.the-big-picture» (to "the-big-picture")
% «.the-big-picture-diag» (to "the-big-picture-diag")
% «.eilenberg-steenrod» (to "eilenberg-steenrod")
% «.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")
%
% «.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")
%
% «.motivation» (to "motivation")
% «.three-yoneda-lemmas» (to "three-yoneda-lemmas")
%
% «.internal-view-to-do» (to "internal-view-to-do")
% «.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]{article}
\usepackage{ifluatex}
\ifluatex
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\else
\usepackage[utf8]{inputenc}
\input 2019oxford-chars.tex % (find-LATEX "2019oxford-chars.tex")
\fi
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=violet]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
\usepackage{color} % (find-LATEX "edrx15.sty" "colors")
\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
\usepackage{stmaryrd}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15} % (find-LATEX "edrx15.sty")
%\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
%\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
%
% (find-angg ".emacs.papers" "latexgeom")
% (find-LATEXfile "2016-2-GA-VR.tex" "{geometry}")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[paperwidth=11.5cm, paperheight=9.5cm,
%total={6.5in,4in},
%textwidth=4in, paperwidth=4.5in,
%textheight=5in, paperheight=4.5in,
%a4paper,
top=1.5cm, bottom=.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")
%
\begin{document}
% \catcode`\^^J=10
% \directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% (find-dednat6 "demo-write-dnt.tex")
%
\ifluatex
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}
\else
% \input\jobname.dnt
\input 2019notes-yoneda.dnt
\def\pu{}
\fi
%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")
% Adapted from:
% (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 (for example, 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{Riehl\\YL}
%D ren A1 ==> \BTL{CWM\\YL}
%D ren A2 ==> \BTL{my\\YL}
%D ren A3 ==> \BTL{types\\and\\defs}
%D ren B0 ==> \BTL{Riehl\\pages\\57--59}
%D ren B1 ==> \BTL{CWM\\pages\\59--61}
%D ren B2 ==> \BTL{Riehl\\diag\\p.80}
%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
% _____ _ _ ____ _ _
% | ____(_) | / ___|| |_ ___ ___ _ __ __ _ _ _ ___ | |_ ___
% | _| | | | \___ \| __/ _ \/ _ \ '_ \ / _` | | | |/ _ \| __/ _ \
% | |___| | | ___) | || __/ __/ | | | | (_| | |_| | (_) | || __/
% |_____|_|_| |____/ \__\___|\___|_| |_| \__, |\__,_|\___/ \__\___|
% |_|
%
% «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
% «missing-diags-elephant» (to ".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
% _____ _ ______ ____ __
% | ____|_ _____ _ __ ___(_)___ ___ / ___\ \ / / \/ |
% | _| \ \/ / _ \ '__/ __| / __|/ _ \ | | \ \ /\ / /| |\/| |
% | |___ > < __/ | | (__| \__ \ __/ | |___ \ V V / | | | |
% |_____/_/\_\___|_| \___|_|___/\___| \____| \_/\_/ |_| |_|
%
% «exercise-cwm» (to ".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}
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 13 "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 14 "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 15 "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 16 "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 17 "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 18 "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 19 "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 13 "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 14 "curry-howard")
% (nyo "curry-howard")
{\bf Curry-Howard in one slide}
(Suggested reading: \cite{GLT}, \cite{WadlerPaT})
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 15 "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 16 "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 17 "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 18 "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 19 "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.
\newpage
% ____ _ _ _____
% / ___|___ _ ____ __ | \ | |_ _|__
% | | / _ \| '_ \ \ / / | \| | | |/ __|
% | |__| (_) | | | \ V / | |\ | | |\__ \
% \____\___/|_| |_|\_/ |_| \_| |_||___/
%
% «convention-NTs» (to ".convention-NTs")
% (nyop 20 "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 21 "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}
$$
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage
\newpage
% «that-looks-like-logic» (to ".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 4 "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 5 "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")
{\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 7 "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 8 "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
% __ __ _ _ _ _
% | \/ | ___ | |_(_)_ ____ _| |_(_) ___ _ __
% | |\/| |/ _ \| __| \ \ / / _` | __| |/ _ \| '_ \
% | | | | (_) | |_| |\ V / (_| | |_| | (_) | | | |
% |_| |_|\___/ \__|_| \_/ \__,_|\__|_|\___/|_| |_|
%
% «motivation» (to ".motivation")
% (nyop 2 "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
% _____ __ ___
% |___ / \ \ / / | ___
% |_ \ \ V /| | / __|
% ___) | | | | |___\__ \
% |____/ |_| |_____|___/
%
% «three-yoneda-lemmas» (to ".three-yoneda-lemmas")
% (nyop 3 "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
\vspace*{20pt}
\begin{center}
\Huge{\bf BACK TO THE} \\[0pt]
\Huge{\bf YONEDA} \\
\Huge{\bf LEMMA} \\
\end{center}
\thispagestyle{empty}
\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 27 "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
\printbibliography
\end{document}
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% <make>
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2019notes-yoneda veryclean
make -f 2019.mk STEM=2019notes-yoneda pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "nyo"
% End: