|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2022on-the-missing.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2022on-the-missing.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2022on-the-missing.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2022on-the-missing.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2022on-the-missing.pdf"))
% (defun e () (interactive) (find-LATEX "2022on-the-missing.tex"))
% (defun u () (interactive) (find-latex-upload-links "2022on-the-missing"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2022on-the-missing.pdf"))
% (code-eec-LATEX "2022on-the-missing")
% (find-pdf-page "~/LATEX/2022on-the-missing.pdf")
% (find-pdf-text "~/LATEX/2022on-the-missing.pdf")
% (find-sh0 "cp -v ~/LATEX/2022on-the-missing.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2022on-the-missing.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2022on-the-missing.pdf
% file:///tmp/2022on-the-missing.pdf
% file:///tmp/pen/2022on-the-missing.pdf
% http://anggtwu.net/LATEX/2022on-the-missing.pdf
% (find-LATEX "2019.mk")
% (find-lualatex-links "2022on-the-missing")
% (find-math-b-links "md" "2022on-the-missing")
% (find-efunctionpp 'ce)
% (find-efunctionpp 'cv)
% «.ifluatex-0» (to "ifluatex-0")
% «.ifluatex-1» (to "ifluatex-1")
%
% «.defs» (to "defs")
% «.defs-slowdiag» (to "defs-slowdiag")
% «.title» (to "title")
% «.abstract» (to "abstract")
% «.toc» (to "toc")
%
% «.introduction» (to "introduction")
% «.introduction-es» (to "introduction-es")
% «.introduction-idarct» (to "introduction-idarct")
% «.introduction-la» (to "introduction-la")
% «.introduction-ol» (to "introduction-ol")
% «.introduction-ol2» (to "introduction-ol2")
% «.introduction-act2019» (to "introduction-act2019")
% «.introduction-tal» (to "introduction-tal")
% «.the-conventions» (to "the-conventions")
% «.to-deserve-a-name» (to "to-deserve-a-name")
% «.freyd» (to "freyd")
% «.freyd-notation» (to "freyd-notation")
% «.freyd-with-quantifiers» (to "freyd-with-quantifiers")
% «.freyd-with-functors» (to "freyd-with-functors")
% «.internal-views» (to "internal-views")
% «.reductions» (to "reductions")
% «.internal-view-functor» (to "internal-view-functor")
% «.internal-view-NT» (to "internal-view-NT")
% «.internal-view-adjunction» (to "internal-view-adjunction")
% «.teaching-adjunctions» (to "teaching-adjunctions")
% «.types-for-children» (to "types-for-children")
% «.dependent-types» (to "dependent-types")
% «.witnesses» (to "witnesses")
% «.judgments» (to "judgments")
% «.comprehensions» (to "comprehensions")
% «.omitting-types» (to "omitting-types")
% «.indefinite-articles» (to "indefinite-articles")
% «.phys-not» (to "phys-not")
% «.basic-example-as-skel» (to "basic-example-as-skel")
% «.basic-example-functors» (to "basic-example-functors")
% «.basic-example-NTs» (to "basic-example-NTs")
% «.basic-example-NT» (to "basic-example-NT")
% «.basic-example-bij» (to "basic-example-bij")
% «.basic-example-full» (to "basic-example-full")
% «.extensions» (to "extensions")
% «.comma-categories» (to "comma-categories")
% «.ness» (to "ness")
% «.yoneda-lemma» (to "yoneda-lemma")
% «.representable-functors» (to "representable-functors")
% «.yoneda-embedding» (to "yoneda-embedding")
% «.opposite-categories» (to "opposite-categories")
% «.representable-functors» (to "representable-functors")
% «.representable-functor-ex» (to "representable-functor-ex")
% «.2-category-of-cats» (to "2-category-of-cats")
% «.kan-extensions» (to "kan-extensions")
% «.all-concepts» (to "all-concepts")
% «.kan-formula» (to "kan-formula")
% «.functors-as-objects» (to "functors-as-objects")
% «.gms-for-children» (to "gms-for-children")
% «.reading-the-elephant» (to "reading-the-elephant")
% «.how-to-name-this-language» (to "how-to-name-this-language")
% «.why-my-conventions» (to "why-my-conventions")
% «.related-and-unrelated» (to "related-and-unrelated")
% «.references» (to "references")
% «.ifluatex-2» (to "ifluatex-2")
%
% «.save-body» (to "save-body")
% «.extract-cites» (to "extract-cites")
% «.TODO» (to "TODO")
% «.make-arxiv» (to "make-arxiv")
% «.make» (to "make")
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,
%linkcolor=DarkRed,
citecolor=DarkRed,
urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{tocloft} % (find-es "tex" "tocloft")
\usepackage{indentfirst}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{stmaryrd}
\usepackage{bm} % (find-es "tex" "bm")
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (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
%
% «ifluatex-0» (to ".ifluatex-0")
% (find-dednat6file "demo-write-dnt.tex")
\usepackage{ifluatex} %
\ifluatex %
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex % (find-LATEX "edrx21chars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\else %
\usepackage[utf8]{inputenc} %
\input edrx21chars-d.tex % (find-LATEX "edrx21chars-d.tex")
\fi %
\usepackage{edrx21} % (find-LATEX "edrx21.sty")
%
%
\usepackage[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-ab.bib} % (find-LATEX "catsem-ab.bib")
%
% (find-es "tex" "geometry")
\begin{document}
% «ifluatex-1» (to ".ifluatex-1")
\ifluatex
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}
\else
\input\jobname.dnt % (find-LATEXfile "2022on-the-missing.dnt")
\def\pu{}
\fi
% «defs» (to ".defs")
% (find-es "tex" "co")
% \co: a low-level way to typeset code; a poor man's "\verb"
\def\co#1{{%
\def\%{\char37}%
\def\\{\char92}%
\def\^{\char94}%
\def\~{\char126}%
\tt#1%
}}
\def\qco#1{`\co{#1}'}
\def\qqco#1{``\co{#1}''}
\def\ph{\phantom}
\def\respcomp{\mathsf{respcomp}}
\def\respids {\mathsf{respids}}
\def\sqcond {\mathsf{sqcond}}
\def\assoc {\mathsf{assoc}}
\def\idL {\mathsf{idL}}
\def\idR {\mathsf{idR}}
\def\univ {\mathsf{univ}}
\def\Ran {\mathsf{Ran}}
\def\sfC {\mathsf{C}}
\def\sfSet{\mathsf{Set}}
\def\Ring {\mathbf{Ring}}
\def\nameof#1{\ulcorner#1\urcorner}
\def\catK {\mathbf{K}}
\def\Dn {\Downarrow}
\def\veq{\rotatebox{90}{$=$}}
\def\liml{\underleftarrow {\lim}{}}
\def\limr{\underrightarrow{\lim}{}}
\def\veq{\rotatebox{90}{$=$}}
\def\Yzero {\mathsf{Y0}}
\def\Yzeroplus{\mathsf{Y0^+}}
\def\Yone {\mathsf{Y1}}
\def\Ytwo {\mathsf{Y2}}
\def\Ythree {\mathsf{Y3}}
\def\Yfour {\mathsf{Y4}}
\def\Yfive {\mathsf{Y5}}
\def\origphi{\phi}
\def\AProofOf #1{\llangle#1\rrangle}
\def\AllProofsOf#1{\llbracket#1\rrbracket}
\def\DONE{(DONE)}
\def\DONE{}
% «defs-slowdiag» (to ".defs-slowdiag")
% (to "make")
\def\slowdiag#1{\standout{#1}}
\def\slowdiag#1{\diag{#1}}
% (defun s () (interactive) (insert "\\standout{}"))
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title» (to ".title")
% (misp 1 "title")
% (misa "title")
\title{On the the missing diagrams \\ in Category Theory \\ (first-person version)}
\author{%
Eduardo Ochs%
%{\large Eduardo Ochs}%
\thanks{eduardoochs@gmail.com}\\
%{\small UFF, Rio das Ostras, RJ, Brasil}\\
}
\maketitle
% «abstract» (to ".abstract")
% Orig: (favp 1 "abstract")
% (fava "abstract")
\begin{abstract}
Most texts on Category Theory are written in a very terse style, in
which people pretend a) that all concepts are visualizable, and b)
that the readers can reconstruct the diagrams that the authors had
in mind based on only the most essential cues. As an outsider I
spent years believing that the techniques for drawing diagrams were
part of the oral culture of the field, and that the insiders could
read texts on CT reconstructing the ``missing diagrams'' in them
line by line and paragraph by paragraph, and drawing for each page
of text a page of diagrams with all the diagrams that the authors
had omitted. My belief was wrong: there are lots of conventions for
drawing diagrams scattered through the literature, but that unified
diagrammatic language did not exist. In this chapter I will show an
attempt to reconstruct that (imaginary) language for missing
diagrams: we will see an extensible diagrammatic language, called
DL, that follows the conventions of the diagrams in the literature
of CT whenever possible and that seems to be adequate for drawing
``missing diagrams'' for Category Theory. Our examples include the
``missing diagrams'' for adjunctions, for the Yoneda Lemma, for Kan
extensions, and for geometric morphisms, and how to formalize them
in Agda.
% Deleted in 2022mar09:
%
% % I used to believe that my conventions for drawing diagrams for
% % categorical statements could be written down in one page or less,
% % and that the only tricky part was a certain technique for
% % reconstructing objects ``from their names''... but then I found out
% % that this is not so.
%
% Most texts on Category Theory are written in a very terse style, in
% which people pretend a) that all concepts are visualizable, and b)
% that the readers can reconstruct the diagrams that the authors had
% in mind based on only the most essential cues. As an outsider I
% spent years believing that the techniques for drawing diagrams were
% part of the oral culture of the field, and that the insiders could
% read texts on CT reconstructing the ``missing diagrams'' in them
% line by line and paragraph by paragraph, and drawing for each page
% of text a page of diagrams with all the diagrams that the authors
% had omitted.
%
% A classical text on the formalization of Mathematics
% (\cite{VanBenthemJutting77}) has this sentence: ``An aspect which
% has not been mentioned so far is the ratio between the length of
% pieces of AUT-QE text and the length of the corresponding German
% texts. Our claim at the outset was that this ratio can be kept
% constant''. This may be true for Category Theory too --- each page
% of text would correspond to one page of missing diagrams, at least
% for {\sl some} parts of {\sl some} textbooks, with the right choice
% of font, the right conventions for drawing diagrams, and the right
% way to omit the ``obvious'' details.
%
% In this chapter we will show an extensible diagrammatic language
% that seems to be adequate for drawing ``missing diagrams'' for CT.
%
% % \standout{Explain:} diagrammatic language, conventions, folklore,
% % level of detail, omitting the ``obvious'' parts.
%
% % (find-books "__logic/__logic.el" "automath")
% % (find-LATEX "catsem-ab.bib" "bib-VanBenthemJutting77")
%
% % This is an attempt to explain, with motivations and examples, all
% % the conventions behind a certain diagram, called the ``Basic
% % Example'' in the text. Once the conventions are understood that
% % diagram becomes a ``skeleton'' for a certain lemma related to the
% % Yoneda Lemma, in the sense that both the statement and the proof of
% % that lemma can be reconstructed from the diagram. The last sections
% % discuss some simple ways to extend the conventions; we see how to
% % express in diagrams the (``real'') Yoneda Lemma and a corollary of
% % it, how to define comma categories,
% % %
% % % how to define certain limits using comma categories,
% % %
% % and how to formalize the diagram for ``geometric morphism for
% % children'' mentioned in sec.\ref{missing-diagrams}.
%
% % \msk
%
% % People in CT usually only share their ways of visualizing things
% % when their diagrams cross some threshold of mathematical relevance
% % --- and this usually happens when they prove new theorems with their
% % diagrams, or when they can show that their diagrams can translate
% % calculations that used to be huge into things that are much easier
% % to visualize. The diagrammatic language that I present here lies
% % below that threshold --- and so it is a ``private'' diagrammatic
% % language, that I am making public as an attempt to establish a
% % dialogue with other people who have also created their own private
% % diagrammatic languages.
\end{abstract}
\newpage
% _____ ___ ____
% |_ _/ _ \ / ___|
% | || | | | |
% | || |_| | |___
% |_| \___/ \____|
%
% «toc» (to ".toc")
% Orig: (favp 2 "toc")
% (fava "toc")
% sec:
% (find-es "tex" "tocloft")
\renewcommand{\cfttoctitlefont}{\bfseries}
\setlength{\cftbeforesecskip}{2.5pt}
\tableofcontents
% beginning of body
% ___ _ _ _ _
% |_ _|_ __ | |_ _ __ ___ __| |_ _ ___| |_(_) ___ _ __
% | || '_ \| __| '__/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \
% | || | | | |_| | | (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__|_| \___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%
% «introduction» (to ".introduction")
% (misp 3 "introduction")
% (misa "introduction")
% Orig: (favp 3 "missing-diagrams")
% (fava "missing-diagrams")
% sec:
\section{Introduction}
\label{missing-diagrams}
\label{introduction}
One of the main themes of this text is a diagrammatic language ---
let's call it DL --- that can be used to draw ``missing diagrams'' for
Category Theory. DL is a {\sl reconstructed language}, and it's easier
to explain it if I explain how it was reconstructed, and which of its
conventions were improvised. It is easier to do it in the first
person.
Suppose that your native language is $A$ and you are learning a
language $B$ by a method that includes conversation classes. You will
have to improvise a lot, but you will usually get feedback quickly.
Now suppose that you are studying a language $C$ --- for example,
Aeolic Greek (\cite{CarsonSappho}) --- mostly by yourself, and the
corpus of texts in $C$ is small. A good exercise is to try to write
your thoughts in $C$, using loanwords and improvised syntactical
constructs when needed, but marking mentally the places in which you
had to improvise. In most cases, but not all, you will eventually find
ways to rewrite those parts to make them look more like $C$.
The conventions of DL are explained in sec.\ref{the-conventions}. A
few of them don't correspond to anything that I could find in the
literature; they are listed at the end of that section.
\msk
{\bf This text has two versions.} The title of this one is ``On the
missing diagrams in Category Theory (first-person version)'', and the
title of the other is just ``On the missing diagrams in Category
Theory''; they (will) have the same technical content, but different
styles. Here's how this happened. Two of the editors of the ``Handbook
of Abductive Cognition'' --- Gianluca Caterina and Rocco Gangle ---
asked me if I could rewrite my notes in \cite{FavC} and submit the
rewritten version as a chapter for the Handbook. I did that, and I
wrote this version, that uses the first person a lot --- for example
to tell stories, and to explain why the current version of DL has a
certain convention, that replaces another, older, convention, that
didn't work very well. Then the other editors asked me of I could
prepare another version that would follow the editorial guidelines
more closely, including the part that says to avoid the first person.
At this moment (april/2022) the ``non-first-person version'' is not
ready yet; the ``first-person version'' will probably be more fun to
read.
\bsk
The best way to introduce DL is to tell the full story of how it
evolved from a long sequence of wrong assumptions and from some
``thoughts that I wanted to express in DL''.
% (sec.\ref{related-and-unrelated}).
% «introduction-es» (to ".introduction-es")
Let me start with some quotes. This one is from Eilenberg and Steenrod
(\cite[p.ix]{EilenbergSteenrod}, but I learned it from
\cite[pp.82--83]{Kromer}):
\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, the reader can usually supply it
himself.
\end{quotation}
I spent a {\sl lot} of my time studying Category Theory trying to
``supply the diagrams myself''. In \cite{EilenbergSteenrod} supplying
the diagrams is not very hard (I guess), but in books like
\cite{CWM2}, in which most important concepts involve several
categories, I had to rearrange my diagrams hundreds of times until I
reached ``good'' diagrams...
% (find-angg ".emacs" "idarct-preprint")
% (find-idarctpage 1 "1. Mental Space and Diagrams")
% (find-idarcttext 1 "1. Mental Space and Diagrams")
% (find-idarctpage 15 "12. Skeletons of proofs")
% (find-idarcttext 15 "12. Skeletons of proofs")
% (find-idarctpage 23 "16. Archetypal Models")
% (find-idarcttext 23 "16. Archetypal Models")
% «introduction-idarct» (to ".introduction-idarct")
The problem is that I expected too much from ``good'' diagrams. The
next quotes are from the sections 1 and 12 of an article that I wrote
about that (\cite{IDARCT}):
\begin{quotation}
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=60pt]{2020notes-yoneda-frob.pdf}
\end{center}
\noindent and I reconstruct the formula from it.
\end{quotation}
\begin{quotation}
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.
\end{quotation}
I was searching for a diagrammatic language that would let me express
the ``skeletons'' of categorical definitions and proofs. I wanted
these skeletons to be easy to remember --- partly because they would
have shapes that were easy to remember, and partly because they would
be similar to ``archetypal cases'' (\cite[section 16]{IDARCT}).
\bsk
% «introduction-la» (to ".introduction-la")
In 2016 and 2017 I taught a seminar course for undergraduates that
covered a bit of Category Theory in the end --- see Section
\ref{teaching-adjunctions} and \cite{OchsWLD2019} --- and this forced
me to invent new techniques for working in two different styles in
parallel: a style ``for adults'', more general, abstract, and formal,
and another ``for children'', with more diagrams and examples. After
some semesters, and after writing most of the material that became
\cite{PH1}, I tried to read again some parts of Johnstone's ``Sketches
of an Elephant'', a book that always felt quite impenetrable to me,
and I found a way to present geometric morphisms in toposes to
``children''. It was based on this diagram,
%
% (jopp 23 "Set-PA")
% (joe "Set-PA")
%
%L sesw = {[" w"]="↙", [" e"]="↘"}
%
%R local Aargs, Bargs = 3/#1 #2 \, 3/ #1 \
%R | e w e | | w e |
%R \ #3 #4 / |#2 #3 |
%R | e w e |
%R | #4 #5 |
%R | e w |
%R \ #6 /
%R
%R Aargs:tozmp({def="pshAargs#1#2#3#4", scale="11pt", meta="p"}):addcells(sesw):output()
%R Bargs:tozmp({def="pshBargs#1#2#3#4#5#6", scale="11pt", meta="p"}):addcells(sesw):output()
%
%D diagram gm-for-children
%D 2Dx 100 +70
%D 2D 100 A0 A1
%D 2D
%D 2D +60 A2 A3
%D 2D
%D 2D +30 A4 A5
%D 2D
%D 2D +15 A6 A7
%D 2D
%D ren A0 A1 ==> f^*G G
%D ren A2 A3 ==> H f_*H
%D ren A0 A1 ==> \LG \G
%D ren A2 A3 ==> \H \RH
%D ren A4 A5 ==> \Set^\catA \Set^\catB
%D ren A6 A7 ==> \catA \catB
%D
%D (( A0 A1 <-|
%D A0 A2 ->
%D A1 A3 ->
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil <->
%D A4 A5 <- sl^ .plabel= a f^*
%D A4 A5 -> sl_ .plabel= b f_*
%D A6 A7 -> .plabel= a f
%D ))
%D enddiagram
%D
%D diagram gm-for-adults
%D 2Dx 100 +20
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +15 A4 A5
%D 2D
%D 2D +15 A6 A7
%D 2D
%D ren A0 A1 ==> f^*G G
%D ren A2 A3 ==> H f_*H
%D ren A4 A5 ==> \calE \calF
%D ren A6 A7 ==> \catA \catB
%D
%D (( A0 A1 <-|
%D A0 A2 ->
%D A1 A3 ->
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil <->
%D A4 A5 <- sl^ .plabel= a f^*
%D A4 A5 -> sl_ .plabel= b f_*
%D # A6 A7 -> .plabel= a f
%D ))
%D enddiagram
%D
\pu
$$
\diag{gm-for-adults}
\qquad
\def\LG{\pshAargs{G_2}{G_3}{G_4}{G_5}}
\def\G {\pshBargs{G_1}{G_2}{G_3}{G_4}{G_5}{G_6}}
\def\H {\pshAargs{H_2}{H_3}{H_4}{H_5}}
\def\RH{\pshBargs{H_2{×_{H_4}}H_3}{H_2}{H_3}{H_4}{H_5}{1}}
\scalebox{0.6}{$
\diag{gm-for-children}
$}
$$
%
that we will discuss in detail in \ref{gms-for-children}. Its left
half is a generic geometric morphism (``for adults''), and its right
half is a very specific geometric morphism (``for children'') in which
everything is easy to understand and to visualize, and that turns out
to be ``archetypal enough''.
I showed that to the few categorists with whom I had contact and the
feedback that I got was quite positive. A few of them --- the ones who
were strictly ``adults'' --- couldn't understand why I was playing
with particular cases, and even worse, with finite categories, instead
of proving things in the most general case possible, but some others
said that these ideas were very nice, that they knew a few bits about
geometric morphisms but those bits didn't connect well, and that now
they had a family of particular cases to think about, and they had
much more intuition than before.
% «introduction-ol» (to ".introduction-ol")
That was the first time that my way of using diagrams yielded
something so nice! This was the excuse that I needed to organize a
workshop on diagrammatic languages and ways to use particular
cases; here's how I advertised it (from \cite{OchsLucatelli}):
%
\begin{quotation}
When we explain a theorem to children --- in the strict sense of the
term --- we focus on concrete examples, and we avoid
generalizations, abstract structures and infinite objects.
When we present something to ``children'', in a wider sense of the
term that means ``people without mathematical maturity'', or even
``people without expertise in a certain area'', we usually do
something similar: we start from a few motivating examples, and then
we generalize.
One of the aims of this workshop is to discuss techniques for {\sl
particularization} and {\sl generalization}. Particularization is
easy; substituing variables in a general statement is often enough
to do the job. Generalization is much harder, and one way to
visualize how it works is to regard particularization as a
projection: a coil projects a circle-like shadow on the ground, and
we can ask for ways to ``lift'' pieces of that circle to the coil
continously. {\sl Projections} lose dimensions and may collapse
things that were originally different; {\sl liftings} try to
reconstruct the missing information in a sensible way. There may be
several different liftings for a certain part of the circle, or
none. Finding good generalizations is somehow like finding good
liftings.
The second of our aims is to discuss {\sl diagrams}. For example, in
Category Theory statements, definitions and proofs can be often
expressed as diagrams, and if we start with a general diagram and
particularize it we get a second diagram with the same shape as the
first one, and that second diagram can be used as a version ``for
children'' of the general statement and proof. Diagrams were for a
long time considered second-class entities in CT literature
(\cite{Kromer} discusses some of the reasons), and were omitted;
readers who think very visually would feel that part of the work
involved in understanding CT papers and books would be to
reconstruct the ``missing'' diagrams from algebraic statements.
Particular cases, even when they were the motivation for the general
definition, are also treated as somewhat second-class --- and this
inspires a possible meaning for what can call ``Category Theory for
Children'': to start from the diagrams for particular cases, and
then ``lift'' them to the general case. Note that this can be done
outside Category Theory too; \cite{Jamnik} is a good example.
Our third aim is to discuss {\sl models}. A standard example is that
every topological space is a Heyting Algebra, and so a model for
Intuitionistic Predicate Logic, and this lets us explain visually
some features of IPL. Something similar can be done for some modal
and paraconsistent logics; we believe that the figures for that
should be considered more important, and be more well-known.
\end{quotation}
% «introduction-ol2» (to ".introduction-ol2")
This is from the second announcement:
\begin{quotation}
If we say that categorical definitions are ``for adults'' - because
they may be very abstract - and that particular cases, diagrams, and
analogies are ``for children'', then our intent with this workshop
becomes easy to state. ``Children'' are willing to use ``tools for
children'' to do mathematics, even if they will have to translate
everything to a language ``for adults'' to make their results
dependable and publishable, and even if the bridge between their
tools ``for children'' and ``for adults'' is somewhat defective,
i.e., if the translation only works on simple cases...
We are interested in that {\sl bridge} between maths ``for adults''
and ``for children'' in several areas. Maths ``for children'' are
hard to publish, even informally as notes (see this thread
\msk
\centerline{\url{http://anggtwu.net/categories-2017may02.html}}
\msk
\noindent in the Categories mailing list), so often techniques are
rediscovered over and over, but kept restricted to the ``oral
culture'' of the area.
Our main intents with this workshop are:
\begin{itemize}
\item to discuss (over coffe breaks!) the techniques of the
``bridge'' that we currently use in seemingly ad-hoc ways,
\item to systematize and ``mechanize'' these techniques to make
them quicker to apply,
\item to find ways to publish those techniques --- in journals or
elsewhere,
\item to connect people in several areas working in related
ideas, and to create repositories of online resources.
\end{itemize}
\end{quotation}
In the UniLog 2018 I was able to chat with several categorists, and
they told me that the oral culture of CT was not as I was expected: if
there are standard ways to draw diagrams they are not widely known. I
also spent two evenings with Peter Arndt working on a certain
factorization of geometric morphisms ``for children'' --- and this
made me feel that at some point I would be able to present
applications of this diagrammatic language in ``top-tier'' conferences
that would not accept works with holes.
% (favp 2 "missing-diagrams")
% (favp 7 "missing-diagrams")
% (fava "missing-diagrams" "Peter Arndt")
% «introduction-act2019» (to ".introduction-act2019")
The following quote is from the abstract of my submission (\cite{MDE})
to the ACT2019:
%
\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.
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}
%
% «introduction-tal» (to ".introduction-tal")
%
and this from my submission (\cite{OchsTallinnAbs}) to Diagrams 2020:
%
\begin{quotation}
Category Theory gives the impression of being an area where most
concepts and arguments are stated and formalized via diagrams, but
this is not exactly true... in most texts almost everything is done
algebraically, and the reader is expected to be able to reconstruct
the ``missing diagrams'' by himself.
I used to believe, as an outsider, that some people who grew up
immersed the oral culture of the area would know several techniques
for ``drawing the missing diagrams''. My main intent when I
organized the workshop ``Logic for Children'' at the UniLog 2018
\cite{OchsLucatelli} was to collect some of these folklore
techniques, compare them with the ones that I had developed myself
to study CT, and formalize them all --- but what I found instead was
that everybody that I could get in touch with used their own ad-hoc
techniques, and that what I was trying to do was either totally new
to them, or at least new in its level of detail.
\end{quotation}
The story will continue at the end of sec.\ref{the-conventions}, after
the list of conventions.
% (find-books "__logic/__logic.el" "nederpelt-geuvers")
% (find-ttafpaipage (+ 29 179) "General theorem: (Bezout's Lemma)")
% (find-ttafpaitext (+ 29 179) "General theorem: (Bezout's Lemma)")
% and in minicourses in conferences, and this sort of forced me to
% invent new techniques for working in several levels of abstraction
% --- ``for adults'' and ``for children'' --- in parallel, and for
% translating between these styles. After that I tried to apply these
% techniques to Johnstone's ``Elephant'', a book that always made me
% think ``Help! I need a version for children of this!!!'', and they
% {\sl worked} --- I found a nice way to visualize two of its
% factorizations of geometric morphisms...
% ...and I discovered, with Peter Arndt, that if we start with toposes
% of the form $\Set^D$, where $D$ is a finite category, and a
% geometric morphism between them, we can perform these two
% factorizations by going through other toposes of the form $\Set^D$.
% From that point on I had concrete evidence that this diagrammatic
% language could be used to formulate conjectures and to obtain their
% proofs, and I had a theorem that I had obtained with it that seemed
% to be new...
% (nyop 11 "missing-diags-elephant")
% (nyo "missing-diags-elephant")
% (oxap 1 "title" "Aleks and Bob")
% (oxa "title" "Aleks and Bob")
% ____ _ _
% / ___|___ _ ____ _____ _ __ | |_(_) ___ _ __ ___
% | | / _ \| '_ \ \ / / _ \ '_ \| __| |/ _ \| '_ \/ __|
% | |__| (_) | | | \ V / __/ | | | |_| | (_) | | | \__ \
% \____\___/|_| |_|\_/ \___|_| |_|\__|_|\___/|_| |_|___/
%
% «the-conventions» (to ".the-conventions")
% (misp 9 "the-conventions")
% (misa "the-conventions")
% Orig: (favp 8 "the-conventions")
% (fava "the-conventions")
% sec:
\section{The conventions \DONE}
\label{the-conventions}
The conventions that I will present now are the ones that we will need
to interpret the diagram below, that is essentially the Proposition 1
in the proof of the Yoneda Lemma in \cite[Section III.2]{CWM2}; we
will call that diagram the ``Basic Example'' and also ``diagram
$\Yzero$''. In the sections \ref{extensions}--\ref{gms-for-children}
we will see how extend DL to make it able to interpret the diagram for
geometric morphisms of the Introduction.
%
%D diagram Basic-Example
%D 2Dx 100 +40
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 |-> A3
%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 ==> A
%D ren A2 A3 ==> C RC
%D ren B0 B1 ==> \catB \catA
%D ren C0 C1 C2 ==> \catB(C,-) \catA(A,R-) ?
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D
%D B0 B1 -> .plabel= a R\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= ^15pt
%D ))
%D enddiagram
%
\pu
$$\scalebox{2.0}{$
\slowdiag{Basic-Example}
$}
$$
\begin{itemize}
\item[(CD)] Our diagrams are made of components that are nodes and
arrows. The nodes can contain arbitrary expressions. The arrows work
as connectives, and each arrow can be interpreted as the top-level
connective in the smallest subexpression that contains it. For
example, the curved arrow in the diagram above can be interpreted
as:
%
$$(A\ton{η}RC)↔(\catB(C,-) \ton{T} \catA(A,R-)).
$$
\item[(C$→$)] Arrows that look like `$→$' (\qqco{\\to}) represent
hom-sets, or, in $\Set$, spaces of functions. When a `$→$' arrow is
named the name stands for an element of that hom-set. For example,
in $A \ton{η} RC$ we have $η:A→RC$.
\item[(C$↦$)] Arrows that look like `$↦$' (\qqco{\\mapsto}) represent
internal views of functions or functors. This has some subtleties;
see Section \ref{internal-views}.
\item[(C$↔$)] Arrows that look like `$↔$' (\qqco{\\leftrightarrow})
represent bijections or isomorphisms.
\item[(CAI)] ``Above'' usually means ``inside'', or ``internal view''.
In the diagram above the morphism $η:A→RC$ is in $\catA$ and $C$ is
an object of $\catB$. Also, the arrow $C \mapsto RC$ is above $\catB
\ton{R} \catA$, and this means that it is an internal view of the
functor $R$. Note that {\sl usually} is not {\sl always} --- and
$\catB \ton{R} \catA$ is not an internal view of $\catB(C,-) \ton{T}
\catA(A,R-)$.
\item[(CO)] When the definition of a component of our diagram is
``obvious'' in the sense of ``there is a unique natural construction
for an object with that name'', we will usually omit its definition
and {\sl pretend} that it is obvious; same for its uniqueness. See
Section \ref{to-deserve-a-name}.
\item[(CC)] Everything commutes by default, and non-commutative cells
have to be indicated explicitly. See Section \ref{freyd-notation}.
\item[(CTL)] The default ``meaning'' for a diagram {\sl without
quantifiers} is the definition of its top-level component. There
is a natural partial order on the components of a diagram, in which
$α \prec β$ iff $α$ is ``more basic'' than $β$, or, in other words,
if $α$ needs to be defined before $β$. In the diagram above the
top-level component is the curved bijection.
\item[(CMQ)] The default ``meaning'' for a diagram with quantifiers is
a proposition. See Sections
\ref{freyd-notation}--\ref{freyd-with-functors} for how to obtain
that proposition.
\item[(CAdj)] {\sl I use shapes based on my way of drawing adjunctions
whenever possible.} I like adjunctions so much that when I want to
explain Category Theory to someone who knows just a little bit of
Maths I always start by the adjunction $({×}B)⊣(B{→})$ of Section
\ref{internal-view-adjunction}; I always draw it in a canonical way,
with the left adjoint going left, the right adjoint going right, and
the morphisms going down. In Proposition 1 of \cite[Section
III.2]{CWM2} the map $η$ is a universal arrow, and someone who
learns adjunctions first sees the unit maps $η:A→(B{→}(A{×}B))$ as
the first examples of universal arrows --- so that's why the upper
part of the diagram above is drawn in this position.
\item[(CYo)] {\sl I use shapes based on my way of drawing the Yoneda
Lemma whenever possible.} Look at the sections
\ref{basic-example-as-skel}--\ref{basic-example-full} and
\ref{yoneda-lemma}--\ref{representable-functors}: the upper parts of
their diagrams look like parts of adjunctions, but the other parts
do not. For example, I draw ``The functor $U:\Ring→\Set$ is
representable'' as:
%
% (mdyp 1 "Y3+diag")
% (mdya "Y3+diag")
%
%D diagram Y3+diag
%D 2Dx 100 +35
%D 2D 100 A1
%D 2D |
%D 2D +25 A2 - A3
%D 2D
%D 2D +15 B0 - B1
%D 2D
%D 2D +15 C0 - C1
%D 2D \ |
%D 2D +20 C3
%D 2D
%D ren A1 ==> \ga{A1}
%D ren A2 A3 ==> \ga{A2} \ga{A3}
%D ren B0 B1 ==> \ga{B0} \ga{B1}
%D ren C0 C1 ==> \ga{C0} \ga{C1}
%D ren C3 ==> \ga{C3}
%D
%D (( A1 A3 -> .plabel= r \ga{A13}
%D A2 A3 |->
%D
%D B0 B1 -> .plabel= a \ga{B01}
%D
%D # C0 C1 -> .plabel= a \ga{C01}
%D C0 C3 <-> .plabel= b \ga{C03}
%D # C1 C3 <-> .plabel= r \ga{C13}
%D ))
%D enddiagram
\pu
%
\sa{Y3+diag-Z[x]}{
\sa{A1}{1}
\sa{A2}{\Z[x]} \sa{A3}{U(\Z[x])}
\sa{B0}{\Ring} \sa{B1}{\Set}
\sa{C0}{\Ring(\Z[x],-)}
\sa{C3}{U}
%
\sa{A13}{\sm{\nameof{x}\\\univ}}
\sa{B01}{U}
\sa{C03}{}
%
\diag{Y3+diag}
}
%
$$\ga{Y3+diag-Z[x]}
$$
\item[(CDT)] A diagram acts a dictionary of default types for
symbols. See sec.\ref{omitting-types}.
\item[(CIA)] Default types allow us to use indefinite articles in a
precise way. An example: we have $η:\Hom_\catA(A,RC)$, so ``an $η$''
means ``an element of $\Hom_\catA(A,RC)$''. See
sec.\ref{indefinite-articles}.
\item[(COT)] We use a notation as close to the original text as
possible, especially when we are trying to draw the missing diagrams
for some existing text. If we were drawing the missing diagrams for
the Proposition 1 of \cite[Section III.2]{CWM2} our diagram would be
this:
%
%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
%
$$\pu
\slowdiag{yoneda-cwm-0-small}
$$
%
but I hate Mac Lane's choice of letters, so I decided to use another
notation here.
\item[(CSk)] Suppose that we have a piece of text --- say, a paragraph
$P$ --- and we want to reconstruct the ``missing diagram'' $D$ for
$P$. Ideally this $D$ should be a ``skeleton'' for $P$, in the sense
that it should be possible to reconstruct the ideas in $P$ from the
diagram $D$ using very few extra hints; see \cite[sec.12]{IDARCT}.
\item[(CTT)] Our diagrams should be close to Type Theory: it should be
possible to use them as a scaffolding for formalizing our text in
(pseudocode for) a proof assistant.
\item[(CFSh)] The image by a functor of a diagram $D$ is drawn with
the same shape as $D$.
\item[(CISh)] The internal view of a diagram $D$ is drawn with the
same shape as $D$, modulo duplications --- see section
\ref{internal-views}.
\item[(CPSh)] A particular case of a diagram $D$ is drawn with the
same shape as $D$.
\item[(CNSh)] A translation of a diagram $D$ to another notation is
drawn with the same shape as $D$.
\end{itemize}
The conventions (CD)--(CMQ) and (CFSh)--(CNSh) all appear in diagrams
in \cite{MacLaneNotes}, \cite{Freyd76}, \cite{FreydScedrov},
\cite{Taylor}, \cite{Riehl}, \cite{Leinster}, but very few of them are
spelled out explicitly, and the idea of ``same shape'' is never
stressed. See \cite[p.179]{NederpeltGeuvers} for a neat example of
``substitution produces something with the same shape'' and
\cite{PenroseSIGGRAPH2020} for a language for drawing diagrams from
high-level specifications in which it may be possible to implement the
rules about ``same shape''.
The other conventions {\sl may} be new, but remember from the
introduction that most of the work on diagrammatic languages lies
below the threshold of publishability... so conventions corresponding
to those may be folklore knowledge in groups that I don't have contact
with {\sl yet}.
The convention (COT) is obvious in retrospect, but giving a name to it
saved me from my tendency to invent new notations. The conventions
(CDT) and (CIA) replace the idea of downcasings from
\cite[sec.3]{IDARCT}, that didn't work well. Sections
\ref{extensions}--\ref{gms-for-children} show how to add new
conventions to DL, and sec.\ref{opposite-categories} shows that we can
add a bad convention and mark it as a temporary hack.
There are many notations for Type Theory. To make this chapter more
readable in the convention (CTT) I will use a pseudocode that is
halfway between standard mathematical notation and Agda; the companion
paper \cite{MissingAgda} will show how to translate it to real Agda
(with the library \cite{HuCarette}).
Most texts on CT use diagrams to {\sl prove} theorems. Here will use
them to {\sl understand} theorems, and to translate between languages.
Our approach can be seen as an extension of \cite{Ganesalingam} to
Category Theory; see also \cite{DSLsofMath}, that is a recent book
that follows many of the ideas in \cite{Ganesalingam}.
% (find-books "__cats/__cats.el" "hu-carette")
% (find-angg ".emacs.agda" "wadler-smbf")
% (find-angg ".emacs.agda" "wadler-smbf")
% % (find-books "__comp/__comp.el" "penrose")
%
% \standout{Rewrite} Note that I have presented these conventions in a
% human-friendly way, that is somewhat informal and admits exceptions
% and extensions. Some simple examples of extensions will be discussed
% in Section \ref{extensions}.
%
% ____
% | _ \ ___ ___ ___ _ ____ _____ _ __ __ _ _ __ ___ ___
% | | | |/ _ \/ __|/ _ \ '__\ \ / / _ \ | '_ \ / _` | '_ ` _ \ / _ \
% | |_| | __/\__ \ __/ | \ V / __/ | | | | (_| | | | | | | __/
% |____/ \___||___/\___|_| \_/ \___| |_| |_|\__,_|_| |_| |_|\___|
%
% «to-deserve-a-name» (to ".to-deserve-a-name")
% Orig: (favp 11 "to-deserve-a-name")
% (fava "to-deserve-a-name")
% sec: 3
%
\section{Finding ``the'' object with a given name \DONE}
\label{to-deserve-a-name}
One of the books that I tried to read when I was starting to learn
Category Theory was Mac Lane's \cite{CWM2}. It is written for readers
who know a lot of mathematics and who can follow some steps that it
treats as obvious. I was not (yet) a reader like that, but I wanted to
become one.
There is one specific thing that \cite{CWM2} does pretending that it
is obvious that I found especially fascinating. It ``defines''
functors by describing their actions on objects, and it leaves to the
reader the task of discovering their actions on morphisms. Let's see
how to find these actions on morphisms.
A functor $F:\catA→\catB$ has four components:
%
$$F=(F_0, F_1, \respids_F, \respcomp_F).$$
%
They are its action on objects, its action on morphisms, the assurance
that it takes identity maps to identity maps, and the assurance that
it respects compositions. When Mac Lane says this,
%
\begin{quote}
Fix a set $B$. Let $(×B)$ denote {\sl the} functor that takes each set
$A$ to $A×B$.
\end{quote}
%
he is saying that $(×B)_0 A = A×B$, or, more precisely, this:
%
$$(×B)_0 := λA.\,A×B$$
The ``{\sl the}'' in the expression ``Let $(×B)$ denote {\sl the}
functor...'' implies that the precise meaning of $(×B)_1$ is easy to
find, and that it is easy to prove $\respids_{(×B)}$ and
$\respcomp_{(×B)}$.
If $f:A'→A$ then $(×B)_1 f : (×B)_0 A' → (×B)_0 A$. We know the {\sl
name} of the image morphism, $(×B)_1 f$, and its {\sl type},
%
$$(×B)_1 f : A'×B → A×B,$$
%
and it is implicit that there is an ``obvious'' natural construction
for this $(×B)_1 f$ from $f$. A natural construction is ---
TA-DAAAA!!! --- a $λ$-term, so we are looking for a term of type $A'×B
→ A×B$ that can be constructed from $f:A'→A$.
In a big diagram:
%:
%:
%: [p:A'{×}B]^1
%: ------------
%: πp:A' f:A'→A [p:A'{×}B]^1
%: -------------- ------------
%: f(πp):A π'p:B
%: ----------------------
%: f:A'→A (f(πp),π'p):A{×}B
%: ==================== => -----------------------------------1
%: (×B)_1f:A'{×}B→A{×}B (λp⠆A'{×}B.(f(πp),π'p):A'{×}B→A{×}B
%:
%: ^foo1 ^foo2
%:
\pu
$$\ded{foo1} \quad ⇒ \ded{foo2}$$
A double bar in a derivation means ``there are several omitted steps
here'', and sometimes a double bar suggests that these omitted steps
are obvious. The derivation on the left says that there is an
``obvious'' way to build a $(×B)_1f:A'{×}B→A{×}B$ from a
``hypothesis'' $f:A'→A$. If we expand its double bar we get the tree
at the right, that shows that the ``precise meaning'' for $(×B)_1f$ is
$(λp⠆A'{×}B.(f(πp),π'p)$. More formally (and erasing a typing),
%
$$(×B)_1 := λf.(λp.(f(πp),π'p)).$$
The expansion of the double bar above becomes something more familiar
if we translate the trees to Logic using Curry-Howard:
%:
%:
%: [P∧R]^1
%: -------
%: P P→Q [P∧R]^1
%: ---------- -------
%: Q R
%: -----------
%: P→Q Q∧R
%: ======= => ------------1
%: P∧R→Q∧R P∧R→Q∧R
%:
%: ^foo-logic1 ^foo-logic2
%:
\pu
$$\ded{foo-logic1} \quad ⇒ \ded{foo-logic2}$$
We obtain the tree at the right by {\sl proof search}.
Let's give a name for the operation above that obtained a term of type
$A'×B→A×B$: we will call that operation {\sl term search}, or, as it
is somewhat related to type inference, {\sl term inference}.
Term search may yield several different construction and trees, and so
several non-equivalent terms of the desired type. When Mac Lane says
``{\sl the} functor $(×B)$'' he is indicating that:
\begin{itemize}
\item a term for $(×B)_1$ is easy to find (note that we use the
expression ``a {\sl precise meaning} for $(×B)_1$''),
\item all other natural constructions for something that ``deserves
the name'' $(×B)_1$ yield terms equivalent to that first, most
obvious one,
\item proving $\respids_{(×B)}$ and $\respcomp_{(×B)}$ is trivial.
\end{itemize}
In many situations we will start by just the name of a functor, as the
``$(×B)$'' in the example above, and from that name it will be easy to
find {\sl the} ``precise meaning'' for $(×B)_0$, and from that the
``precise meaning'' for $(×B)_1$, and after that proofs that
$\respids_{(×B)}$ and $\respcomp_{(×B)}$. We will use the expression
``...deserving the name...'' in this process --- terms for $(×B)_0$,
$(×B)_1$, $\respids_{(×B)}$, and $\respcomp_{(×B)}$ ``deserve their
names'' if they obey the expected constraints.
For a more thorough discussion see \cite{IDARCT}.
\msk
These ideas of ``finding a precise meaning'' and ``finding (something)
deserving that name'' can also be applied to morphisms, natural
transformations, isomorphisms, and so on.
In Section \ref{basic-example-NTs} we will see how to find natural
constructions for the two directions of the bijection in the Basic
Example --- or how the expand the double bars in the two derivations
here:
%:
%: η:A→RC
%: ========================
%: α:\catB(C,-)→\catA(A,R-)
%:
%: ^bij-down
%:
%: α:\catB(C,-)→\catA(A,R-)
%: ========================
%: η:A→RC
%:
%: ^bij-up
%:
$$\pu
\slowdiag{Basic-Example}
\qquad
\begin{array}{c}
\ded{bij-down}
\\ \\
\ded{bij-up}
\end{array}
$$
\msk
I am not aware of any papers or books on CT that discuss how to
(re)construct a functor from its action on objects or from its name,
but Agda has a tool that can be used for that: look for the section on
``Automatic Proof Search'' in \cite{AgdaUserManual}.
% (find-LATEX "catsem-ab.bib" "bib-AgdaUserManual")
% (find-es "agda" "agsy")
% (find-idarctpage 8 "(Figure 4B)")
% _____ _
% | ___| __ ___ _ _ __| |
% | |_ | '__/ _ \ | | |/ _` |
% | _|| | | __/ |_| | (_| |
% |_| |_| \___|\__, |\__,_|
% |___/
%
% «freyd» (to ".freyd")
% «freyd-notation» (to ".freyd-notation")
% (misp 16 "freyd-notation")
% (misa "freyd-notation")
% sec: 4
% Orig: (favp 14 "freyd")
% (fava "freyd")
% sec: 4
\section{Freyd's diagrammatic language \DONE}
\label{freyd-notation}
In \cite{Freyd76} Peter Freyd presents a very nice diagrammatic
language that can be used to express {\sl some} definitions from
Category Theory. For example, this is the statement that a category
has all equalizers:
%
%L forths["-"] = function () pusharrow("-") end
%
%D diagram cat-has-equalizers
%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 ==> ∀ {} X E A B
%D ren U1 L1 B0 B1 B2 B3 ==> ∃ {} X E A B
%D ren U2 L2 C0 C1 C2 C3 ==> ∀ {} X E A B
%D ren U3 L3 D0 D1 D2 D3 ==> ∃! {} X E A B
%D
%D (( U0 L0 -
%D A2 A3 -> sl^^ .plabel= a f
%D A2 A3 -> sl__ .plabel= b g
%D A2 A3 midpoint .TeX= \scriptstyle? place
%D ))
%D (( U1 L1 -
%D B2 B3 -> sl^^ .plabel= a f
%D B2 B3 -> sl__ .plabel= b g
%D B2 B3 midpoint .TeX= \scriptstyle? 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= \scriptstyle? 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= \scriptstyle? 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{cat-has-equalizers}
$}
$$
All cells in these diagrams commute by default, and non-commuting
cells have to be indicated with a `?'. Each vertical bar with a `$∀$'
above it means ``for all extensions of the previous diagram to this
one such that everything commutes''; a vertical bar with a `$∃!$'
above it means ``there exists a unique extension of the previous
diagram to this one such that everything commutes'', and so on. See
the scan in \cite{Freyd76} for the basic details of how to formalize
these diagrams, and the book \cite[p.28 onwards]{FreydScedrov}, for
tons of extra details, examples, and applications.
Let's call the subdiagrams of a diagram like the one above its
``stages''. Its stage 0 is empty, its stage 1 has two objects and two
arrows, its last stage has four objects and five arrows, and the
quantifiers separating the stages are $Q_1=∀$, $Q_2=∃$, $Q_3=∀$,
$Q_4=∃!$. They are structured like this:
%
%D diagram freyd-stages-1
%D 2Dx 100 +20 +20 +20 +20 +20 +20 +20 +20
%D 2D 100 SQ0 SQ1 SQ2 SQ3 SQ4
%D 2D
%D 2D 100 U0 U1 U2 U3
%D 2D
%D 2D +20 S0 S1 S2 S3 S4
%D 2D
%D 2D +20 L0 L1 L2 L3
%D 2D
%D ren U0 L0 ==> Q_1 {}
%D ren U1 L1 ==> Q_2 {}
%D ren U2 L2 ==> Q_3 {}
%D ren U3 L3 ==> Q_4 {}
%D ren S0 S1 S2 S3 S4 ==> S_0 S_1 S_2 S_3 S_4
%D ren SQ0 SQ1 SQ2 SQ3 SQ4 ==> SQ_0 SQ_1 SQ_2 SQ_3 SQ_4
%D
%D (( S0 place S1 place S2 place S3 place S4 place
%D U0 L0 -
%D U1 L1 -
%D U2 L2 -
%D U3 L3 -
%D ))
%D enddiagram
%D
%D diagram freyd-stages-2
%D 2Dx 100 +20 +20 +20 +20 +20 +20 +20 +20
%D 2D 100 SQ0 SQ1 SQ2 SQ3 SQ4
%D 2D
%D 2D +20 U0 U1 U2 U3
%D 2D
%D 2D +20 S0 S1 S2 S3 S4
%D 2D
%D 2D +20 L0 L1 L2 L3
%D 2D
%D ren U0 L0 ==> Q_1 {}
%D ren U1 L1 ==> Q_2 {}
%D ren U2 L2 ==> Q_3 {}
%D ren U3 L3 ==> Q_4 {}
%D ren S0 S1 S2 S3 S4 ==> S_0 S_1 S_2 S_3 S_4
%D ren SQ0 SQ1 SQ2 SQ3 SQ4 ==> SQ_0 SQ_1 SQ_2 SQ_3 SQ_4
%D
%D (( # SQ0 S0 .>
%D # SQ1 S1 .>
%D # SQ2 S2 .>
%D # SQ3 S3 .>
%D # SQ4 S4 .>
%D SQ0 SQ1 <--
%D SQ1 SQ2 <--
%D SQ2 SQ3 <--
%D SQ3 SQ4 <--
%D # U0 L0 -
%D # U1 L1 -
%D # U2 L2 -
%D # U3 L3 -
%D ))
%D enddiagram
%D
\pu
$$
\diag{freyd-stages-1}
$$
%$$\pu
% \diag{freyd-stages-2}
%$$
I was not very good at drawing all stages separately --- it was
boring, it took me too long, and I often got distracted and committed
errors --- so I started to play with extensions of that diagrammatic
language.
% _____ _ _ _ _ ___
% | ___| __ ___ _ _ __| | __ _(_) |_| |__ / _ \ ___
% | |_ | '__/ _ \ | | |/ _` | \ \ /\ / / | __| '_ \ | | | / __|
% | _|| | | __/ |_| | (_| | \ V V /| | |_| | | | | |_| \__ \
% |_| |_| \___|\__, |\__,_| \_/\_/ |_|\__|_| |_| \__\_\___/
% |___/
%
% «freyd-with-quantifiers» (to ".freyd-with-quantifiers")
% Orig: (favp 15 "freyd-with-quantifiers")
% (fava "freyd-with-quantifiers")
% sec: 4.1
\subsection{Adding quantifiers \DONE}
\label{freyd-with-quantifiers}
Here is a simple way to draw all stages at once. We start from a
diagram for the ``last stage with quantifiers'', that we will call
$LSQ$:
%
%D diagram cat-has-equalizers-with-quants
%D 2Dx 100 +30 +30
%D 2D 100 D0
%D 2D | \
%D 2D +30 D1 -- D2 == D3
%D 2D
%D ren D0 D1 D2 D3 ==> ∀_3X ∃_2E ∀_1A ∀_1B
%D
%D (( D2 D3 -> sl^^ .plabel= a ∀_1f
%D D2 D3 -> sl__ .plabel= b ∀_1g
%D D2 D3 midpoint .TeX= \scriptstyle? place
%D D1 D2 -> .plabel= b ∃_2e
%D D0 D2 -> .plabel= r ∀_3h
%D D0 D1 -> .plabel= l ∃!_4k
%D ))
%D enddiagram
%D
$$\pu
\scalebox{1.75}{$
\diag{cat-has-equalizers-with-quants}
$}
$$
We can recover all the stages and quantifiers from it. The numbered
quantifiers in it are $∀_1$, $∃_2$, $∀_3$, and $∃!_4$. The highest
number in them is 4, so we set $n=4$ ($n$ is the index of the last
stage), and we set ``stage 4 with quantifiers'', $SQ_4$, to $LSQ$. To
obtain the $SQ_3$ from $SQ_4$ we delete all nodes an arrows in $SQ_4$
that are annotated with a `$∃!_4$'; to obtain $SQ_2$ from $SQ_3$ we
delete all nodes an arrows in $SQ_3$ that are annotated with a
`$∀_3$', and so on until we get a diagram $SQ_0$, that in this example
is empty. To obtain each $S_k$ --- a stage in the original
diagrammatic language from Freyd, that doesn't have quantifiers ---
from the corresponding $SQ_k$ we treat all the quantifiers in $SQ_k$
as mere annotations, and we erase them; for example, `$∃_2e$' becomes
`$e$', and $∀_1A$ becomes $A$. To obtain the quantifiers $Q_1$, $Q_2$,
$Q_3$, $Q_4$ that are put in the vertical bars that separate the
stages, we just assign $∀_1$, $∃_2$, $∀_3$, and $∃!_4$ to them,
without the numbers in the subscripts.
Bonus convention: when the quantifiers in a diagram are just `$∀$'s
and `$∃!$'s without subscripts the `$∀$'s are to be interpreted as
`$∀_1$' and the `$∃!$'s as `$∃!_2$'s.
% _____ _ _ _ _ _____
% | ___| __ ___ _ _ __| | __ _(_) |_| |__ | ___|__
% | |_ | '__/ _ \ | | |/ _` | \ \ /\ / / | __| '_ \ | |_ / __|
% | _|| | | __/ |_| | (_| | \ V V /| | |_| | | | | _|\__ \
% |_| |_| \___|\__, |\__,_| \_/\_/ |_|\__|_| |_| |_| |___/
% |___/
%
% «freyd-with-functors» (to ".freyd-with-functors")
% (misp 17 "freyd-with-functors")
% (misa "freyd-with-functors")
% sec: 4.1
% Orig: (favp 16 "freyd-with-functors")
% (fava "freyd-with-functors")
% sec: 4.2
\subsection{Adding functors \DONE}
\label{freyd-with-functors}
Freyd's language can't represent functors --- in the sense of diagrams
like the ones in sec.\ref{internal-view-functor} --- and I wanted to
use it to draw the missing diagrams for definitions involving
functors, so I had to extend it again.
% (find-books "__cats/__cats.el" "freyd-scedrov")
Let me use an example to discuss this. This is the definition of
universal arrow in \cite[p.55]{CWM2}, including the original diagram,
modulo change of letters:
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 55) "1. Universal Arrows")
%
%D diagram univ-arrow-cwm-my-letters
%D 2Dx 100 +25 +25
%D 2D 100 A0 A1 A2
%D 2D
%D 2D +25 A3 A4 A5
%D 2D
%D ren A0 A1 A2 ==> A RB B
%D ren A3 A4 A5 ==> A RB', B'.
%D
%D (( A0 A1 -> .plabel= a η
%D A0 A3 midpoint .TeX= \veq place
%D A1 A4 .> .plabel= r Rf
%D A2 A5 .> .plabel= r f
%D A3 A4 -> .plabel= a g
%D ))
%D enddiagram
\begin{quotation}
{\bf Definition.} If $R: \catB→\catA$ is a functor and $A$ an object
of $\catA$, a universal arrow from $A$ to $R$ is a pair $(B,η)$
consisting of an object $B$ of $\catB$ and and arrow $η:A→RB$ of
$\catA$ such that to every pair $(B',g)$ with $B'$ an object of
$\catB$ and $g:A→RB'$ an arrow of $\catA$, there is a unique arrow
$f:B→B'$ of $\catB$ with $Rf∘η=g$. In other words, every arrow $h$
to $R$ factors uniquely through the universal arrow $η$, as in the
commutative diagram:
%
$$\pu
\diag{univ-arrow-cwm-my-letters}
$$
\end{quotation}
The definition itself goes only up to the ``with $Rf∘η=g$.'', so let
me ignore the part starting from ``In other words'', and draw a better
``missing diagram'' for the definition:
%
%D diagram universal-arrow-stages
%D 2Dx 100 +20 +20 +20 +20 +20 +20 +20
%D 2D 100 U0 U1
%D 2D
%D 2D +10 A1 B1 C1
%D 2D | | |
%D 2D +20 A2 A3 B2 B3 C2 C3
%D 2D | | | | | |
%D 2D +20 A4 A5 B4 B5 C4 C5
%D 2D
%D 2D +15 A6 A7 B6 B7 C6 C7
%D 2D
%D 2D +10 L0 L1
%D 2D
%D ren A1 A2 A3 A4 A5 A6 A7 ==> A B RB B' RB' \catB \catA
%D ren B1 B2 B3 B4 B5 B6 B7 ==> A B RB B' RB' \catB \catA
%D ren C1 C2 C3 C4 C5 C6 C7 ==> A B RB B' RB' \catB \catA
%D ren U0 L0 ==> ∀ {}
%D ren U1 L1 ==> ∃! {}
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D A6 A7 -> .plabel= a R
%D U0 L0 -
%D ))
%D (( B1 B3 -> .plabel= r η
%D B2 B3 |->
%D B4 B5 |->
%D B1 B5 -> .slide= 15pt .plabel= r g
%D B6 B7 -> .plabel= a R
%D U1 L1 -
%D ))
%D (( C1 C3 -> .plabel= r η
%D C2 C3 |->
%D C2 C4 -> .plabel= l f
%D C3 C5 -> .plabel= r Rf
%D C2 C5 harrownodes nil 20 nil |->
%D C4 C5 |->
%D C1 C5 -> .slide= 20pt .plabel= r g
%D C6 C7 -> .plabel= a R
%D ))
%D enddiagram
%D
$$\pu
\diag{universal-arrow-stages}
$$
This diagram is quite close to being a skeleton for the definition of
universal arrow. It can be interpreted as a proposition, and the only
extra hint that we need is that ``universalness'' for the arrow $η$
corresponds to the truth of that proposition. Here's how to extract
the proposition from it:
%
$$\begin{array}{rl}
\text{In a context where:}
& \catA \text{ is a category}, \\
& \catB \text{ is a category}, \\
& R:\catB \to \catA, \\
& A ∈ \catA, \\
& B ∈ \catB, \\
& η:A→RB, \\
\text{for all}
& B'∈\catB \text{ and} \\
& g:A→RB', \\
\text{there exists a unique}
& f:B→B' \text { such that} \\
& Rf∘η=g. \\
\end{array}
$$
To convert that to a definition of universalness we just have to
replace the ``for all'' by ``$(B,η)$ is a universal arrow for $A$ to
$R$ iff for all''.
The convention for quantifiers from sec.\ref{freyd-with-quantifiers}
lets us rewrite the diagram in three stages above as:
%
%D diagram universal-arrow-quants
%D 2Dx 100 +20
%D 2D 100 C1
%D 2D |
%D 2D +20 C2 C3
%D 2D | |
%D 2D +20 C4 C5
%D 2D
%D 2D +15 C6 C7
%D 2D
%D ren C1 C2 C3 C4 C5 C6 C7 ==> A B RB ∀B' RB' \catB \catA
%D
%D (( C1 C3 -> .plabel= r η
%D C2 C3 |->
%D C2 C4 -> .plabel= l ∃!f
%D C3 C5 -> .plabel= r Rf
%D C2 C5 harrownodes nil 20 nil |->
%D C4 C5 |->
%D C1 C5 -> .slide= 20pt .plabel= r ∀g
%D C6 C7 -> .plabel= a R
%D ))
%D enddiagram
%D
$$\pu
\scalebox{1.5}{$
\diag{universal-arrow-quants}
$}
$$
Also, I noticed that I could omit most typings when they could be
inferred from the diagram. I could ``formalize'' the diagram above as:
``in a context where $(\catA, \catB, R, A, B, η)$ are as in the
diagram above, we say that $(B,η)$ is a universal arrow from $A$ to
$R$ when $∀(B',g).∃!f.(Rf∘η=g)$''. This looked too loaded to be used
in public, but it was practical for private notes --- and I could even
omit the ``$Rf∘η=g$'', as everything commutes by default. In
sec.\ref{omitting-types} we will see a way to formalize this method
for omitting and reconstructing types, and in
sec.\ref{indefinite-articles} we will see a second way to define
universalness.
\bsk
Note that when we erase a node or arrow we also erase everything that
depends on it. In the example above $SQ_2$ has an arrow labeled
$∃!_2f$; to obtain $SQ_1$ from $SQ_2$ we have to erase that arrow, the
arrow $Rf$, and the arrow $f \mapsto Rf$ --- and to obtain $SQ_0$ from
$SQ_1$ we have to erase the arrow $g$, the node $B'$, the node $RB'$,
and the arrow $B' \mapsto RB'$.
% ___ _ _ _
% |_ _|_ __ | |_ ___ _ __ _ __ __ _| | __ _(_) _____ _____
% | || '_ \| __/ _ \ '__| '_ \ / _` | | \ \ / / |/ _ \ \ /\ / / __|
% | || | | | || __/ | | | | | (_| | | \ V /| | __/\ V V /\__ \
% |___|_| |_|\__\___|_| |_| |_|\__,_|_| \_/ |_|\___| \_/\_/ |___/
%
% «internal-views» (to ".internal-views")
% (misp 20 "internal-views")
% (misa "internal-views")
% sec: 5
% Orig: (favp 19 "internal-views")
% (fava "internal-views")
\section{Internal views \DONE}
\label{internal-views}
My favorite way of introducing internal views is with the diagram
below:
%
% (nyop 19 "blob-sets")
% (nyo "blob-sets")
% (nyop 20 "blob-sets-2")
% (nyo "blob-sets-2")
% (nyop 21 "blob-cats-and-functors")
% (nyo "blob-cats-and-functors")
%
\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}
$$
\def\longmapsto{\diagxyto/|->/}
The parts with the two blobs and `$\longmapsto$'s between them is
based on how I was taught sets and functions when I was a kid; it is
an internal view of the $\N \ton{\sqrt{\phantom{a}}} \R$ below it. Not
all elements of $\N$ are shown in the blob-view of $\N$, but the ones
that are shown are named; compare this with \cite[p.2
onwards]{LawvereRosebrugh}, in which the elements are usually dots.
The arrow $n \longmapsto \sqrt{n}$ between the blobs shows a {\sl
generic element} of $\N$ and its image, and the other
`$\longmapsto$'s are {\sl substitution instances of it}, like this:
%
$$(n \longmapsto \sqrt{n}) [n:=2] = (2 \longmapsto \sqrt{2})$$
In some cases, like $4 \longmapsto 2$, we write 2 instead of
$\sqrt{4}$ because $\sqrt{4}$ ``reduces to'' 2, as explained in the
next section.
% ____ _ _ _
% | _ \ ___ __| |_ _ ___| |_(_) ___ _ __ ___
% | |_) / _ \/ _` | | | |/ __| __| |/ _ \| '_ \/ __|
% | _ < __/ (_| | |_| | (__| |_| | (_) | | | \__ \
% |_| \_\___|\__,_|\__,_|\___|\__|_|\___/|_| |_|___/
%
% «reductions» (to ".reductions")
% Orig: (favp 19 "reductions")
% (fava "reductions")
% sec: 5.1
%
\subsection{Reductions \DONE}
\label{reductions}
\def\squigton#1{\overset{#1}{\squigto}}
The convention (C$\mapsto$) says that an arrow $α \mapsto β$ above an
arrow $A \ton{f} B$ should be interpreted as meaning $f(α) \squigto
β$, where `$\squigto$' means ``reduces to''; the standard example is
$\sqrt{4} \squigto 2$. In a diagram:
%
%D diagram reductions-0
%D 2Dx 100 +20 +25 +40 +20 +25
%D 2D 100 A0 A1 B0
%D 2D +8 A2 A3 C0 C1 E0
%D 2D
%D 2D +15 A4 A5 C2 C3
%D 2D
%D ren A0 A1 ==> 4 2
%D ren A2 A3 ==> n \sqrt{n}
%D ren A4 A5 ==> \N \R
%D ren B0 ==> \sqrt{4}\squigto2
%D ren C0 C1 ==> α β
%D ren C2 C3 ==> A B
%D ren E0 ==> f(α)\squigtoβ
%D
%D (( A0 A1 |->
%D A2 A3 |->
%D A4 A5 -> .plabel= a \sqrt{\phantom{a}}
%D B0 place
%D C0 C1 |->
%D C2 C3 -> .plabel= a f
%D E0 place
%D ))
%D enddiagram
%D
$$\pu
\diag{reductions-0}
$$
The idea of reduction comes from $λ$-calculus. We write $α
\squigton{1} β$ to say that the term $α$ reduces to $β$ in one step,
and $α \squigton{*} γ$ to say that there is a finite sequence of
one-step reductions that reduce $α$ to $γ$. Here we are interested in
reduction in a system with constants, in which for example
$(\sqrt{\phantom{a}})(4) \squigton{1} 2$.
Here is a directed graph that shows all the one-step reductions
starting from $g(2+3)$, considering $g(a) = a·a+4$:
%
% (lam181p 5 "lambda")
% (lam181 "lambda")
%
%D diagram reduce-g
%D 2Dx 100 +30 +30 +40 +30
%D 2D 100 A ----> B
%D 2D | |
%D 2D v v
%D 2D +25 E |
%D 2D | \ |
%D 2D | v |
%D 2D +20 | F |
%D 2D | \ |
%D 2D v v v
%D 2D +20 G ----> H -> I -> J
%D 2D
%D ren A B ==> g(2+3) g(5)
%D ren E F ==> (2+3)·(2+3)+4 (2+3)·5+4
%D ren G H ==> 5·(2+3)+4 5·5+4
%D ren I J ==> 25+4 29
%D (( A B -> E F -> F H -> G H ->
%D A E -> E G -> B H -> H I -> I J ->
%D ))
%D enddiagram
%D
$$\pu
\diag{reduce-g}
$$
Note that all reductions sequences starting from $g(2+3)$ terminate at
the same term, 29 --- ``the term $g(2+3)$ is strongly normalizing''
---, and reduction sequences from $g(2+3)$ may ``diverge'' but they
``converge'' later --- this is the ``Church-Rosser Property'', a.k.a.
``confluence''.
A good place to learn about reduction in systems with constants is
\cite{SICP}.
% https://en.wikipedia.org/wiki/Confluence_(abstract_rewriting)
% (find-books "__comp/__comp.el" "abelson-sussman")
% (find-sicppage (+ 28 42) "Figure 1.3: A linear recursive process for computing 6!")
% (find-sicptext (+ 28 42) "Figure 1.3: A linear recursive process for computing 6!")
% (find-es "scheme" "sicp-pdf")
% (find-pdf-page "~/usrc/sicp-pdf/src/fig/chap1/Fig1.3c.pdf")
% \begin{center}
% \includegraphics[height=144pt]{2020favorite-conventions-frob.pdf}
% \end{center}
% _____ _
% | ___| _ _ __ ___| |_ ___ _ __ ___
% | |_ | | | | '_ \ / __| __/ _ \| '__/ __|
% | _|| |_| | | | | (__| || (_) | | \__ \
% |_| \__,_|_| |_|\___|\__\___/|_| |___/
%
% «internal-view-functor» (to ".internal-view-functor")
% Orig: (favp 20 "internal-view-functor")
% (fava "internal-view-functor")
% sec: 5.2
%
\subsection{Functors \DONE}
\label{internal-view-functor}
% (nyop 21 "blob-cats-and-functors")
% (nyo "blob-cats-and-functors")
% (nyop 25 "convention-functors")
% (nyo "convention-functors")
By the convention (CFSh) the image of the diagram above $\catA$ in the
diagram below --- remember that {\sl above} usually means {\sl inside}
---
%
%D diagram internal-view-functor-0
%D 2Dx 100 +10 +10 +25 +12 +12
%D 2D 100 A1 ____ B1 ____
%D 2D +10 | ____ A3 | ____ B3
%D 2D +10 A2 ____ | B2 ____ |
%D 2D +10 A4 B4
%D 2D
%D 2D +15 \catA ------> \catB
%D 2D
%D ren A1 A2 A3 A4 ==> A_1 A_2 A_3 A_4
%D
%D (( A1 A2 -> .plabel= l f
%D A2 A3 -> .plabel= m g
%D A3 A4 -> .plabel= r h
%D A1 A3 -> .plabel= a k
%D A2 A4 -> .plabel= b m
%D \catA \catB -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-0}
$$
%
is a diagram with the same shape over $\catB$. We draw it like this:
%
%D diagram internal-view-functor-1
%D 2Dx 100 +10 +10 +25 +14 +14
%D 2D 100 A1 ____ B1 ____
%D 2D +10 | ____ A3 | ____ B3
%D 2D +10 A2 ____ | B2 ____ |
%D 2D +10 A4 B4
%D 2D
%D 2D +15 \catA ------> \catB
%D 2D
%D ren A1 A2 A3 A4 ==> A_1 A_2 A_3 A_4
%D ren B1 B2 B3 B4 ==> FA_1 FA_2 FA_3 FA_4
%D
%D (( A1 A2 -> .plabel= l f
%D A2 A3 -> .plabel= m g
%D A3 A4 -> .plabel= r h
%D A1 A3 -> .plabel= a k
%D A2 A4 -> .plabel= b m
%D \catA \catB -> .plabel= a F
%D
%D B1 B2 -> .plabel= l Ff
%D B2 B3 -> .plabel= m Fg
%D B3 B4 -> .plabel= r Fh
%D B1 B3 -> .plabel= a Fk
%D B2 B4 -> .plabel= b Fm
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-1}
$$
In this case we don't draw the arrows like $A_1 \mapsto FA_1$ because
there would be too many of them --- we leave them implicit.
We say that the diagram above is {\sl an} internal view of the functor
$F$. To draw {\sl the} internal view of the functor $F: \catA → \catB$
we start with a diagram in $\catA$ that is made of two generic objects
and a generic morphism between them. We get this:
%D diagram internal-view-functor-2
%D 2Dx 100 +20
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> C FC D FD \catA \catB
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l g
%D A1 A3 -> .plabel= r Fg
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-2}
$$
Compare this with the diagram with blob-sets in Section
\ref{internal-views}, in which the `$n \mapsto \sqrt{n}$' says where a
generic element is taken.
Any arrow of the form $α \mapsto β$ above a functor arrow $\catA
\ton{F} \catB$ is interpreted as saying that $F$ takes $α$ to $β$, or,
in the terminology of the section \ref{reductions}, that $Fα$ reduces
to $β$. So this diagram
%
%D diagram internal-view-functor-3
%D 2Dx 100 +25
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> B A{×}B C A{×}C \Set \Set
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l f
%D A1 A3 -> .plabel= r λp.(πp,f(π'p))
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a (A{×})
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-3}
$$
%
defines $(A×)$ as:
%
$$\begin{array}{rcl}
(A×)_0 &:=& λB.\,A×B,\\
(A×)_1 &:=& λf.λp.(πp,f(π'p)).\\
\end{array}
$$
In this case we can also use internal views of $(A×)$ to define
$(A×)_1$:
%
%D diagram internal-view-functor-4
%D 2Dx 100 +25 +30 +35
%D 2D 100 A0 A1 C0 D0
%D 2D
%D 2D +20 A2 A3 C1 D1
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> B A{×}B C A{×}C \Set \Set
%D ren C0 C1 ==> (a,b) (a,f(b))
%D ren D0 D1 ==> p (πp,f(π'p))
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l f
%D A1 A3 -> .plabel= r (A{×})f
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a (A{×})
%D C0 C1 |->
%D D0 D1 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-4}
$$
% _ _ _____
% | \ | |_ _|__
% | \| | | |/ __|
% | |\ | | |\__ \
% |_| \_| |_||___/
%
% «internal-view-NT» (to ".internal-view-NT")
% Orig: (favp 22 "internal-view-NT")
% (fava "internal-view-NT")
% sec: 22
%
\subsection{Natural transformations \DONE}
\label{internal-view-NT}
Suppose that we have two functors $F,G:\catA → \catB$ and a natural
transformation $T:F→G$. A first way to draw an internal view of $T$ is
this:
%
%D diagram internal-view-NT-0
%D 2Dx 100 +25
%D 2D 100 A1
%D 2D +10 A0
%D 2D +10 A2
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A2 B0 B1 ==> C FC GC \catA \catB
%D
%D (( A0 A1 |->
%D A0 A2 |->
%D A1 A2 -> .plabel= r TC
%D A0 A1 A2 midpoint |->
%D B0 B1 -> sl^ .plabel= a F
%D B0 B1 -> sl_ .plabel= b G
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-NT-0}
$$
If we start with a morphism $h:C→D$ in $\catA$, like this,
%
%D diagram NT-00
%D 2Dx 100 +25
%D 2D 100 A0
%D 2D +20 A1
%D 2D +15 D0 D1
%D 2D
%D ren A0 A1 ==> C D
%D ren D0 D1 ==> \catA \catB
%D
%D (( A0 A1 -> .plabel= l h
%D D0 D1 -> sl^ .plabel= a F
%D D0 D1 -> sl_ .plabel= b G
%D ))
%D enddiagram
%
$$\pu
\diag{NT-00}
$$
%
the convention (CFSh) would yield an image of $h$ by $F$ and another
by $G$, and we can draw the arrows $TC$ and $TD$ to obtain a commuting
square in $\catB$:
%
%D diagram NT-0
%D 2Dx 100 +20 +15 +15
%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 2D +15 D0 D1
%D 2D
%D ren A0 A1 ==> C D
%D ren B0 B1 B2 B3 ==> FC GC FD GD
%D ren C0 C1 ==> F G
%D ren D0 D1 ==> \catA \catB
%D
%D (( A0 B0 |->
%D A0 B1 |->
%D A1 B2 |->
%D A1 B3 |->
%D
%D A0 A1 -> .plabel= l h
%D B0 B1 -> .plabel= b TC
%D B0 B2 -> .plabel= r Fh
%D B1 B3 -> .plabel= r Gh
%D B2 B3 -> .plabel= b TD
%D C0 C1 -> .plabel= a T
%D D0 D1 -> sl^ .plabel= a F
%D D0 D1 -> sl_ .plabel= b G
%D ))
%D enddiagram
%
$$\pu
\diag{NT-0}
$$
This way of drawing internal views of natural transformations yields
diagrams that are too heavy, so we will usually draw them as just
this:
%
%D diagram NT-1
%D 2Dx 100 +20 +25
%D 2D 100 A0 B0 B1
%D 2D
%D 2D +25 A1 B2 B3
%D 2D +15 C0 C1
%D 2D
%D ren A0 A1 ==> C D
%D ren B0 B1 B2 B3 ==> FC GC FD GD
%D ren C0 C1 ==> F G
%D
%D (( A0 A1 -> .plabel= l h
%D B0 B1 -> .plabel= a TC
%D B0 B2 -> .plabel= l Fh
%D B1 B3 -> .plabel= r Gh
%D B2 B3 -> .plabel= b TD
%D C0 C1 -> .plabel= a T
%D ))
%D enddiagram
%
$$\pu
\diag{NT-1}
$$
%
Note that the input morphism is at the left, and above $F \ton{T} G$
we draw its images by $F$, $G$, and $T$.
When the codomain of $F$ and $G$ is $\Set$ we will sometimes also draw
at the right an internal view of the commuting square, like this:
%
%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 ==> C D
%D ren B0 B1 B2 B3 ==> FC GC FD GD
%D ren C0 C1 ==> F G
%D ren D0 D1 D3' ==> x (TC)(x) (Gh∘TC)(x)
%D ren D2 D3 ==> (Fh)(x) (TD∘Ff)(x)
%D
%D (( A0 A1 -> .plabel= l h
%D B0 B1 -> .plabel= a TC
%D B0 B2 -> .plabel= l Fh
%D B1 B3 -> .plabel= r Gh
%D B2 B3 -> .plabel= a TD
%D C0 C1 -> .plabel= a T
%D D0 D1 |-> D1 D3' |-> D0 D2 |-> D2 D3 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{NT-2}
$$
%
Then the commutativity of the middle square is equivalent to
$∀x∈FC.(Gh∘TC)(x)=(TD∘Ff)(x)$. Note that in this case the square at
the right is an internal view of an internal view.
In Section \ref{to-deserve-a-name} we saw that a functor has four
components. A natural transformation has two: $T=(T_0, \sqcond_T)$,
where $T_0$ is the operation $C \mapsto TC$ and $\sqcond_T$ is the
guarantee that all the induced squares commute.
% Sometimes we will use the upper line of the internal view of the
% internal view to define $T_0$ --- see Section \ref{basic-example-NT}
% for an example of this.
%
% \standout{TODO:} Fix the reference above.
% Tom Leinster has a diagram like my internal view of
% the internal view...
% (find-books "__cats/__cats.el" "leinster-basic")
% (find-leinsterbasicpage (+ 8 86) "Lemma 4.1.10")
% (find-leinsterbasictext (+ 8 86) "Lemma 4.1.10")
% _ _ _ _ _
% / \ __| |(_)_ _ _ __ ___| |_(_) ___ _ __ ___
% / _ \ / _` || | | | | '_ \ / __| __| |/ _ \| '_ \/ __|
% / ___ \ (_| || | |_| | | | | (__| |_| | (_) | | | \__ \
% /_/ \_\__,_|/ |\__,_|_| |_|\___|\__|_|\___/|_| |_|___/
% |__/
%
% «internal-view-adjunction» (to ".internal-view-adjunction")
% Orig: (favp 24 "internal-view-adjunction")
% (fava "internal-view-adjunction")
% sec: 5.4
%
\subsection{Adjunctions \DONE}
\label{internal-view-adjunction}
% (nyop 35 "convention-adjs")
% (nyo "convention-adjs")
We will draw adjunctions like this,
%
%D diagram generic-adjunction
%D 2Dx 100 +25
%D 2D 100 LB <-| B
%D 2D | |
%D 2D v v
%D 2D +20 C |--> RC
%D 2D
%D 2D +15 E <==> F
%D 2D
%D ren LB B ==> LA A
%D ren C RC ==> B RB
%D ren E F ==> \catB \catA
%D
%D (( LB B <-| # .plabel= a L_0
%D C RC |-> # .plabel= b R_0
%D
%D LB RC harrownodes nil 20 nil <->
%D
%D LB C -> # .plabel= l \sm{g^♭\\f}
%D B RC -> # .plabel= r \sm{g\\f^♯}
%D E F <- sl^ .plabel= a L
%D E F -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\pu
\diag{generic-adjunction}
$$
%
with the left adjoint going left and the right adjoint going right. My
favorite names for the left and right adjoints are $L$ and $R$. The
standard notation for that adjunction is $L⊣R$.
The top-level component of the diagram above is the bijection arrow in
the middle of the square --- it says that $\Hom(LA,B) ↔ \Hom(A,RB)$.
It is implicit that we have bijections like that for all $A$ and $B$;
it is also implicit that that bijection is natural in some sense.
We will sometimes expand adjunction diagrams by adding unit and counit
maps, the unit and the unit as natural transformations, the actions of
$L$ and $R$ on morphisms, and other things. For example:
%
%D diagram generic-adjunction-with-with
%D 2Dx 100 +20 +20 +20 +20 +20
%D 2D 100 D0 D1
%D 2D +20 B0 C0 D2 D3 E0 F0
%D 2D +20 B1 C1 D4 D5 E1 F1
%D 2D +20 D6 D7
%D 2D +15 H0 H1
%D 2D
%D ren D0 D1 ==> LA' A'
%D ren B0 C0 D2 D3 E0 F0 ==> LR LRB LA A A \id_\catA
%D ren B1 C1 D4 D5 E1 F1 ==> \id_\catB B B RB RLA LR
%D ren D6 D7 ==> B' RB'
%D ren H0 H1 ==> \catB \catA
%D
%D (( B0 B1 -> .plabel= l ε
%D C0 C1 -> .plabel= l ε_B
%D
%D D0 D1 <-|
%D D0 D2 -> .plabel= l Lf
%D D1 D3 -> .plabel= r f
%D D0 D3 harrownodes nil 20 nil <-|
%D D2 D3 <-|
%D D2 D4 -> .plabel= l \sm{h^♭\\g}
%D D3 D5 -> .plabel= r \sm{h\\g^♯}
%D D2 D5 harrownodes nil 20 nil <-| sl^
%D D2 D5 harrownodes nil 20 nil |-> sl_
%D D4 D5 |->
%D D4 D6 -> .plabel= l k
%D D5 D7 -> .plabel= r Rk
%D D6 D7 |->
%D D4 D7 harrownodes nil 20 nil |->
%D
%D E0 E1 -> .plabel= r η_A
%D F0 F1 -> .plabel= r η
%D
%D H0 H1 <- sl^ .plabel= a L
%D H0 H1 -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\pu
\diag{generic-adjunction-with-with}
$$
\def\HomA#1{HomA(#1)}
\def\HomB#1{HomB(#1)}
\def\HomA#1{\catA(#1)}
\def\HomB#1{\catB(#1)}
We can obtain the naturality conditions by regarding $♭$ and $♯$ as
natural transformations and drawing the internal views of their
internal views:
%
%D diagram adj-nat-conditions
%D 2Dx 100 +35 +45 +45 +45
%D 2D 100 A0 B0 - B1 D0 - D1
%D 2D | | | | |
%D 2D +17 | | | D2' |
%D 2D +8 A1 B2 - B3 D2 - D3
%D 2D
%D 2D +15 A2 C0 = C1
%D 2D
%D 2D +20 E0 F0 - F1 H0 - H1
%D 2D | | | | |
%D 2D +17 | | | | H3'
%D 2D +8 E1 F2 - F3 H2 - H3
%D 2D
%D 2D +15 E2 G0 = G1
%D 2D
%D ren A0 A1 A2 ==> (A,B) (A',B') \catA^\op{×}\catB
%D ren B0 B1 D0 D1 ==> \HomB{LA,B} \HomA{A,RB} h^♭ h
%D ren D2' ==> k∘h^♭∘Lf
%D ren B2 B3 D2 D3 ==> \HomB{LA',B'} \HomA{A',RB'} (Rk∘h∘f)^♭ Rk∘h∘f
%D ren C0 C1 ==> \HomB{L-,-} \HomA{-,R-}
%D
%D ren E0 E1 E2 ==> (A,B) (A',B') \catA^\op{×}\catB
%D ren F0 F1 H0 H1 ==> \HomB{LA,B} \HomA{A,RB} g g^♯
%D ren H3' ==> Rk∘g^♯∘f
%D ren F2 F3 H2 H3 ==> \HomB{LA',B'} \HomA{A',RB'} k∘g∘Lf (k∘g∘Lf)^♯
%D ren G0 G1 ==> \HomB{L-,-} \HomA{-,R-}
%D
%D (( A0 A1 -> .plabel= l (f^\op,g)
%D # A2 place
%D B0 B1 <-
%D B0 B2 ->
%D B1 B3 ->
%D B2 B3 <-
%D C0 C1 <- .plabel= a ♭
%D D0 D1 <-|
%D D0 D2' |->
%D D1 D3 |->
%D D2 D3 <-|
%D
%D E0 E1 -> .plabel= l (f^\op,g)
%D # E2 place
%D F0 F1 ->
%D F0 F2 ->
%D F1 F3 ->
%D F2 F3 ->
%D G0 G1 -> .plabel= a ♯
%D H0 H1 |-> H1 H3' |->
%D H0 H2 |-> H2 H3 |->
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{adj-nat-conditions}
$$
% _____ _ _ _ _
% |_ _|__ __ _ ___| |__ (_)_ __ __ _ __ _ __| |(_)___
% | |/ _ \/ _` |/ __| '_ \| | '_ \ / _` | / _` |/ _` || / __|
% | | __/ (_| | (__| | | | | | | | (_| | | (_| | (_| || \__ \
% |_|\___|\__,_|\___|_| |_|_|_| |_|\__, | \__,_|\__,_|/ |___/
% |___/ |__/
%
% «teaching-adjunctions» (to ".teaching-adjunctions")
% Orig: (favp 25 "teaching-adjunctions")
% (fava "teaching-adjunctions")
% sec: 5.5
\subsection{A way to teach adjunctions \DONE}
\label{teaching-adjunctions}
I mentioned in the first sections that I have tested some parts of
this language in a seminar course --- described here:
\cite{OchsWLD2019} --- and that in it I taught Categories starting by
adjunctions. Here's how: we started by the basics of $λ$-calculus and
some sections of \cite{PH1}, and then I asked the students to define
each one of the operations in the right half of the diagram below as
$λ$-terms:
%
% --- where $(C{→}D) = D^C$:
%
%D diagram generic-adjunction-big
%D 2Dx 100 +20 +25 +20
%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 +15 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 +30 +25 +35
%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 +15 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-big}
\qquad
\diag{(xB)-|(B->)}
$$
Then we saw the definition of functors, natural transformations and
adjunctions, and we checked that the right half is a particular case
(``for children''!) of the diagram for a generic adjunction in the
left half. After that, and after also checking that in the Planar
Heyting Algebras of \cite{PH1} we have an adjunction $(∧Q)⊣(Q→)$, I
helped the students to decypher some excerpts of \cite{Awodey}.
\msk
From the components of the generic adjunction in the diagram above it
is possible to build this big diagram:
%
%D diagram teaching-adjunctions-1
%D 2Dx 100 +20 +20 +20 +20 +20 +20 +20 +20
%D 2D 100 A0 A1
%D 2D +20 A2 A3
%D 2D +20 A4 A5
%D 2D
%D 2D +20 B0 B1 D0 D1
%D 2D +20 B2 B3 C0 D2 D3 E0 F0 F1
%D 2D +20 B4 B5 C1 D4 D5 E1 F2 F3
%D 2D +20 D6 D7 F4 F5
%D 2D
%D 2D +20 G0 G1
%D 2D +20 G2 G3
%D 2D +20 G4 G5
%D 2D
%D 2D +20 H0 H1
%D 2D
%D
%D ren A0 A1 ==> LA' A'
%D ren A3 ==> A
%D ren A4 A5 ==> LA RLA
%D
%D ren B0 B1 D0 D1 ==> LA A LA' A'
%D ren B2 B3 C0 D2 D3 E0 F1 ==> LRB RB LRB LA A A A
%D ren B4 C1 D4 D5 E1 F2 F3 ==> B B B RB RLA LA RLA
%D ren D6 D7 F4 F5 ==> B' RB' B RB
%D
%D ren G0 G1 ==> LRB RB
%D ren G2 ==> B
%D ren G4 G5 ==> B' RB'
%D
%D ren H0 H1 ==> \catB \catA
%D
%D ((
%D ))
%D (( A0 A1 <-|
%D A0 A4 -> .plabel= l Lf
%D A1 A3 -> .plabel= r f
%D A3 A5 -> .plabel= r η_A
%D A1 A5 -> .slide= -10pt
%D A0 A5 harrownodes nil 15 5 <-|
%D A4 A5 <-|
%D
%D B0 B1 <-|
%D B0 B2 -> .plabel= l Lh
%D B1 B3 -> .plabel= r h
%D B0 B3 harrownodes nil 20 nil <-|
%D B2 B3 <-|
%D B2 B4 -> .plabel= l ε_B
%D B0 B4 -> .slide= -20pt .plabel= l g
%D
%D C0 C1 -> .plabel= l ε_B
%D
%D D0 D1 <-|
%D D0 D2 -> .plabel= l Lf
%D D1 D3 -> .plabel= r f
%D D0 D3 harrownodes nil 20 nil <-|
%D D2 D3 <-|
%D D2 D4 -> .plabel= l \sm{h^♭\\g}
%D D3 D5 -> .plabel= r \sm{h\\g^♯}
%D D2 D5 harrownodes nil 20 nil <-| sl^
%D D2 D5 harrownodes nil 20 nil |-> sl_
%D D4 D5 |->
%D D4 D6 -> .plabel= l k
%D D5 D7 -> .plabel= r Rk
%D D6 D7 |->
%D D4 D7 harrownodes nil 20 nil |->
%D
%D E0 E1 -> .plabel= r η_A
%D
%D F1 F3 -> .plabel= r η_A
%D F2 F3 |->
%D F2 F4 -> .plabel= l g
%D F3 F5 -> .plabel= r Rg
%D F4 F5 |->
%D F2 F5 harrownodes nil 20 nil |->
%D F1 F5 -> .slide= 20pt .plabel= r h
%D
%D G0 G1 |->
%D G0 G2 -> .plabel= l η_B
%D G2 G4 -> .plabel= l k
%D G0 G4 -> .slide= 10pt
%D G1 G5 -> .plabel= r Rk
%D G4 G5 |->
%D G0 G5 harrownodes 5 15 nil |->
%D
%D H0 H1 <- sl^ .plabel= a L
%D H0 H1 -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\pu
\diag{teaching-adjunctions-1}
$$
Let's use these names for its subdiagrams: $\sm{ A \\ BCDEF \\ G \\ I}$.
% (find-riehlccpage (+ 18 124) "fully-specified adjunction")
% (find-riehlcctext (+ 18 124) "fully-specified adjunction")
A {\sl fully-specified adjunction} between categories $\catB$ and
$\catA$ has lots of components: $(L, R, ε, η, ♭, ♯, \univ(ε),
\univ(η))$, and maybe even others, but usually we define only some of
these components; there is a Big Theorem About Adjunctions (below!)
that says how to reconstruct the fully-specified adjunction from some
of its components.
Some parts of the diagram above can be interpreted as definitions,
like these:
%
$$\begin{array}{c}
Lf := (η_A∘f)^♭ \\
[5pt]
g := ε_B∘Lh
\qquad ε_B := (\id_{RB})^♭
\qquad η_A := (\id_{LA})^♯
\qquad h := Rg∘η_A \\
[5pt]
Rk := (k∘η_B)^♯ \\
\end{array}
$$
The subdiagrams $B$ and $F$ can also be interpreted in the opposite
direction, as:
%
$$\begin{array}{rclcrcl}
g^♯ &:=& (∀A.∀g.∃!h)Ag &\phantom{mmmmmm}& h^♭ &:=& (∀B.∀h.∃!g)Bh \\
&=& (\univ_{ε_B})Ag && &=& (\univ_{η_A}) Bh \\
\end{array}
$$
The notations $(∀A.∀g.∃!h)Ag$ and $(\univ_{ε_B})Ag$ are clearly abuses
of language --- but it's not hard to translate them to something
formal, and these notations inspired great discussions in the
classroom... also, they can help us to understand and formalize
constructions like this one,
%
%D diagram building-L_1f
%D 2Dx 100 +25 +25
%D 2D 100 A1
%D 2D
%D 2D +25 A2 A3 B1
%D 2D
%D 2D +25 B2 B3
%D 2D
%D 2D +15 C0 C1
%D 2D
%D ren A1 A2 A3 ==> A' LA' RLA'
%D ren B1 B2 B3 ==> A LA RLA
%D ren C0 C1 ==> \catB \catA
%D
%D (( A1 A3 -> .plabel= l \sm{η_{A'}\\\univ}
%D A2 A3 |->
%D B1 B3 -> .plabel= r \sm{η_A\\\univ}
%D B2 B3 |->
%D A1 B1 -> .plabel= a f
%D A2 B2 -> .plabel= l Lf
%D A3 B3 -> .plabel= m RLf
%D A2 B3 harrownodes nil 15 2 |->
%D C0 xy+= 12 0
%D C1 xy+= 12 0
%D C0 C1 -> .plabel= b R
%D ))
%D enddiagram
%D
$$\pu
Lf := (\univ_{η_A})(LA)(η_A∘f)
\qquad
\diag{building-L_1f}
$$
%
that are needed in cases like the part (ii) of the Big Theorem.
The Big Theorem About Adjunctions is this --- it's the Theorem 2 in
\cite[page 83]{CWM2}, but with letters changed to match the ones we
are using in our diagrams:
\def\ORIG#1{\msk\ColorBrown{#1}}
\def\ORIG#1{}
\newpage
\begin{quotation}
\ORIG{{\bf Theorem 2.} Each adjunction $〈F,G,φ〉: X \rightharpoonup
A$ is completely determined by the items in any one of the
following lists:}
{\bf Big Theorem About Adjunctions.} Each adjunction $〈L,R,♯〉: \catA
\rightharpoonup \catB$ is completely determined by the items in any
one of the following lists:
\ORIG{(i) Functors $F$, $G$, and a natural transformation $η: 1_X
\tnto GF$ such that each $η_x: x→GFx$ is universal to $G$ from
$x$. Then $φ$ is defined by (6).}
(i) Functors $L$, $R$, and a natural transformation $η:
\id_\catA→RL$ such that each $η_A: A→RLA$ is universal to $R$ from
$A$. Then $♯$ is defined by (6).
\ORIG{(ii) The functor $G: A → X$ and for each $x∈X$ an
object $F_0x∈A$ and a universal arrow $η_x:x→GF_0x$ from $x$
to $G$. Then the functor $F$ has object function $F_0$ and is
defined on arrows $h:x→x'$ by $GFh∘η_x = η_{x'}∘h$.}
(ii) The functor $R: \catB → \catA$ and for each $A∈\catA$ an object
$L_0A∈\catB$ and a universal arrow $η_A:A→RL_0A$ from $A$ to $R$.
Then the functor $L$ has object function $L_0$ and is defined on
arrows $f:A'→A$ by $RLf∘η_{A'} = η_A∘f$.
\ORIG{(iii) Functors $F$, $G$, and a natural transformation $ε: FG
\tnto I_A$ such that each $ε_a:FGa→a$ is universal from $F$ to
$a$. Here $φ^{-1}$ is defined by (7).}
(iii) Functors $L$, $R$, and a natural transformation $ε:
LR→\id_\catB$ such that each $ε_B:LRB→B$ is universal from $L$ to
$B$. Here $♭$ is defined by (7).
\ORIG{(iv) The functor $F:X→A$ and for each $a∈A$ an object $G_0a∈X$
and an arrow $ε_a:FG_0a→a$ universal from $F$ to $a$.}
(iv) The functor $L:\catA→\catB$ and for each $B∈\catB$ an object
$R_0B∈\catA$ and an arrow $ε_B:LR_0B→B$ universal from $L$ to $B$.
\ORIG{(v) Functors $F$, $G$ and natural transformations $η:I_x \tnto
GF$ and $ε: FG \tnto I_A$ such that both composites (8) are the
identity transformations. Here $φ$ is defined by (6) and $φ^{-1}$
by (7).}
(v) Functors $L$, $R$ and natural transformations $η:\id_\catA→RL$
and $ε:LR→\id_\catB$ such that both composites (8) are the identity
transformations. Here $♯$ is defined by (6) and $♭$ by (7).
\end{quotation}
% My plan for the next incarnation of the course is to ask the students
% to 1) visualize in the big diagram all the objects and constructions
% in the Big Theorem, 2) take the original Theorem 2 in \cite{CWM2} and
% draw the missing diagrams for it, 3) decypher some other parts of the
% section about adjunctions in \cite{CWM2}.
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 79) "IV. Adjoints")
% (find-cwm2page (+ 13 79) "1. Adjunctions")
% (find-cwm2text (+ 13 79) "1. Adjunctions")
% (find-cwm2page (+ 13 83) "Theorem 2.")
% (find-cwm2text (+ 13 83) "Theorem 2.")
\newpage
% _____ __ _ _ _ _
% |_ _| _ _ __ ___ / _| ___ _ __ ___| |__ (_) | __| |_ __ ___ _ __
% | || | | | '_ \/ __| | |_ / _ \| '__| / __| '_ \| | |/ _` | '__/ _ \ '_ \
% | || |_| | |_) \__ \ | _| (_) | | | (__| | | | | | (_| | | | __/ | | |
% |_| \__, | .__/|___/ |_| \___/|_| \___|_| |_|_|_|\__,_|_| \___|_| |_|
% |___/|_|
%
% «types-for-children» (to ".types-for-children")
% (misp 29 "types-for-children")
% (misa "types-for-children")
% Sec: 6
\section{Types for Children}
\label{types-for-children}
% \cite{MartinLofCMCP}
% \cite{SelingerLN}
% \cite{Norell08}
% (find-books "__logic/__logic.el" "martin-lof-cmcp")
We will need a bit of Type Theory in the sections \ref{ness} and
\ref{comma-categories}. We will need some non-standard notational
conventions that appear more or less naturally when we present Theory
Theory ``for children'' in the right way --- let's see the details.
\msk
% (find-books "__cats/__cats.el" "selinger-ln")
% (find-selingerlnpage 51 "6 Simply-typed lambda calculus...")
Section 6 of \cite{SelingerLN} has a very good presentation of types
``for adults'': it uses expressions like $A×B$ and $A→B$ as and treats
them as purely syntactical objects, but each one comes with an
``intended meaning''. Let's start by defining a version ``for
children'' of that in which these intended meanings become more
concrete, and then we will work in the version ``for children'' and in
the version ``for adults'' in parallel.
% «dependent-types» (to ".dependent-types")
% (misp 29 "dependent-types")
% (misa "dependent-types")
% Sec: 6.1
\subsection{Dependent types}
\label{dependent-types}
In our version ``for children'':
\begin{itemize}
\item all types are sets,
\item some sets are types,
\item every finite subset of $\N$ is a type,
\item if $A$ and $B$ are types then $A×B$ and $A→B$ are types. $A×B$
is the space of pairs of the form $(a,b)$ in which $a∈A$ and $b∈B$,
and $A→B$ is the space of functions from $A$ to $B$,
\item $a:A$ means $a∈A$ --- the distinction between `$:$' and `$∈$'
will only appear in other settings,
\item ``space of'' means ``set of''. The space of functions from $A$
to $B$ is the set of all functions from $A$ to $B$, and each
function is considered as a set of input-output pairs. So, for
example, if $A=\{2,3\}$ and $B=\{4,5\}$ then:
%
$$\def\fa#1#2{\csm{(2,#1),\\(3,#2)\,}}
\begin{array}{rcl}
A×B &=& \{(2,4),
(2,5),
(3,4),
(3,5),
\}, \\
A→B &=& \left\{ \fa44, \fa45, \fa54, \fa55
\right\} \\
\end{array}
$$
\item if $A$ is a type and $(C_a)_{a∈A}$ is a family of types indexed
by $A$ then $Πa{:}A.C_a$ and $Σa{:}A.C_a$ are dependent types
defined in the usual way, and $(a{:}A) → C_a$ and $(a{:}A)×C_a$ are
alternate notations for $Πa{:}A.C_a$ and $Σa{:}A.C_a$ (see
\cite[section 2]{Norell08}). Formally,
%
$$\def\aCa{\bigcup_{a∈A}C_a}
\begin{array}{rcl}
Σa{:}A.C_a &=& \setofst{(a,c)∈A × (\aCa) }{a∈A, \; c∈C_a} \\
(a{:}A)×C_a &=& \setofst{(a,c)∈A × (\aCa) }{a∈A, \; c∈C_a} \\
Πa{:}A.C_a &=& \setofst{f:A→(\aCa) }{∀a∈A.\;f(a)∈C_a} \\
(a{:}A)→C_a &=& \setofst{f:A→(\aCa) }{∀a∈A.\;f(a)∈C_a} \\
\end{array}
$$
%
If $A=\{2,3\}$, $C_2=\{6,7\}$, and $C_3=\{7,8\}$ then:
%
$$\def\fa#1#2{\csm{(2,#1),\\(3,#2)\,}}
\begin{array}{rcl}
(a{:}A)×C_a &=& \{(2,6),
(2,7),
(3,7),
(3,8),
\}, \\
(a{:}A)→C &=& \left\{ \fa67, \fa68, \fa77, \fa78
\right\}. \\
\end{array}
$$
\end{itemize}
% «witnesses» (to ".witnesses")
% (misp 29 "witnesses")
% (misa "witnesses")
% Sec: 6.2
\subsection{Witnesses}
\label{witnesses}
If $P$ is a proposition we will write $⟦P⟧$ for its {\sl space of
witnesses}, or its {\sl space of proofs}. The exact definition of
$⟦P⟧$ will usually depend on the context, but we always have $⟦P⟧=∅$
when $P$ is false and $⟦P⟧\neq∅$ when $P$ is true. In some situations
all the witnesses of a proposition $P$ will be identified --- this is
called {\sl proof irrelevance}; see \cite[p.340]{NederpeltGeuvers} ---
and all the spaces of witnesses will be either singletons or empty
sets; in other situations some `$⟦P⟧$'s will have more than one
element.
% (find-books "__logic/__logic.el" "nederpelt-geuvers")
% (find-ttafpaipage (+ 29 340) "14.13 Irrelevance of proof")
The notation $\AProofOf{P}$ will denote a witness that $P$ is true.
Formally, $\AProofOf{P}$ is a variable (with a long name!) whose type
is $\AllProofsOf{P}$. A good way to remember this notation is that
$\AllProofsOf{P}$ looks like a box and $\AProofOf{P}$ looks like
something that comes in that box.
\msk
{
\def\a{\mathsf{a}}
\def\b{\mathsf{b}}
In Agda the operation `$≡$' returns a space of proofs of equality. If
$\a$ and $\b$ are expressions with the same type then Agda's `$\a≡\b$'
corresponds to our $\AllProofsOf{\a=\b}$, and people sometimes use the
name `$\a{≡}\b$' to denote an element of $\a≡\b$ --- we use
$\AProofOf{\a=\b}$ for that. See the section ``Equality'' in
\cite{WadlerPLFA} for simple examples, and Agda's standard library for
more examples.
}
%\standout{TODO:} mention that in Agda we write $a{≡}b : a≡b$. Point to
%\cite{WadlerPLFA}.
% (find-LATEX "catsem-ab.bib" "bib-WadlerPLFA")
% (find-angg ".emacs.agda" "plfa5")
% (find-plfa5page 5 "Chains of equations")
% (find-plfa5text 5 "Chains of equations")
% «judgments» (to ".judgments")
% (misp 30 "judgments")
% (misa "judgments")
% Sec: 6.3
\subsection{Judgments}
% (find-books "__logic/__logic.el" "nederpelt-geuvers")
% (find-ttafpaipage (+ 29 127) "Figure 6.4 Derivation rules")
% (find-ttafpaitext (+ 29 127) "Figure 6.4 Derivation rules")
The main objects of Type Theory are {\sl derivable judgements}. A
derivable judgment is one that can appear as the root node of a
derivation in which each bar is an application of one the rules in
\cite[p.127]{NederpeltGeuvers}. These derivations are usually huge ---
for example, here is a derivation for $A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ$:
%:
%: ----a ----a ----a ----a ----a
%: ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□
%: ----a ----a ----a -----------w_□ -------v_□ -----------w_□
%: ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□ A⠆Θ⊢Θ⠆□ A⠆Θ⊢A⠆Θ A⠆Θ⊢Θ⠆□
%: -----------w_□ -------v_□ -----------------------w_□ -----------v_□
%: A⠆Θ⊢Θ⠆□ A⠆Θ⊢A⠆Θ A⠆Θ,B⠆Θ⊢A⠆Θ A⠆Θ,B⠆Θ⊢B⠆Θ
%: -----------------------w_□ ---------------------------------w_Θ
%: A⠆Θ,B⠆Θ⊢A⠆Θ A⠆Θ,B⠆Θ,a⠆A⊢B⠆Θ
%: --------------------------------------------------Π_{ΘΘΘ}
%: A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ
%:
%: ^depprod1
%:
\pu
$$\resizebox{0.7\textwidth}{!}{$
\ded{depprod1}
$}
$$
%
so rarely draw them explicitly, and we use other tools to show that
certain judgments are derivable.
Every derivable judgment obeys this (taken verbatim from
\cite[p.52]{SelingerLN}):
%
% (find-books "__cats/__cats.el" "selinger-ln")
% (find-selingerlnpage 52 "typing judgment")
% (find-selingerlntext 52 "typing judgment")
%
\begin{quotation}
A typing judgment is an expression of the form
%
$$x_1:A_1, x_2:A_2, \ldots, x_n:A_n ⊢ M:A.$$
Its meaning is: "under the assumption that $x_i$ is of type $A_i$ ,
for $i=1\ldots n$, the term $M$ is a well-typed term of type $A$.'' The
free variables of $M$ must be contained in $x_1, \ldots, x_n$.
\end{quotation}
Understanding what this means in the version ``for children'' will
take us quite close to understanding that in Type Theory ``for
adults''. We will do that in the next section.
Let me just correct a simplification. The main objects of the Type
Theory used in Agda and in most other proof assistants are derivable
judgments {\sl with definitions}, as explained in the chapters 8--10
of \cite{NederpeltGeuvers}. A judgment with definitions is written as
$Δ;Γ⊢M:N$, where $Δ$ is a list of definitions
(\cite[def.9.2.1]{NederpeltGeuvers}); we will mostly ignore the `$Δ$'
here.
% (find-books "__logic/__logic.el" "nederpelt-geuvers")
% (find-books "__logic/__logic.el" "nederpelt-geuvers" "8 Definitions")
% (find-ttafpaipage (+ 29 191) "Definition 9.2.1 (Judgement with definitions; extended judgement)")
% (find-ttafpaitext (+ 29 191) "Definition 9.2.1 (Judgement with definitions; extended judgement)")
% «comprehensions» (to ".comprehensions")
% (misp 31 "comprehensions")
% (misa "comprehensions")
% Sec: 6.4
\subsection{Set comprehensions}
\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\def\ug#1{#1}
\def\uf#1{#1}
\def\ue#1{#1}
\def\uc#1{#1}
\def\UG#1{\und{#1}{generator}}
\def\UF#1{\und{#1}{filter}}
\def\UE#1{\und{#1}{expression}}
\def\UC#1{\und{#1}{context}}
The part at the left of the `$⊢$' in a typing judgment is called a
{\sl typing context}. Typing contexts also appear in set
comprehensions. Let's see an example:
%
$$\begin{array}{rl}
& \setofst {\ue{10a+b}}
{\uc{\ug{a∈\{1,2\}}, \ug{b∈\{2,3\}}, \uf{a<b}}} \\[7.5pt]
\squigto \phantom{mm}
& \setofsc {\UC{\UG{a∈\{1,2\}}, \UG{b∈\{2,3\}}, \UF{a<b}}}
{\UE{10a+b}} \\
\end{array}
$$
\def\acontext{\ang{\textsf{context}}}
\def\aexpr {\ang{\textsf{expr}}}
We rewrote the comprehension $\setofst{ \aexpr }{ \acontext }$ to
$\setofsc{ \acontext }{ \aexpr }$ for clarity, and we marked which
parts of the context act as ``generators'' and which ones act as
``filters''. The context above can be rewritten in type-theoretical
notation as:
%
$$ a : \{1,2\},
\; b : \{2,3\},
\; \AProofOf{a{<}b} : \AllProofsOf{a{<}b}
$$
A {\sl value} for that context is a triple $(a,b,\AProofOf{a{<}b})$,
where $a∈\{1,2\}$, $b∈\{2,3\}$, and $\AProofOf{a{<}b}$ is a guarantee
that $a<b$ is true.
% (find-selingerlnpage 52 "typing judgment")
% (find-selingerlntext 52 "typing judgment")
% (excp 38 "contexts")
% (exca "contexts")
% «omitting-types» (to ".omitting-types")
% (misp 32 "omitting-types")
% (misa "omitting-types")
% Sec: 6.5
\subsection{Omitting types}
\label{omitting-types}
% (misp 16 "freyd-with-functors")
% (misa "freyd-with-functors")
The diagram at the left below is a copy of the one from
sec.\ref{freyd-with-functors}, but now we will interpret it in a
different way, as a ``dictionary of (default) types''. For example, it
says that when the symbol $η$ appears without a type its type will be
the default one given by the diagram: $η:A→RC$, or $η:\catA(A,RC)$.
The default types are listed at the right.
%D diagram universal-arrow-omitting-1
%D 2Dx 100 +25
%D 2D 100 C1
%D 2D |
%D 2D +25 C2 C3
%D 2D | |
%D 2D +25 C4 C5
%D 2D
%D 2D +15 C6 C7
%D 2D
%D ren C1 => A
%D ren C2 C3 => C RC
%D ren C4 C5 => D RD
%D ren C6 C7 => \catB \catA
%D
%D (( C1 C3 -> .plabel= r η
%D C2 C3 |->
%D C2 C4 -> .plabel= l f
%D C3 C5 -> .plabel= r Rf
%D C2 C5 harrownodes nil 20 nil |->
%D C4 C5 |->
%D C1 C5 -> .slide= 20pt .plabel= r g
%D C6 C7 -> .plabel= a R
%D ))
%D enddiagram
%D
$$\pu
\scalebox{1.0}{$
\diag{universal-arrow-omitting-1}
$}
\qquad
\begin{array}{rcl}
\catA &\text{is}& \text{a category} \\
\catB &\text{is}& \text{a category} \\
R &:& \catA → \catB \\
A &∈& \catA \\
C &∈& \catB \\
D &∈& \catB \\
η &:& A→RC \\
f &:& C→D \\
g &:& A→RD \\
\end{array}
$$
% «indefinite-articles» (to ".indefinite-articles")
% (misp 32 "indefinite-articles")
% (misa "indefinite-articles")
\subsection{Indefinite articles}
\label{indefinite-articles}
We will use the diagram above to redefine universalness. In our old
definition, from sec.\ref{freyd-with-functors}, universalness is just a
``property''; in our new definition it will be a pair made of a
``structure'' and a ``property'' (see sec.\ref{ness}).
Suppose that
%
$$\begin{array}{rcl}
\catA &\text{is}& \text{a category}, \\
\catB &\text{is}& \text{a category}, \\
R &:& \catA → \catB, \\
A &∈& \catA, \\
C &∈& \catB, \\
η &:& A→RC, \\
\end{array}
$$
%
and let $♯$ be this operation:
%
$$♯ \;\;=\;\; λD.λf.\;Rf∘η.
$$
\def\asharpis{\AProofOf {♭ = ♯^{-1}}}
\def\psharpis{ (♭ = ♯^{-1})}
\def\Ssharpis{\AllProofsOf{♭ = ♯^{-1}}}
Note that the types of $D$ and $f$ are given by the diagram: $D$ is an
object of $\catB$, and $f:C→D$. Then ``universalness'' for the tuple
$(\catA,\catB,R,A,C,η)$ is a pair $(♭,\asharpis)$, in which $♭$ is an
operation ``that for each $D$ takes each $g$ to an $f$'' and
$\psharpis$ is a shorthand for this proposition:
%
$$\begin{array}{rl}
(∀D.∀f.\; ♭\,D\,(♯\,D\,f) = f)\, & ∧ \\
(∀D.∀g.\; ♯\,D\,(♭\,D\,g) = g).
\end{array}
$$
%
The component $\asharpis$ of the universalness is a witness that
guarantess that this proposition holds.
The types of $♭$ and $\asharpis$ are:
%
$$\begin{array}{rcl}
♭ &:& (D : \Objs_\catB) → (\catA(A,RD) → \catB(C,D)) \\[2.5pt]
\asharpis &:& ⟦ \; (∀D.∀f.\; ♭\,D\,(♯\,D\,f) = f) \;\; ∧ \\
&& \phantom{m} (∀D.∀g.\; ♯\,D\,(♭\,D\,g) = g) \; ⟧
\end{array}
$$
We can use a trick with indefinite articles to obtain the type of $♭$.
Let's overload the notations $\AllProofsOf{·}$ and $\AProofOf{·}$:
with their new meanings `$\AllProofsOf{α}$' will be pronounced ``the
type of $α$'', and `$\AProofOf{α}$' will be ``an $α$'', ``an object
with the same type of $α$'', or ``an element of $\AllProofsOf{α}$''.
Then
%
\begin{quote}
$♭$ is an operation that for each $D$ takes each $g$ to an $f$
\end{quote}
%
becomes:
%
$$♭ \;\;=\;\; λD.λg.\AProofOf{f}
$$
The indefinite article in this $\AProofOf{f}$ is contagious: we read
the equality above not as ``$♭$ is {\sl the} operation that takes each
$D$...'' but as ``$♭$ is {\sl an} operation that...''. We don't know
the value of $λD.λg.\AProofOf{f}$ but we can calculate its type:
%
$$\begin{array}{rcl}
f &:& C→D \\
\AllProofsOf{f} &=& \catB(C,D) \\
\AProofOf {f} &:& \catB(C,D) \\
g &:& A→RD \\
\AllProofsOf{g} &=& \catA(A,RD) \\
D &:& \Objs_\catB \\
\AllProofsOf{λD.λg.\AProofOf{f}} &=& \Objs_\catB → (\catA(A,RD) → \catB(C,D)) \\
\end{array}
$$
We will see how to represent universalness in diagrams in
sec.\ref{ness}.
% Let $♯ = λD.λf.Rf∘η$.
% Let $♭ = λD.λg.\angg{f}$.
% Then $⟦♭⟧ = \ldots$.
% $(♭=♯^{-1}) = (∀D.∀f.♭D(♯Df)=f)∧(∀D.∀g.♯D(♭Dg=g))$
% (misp 16 "freyd-with-functors")
% (misa "freyd-with-functors")
% \subsection{Quantifiers}
% % (find-ttafpaipage (+ 29 112) "V. Universal quantification")
% % (find-ttafpaitext (+ 29 112) "V. Universal quantification")
% In Type Theory we define
% %
% $$\begin{array}{rcl}
% \AllProofsOf{∀a{:}A.P(a)} &:=& (a:A)→\AllProofsOf{P(a)}, \\
% \AllProofsOf{∃a{:}A.P(a)} &:=& (a:A)×\AllProofsOf{P(a)}. \\
% \end{array}
% $$
% %
% For example, $A=\{2,3,5\}$ and $P(a)=(a<4)$ then every element of
% $(a:A)→⟦P(a)⟧$ is of the form:
% %
% $$\{(2,\AProofOf{2{<}4}),
% (3,\AProofOf{3{<}4}),
% (5,\AProofOf{5{<}4})
% \}
% $$
% %
% but $\AllProofsOf{5<4}=∅$, so $\AProofOf{5{<}4}$ is a variable ranging
% over an empty set; so there are no possible values for
% $\AProofOf{5<4}$, there are no elements of this form above, and
% $(a:A)→⟦P(a)⟧=∅$. This is standard; see
% \cite[p.112]{NederpeltGeuvers}. What is non-standard here is that we
% are using variables, like $\AProofOf{5<4}$, whose types can be
% inferred from their names. In cases like these it makes sense to use
% indefinite articles: ``a $\AProofOf{2<4}$'' means ``an element of
% $\AllProofsOf{2<4}$''.
% (find-LATEX "catsem-u.bib" "bib-HOTT")
% (find-books "__logic/__logic.el" "hott")
% (find-hottpage (+ 12 18) "a witness to the provability of A")
% (find-hotttext (+ 12 18) "a witness to the provability of A")
% \subsection{Underbrace diagrams}
% In diagrams with underbraces like the ones below at the left each
% underbrace corresponds to an assertion about the subexpression above
% it. The corresponding assertions are listed at the right.
% \sa{und1} {\und{ (a:\und{A}{a:}) → \und{C_a}{f(a):} }{f:}}
% \sa{und1:s}{
% \begin{array}[t]{rcl}
% a &:& A \\
% f(a) &:& C_a \\
% f &:& (a:A)→C_a \\
% \end{array}
% }
% \sa{und2} {\und{f}{:(a:A)→C_a}(\und{a}{:A})}
% \sa{und2:s}{
% \begin{array}[t]{rcl}
% a &:& A \\
% f(a) &:& C_a \\
% f &:& (a:A)→C_a \\
% \end{array}
% }
% $$\def\und#1#2{\underbrace{#1}_{#2}}
% \begin{array}{rcl}
% \ga{und1} &\phantom{mmm} & \ga{und1:s} \\[50pt]
% \ga{und2} &\phantom{mmm} & \ga{und2:s} \\
% \end{array}
% $$
% «phys-not» (to ".phys-not")
\subsection{``Physicists' notation''}
Books like \cite{ThompsonGardner} use a notation in which expressions
like ``$z=z(x,y(x))$'' are allowed --- the same symbol can be used
both as a (dependent!) variable and as the name of a function, and
arguments can be omitted --- and in a context in which $y=y(x)$ the
default meaning for $y_0$ is $y(x_0)$. In many areas of Mathematics
that notation has been phased out (see \cite[sec.3.3]{DSLsofMath}) and
replaced by one in which the names of the bound variables matter very
little.
Let's call the older notation ``physicist's notation'' and the newer
one ``mathematician's notation''; these names are not standard at all.
If we apply the ideas of the ``physicist's notation'' to judgments we
can abbreviate
%
$$a:A, b:B(a), c:C(a,b) ⊢ d(a,b,c):D(a,b,c)
$$
%
to just $a:A, b:B, c:C ⊢ d:D$, or even to $a,b,c⊢d$. Some of the
conventions of DL were inspired by conventions from ``physicist's
notation''.
% \standout{TODO:} rewrite this. This idea may be useful to write
% pseudocode for Agda. Cite lifting.
% \subsection{Witnesses}
% In the beginning `$:$' will be a synonym for `$∈$' --- they will be
% made distinct later --- and our ``basic'' types will be finite subsets
% of $\N$, like $\{0,1,2\}$, $\{42,99\}$, and $\{\}$. We will see some
% ways to build ``new'' types from ``old'' types, but we will not define
% which sets are types and which ones are not.
% For each two types $A$ and $B$ we can form the types $A×B$ and $A→B$
% in the obvious way: the elements of $A×B$ are pairs of the form
% $(a,b)$, where $a:A$ and $b:B$, and the elements of $A→B$ are the
% functions $f:A→B$, where each function is represented as a set of
% input-output pairs. So, for example,
% %
% All the books on Type Theory that I know present TT in a very abstract
% way; here we will use some ideas of the sections
% \ref{missing-diagrams} and \ref{the-conventions} to see how TT ``for
% children'' and TT ``for adults'' can be taught in parallel.
% When people learn complex numbers, or fields, they start with
% naturals, then integers, then rationals, then reals, and only then
% complex numbers, fields, and algebraically closed fields. At each
% level we know some operations on, and properties of, our ``numbers'',
% and we want most of them to also hold on the ``numbers'' of the level.
% Here we will start by understanding the basic operations of TT on
% certain simple particular cases (...) and we will use the convention
% (CPSh) of sec.\ref{the-conventions} to draw these particular cases and
% the corresponding general cases in parallel.
% (excp 26 "types-after-discrete")
% (exca "types-after-discrete")
% \GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
% \end{document}
\newpage
% ____ _ _____ _ _
% | __ ) __ _ ___(_) ___ | ____|_ __ ___| | _____| |
% | _ \ / _` / __| |/ __| | _| \ \/ / / __| |/ / _ \ |
% | |_) | (_| \__ \ | (__ | |___ > < \__ \ < __/ |
% |____/ \__,_|___/_|\___| |_____/_/\_\ |___/_|\_\___|_|
%
% «basic-example-as-skel» (to ".basic-example-as-skel")
% (misp 36 "basic-example-as-skel")
% (misa "basic-example-as-skel")
% sec: 7
% Orig: (favp 29 "basic-example-as-skel")
% (fava "basic-example-as-skel")
% sec: 6
%
\section{The Basic Example as a skeleton \DONE}
\label{basic-example-as-skel}
In the sections \ref{the-conventions} and \ref{to-deserve-a-name} I
claimed that the diagram of the Basic Example is a ``skeleton'' of a
certain theorem, in the sense that both the statement and the proof of
that theorem can be reconstructed from just the diagram and very few
extra hints. Let's see the details of this.
% ____ _ _____ __ _
% | __ ) __ _ ___(_) ___ | ____|_ __ / _|_ _ _ __ ___| |_
% | _ \ / _` / __| |/ __| | _| \ \/ / | |_| | | | '_ \ / __| __|
% | |_) | (_| \__ \ | (__ | |___ > < | _| |_| | | | | (__| |_
% |____/ \__,_|___/_|\___| |_____/_/\_\ |_| \__,_|_| |_|\___|\__|
%
% «basic-example-functors» (to ".basic-example-functors")
% Orig: (favp 29 "basic-example-functors")
% (fava "basic-example-functors")
% sec: 6.1
%
\subsection{Reconstructing its functors \DONE}
\label{basic-example-functors}
Let's call this diagram --- the diagram of the Basic Example ---
$\Yzero$:
%
$$\Yzero \qquad := \quad \diag{Basic-Example}$$
We don't know yet the precise meaning of the functors $\catB(C,-)$ and
$\catA(A,R-)$, but if we enlarge $\Yzero$ to this --- note that we are
omitting the curved bijection by convenience,
%
%D diagram Basic-Example-plus
%D 2Dx 100 +40
%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 ==> A
%D ren A2 A3 ==> C RC
%D ren A4 A5 ==> D RD
%D ren A6 A7 ==> E RE
%D ren B0 B1 ==> \catB \catA
%D ren C0 C1 C2 ==> \catB(C,-) \catA(A,R-) ?
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D A2 A4 -> .plabel= l f
%D A3 A5 -> .plabel= r Rf
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D A4 A6 -> .plabel= l g
%D A5 A7 -> .plabel= r Rg
%D A4 A7 harrownodes nil 20 nil |->
%D A6 A7 |->
%D A1 A5 -> .slide= 20pt .plabel= r h
%D
%D B0 B1 -> .plabel= a R
%D
%D C0 C1 -> .plabel= a α
%D # C0 C2 -> .plabel= l \sm{ψ\\\text{(iso)}}
%D # C1 C2 <->
%D
%D # C0 C1 midpoint A1 A3 midpoint <-> .curve= ^15pt
%D ))
%D enddiagram
%
$$\pu
\Yzeroplus \qquad := \quad \slowdiag{Basic-Example-plus}
$$
%
and we draw the internal views of $\catB(C,-)$ and $\catA(A,R-)$, then
the meanings for $\catB(C,-)$ and $\catA(A,R-)$ become obvious:
%
%D diagram basic-example-obvious-functors
%D 2Dx 100 +30 +25 +30 +35 +35
%D 2D 100 A0 - A1 C0 D0 - D1 F0
%D 2D | | | | | |
%D 2D +20 A2 - A3 C1 D2 - D3 F1
%D 2D
%D 2D +15 B0 - B1 E0 - E1
%D 2D
%D ren A0 A1 C0 ==> D \catB(C,D) f
%D ren A2 A3 C1 ==> E \catB(C,E) g∘f
%D ren B0 B1 ==> \catB \Set
%D ren D0 D1 F0 ==> D \catA(A,RD) h
%D ren D2 D3 F1 ==> E \catA(A,RE) Rg∘h
%D ren E0 E1 ==> \catB \Set
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l g
%D A1 A3 -> .plabel= r \catB(C,g)
%D A2 A3 |->
%D B0 B1 -> .plabel= a \catB(C,-)
%D C0 C1 |->
%D
%D D0 D1 |->
%D D0 D2 -> .plabel= l g
%D D1 D3 -> .plabel= r \catA(A,Rg)
%D D2 D3 |->
%D E0 E1 -> .plabel= a \catA(A,R-)
%D F0 F1 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{basic-example-obvious-functors}
$$
So:
%
$$\begin{array}{rcl}
\catB(C,-) &:& \catB → \Set \\
\catB(C,-)_0 &:=& λD.\catB(C,D) \\
\catB(C,-)_1 &:=& λg.λf.g∘f \\
[5pt]
\catA(A,R-) &:& \catB → \Set \\
\catA(A,R-)_0 &:=& λD.\catA(A,RD) \\
\catA(A,R-)_1 &:=& λg.λh.Rg∘h \\
\end{array}
$$
% ____ _ _____ _ ___ __ __ _____
% | __ ) __ _ ___(_) ___ | ____|_ __ | \ | \ \ / / \ \ / / _ \
% | _ \ / _` / __| |/ __| | _| \ \/ / | \| |\ V / \ V / | | |
% | |_) | (_| \__ \ | (__ | |___ > < | |\ | | | | || |_| |
% |____/ \__,_|___/_|\___| |_____/_/\_\ |_| \_| |_| |_| \___/
%
% «basic-example-NTs» (to ".basic-example-NTs")
% (misp 37 "basic-example-NTs")
% (misa "basic-example-NTs")
\subsection{Natural transformations}
\label{basic-example-NTs}
% (mdyp 3 "Y72+l")
% (mdya "Y72+l")
%
%D diagram Y72+l
%D 2Dx 100 +40
%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 ren A1 ==> \ga{A1}
%D ren A2 A3 ==> \ga{A2} \ga{A3}
%D ren A4 A5 ==> \ga{A4} \ga{A5}
%D ren A6 A7 ==> \ga{A6} \ga{A7}
%D ren B0 B1 ==> \ga{B0} \ga{B1}
%D ren C0 C1 ==> \ga{C0} \ga{C1}
%D
%D (( A1 A3 -> .plabel= r \ga{A13}
%D A2 A3 |->
%D A2 A4 -> .plabel= l \ga{A24}
%D A3 A5 -> .plabel= r \ga{A35}
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D A4 A6 -> .plabel= l \ga{A46}
%D A5 A7 -> .plabel= r \ga{A57}
%D A4 A7 harrownodes nil 20 nil |->
%D A6 A7 |->
%D
%D A1 A5 -> .slide= 20pt .plabel= r \ga{A15}
%D
%D B0 B1 -> .plabel= a \ga{B01}
%D
%D C0 C1 -> .plabel= a \ga{C01}
%D ))
%D enddiagram
\pu
%D diagram Y72+klm
%D 2Dx 100 +40
%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 ren A1 ==> \ga{A1}
%D ren A2 A3 ==> \ga{A2} \ga{A3}
%D ren A4 A5 ==> \ga{A4} \ga{A5}
%D ren A6 A7 ==> \ga{A6} \ga{A7}
%D ren B0 B1 ==> \ga{B0} \ga{B1}
%D ren C0 C1 ==> \ga{C0} \ga{C1}
%D
%D (( A1 A3 -> .plabel= r \ga{A13}
%D A2 A3 |->
%D A2 A4 -> .plabel= l \ga{A24}
%D A3 A5 -> .plabel= r \ga{A35}
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D A4 A6 -> .plabel= l \ga{A46}
%D A5 A7 -> .plabel= r \ga{A57}
%D A4 A7 harrownodes nil 20 nil |->
%D A6 A7 |->
%D
%D A2 A6 -> .slide= -25pt .plabel= l \ga{A26}
%D A1 A5 -> .slide= 20pt .plabel= r \ga{A15}
%D A1 A7 -> .slide= 60pt .plabel= r \ga{A17}
%D
%D B0 B1 -> .plabel= a \ga{B01}
%D
%D C0 C1 -> .plabel= a \ga{C01}
%D ))
%D enddiagram
\pu
\sa{Y72+l-basicnames}{{
\sa{A1}{A}
\sa{A2}{C} \sa{A3}{RC}
\sa{A4}{D} \sa{A5}{RD}
\sa{A6}{E} \sa{A7}{RE}
\sa{B0}{\catB} \sa{B1}{\catA}
\sa{C0}{\catB(C,-)} \sa{C1}{\catA(A,R-)}
\sa{A13}{η}
\sa{A24}{f} \sa{A35}{Rf}
\sa{A46}{g} \sa{A57}{Rg}
%
\sa{A15}{\sm{ℓ,\\αDf}}
%
\sa{B01}{R}
\sa{C01}{α}
%
\diag{Y72+l}
}}
\sa{Y72+klm-idC}{{
\sa{A1}{A}
\sa{A2}{C} \sa{A3}{RC}
\sa{A4}{C} \sa{A5}{RC}
\sa{A6}{D} \sa{A7}{RD}
\sa{B0}{\catB} \sa{B1}{\catA}
\sa{C0}{\catB(C,-)} \sa{C1}{\catA(A,R-)}
\sa{A13}{η}
\sa{A24}{\sm{ι,\\\id_C}} \sa{A35}{Rι}
\sa{A46}{f} \sa{A57}{Rf}
%
\sa{A26}{\sm{f∘ι,\\f∘\id_C,\\f}}
\sa{A15}{\sm{m,\\αCι,\\αC\id_C}}
\sa{A17}{\sm{Rf∘(αCι),\\αD(f∘ι),\\Rf∘(αC\id_C),\\αDf}}
%
\sa{B01}{R}
\sa{C01}{α}
%
\diag{Y72+klm}
}}
% Debug the diagrams above with:
%$$\ga{Y72+l-basicnames}
% \qquad
% \ga{Y72+klm-idC}
%$$
% (mdyp 3 "sqcond-inner")
% (mdya "sqcond-inner")
%
%D diagram Y0-NT-sqcond-inner
%D 2Dx 100 +30 +40 +35 +40 +35
%D 2D 100 A0 B0 -> B1 D0 -> D1 E1
%D 2D | | | | | |
%D 2D +17 v v v v D3' E3'
%D 2D +8 A1 B2 -> B3 D2 -> D3
%D 2D
%D 2D +15 C0 -> C1
%D 2D
%D ren A0 B0 B1 D0 D1 ==> \ga{A0} \ga{B0} \ga{B1} \ga{D0} \ga{D1}
%D ren A1 B2 B3 D2 D3 ==> \ga{A1} \ga{B2} \ga{B3} \ga{D2} \ga{D3}
%D ren D3' E1 E3' C0 C1 ==> \ga{D3'} \ga{E1} \ga{E3'} \ga{C0} \ga{C1}
%D
%D (( A0 A1 -> .plabel= l \ga{A01}
%D B0 B1 -> .plabel= a \ga{B01}
%D B0 B2 -> .plabel= l \ga{B02}
%D B1 B3 -> .plabel= r \ga{B13}
%D B2 B3 -> .plabel= a \ga{B23}
%D C0 C1 -> .plabel= a \ga{C01}
%D D0 D1 |->
%D D1 D3' |->
%D D0 D2 |->
%D D2 D3 |->
%D E1 E3' |->
%D ))
%D enddiagram
%D
\pu
\sa{Y0-NT-sqcond-alpha}{{
\sa{A0}{D} \sa{B0}{\catB(C,D)} \sa{B1}{\catA(A,RD)}
\sa{A1}{E} \sa{B2}{\catB(C,E)} \sa{B3}{\catA(A,RE)}
\sa{C0}{\catB(C,-)} \sa{C1}{\catA(A,R-)}
\sa{D0}{f} \sa{D1}{αDf} \sa{E1}{ℓ}
\sa{D3'}{Rg∘(αDf)} \sa{E3'}{Rg∘ℓ}
\sa{D2}{g∘f} \sa{D3}{αE(g∘f)}
\sa{A01}{g}
\sa{B01}{} \sa{B02}{} \sa{B13}{} \sa{B23}{}
\sa{C01}{α}
\diag{Y0-NT-sqcond-inner}
}}
\sa{Y0-NT-sqcond-eta}{{
\sa{A0}{D} \sa{B0}{\catB(C,D)} \sa{B1}{\catA(A,RD)}
\sa{A1}{E} \sa{B2}{\catB(C,E)} \sa{B3}{\catA(A,RE)}
\sa{C0}{\catB(C,-)} \sa{C1}{\catA(A,R-)}
\sa{D0}{f} \sa{D1}{Rf∘η} \sa{E1}{ℓ}
\sa{D3'}{Rg∘(Rf∘η)} \sa{E3'}{Rg∘ℓ}
\sa{D2}{g∘f} \sa{D3}{R(g∘f)∘η}
\sa{A01}{g}
\sa{B01}{} \sa{B02}{} \sa{B13}{} \sa{B23}{}
\sa{C01}{α_η}
\diag{Y0-NT-sqcond-inner}
}}
\sa{Y0-NT-sqcond-idC-iota}{{
\sa{A0}{C} \sa{B0}{\catB(C,C)} \sa{B1}{\catA(A,RC)}
\sa{A1}{D} \sa{B2}{\catB(C,D)} \sa{B3}{\catA(A,RD)}
\sa{C0}{\catB(C,-)} \sa{C1}{\catA(A,R-)}
\sa{D0}{ι} \sa{D1}{αCι} \sa{E1}{m}
\sa{D3'}{Rf∘(αCι)} \sa{E3'}{Rf∘m}
\sa{D2}{f∘ι} \sa{D3}{αD(f∘ι)}
\sa{A01}{f}
\sa{B01}{} \sa{B02}{} \sa{B13}{} \sa{B23}{}
\sa{C01}{α}
\diag{Y0-NT-sqcond-inner}
}}
\sa{Y0-NT-sqcond-idC-id}{{
\sa{A0}{C} \sa{B0}{\catB(C,C)} \sa{B1}{\catA(A,RC)}
\sa{A1}{D} \sa{B2}{\catB(C,D)} \sa{B3}{\catA(A,RD)}
\sa{C0}{\catB(C,-)} \sa{C1}{\catA(A,R-)}
\sa{D0}{\id_C} \sa{D1}{αC\id_C} \sa{E1}{m}
\sa{D3'}{Rf∘(αC\id_C)} \sa{E3'}{Rf∘m}
\sa{D2}{f} \sa{D3}{αDf}
\sa{A01}{f}
\sa{B01}{} \sa{B02}{} \sa{B13}{} \sa{B23}{}
\sa{C01}{α}
\diag{Y0-NT-sqcond-inner}
}}
% Debug the diagrams above with:
%$$\scalebox{0.8}{$
% \begin{array}{c}
% \ga{Y72+l-basicnames}
% \qquad
% \ga{Y72+klm-idC}
% \\ \\
% \ga{Y0-NT-sqcond-alpha}
% \\ \\
% \ga{Y0-NT-sqcond-eta}
% \\ \\
% \ga{Y0-NT-sqcond-idC-iota}
% \\ \\
% \ga{Y0-NT-sqcond-idC-id}
% \end{array}
% $}
%$$
In sec.\ref{internal-view-NT} we saw that a natural transformation is
a pair. An NT $α:\catB(C,-)→\catA(A,R-)$ is a pair $(α_0, \sqcond_α)$,
where $\sqcond_α$ is this:
%
$$\begin{array}{rcl}
\sqcond_α &=& ∀D.∀E.∀g.∀f.\; (\catA(A,Rf)∘αD) = (αE∘\catB(C,f)) \\
&=& ∀D.∀E.∀g.∀f.\; (Rg∘(αDf)) = (αE(g∘f)) \\
&=& ∀D.∀E.∀g.∀f.\; (Rg∘(α_0Df)) = (α_0E(g∘f)) \\
\end{array}
$$
We can visualize what this ``means'' using the two diagrams at the top
in the next page.
\msk
Suppose that we define a natural transformation $α_η$ by saying that
$(α_η)_0 = λD.λf.Rf∘η$. Then we can either affirm that $\sqcond_{α_η}$
``is obvious'' or verify that it holds. Substituing $α_0$ by
$λD.λf.Rf∘η$ we obtain:
%
$$\begin{array}{rcl}
\sqcond_{α_η} &=& ∀D.∀E.∀g.∀f.\; (Rg∘(Rf∘η)) = (R(g∘f)∘η) \\
\end{array}
$$
%
which is clearly true, so $\sqcond_{α_η}$ holds, and $α_η$ is a
natural transformation for every $η:A→RC$. We can define an operation
$(η→α)$ by:
%
$$\begin{array}{rcl}
(η↦α) &:=& λη.((α_η)_0, \sqcond_{α_η}) \\
\end{array}
$$
Without abbreviations this definition would be very big. The lower
third of the diagram in the next page shows how visualize what
$\sqcond_{α_η}$ means.
\newpage
$$\scalebox{1.0}{$
\begin{array}{l}
\phantom{mmmm}
\ga{Y72+l-basicnames}
\\ \\ \\ \\
\ga{Y0-NT-sqcond-alpha}
\\ \\ \\
\ga{Y0-NT-sqcond-eta}
\end{array}
$}
$$
\newpage
We can define an operation $(α↦η)$ by:
%
$$\begin{array}{lcl}
(α↦η) &:=& λα.\, α_0 \, C \, \id_C, \\
(η↦α_0) &:=& λη.λD.λf.\,Rf∘η, \\
(η↦α) &:=& λη.((η↦α_0)(η), \; \sqcond_{\text{(something)}}). \\
\end{array}
$$
We can prove that the operations $(η↦α)$ and $(α↦η)$ are mutually
inverse, but this is tricky. The proof contains a step that is hard to
visualize, and that is often stated as a slogan, like this (from
\cite[p.97]{Leinster} and \cite[p.61]{CWM2}):
%
% (find-books "__cats/__cats.el" "leinster-basic")
% (find-leinsterbasicpage (+ 8 97) "is determinded by its value at 1_A")
% (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).")
%
\begin{quote}
A natural transformation $α:\catB(C,-)→\catA(A,R-)$ \\
is determined by its value at $\id_C$.
\end{quote}
The proof of that step requires instantiating $\sqcond_α$, i.e.,
%
$$\begin{array}{c}
∀D.∀E.∀g:D→E.\;∀f:C→D.\; (Rg∘(α_0Df)) = (α_0E(g∘f)) \\
\end{array}
$$
%
at $D:=C$, $E:=D$, $g:=f$, and $f:=\id_C$. If we do this in two
sub-steps --- first $D:=C$ and $E:=D$, and then $g:=f$ and
$f:=\id_C$ --- we see that after the first sub-step we get this:
%
$$\begin{array}{c}
∀g:C→D.\;∀f:C→C.\; (Rg∘(α_0Cf)) = (α_0D(g∘f)) \\
\end{array}
$$
The variables $g$ and $f$ have sort of changed their types, and some
people (like me!) would prefer to rename them, to, say:
%
$$\begin{array}{c}
∀f:C→D.\;∀ι:C→C.\; (Rf∘(α_0Cι)) = (α_0D(f∘ι)) \\
\end{array}
$$
The diagrams in the next page show the renamed version.
To prove that our operations $(α↦η)$ and $(η↦α)$ are mutually inverse
we need to prove that the round trips $(α↦η↦α)$ and $(η↦α↦η)$ are both
identities. To prove that $(α↦η↦α)=\id$, let's define
$η_α := (α→η)(α)$ and $α_{η_α} := (η↦α)(η_α)$ and . The proof of
$(α↦η↦α)=\id$ includes this sequence of equalities:
%
$$\begin{array}{rcl}
(α_{η_α})_0 D f &=& (η↦α_0) ((α↦η) (α)) D f \\
&=& (η↦α_0) (α C \id_C) D f \\
&=& (λη.λD.λf.\;Rf∘η) (α C \id_C) D f \\
&=& (λD.λf.\;Rf∘(α C \id_C)) D f \\
&=& Rf∘(α C \id_C) \\
&=& αDf \\
\end{array}
$$
%
that uses our hard step in its last equality. The details, including
the proof of $(η↦α↦η)=\id$, can be found in \cite{MissingAgda}.
$$\scalebox{1.0}{$
\begin{array}{l}
\phantom{i.}
\ga{Y72+klm-idC}
\\ \\
\ga{Y0-NT-sqcond-idC-iota}
\\ \\
\ga{Y0-NT-sqcond-idC-id}
\end{array}
$}
$$
% ____ _ _____ _ _ _____
% | __ ) __ _ ___(_) ___ | ____|_ __ | \ | |_ _|
% | _ \ / _` / __| |/ __| | _| \ \/ / | \| | | |
% | |_) | (_| \__ \ | (__ | |___ > < | |\ | | |
% |____/ \__,_|___/_|\___| |_____/_/\_\ |_| \_| |_|
%
% «basic-example-NT» (to ".basic-example-NT")
% Orig: (favp 27 "basic-example-NT")
% (fava "basic-example-NT")
% sec: 30
%
%\subsection{Reconstructing its natural transformation \DONE}
%\label{basic-example-NT}
%
%We also don't know --- yet --- what is the natural transformation
%%
%$$\catB(C,-) \ton{T} \catA(A,R-).$$
%%
%Its internal view is this:
%%
%%D diagram basic-example-obvious-NT
%%D 2Dx 100 +25 +40 +30 +25
%%D 2D 100 A0 B0 B1 D0 D1
%%D 2D
%%D 2D +25 A1 B2 B3 D2 D3
%%D 2D
%%D 2D +15 C0 C1
%%D 2D
%%D ren A0 B0 B1 D0 D1 ==> D \catB(C,D) \catA(A,RD) f h
%%D ren A1 B2 B3 D2 D3 ==> E \catB(C,E) \catA(A,RE) g∘f Rg∘h
%%D ren C0 C1 ==> \catB(C,-) \catA(A,R-)
%%D
%%D (( A0 A1 -> .plabel= l g
%%D B0 B1 -> .plabel= a TD
%%D B0 B2 -> .plabel= l \catB(C,g)
%%D B1 B3 -> .plabel= r \catA(A,Rg)
%%D B2 B3 -> .plabel= a TE
%%D C0 C1 -> .plabel= a T
%%D D0 D2 |->
%%D D1 D3 |->
%%D ))
%%D enddiagram
%%D
%$$\pu
% \diag{basic-example-obvious-NT}
%$$
%%
%Note that we only drew the vertical arrows of the internal view of the internal view.
%
%\standout{We only have this arrow sometimes!}
%
%If we have an arrow $η:A→RC$ then we have a natural construction for
%$T_0$: $TD(f):=Rf∘η$, and we can redraw the internal view of the
%internal view as:
%%
%%D diagram basic-example-obvious-NT-2
%%D 2Dx 100 +40 +35
%%D 2D 100 D0 D1 E0
%%D 2D
%%D 2D +17 D3' E1
%%D 2D +8 D2 D3
%%D 2D
%%D ren D0 D1 E0 ==> f Rf∘η h
%%D ren D3' E1 ==> Rg∘(Rf∘η) Rg∘h
%%D ren D2 D3 ==> g∘f R(g∘f)∘η
%%D
%%D (( D0 D1 |->
%%D D0 D2 |->
%%D D1 D3' |->
%%D D2 D3 |->
%%D E0 E1 |->
%%D ))
%%D enddiagram
%%D
%$$\pu
% \diag{basic-example-obvious-NT-2}
%$$
%%
%The square condition clearly holds, because:
%%
%$$\begin{array}{rcl}
% Rg∘(Rf∘η) &=& (Rg∘Rf)∘η \\
% &=& R(g∘f)∘η. \\
% \end{array}
%$$
%
%So
%%
%$$\begin{array}{rcl}
% T_0 &:=& λD.λf.Rf∘η. \\
% \end{array}
%$$
%
%\standout{So what?}
%
%\standout{Should I draw the bigger diagram?}
%
%
%
%% ____ _ _____ _ _ _
%% | __ ) __ _ ___(_) ___ | ____|_ __ | |__ (_)(_)
%% | _ \ / _` / __| |/ __| | _| \ \/ / | '_ \| || |
%% | |_) | (_| \__ \ | (__ | |___ > < | |_) | || |
%% |____/ \__,_|___/_|\___| |_____/_/\_\ |_.__/|_|/ |
%% |__/
%%
%% «basic-example-bij» (to ".basic-example-bij")
%% Orig: (favp 31 "basic-example-bij")
%% (fava "basic-example-bij")
%% sec: 6.3
%%
%\subsection{Reconstructing its bijection \DONE}
%\label{basic-example-bij}
%
%We can give names like `$d$' and `$u$' for the two components of the
%curved bijection, like this:
%%
%%D diagram basic-example-bij-1
%%D 2Dx 100 +55 +10 +25 +12 +25 +10
%%D 2D 100 A0 B0 B1 C0 C1 D0 D1
%%D 2D
%%D 2D +20 A1 B2 B3 C2 C3 D2 D3
%%D 2D
%%D ren A0 A1 ==> \Hom(A,RC) \Hom(\catB(C,-),\catA(A,R-))
%%D ren B0 B1 C0 C1 D0 D1 ==> η η η u(T) η η_T
%%D ren B2 B3 C2 C3 D2 D3 ==> T T d(η) T T_η T
%%D
%%D (( A0 A1 -> sl_ .plabel= l d
%%D A0 A1 <- sl^ .plabel= r u
%%D B0 B2 |->
%%D B1 B3 <-|
%%D C0 C2 |->
%%D C1 C3 <-|
%%D D0 D2 |->
%%D D1 D3 <-|
%%D ))
%%D enddiagram
%%D
%$$\pu
% \diag{basic-example-bij-1}
%$$
%%
%but the notation at the right will be clearer.
%
%We just saw how the direction `$d$' of the bijection works:
%%
%$$\begin{array}{rcl}
% (T_η)_0 &:=& λD.λf.Rf∘η. \\
% \end{array}
%$$
%
%Here's how to find a natural construction for $u$. Suppose that we
%have a natural transformation $T$. Then $TC(\id_C)$ is an element of
%$\catA(A,RC)$:
%%
%%D diagram basic-example-bij-2
%%D 2Dx 100 +25 +40 +30 +30
%%D 2D 100 A0 B0 B1 D0 D1
%%D 2D
%%D 2D 100 A1 B2 B3 D2 D3
%%D 2D
%%D 2D +15 C0 C1
%%D 2D
%%D ren A1 B2 B3 D2 D3 ==> C \catB(C,C) \catA(A,RC) \id_C TC(\id_C)
%%D ren C0 C1 ==> \catB(C,-) \catA(A,R-)
%%D
%%D (( A1 place
%%D B2 B3 -> .plabel= a TC
%%D C0 C1 -> .plabel= a T
%%D D2 D3 |->
%%D ))
%%D enddiagram
%%D
%$$\pu
% \diag{basic-example-bij-2}
%$$
%
%We can define:
%%
%$$\begin{array}{rcl}
% η_T &:=& TC(\id_C). \\
% \end{array}
%$$
%
%Now we need to check that $d$ and $u$ are mutually inverse, or, in the
%other notation, that the round trips $η \mapsto T_η \mapsto η_{(T_η)}$
%and $T \mapsto η_T \mapsto T_{(η_T)}$ are identity maps. Here is a
%good way to draw the round trips:
%%
%%D diagram basic-example-bij-3
%%D 2Dx 100 +10 +30 +10
%%D 2D 100 A0 A1 B0 B1
%%D 2D | ^ | ^
%%D 2D v | v |
%%D 2D +20 A2 A3 B2 B3
%%D 2D
%%D ren A0 A1 B0 B1 ==> η η_{(T_η)} η_T η_T
%%D ren A2 A3 B2 B3 ==> T_η T_η T_{(η_T)} T
%%D
%%D (( A0 A2 |-> A1 A3 <-|
%%D B0 B2 |-> B1 B3 <-|
%%D ))
%%D enddiagram
%%D
%$$\pu
% \diag{basic-example-bij-3}
%$$
%
%Checking that $η \mapsto T_η \mapsto η_{(T_η)}$ yields back the
%original $η$ is easy --- we just have to start with $η_{(T_η)}$ and
%reduce it as most as we can:
%%
%% (nyop 63 "first-yoneda-bijection-2")
%% (nyo "first-yoneda-bijection-2")
%%
%$$\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}
%$$
%
%Checking that the other round trip, $T \mapsto η_T \mapsto T_{(η_T)}$,
%yields back the original $T$ is not trivial. In the terminology of the
%convention (CSk) from Section \ref{the-conventions}, to reconstruct
%that proof we need an extra hint: that at some point in the proof we
%will have to use that the original $T$ obeys $\sqcond_T$, and that
%we will have to ``evaluate'' $\sqcond_T$ on these inputs:
%
%%D diagram Y0-NT-2
%%D 2Dx 100 +10 +25 +15 +25 +35
%%D 2D 100 A0 B0 - B1 D0 |-----> D1
%%D 2D +0 | | | | D3'
%%D 2D +20 A1 B2 - B3 D2 = D2' - D3
%%D 2D
%%D 2D +10 C0 - C1
%%D 2D
%%D ren A0 A1 ==> C D
%%D ren B0 B1 B2 B3 ==> \catB(C,C) \catA(A,RC) \catB(C,D) \catA(A,RD)
%%D ren C0 C1 ==> \catB(C,-) \catA(A,R-)
%%D ren C0 C1 ==> · ·
%%D ren D0 D1 D3' ==> \id_C TC(\id_C) Rf∘(TC(\id_C))
%%D ren D2 D2' D3 ==> f∘\id_C f TD(f)
%%D
%%D (( A0 A1 -> .plabel= l f
%%D C0 C1 -> .plabel= a T
%%D D0 place
%%D ))
%%D enddiagram
%%D
%$$\pu
% \diag{Y0-NT-2}
%$$
%
%This yields:
%%
%%D diagram Y0-NT-3
%%D 2Dx 100 +25 +40 +30 +25 +35
%%D 2D 100 A0 B0 - B1 D0 |-----> D1
%%D 2D +17 | | | | D3'
%%D 2D +8 A1 B2 - B3 D2 = D2' - D3
%%D 2D
%%D 2D +15 C0 - C1
%%D 2D
%%D ren A0 A1 ==> C D
%%D ren B0 B1 B2 B3 ==> \catB(C,C) \catA(A,RC) \catB(C,D) \catA(A,RD)
%%D ren C0 C1 ==> \catB(C,-) \catA(A,R-)
%%D ren D0 D1 D3' ==> \id_C TC(\id_C) Rf∘(TC(\id_C))
%%D ren D2 D2' D3 ==> f∘\id_C f TD(f)
%%D
%%D (( A0 A1 -> .plabel= l f
%%D B0 B1 -> .plabel= a TC
%%D B0 B2 -> .plabel= l \catB(C,f)
%%D B1 B3 -> .plabel= r \catA(A,Rf)
%%D B2 B3 -> .plabel= a TD
%%D C0 C1 -> .plabel= a T
%%D D0 D1 |-> D1 D3' |->
%%D D0 D2 |-> D2 D2' = D2' D3 |->
%%D ))
%%D enddiagram
%%D
%$$\pu
% \diag{Y0-NT-3}
%$$
%%
%so $Rf∘(TC(\id_C)) = TD(f)$.
%
%We want to check that for all $D$ and $f$ we have $T_{(η_T)}D(f) =
%TD(f)$. We have:
%%
%$$\begin{array}{rcl}
% T_{(η_T)}D(f) &=& (λD.λf.Rf∘η_T)D(f) \\
% &=& (λf.Rf∘η_T)(f) \\
% &=& Rf∘η_T \\
% &=& Rf∘(TC(\id_C)) \\
% &=& TD(f). \\
% \end{array}
%$$
%
%It works! So we have a natural construction for the bijection $T ↔ η$,
%given by:
%%
%$$\begin{array}{rcl}
% T_0 &:=& λD.λf.Rf∘η \\
% η &:=& TC(\id_C) \\
% \end{array}
%$$
% ____ _ _____ __ _ _
% | __ ) __ _ ___(_) ___ | ____|_ __ / _|_ _| | |
% | _ \ / _` / __| |/ __| | _| \ \/ / | |_| | | | | |
% | |_) | (_| \__ \ | (__ | |___ > < | _| |_| | | |
% |____/ \__,_|___/_|\___| |_____/_/\_\ |_| \__,_|_|_|
%
% «basic-example-full» (to ".basic-example-full")
% (misp 40 "basic-example-full")
% (misa "basic-example-full")
% sec: 7.3
% Orig: (favp 33 "basic-example-full")
% (fava "basic-example-full")
% sec: 6.4
%
\subsection{The full reconstruction \DONE}
\label{basic-example-full}
We have just reconstructed all the typings and definitions for the
diagram $\Yzero$. Here is the full reconstruction, except for the
``proof terms'' like $\respids$, $\assoc$, $\idL$ and $\idR$ for each
functor, $\sqcond$ for each natural transformations, and the proofs
that both round trips in the bijections are identity maps:
%
$$\slowdiag{Basic-Example}
\qquad
\begin{array}{rl}
& \catA \text{ is a category}, \\
& \catB \text{ is a category}, \\
& R:\catB \to \catA, \\
& A ∈ \catA, \\
& C ∈ \catB, \\
& η:A→RD, \\
[5pt]
& \catB(C,-) : \catB → \Set, \\
& \catB(C,-)_0 := λD.\catB(C,D), \\
& \catB(C,-)_1 := λg.λf.\;g∘f, \\
[5pt]
& \catA(A,R-) : \catA → \Set, \\
& \catA(A,R-)_0 := λD.\catA(A,RD), \\
& \catA(A,R-)_1 := λg.λh.Rg∘h, \\
[5pt]
& α : \catB(C,-) → \catA(A,R-), \\
[5pt]
& (η↦α_0) := λη.λD.λf.\;Rf∘η, \\
& (α↦η) := λα.\; αC(\id_C), \\
[5pt]
& \text{or:} \\
& α_0 := λD.λf.Rf∘η, \\
& η := αC(\id_C). \\
\end{array}
$$
% (find-idarctpage 27 "19. The syntactical world")
% (find-idarcttext 27 "19. The syntactical world")
It is quite short --- {\sl if we treat the proof terms as
``obvious''.}
%\standout{Rewrite this part:}
%
%It shouldn't be hard --- for someone with practice --- to translate
%the types and definitions at the right above to the language of some
%proof assistant. I tried to do this in Idris (\cite{Brady}) using
%\cite{IdrisCT2019} but I didn't go very far... I implemented the
%protocategories, protofunctors and proto-NTs of \cite[section
% 19]{IDARCT} to be able to skip the proof terms on my first
%prototypes, but I got stuck trying to implement the formalization of
%$\Yzero$ as a single datatype...
%
%\bsk
%
%{\sl (Help would be greatly appreciated!...)}
\newpage
% _____ _ _
% | ____|_ _| |_ ___ _ __ ___(_) ___ _ __ ___
% | _| \ \/ / __/ _ \ '_ \/ __| |/ _ \| '_ \/ __|
% | |___ > <| || __/ | | \__ \ | (_) | | | \__ \
% |_____/_/\_\\__\___|_| |_|___/_|\___/|_| |_|___/
%
% «extensions» (to ".extensions")
% Orig: (favp 34 "extensions")
% (fava "extensions")
% sec: 7
%
\section{Extensions to the diagrammatic language \DONE}
\label{extensions}
Our diagrammatic language and the list of conventions in Section
\ref{the-conventions} can be extended --- ``by the user'' --- in
zillions of ways. Let's see some examples of extensions.
% ____ _
% / ___|___ _ __ ___ _ __ ___ __ _ ___ __ _| |_ ___
% | | / _ \| '_ ` _ \| '_ ` _ \ / _` | / __/ _` | __/ __|
% | |__| (_) | | | | | | | | | | | (_| | | (_| (_| | |_\__ \
% \____\___/|_| |_| |_|_| |_| |_|\__,_| \___\__,_|\__|___/
%
% «comma-categories» (to ".comma-categories")
% (misp 40 "comma-categories")
% (misa "comma-categories")
% Sec 8.1
% Orig: (favp 34 "comma-categories")
% (fava "comma-categories")
% sec: 7.1
%
\subsection{A way to define new categories \DONE}
\label{comma-categories}
We saw in the sections \ref{internal-view-functor} and
\ref{basic-example-functors} how to use diagrams to define functors,
and in sections \ref{internal-view-NT} and \ref{basic-example-NTs} how
to define natural transformations. We can define new categories by
diagrams, too.
% (find-books "__cats/__cats.el" "leinster-basic")
% (find-leinsterbasicpage (+ 8 59) "comma category")
% (find-leinsterbasictext (+ 8 59) "comma category")
%D diagram comma-obj-0
%D 2Dx 100 +17
%D 2D 100 \A
%D 2D | \f
%D 2D v
%D 2D +15 \B |-> \FB
%D 2D
%D (( \A \FB -> .plabel= r \f
%D \B \FB |->
%D ))
%D enddiagram
\pu
\def\commaobj#1#2#3#4{{
\left( \def\A{#1}
\def\f{#4}
\def\B{#2} \def\FB{#3}
\diag{comma-obj-0}
\right)
}}
% Usage:
% %D (( A .tex= \commaobj{A}{B}{FB}{g} BOX
% %D B .tex= \commaobj{A}{B}{FB}{?} BOX
% %D A B ->
% %D ))
\def\dnAR{{(A{↓}R)}}
%D diagram defining-a-comma-category
%D 2Dx 100 +20 +50 +45
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 A3 B0 C0
%D 2D | | |
%D 2D +20 A4 A5 B1 C1
%D 2D
%D 2D +15 A6 A7 B2 C2
%D 2D
%D ren A1 A2 A3 A4 A5 A6 A7 ==> A C RC D RD \catB \catA
%D ren C0 C1 B2 C2 ==> (C,η) (D,g) \dnAR \dnAR
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D A2 A4 -> .plabel= l f
%D A3 A5 -> .plabel= r Rf
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D A1 A5 -> .slide= 20pt .plabel= r g
%D A6 A7 -> .plabel= a R
%D ))
%D (( B0 xy+= 0 -23
%D B1 xy+= 0 -8
%D B0 .tex= \commaobj{A}{C}{RC}{η} BOX
%D B1 .tex= \commaobj{A}{D}{RD}{g} BOX
%D B0 B1 -> .plabel= l f
%D B2 place
%D ))
%D (( C0 C1 -> .plabel= l f
%D C2 place
%D ))
%D enddiagram
%D
$$\pu
\diag{defining-a-comma-category}
$$
\def\AProofOf #1{\llangle#1\rrangle}
\def\AllProofsOf#1{\llbracket#1\rrbracket}
My favorite way --- a syntax sugar! --- of visualizing the comma
category $\dnAR$ is the middle third of the diagram above, in which
the objects of $\dnAR$ are depicted as L-shaped diagrams. To
understand the typings and the commutativity conditions we have to
look at the left third --- it indicates that $f$ must obey $Rf∘η=g$.
The right third shows a generic morphism in $\dnAR$ without the syntax
sugar, but we still have to look at the left third to type it. We
have:
%
$$\begin{array}{rl}
\text{In a context in which}
& \catA \text{ is a category}, \\
& \catB \text{ is a category}, \\
& R : \catB → \catA, \\
& A \text{ is an object of $\catA$}, \\
\text{we define the category}
& \dnAR \text{ as follows:} \\
%
[5pt]
%
\text{An object of}
& \dnAR \\
\text{is a pair}
& (C,η) \\
\text{in which}
& C : \catB_0 \\
\text{and}
& η : \Hom_\catA(A,RC); \\
\text{so}
& (C,η) : (C⠆\catB_0) × \Hom_\catA(A,RC) \\
\text{and}
& \dnAR_0 := (C⠆\catB_0) × \Hom_\catA(A,RC). \\
%
[5pt]
%
\text{A morphism}
& f: (C,η) → (D,g) \text{ in $\dnAR$} \\
\text{is an}
& f: \Hom_\catB(C,D) \text{ such that $Rf∘η=g$}, \\
\text{or equivalently a pair}
& (f,\AProofOf{Rf∘η=g}); \\
\text{we have}
& (f,\AProofOf{Rf∘η=g}) : (f⠆\Hom_\catB(C,D))×\AllProofsOf{Rf∘η=g}, \\
\text{so}
& \Hom_\dnAR((C,η),(D,g)) := \\
& (f⠆\Hom_\catB(C,D)) × \AllProofsOf{Rf∘η=g}.
\end{array}
$$
% The notations $\AProofOf{P}$ and $\AllProofsOf{P}$ are non-standard.
% For any proposition $P$ we denote by $\AllProofsOf{P}$ the set of
% witnesses of $P$ (see \cite[p.18]{HOTT}) and by $\AProofOf{P}$ a
% witness that $P$ is true; formally, $\AProofOf{P}$ is a variable (with
% a long name!) whose type is $\AllProofsOf{P}$, and $\AllProofsOf{P}$
% is a singleton when $P$ is true and the empty set when $P$ is false. A
% good way to remember this notation is that $\AllProofsOf{P}$ looks
% like a box and $\AProofOf{P}$ looks like something that comes in that
% box.
\msk
This defines formally the first two components of the category
$\dnAR$. Remember that a category $\catC$ has seven components:
%
$$\catC = (\catC_0, \Hom_\catC, \id_\catC, ∘_\catC;
\assoc_\catC, \idL_\catC, \idR_\catC)
$$
%
We are pretending that the other components of $\dnAR$ are ``obvious''
in the sense of Section \ref{to-deserve-a-name}. Note the we used the
notations for dependent types and witnesses of the sections
\ref{dependent-types} and \ref{witnesses}.
% (find-books "__logic/__logic.el" "hott")
% (find-hottpage (+ 12 18) "a witness to the provability of A")
% (find-hotttext (+ 12 18) "a witness to the provability of A")
% _ _
% | \ | | ___ ___ ___
% | \| |/ _ \/ __/ __|
% | |\ | __/\__ \__ \
% |_| \_|\___||___/___/
%
% «ness» (to ".ness")
% (misp 43 "ness")
% (misa "ness")
% sec: 8.2
% Orig: (favp 39 "ness")
% (fava "ness")
% sec: 7.5
\subsection{Universalness as something extra \DONE}
\label{ness}
We can consider that an universal arrow is an arrow $η:A→RC$ with
something extra. We saw how to represent this ``something extra'' in
Type Theory: a universal arrow $η$ is a pair $(η,\univ_η)$, where
$\univ_η$ is its ``universalness'', that we defined in one way in
sec.\ref{freyd-with-functors} and in another way in
sec.\ref{indefinite-articles}.
Universalness is just one `-ness' among many. Several of these
``-ness''es have standard graphical representations: for example
pullbackness is indicated by a `$\pbsymbol7$', and monicness is
indicated by a tail like this: `$\monicto$'. \cite{FreydScedrov}
defines lots of graphical representations for ``-ness''es starting on
its page 37. We will sometimes use an `$:=$' to define a new
annotation that is an abbreviation for extra structure:
%
%D diagram universalness
%D 2Dx 100 +20 +50 +20
%D 2D 100 A1 C1
%D 2D
%D 2D +20 A2 A3 C2 C3
%D 2D
%D 2D +20 A4 A5 C4 C5
%D 2D
%D 2D +15 B0 B1 D0 D1
%D 2D
%D ren A1 A2 A3 B0 B1 ==> A C RC \catB \catA
%D ren C1 C2 C3 C4 C5 D0 D1 ==> A C RC D RD \catB \catA
%D
%D (( A1 A3 -> .plabel= r \sm{η\\\univ}
%D A2 A3 |->
%D B0 B1 -> .plabel= a R
%D
%D C1 C3 -> .plabel= r η
%D C2 C3 |->
%D C2 C4 -> .plabel= l ∃!f
%D C3 C5 -> .plabel= r Rf
%D C4 C5 |->
%D C1 C5 -> .slide= 15pt .plabel= r ∀g
%D D0 D1 -> .plabel= a R
%D C2 C5 harrownodes nil 20 nil |->
%D
%D A3 C4 midpoint .TeX= := place
%D ))
%D enddiagram
%D
$$\pu
\diag{universalness}
$$
This is pullbackness:
%
%D diagram pullbackness
%D 2Dx 100 100 +20 +40 +20 +20
%D 2D 100 A0 B0
%D 2D
%D 2D +20 A1 A2 B1 B2
%D 2D
%D 2D +20 A3 A4 B3 B4
%D 2D
%D ren A0 A1 A2 A3 A4 ==> ∀X A B C D
%D ren B0 B1 B2 B3 B4 ==> ∀X A B C D
%D
%D (( A1 A2 ->
%D A1 A3 ->
%D A2 A4 ->
%D A3 A4 ->
%D A1 relplace 5 5 \pbsymbol{7}
%D A2 relplace 25 5 :=
%D
%D B1 B2 ->
%D B1 B3 ->
%D B2 B4 ->
%D B3 B4 ->
%D B0 B1 -> .plabel= m ∃!
%D B0 B3 -> .plabel= l ∀
%D B0 B2 -> .plabel= a ∀
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{pullbackness}
$$
% ___ _ _ _
% / _ \ _ __ _ __ ___ ___(_) |_ ___ ___ __ _| |_ ___
% | | | | '_ \| '_ \ / _ \/ __| | __/ _ \ / __/ _` | __/ __|
% | |_| | |_) | |_) | (_) \__ \ | || __/ | (_| (_| | |_\__ \
% \___/| .__/| .__/ \___/|___/_|\__\___| \___\__,_|\__|___/
% |_| |_|
%
% «opposite-categories» (to ".opposite-categories")
% (misp 44 "opposite-categories")
% (misa "opposite-categories")
% sec: 8.3
% Orig: (favp 38 "opposite-categories")
% (fava "opposite-categories")
% sec: 7.4
\subsection{Opposite categories \DONE}
\label{opposite-categories}
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 33) "2. Contravariance and Opposites")
% (find-books "__cats/__cats.el" "abramsky-tzevelekos")
% (find-abramskyticclpage 14 "1.1.5 First Notions")
% (find-abramskyticcltext 14 "1.1.5 First Notions")
% (find-abramskyticclpage 15 "Opposite Categories and Duality")
% (find-abramskyticcltext 15 "Opposite Categories and Duality")
\def\Aop{{\catA^\op}}
Suppose that we have a diagram $A \ton{f} B \ton{g} C$ in a category
$\catA$. There are several different notations for the corresponding
diagram in $\Aop$: for example, in \cite[p.33]{CWM2} it would be
written as $A \otn{f^\op} B \otn{g^\op} C$, while in
\cite[p.15]{AbramskyTzevelekos} as $A \otn{f} B \otn{g} C$. The
convention (COT) says that the notation in our diagrams should be as
close as possible to the notation in the original text --- so let's
see how to support the notation in \cite{AbramskyTzevelekos}, that
looks a bit harder than the one in \cite{CWM2}.
We want to define a new category, $\Aop$, using tricks similar to the
ones in Section \ref{comma-categories}, but now we can't pretend that
the new composition is obvious. We will define $(\Aop)_0$,
$\Hom_\Aop$, $\id_\Aop$, and $∘_\Aop$ without any textual
explanations, with just the diagrams to convince the readed that our
definitions are reasonable.
%
%D diagram A-and-Aop
%D 2Dx 100 +35
%D 2D 100 A0 B0
%D 2D
%D 2D +10 A1 B1
%D 2D | |
%D 2D +15 A2 B2
%D 2D
%D 2D +10 A3 B3
%D 2D | |
%D 2D +15 A4 B4
%D 2D
%D 2D +10 A5 B5
%D 2D | |
%D 2D +15 A6 B6
%D 2D | |
%D 2D +15 A7 B7
%D 2D
%D 2D +15 A8 B8
%D 2D
%D ren A0 A1 A2 A3 A4 A5 A6 A7 A8 ==> A A B A A A B C \catA
%D ren B0 B1 B2 B3 B4 B5 B6 B7 B8 ==> A A B A A A B C \catA^\op
%D
%D (( A0 place
%D A1 A2 -> .plabel= r f
%D A3 A4 -> .plabel= r \id_A
%D A5 A6 -> .plabel= r f
%D A6 A7 -> .plabel= r g
%D A5 A7 -> .slide= 15pt .plabel= r g∘f
%D A8 place
%D
%D B0 place
%D B1 B2 <- .plabel= r f
%D B3 B4 <- .plabel= r \id_A
%D B5 B6 <- .plabel= r f
%D B6 B7 <- .plabel= r g
%D B5 B7 <- .slide= 15pt .plabel= r f∘g
%D B8 place
%D ))
%D enddiagram
%D
$$\pu
\diag{A-and-Aop}
\quad
\begin{array}{c}
\catA_0 =: (\Aop)_0 \\
\\
\Hom_\catA(A,B) =: \Hom_\Aop(B,A) \\
\\
\id_\catA(A) =: \id_\Aop(A) \\
\\
g ∘_\catA f =: f ∘_\Aop g \\
\\
\\
\\
\\
\\
\end{array}
$$
In the diagram below $F:\catA^\op→\catB$ is a contravariant functor,
and the $\catA$ above $\catA^\op$ indicates that $g:C→D$ is a morphism
of $\catA$, not of $\catA^\op$. I am not very happy with this trick
but I haven't found a better alternative yet.
%
%D diagram contravariant-functor
%D 2Dx 100 +20
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +12 B0'
%D 2D +8 B0 B1
%D 2D
%D ren A0 A1 ==> C FC
%D ren A2 A3 ==> D FD
%D ren B0' ==> \catA
%D ren B0 B1 ==> \phantom{m}\catA^\op \catB
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l g
%D A1 A3 <- .plabel= r Fg
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0' place
%D B0 B1 -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
\diag{contravariant-functor}
$$
% __ __ _
% \ \ / /__ _ __ ___ __| | __ _
% \ V / _ \| '_ \ / _ \/ _` |/ _` |
% | | (_) | | | | __/ (_| | (_| |
% |_|\___/|_| |_|\___|\__,_|\__,_|
%
% «yoneda-lemma» (to ".yoneda-lemma")
% (misp 43 "yoneda-lemma")
% (misa "yoneda-lemma")
% sec. 8.2
% Orig: (favp 35 "yoneda-lemma")
% (fava "yoneda-lemma")
% sec: 7.2
%
\subsection{The Yoneda Lemma \DONE}
\label{yoneda-lemma}
The formalization of $\Yzero$ as a series of typings and definitions
in Section \ref{basic-example-full} {\sl suggests} that {\sl some}
operations from Type Theory that can be applied on the formalization
side should be translatable to the diagram side; for example,
substitution. This one clearly works: if we substitute $\catA$ by
$\Set$ and $A$ by the set 1 we get this,
%
%D diagram Basic-Example-using-Set-and-1
%D 2Dx 100 +40
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 |-> A3
%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 ==> 1
%D ren A2 A3 ==> C RC
%D ren B0 B1 ==> \catB \Set
%D ren C0 C1 C2 ==> \catB(C,-) \Set(1,R-) ?
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D
%D B0 B1 -> .plabel= a R\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= ^15pt
%D ))
%D enddiagram
%
\pu
$$
\Yzero \bmat{\catA := \Set \\ A := 1}
\qquad = \quad
\slowdiag{Basic-Example-using-Set-and-1}
$$
For each object $S$ of $\Set$ we have a bijection between elements of
$S$ and morphisms $1→S$. We will denote the morphism from 1 to $S$
that ``chooses'' an element $s∈S$ by $\nameof{s}$; the pronounciation
of $\nameof{s}$ is ``the name of $s$''. We have a bijection between
`$s$'s and $\nameof{s}$s:
For each $D∈\catB$ we have a bijection $\Set(1,RD) ↔ RD$ --- and we
can use these bijections to build a natural isomorphism
$\Set(1,R-) ↔ R$. We will draw it vertically, and complete the
triangle:
%D diagram Basic-Example-using-Set-and-1-and-R
%D 2Dx 100 +40
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 |-> A3
%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 ==> 1
%D ren A2 A3 ==> C RC
%D ren B0 B1 ==> \catB \Set
%D ren C0 C1 C2 ==> \catB(C,-) \Set(1,R-) R
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D
%D B0 B1 -> .plabel= a R\phantom{mmm}
%D
%D C0 C1 -> .plabel= b α
%D C0 C2 -> .plabel= l β
%D C1 C2 <->
%D
%D C0 C1 midpoint A1 A3 midpoint <-> .curve= ^15pt
%D ))
%D enddiagram
%
\pu
$$
\Yone
\qquad := \qquad
\slowdiag{Basic-Example-using-Set-and-1-and-R}
$$
We can use that natural isomorphism to obtain `$β$'s from `$α$'s, and
vice-versa, by composition. We could draw an arrow for the bijection
between `$α$'s and `$β$'s and another arrow for the bijection between
`$η$'s and elements of $RC$, but we will prefer to omit them.
We will call the diagram above $\Yone$. It doesn't have a single
top-level arrow, so we can't apply the convention (CTL) to it, and we
need to specify its ``meaning'' explicitly. We will consider that its
three bijections are top-level objects, and so the diagram $\Yone$
says that we have these bijections:
%
$$\begin{array}{l}
RC \\
↔ \; \Set(1,RC) \\
↔ \; \Set^\catB(\catB(C,-),\Set(1,R-)) \\
↔ \; \Set^\catB(\catB(C,-),R) \\
\end{array}
$$
The Yoneda Lemma ``is'' the bijection $RC ↔ \Set^\catB(\catB(C,-),R)$
--- check how it is defined in \cite[thm.4.2.1]{Leinster},
\cite[thm.2.2.4]{Riehl}, \cite[p.61]{CWM2}, \cite[lemma 8.2]{Awodey}.
Some books show how to calculate the element of $RC$ associated to a
given $β$ and vice-versa, and most treat $\Set(1,R-)$ as something
secondary. If we represent this idea of the Yoneda Lemma in the same
format the we used in sec.\ref{basic-example-full}, we get this:
%
%D diagram Y1-minus
%D 2Dx 100 +30
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 |-> A3
%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 ==> 1
%D ren A2 A3 ==> C RC
%D ren B0 B1 ==> \catB \Set
%D ren C0 C1 C2 ==> \catB(C,-) \Set(1,R-) R
%D
%D (( A1 A3 -> .plabel= r \nameof{e}
%D A2 A3 |->
%D
%D B0 B1 -> .plabel= a R
%D
%D # C0 C1 -> .plabel= b α
%D C0 C2 -> .plabel= l β
%D # C1 C2 <->
%D
%D # C0 C1 midpoint A1 A3 midpoint <-> .curve= ^15pt
%D ))
%D enddiagram
%
\pu
$$\Ytwo
\;\; := \;\;
\slowdiag{Y1-minus}
\qquad
\begin{array}{rl}
& \catB \text{ is a category}, \\
& R:\catB \to \Set, \\
& C ∈ \catB, \\
[5pt]
& \catB(C,-) : \catB → \Set, \\
& \catB(C,-)_0 := λD.\catB(C,D), \\
& \catB(C,-)_1 := λg.λf.\;g∘f, \\
[5pt]
& e ∈ RC, \\
& \nameof{e} := λ{*}.e, \\
& β : \catB(C,-) → R, \\
[5pt]
& (e↦β_0) := λe.λD.λf.\;Rf(e), \\
& (β↦e) := λβ.βC\id_C, \\
\end{array}
$$
% (find-books "__cats/__cats.el" "leinster-basic")
% (find-leinsterbasicpage (+ 8 93) "4.2 The Yoneda lemma")
% (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).")
%
% \standout{TODO:} show the diagram for ``every functor to $\Set$ that has a
% left adjoint is representable''.
% __ __ _ _
% \ \ / /__ _ __ ___ __| | __ _ ___ _ __ ___ | |__
% \ V / _ \| '_ \ / _ \/ _` |/ _` | / _ \ '_ ` _ \| '_ \
% | | (_) | | | | __/ (_| | (_| | | __/ | | | | | |_) |
% |_|\___/|_| |_|\___|\__,_|\__,_| \___|_| |_| |_|_.__/
%
% «yoneda-embedding» (to ".yoneda-embedding")
% (misp 46 "yoneda-embedding")
% (misa "yoneda-embedding")
% sec: 8.4
% Orig: (favp 34 "yoneda-embedding")
% (fava "yoneda-embedding")
% sec: 7.3
%
\subsection{The Yoneda embedding \DONE}
\label{yoneda-embedding}
Let's define $\Ythree$ as the result of this substituion:
%
$$\Ythree \;\;=\;\; \Ytwo
\bmat{
R := \catB(B,-) \\
e := φ \\
}
$$
We have:
%
%D diagram Y3
%D 2Dx 100 +30
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 |-> A3
%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 ==> 1
%D ren A2 A3 ==> C \catB(B,C)
%D ren B0 B1 ==> \catB \Set
%D ren C0 C2 ==> \catB(C,-) \catB(B,-)
%D
%D (( A1 A3 -> .plabel= r \nameof{φ}
%D A2 A3 |->
%D B0 B1 -> .plabel= a R
%D C0 C2 -> .plabel= l β
%D ))
%D enddiagram
%
\pu
$$\scalebox{0.9}{$
\Ythree
\;\; = \;\;
\slowdiag{Y3}
\qquad
\begin{array}{rl}
& \catB \text{ is a category}, \\
& \catB(B,-):\catB \to \Set, \\
& C ∈ \catB, \\
[5pt]
& \catB(C,-) : \catB → \Set, \\
& \catB(C,-)_0 := λD.\catB(C,D), \\
& \catB(C,-)_1 := λg.λf.\;g∘f, \\
[5pt]
& φ ∈ \catB(B,C), \\
& \nameof{φ} := λ{*}.φ, \\
& β : \catB(C,-) → \catB(B,-), \\
[5pt]
& (φ↦β_0) := λφ.λD.λf.\;\catB(B,-)_1(f)(φ), \\
& (β↦φ) := λβ.βC\id_C, \\
\end{array}
$}
$$
The formulas in $(φ↦β_0)$ and $(β↦φ)$ can be simplified, and we can
derive this other diagram from it:
%
%D diagram Y-emb-2022mar01
%D 2Dx 100 +30 +30 +25
%D 2D 100 A0 |-> A1 B0 C0
%D 2D | | | |
%D 2D +30 A2 |-> A3 B1 C1
%D 2D D0'
%D 2D +20 D0 --> D1
%D 2D
%D ren A0 A1 ==> C \catB(C,-)
%D ren A2 A3 ==> B \catB(B,-)
%D ren B0 B1 ==> \catB(C,D) \catB(B,D)
%D ren C0 C1 ==> f f∘φ
%D ren D0 D1 ==> \phantom{{}^\op}\catB^\op \Set
%D
%D (( A0 A1 |->
%D A0 A2 <- .plabel= l φ
%D A1 A3 -> .plabel= r β
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil <->
%D B0 B1 ->
%D C0 C1 |->
%D newnode: D0' at: @D0+v(0,-7) .TeX= \catB place
%D D0 D1 -> .plabel= a \mathbf{y}
%D ))
%D enddiagram
%D
$$\pu
\diag{Y-emb-2022mar01}
\qquad
\begin{array}{rl}
& \catB \text{ is a category}, \\
& B ∈ \catB, \\
& C ∈ \catB, \\
[5pt]
& φ : B→C, \\
& β : \catB(C,-)→\catB(B,-), \\
& (φ↦β_0) := λφ.λD.λf.\;f∘φ, \\
& (β↦φ) := λβ.βC\id_C, \\
\end{array}
$$
Let's call it $\Yfour$. This is one of the {\sl Yoneda Embeddings};
compare that diagram with the ones in \cite[p.60]{Riehl}. In
\cite{MissingAgda} we show how to formalize it in Agda as a corollary
of $\Yzero$, $\Yone$, $\Ytwo$, and $\Ythree$.
%
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 60) "Corollary 2.2.8 (Yoneda embedding)")
% (find-riehlcctext (+ 18 60) "Corollary 2.2.8 (Yoneda embedding)")
% (find-books "__cats/__cats.el" "leinster-basic")
Note that the functor $C \mapsto \catB(C,-)$ in $\Yfour$ is
contravariant, and we used the trick from
sec.\ref{opposite-categories} to indicate this.
% ____ _ _ _
% | _ \ ___ _ __ _ __ ___ ___ ___ _ __ | |_ __ _| |__ | | ___
% | |_) / _ \ '_ \| '__/ _ \/ __|/ _ \ '_ \| __/ _` | '_ \| |/ _ \
% | _ < __/ |_) | | | __/\__ \ __/ | | | || (_| | |_) | | __/
% |_| \_\___| .__/|_| \___||___/\___|_| |_|\__\__,_|_.__/|_|\___|
% |_|
% «representable-functors» (to ".representable-functors")
% (misp 47 "representable-functors")
% (misa "representable-functors")
\subsection{Representable functors}
\label{representable-functors}
% (find-books "__cats/__cats.el" "riehl")
% (find-books "__cats/__cats.el" "leinster-basic")
%
Some books, like \cite{Leinster} and \cite{Riehl}, present
representable functors first, then lots of examples, and only then
they present the Yoneda Lemma. In our diagram $\Yone$ a {\sl
representation} for the functor $R$ is a pair $(C,β)$ such that the
natural transformation $β$ is a natural iso. It is easy to see that we
have these bijections, or bi-implications:
%
$$\begin{array}{l}
\text{natural iso-ness of $β$} \\
↔ \; \text{natural iso-ness of $α$} \\
↔ \; \text{universalness of $η$} \\
\end{array}
$$
%
The last one holds in the diagram $\Yzero$ too.
\msk
Many of the textbook examples of representable functors are
consequences of a simple theorem that shows that every functor
$R:\catB→\Set$ with a left adjoint is representable. The diagram
$\Yfive$ below is a skeleton for a proof of that theorem:
%
%D diagram Y5
%D 2Dx 100 +25 +20 +20 +30 +30
%D 2D 100 D0 <-| D1 F0 G0 A1
%D 2D | | | | |
%D 2D +20 D2 |-> D3 F1 G1 A2 |-> A3
%D 2D
%D 2D +15 E0 === E1 B0 --> B1
%D 2D
%D 2D +15 C0 --> C1
%D 2D \ |
%D 2D +20 C2
%D 2D
%D ren A1 ==> 1
%D ren A2 A3 ==> L1 RL1
%D ren B0 B1 ==> \catB \Set
%D ren C0 C2 ==> \catB(L1,-) R
%D ren D0 D1 ==> LA A
%D ren D2 D3 ==> B RB
%D ren E0 E1 ==> \catB \Set
%D ren F0 F1 ==> A RLA
%D ren G0 G1 ==> 1 RL1
%D
%D (( A1 A3 -> .plabel= r \sm{η_1\\univ}
%D A2 A3 |->
%D B0 B1 -> .plabel= a R
%D C0 C2 <-> # .plabel= l β
%D
%D D0 D1 <-|
%D D0 D2 ->
%D D1 D3 ->
%D D2 D3 |->
%D D0 D3 harrownodes nil 20 nil <->
%D E0 E1 <- sl^ .plabel= a L
%D E0 E1 -> sl_ .plabel= b R
%D F0 F1 -> .plabel= r η_A
%D G0 G1 -> .plabel= r η_1
%D ))
%D enddiagram
%
\pu
$$\Yfive \;\; := \;\;\;\;\;
\slowdiag{Y5}
$$
The unit arrow $η_1:1→RL1$ is universal --- note the `$\univ$' in the
upper right arrow --- and so its associated `$β$' is a natural iso; we
drew it with a `$↔$'.
Statements like ``the functor {\sl blah} is representable'' are very
common in CT texts, and their natural isos is usually written just
like ``$R \cong \catB(L1,-)$'', without a name. A good way to draw the
missing diagrams for a text should not force us to invent names, and
so we should be allowed to omit the names of arrows when this is
convenient.
% In the examples of representable functors in \cite{Leinster} and
% \cite{Riehl} the natural iso never has a name
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 51) "Example 2.1.5. The following covariant functors")
% (find-riehlcctext (+ 18 51) "Example 2.1.5. The following covariant functors")
% (find-riehlccpage (+ 18 63) "Example 2.3.4." "Z[x]")
% (find-riehlcctext (+ 18 63) "Example 2.3.4." "Z[x]")
This is the example (iv) in \cite[p.52]{Riehl}:
\begin{quotation}
\begin{enumerate}
\item[(iv)] The functor $U:\Ring→\Set$ is represented by the unital
ring $\Z[x]$, the polynomial ring in one variable with integer
coefficients. A unital ring homomorphism $Z[x]→R$ is uniquely
determined by the image of $x$; put another way, $\Z[x]$ is the {\sl
free unital ring on a single generator}.
\end{enumerate}
\end{quotation}
The diagram below is a good way to visualize that:
%
%D diagram Y5-rings
%D 2Dx 100 +25 +20 +20 +30 +30
%D 2D 100 D0 <-| D1 F0 G0 A1
%D 2D | | | | |
%D 2D +20 D2 |-> D3 F1 G1 A2 |-> A3
%D 2D
%D 2D +15 E0 === E1 B0 --> B1
%D 2D
%D 2D +15 C0 --> C1
%D 2D \ |
%D 2D +20 C2
%D 2D
%D ren A1 ==> 1
%D ren A2 A3 ==> \Z[x] U\Z[x]
%D ren B0 B1 ==> \Ring \Set
%D ren C0 C2 ==> \Ring(\Z[x],-) U
%D ren D0 D1 ==> FA A
%D ren D2 D3 ==> B UB
%D ren E0 E1 ==> \Ring \Set
%D ren F0 F1 ==> A UFA
%D ren G0 G1 ==> 1 U\Z[x]
%D
%D (( A1 A3 -> .plabel= r \sm{\nameof{x}\\\univ}
%D A2 A3 |->
%D B0 B1 -> .plabel= a U
%D C0 C2 <-> # .plabel= l β
%D
%D D0 D1 <-|
%D D0 D2 ->
%D D1 D3 ->
%D D2 D3 |->
%D D0 D3 harrownodes nil 20 nil <->
%D E0 E1 <- sl^ .plabel= a F
%D E0 E1 -> sl_ .plabel= b U
%D F0 F1 -> .plabel= r η_A
%D G0 G1 -> .plabel= r η_1
%D ))
%D enddiagram
%
\pu
$$\slowdiag{Y5-rings}
$$
Its left half is useful for when we want to remember how that
representation is generated by an adjunction of the form $F⊣U$, but it
can be omitted. In sec.\ref{the-conventions} I drew that diagram
without its left half.
% She develops more this example in page 63, as:
%
% \begin{quotation}
%
% {\bf Example 2.3.4.} Recall from Example 2.1.5(iv) that the
% forgetful functor $U:\Ring→\Set$ is represented by the ring $Z[x]$.
% The universal element, which defines the natural isomorphism
% %
% $$\Ring(Z[x], R) ≅ UR,$$
% %
% is the element $x∈\Z[x]$. As in the proof of the Yoneda lemma, the
% bijection above is implemented by evaluating a ring homomorphism
% $ϕ:\Z[x]→R$ at the element $x∈\Z[x]$ to obtain an element $ϕ(x)∈R$.
%
% \end{quotation}
% % ____ __ _
% % | _ \ ___ _ __ _ __ / _|_ _ _ __ ___| |_ ___ _ __ ___
% % | |_) / _ \ '_ \| '__| | |_| | | | '_ \ / __| __/ _ \| '__/ __|
% % | _ < __/ |_) | | | _| |_| | | | | (__| || (_) | | \__ \
% % |_| \_\___| .__/|_| |_| \__,_|_| |_|\___|\__\___/|_| |___/
% % |_|
% %
% % «representable-functors» (to ".representable-functors")
% % Orig: (favp 40 "representable-functors")
% % (fava "representable-functors")
% % sec:
% \subsection{Representable functors \DONE}
% \label{representable-functors}
%
% It is easy to see that in $\Yzero$ the universality of $η$ is
% equivalent to the natural-iso-ness of $T$; in $\Yone$ the universality
% of $η$ is equivalent to the natural-iso-ness of $T$, and this is
% equivalent to the natural-iso-ness of $T'$. The constructions should
% be evident from these diagrams:
% %
% %D diagram univ-arrows-univ-elts
% %D 2Dx 100 +40 +50 +40
% %D 2D 100 A1 D1
% %D 2D | |
% %D 2D +20 A2 |-> A3 D2 |-> D3
% %D 2D | | | |
% %D 2D +20 A4 |-> A5 D4 |-> D5
% %D 2D
% %D 2D +15 B0 --> B1 E0 --> E1
% %D 2D
% %D 2D +15 C0 --> C1 F0 --> F1
% %D 2D \ | \ |
% %D 2D +20 C2 F2
% %D 2D
% %D ren A1 ==> A
% %D ren A2 A3 ==> C RC
% %D ren A4 A5 ==> D RD
% %D ren B0 B1 ==> \catB \catA
% %D ren C0 C1 C2 ==> \catB(C,-) \catA(A,R-) ?
% %D
% %D ren D1 ==> 1
% %D ren D2 D3 ==> C RC
% %D ren D4 D5 ==> D RD
% %D ren E0 E1 ==> \catB \Set
% %D ren F0 F1 F2 ==> \catB(C,-) \Set(1,R-) R
% %D
% %D (( A1 A3 -> .plabel= r \sm{η\\\univ}
% %D A2 A3 |->
% %D A2 A4 -> .plabel= l f
% %D A3 A5 -> .plabel= r Rf
% %D A2 A5 harrownodes nil 20 nil |->
% %D A4 A5 |->
% %D A1 A5 -> .slide= 25pt .plabel= r h
% %D
% %D B0 B1 -> .plabel= a R\phantom{mmm}
% %D
% %D C0 C1 <-> .plabel= b T
% %D C0 C1 midpoint A1 A3 midpoint <-> .curve= ^15pt
% %D ))
% %D (( D1 D3 -> .plabel= r \sm{η\\\univ}
% %D D2 D3 |->
% %D D2 D4 -> .plabel= l f
% %D D3 D5 -> .plabel= r Rf
% %D D2 D5 harrownodes nil 20 nil |->
% %D D4 D5 |->
% %D D1 D5 -> .slide= 25pt .plabel= r h
% %D
% %D E0 E1 -> .plabel= a R\phantom{mmm}
% %D
% %D F0 F1 <-> .plabel= b T
% %D F0 F2 <-> .plabel= l T'
% %D F1 F2 <->
% %D
% %D F0 F1 midpoint D1 D3 midpoint <-> .curve= ^15pt
% %D ))
% %D enddiagram
% %
% $$\pu
% \slowdiag{univ-arrows-univ-elts}
% $$
%
% The diagram at the right above can be seen as the missing diagram for
% Proposition 2 in \cite[p.60]{CWM2}, that says this (I've translated
% its letters to the ones I use):
%
% % (find-books "__cats/__cats.el" "maclane")
% % (find-cwm2page (+ 13 60) "Definition.")
% % (find-cwm2text (+ 13 60) "Definition.")
%
% \begin{quotation}
%
% {\bf Definition.} {\sl Let $\catB$ have small hom-sets. A
% representation of a functor $R:\catB→\Set$ is a pair $〈C,T'〉$,
% with $C$ an object of $\catB$ and
% %
% $$T':\catB(C,-)→R$$
% %
% a natural isomorphism. The object $C$ is called the representing
% object. The functor $R$ is said to be representable when such a
% representation exists.}
%
% \msk
%
% Up to isomorphism, a representable functor is thus just a covariant
% hom-functor $\catB(C,-)$. This notion can be related to universal arrows as
% follows.
%
% \msk
%
% {\bf Proposition 2.} Let 1 denote any one-point set and let $\catB$
% have small hom-sets. If $〈C, η:1→RC〉$ is a universal arrow from $1$
% to $R: \catB→\Set$, then the function $T'$ which for each object $D$
% of $\catB$ sends the arrow $f:C→D$ to $(Rf)(η(*))∈RD$ is a
% representation of $R$. Every representation of $R$ is obtained in
% this way from exactly one such universal arrow.
%
% \end{quotation}
%
% The operations $T'↦η$ and $η↦T'$ can be defined as:
% %
% $$\begin{array}{rcl}
% η &:& 1→RC \\
% T' &:& \catB(C,-)→R \\
% η &:=& λ*.(T'C(\id(C))) \\
% T' &:=& λD.λf.(Rf)(η(*)) \\
% \end{array}
% $$
% % _____ __ __
% % |__ / | _|_ _|_ |
% % / / | |\ \/ /| |
% % / /_ | | > < | |
% % /____| | |/_/\_\| |
% % |__| |__|
% %
% % «representable-functor-ex» (to ".representable-functor-ex")
% % Orig: (favp 42 "representable-functor-ex")
% % (fava "representable-functor-ex")
% % sec:
% \subsection{An example of a representable functor \DONE}
% \label{representable-functor-ex}
%
%
% Here is the ``missing diagram'' for both excerpts:
% %
% %D diagram 2.3.4._Z[x]
% %D 2Dx 100 +55
% %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 \sm{\nameof{x}\\\univ}
% %D A2 A3 |->
% %D A2 A4 -> .plabel= l ϕ
% %D A3 A5 -> .plabel= r Uϕ
% %D A4 A5 |->
% %D A1 A5 -> .slide= 25pt .plabel= r \nameof{ϕ(x)}
% %D A2 A5 harrownodes nil 20 nil |->
% %D B0 B1 -> .plabel= a U
% %D C1 C2 <-> .plabel= b T
% %D C1 C3 <-> .plabel= b T'
% %D C2 C3 <->
% %D ))
% %D enddiagram
% %D
% $$\pu
% \diag{2.3.4._Z[x]}
% $$
%
% That diagram may be a good starting point to explain the Yoneda Lemma
% to ``children''.
% \newpage
% ____ _ __ _
% |___ \ ___ __ _| |_ ___ / _| ___ __ _| |_ ___
% __) |____ / __/ _` | __| / _ \| |_ / __/ _` | __/ __|
% / __/_____| (_| (_| | |_ | (_) | _| | (_| (_| | |_\__ \
% |_____| \___\__,_|\__| \___/|_| \___\__,_|\__|___/
%
% «2-category-of-cats» (to ".2-category-of-cats")
% (misp 40 "2-category-of-cats")
% (misa "2-category-of-cats")
% Orig: (favp 44 "2-category-of-cats")
% (fava "2-category-of-cats")
% sec:
\subsection{The 2-category of categories}
\label{2-category-of-cats}
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 44) "1.7. The 2-category of categories")
\def\Dn#1{\Downarrow\scriptstyle #1}
Natural transformations are often drawn as `$⇒$'s in the middle of
``cells'' whose walls are functors. If $F,G:\catA→\catB$ are functors
and $T:F→G$ is natural transformation, then $\catA, \catB, F, G, T$
are drawn like this:
%
%D diagram 2-cat-1
%D 2Dx 100 +30
%D 2D 100 A B
%D 2D
%D ren A B ==> \catA \catB
%D
%D (( A B -> .curve= ^10pt .plabel= a F
%D A B -> .curve= _10pt .plabel= b G
%D A B midpoint .TeX= \Dn{T} place
%D
%D ))
%D enddiagram
%D
$$\pu
\slowdiag{2-cat-1}
$$
% (find-books "__cats/__cats.el" "power")
There are several ways to compose functors and natural transformations
--- see \cite[section 1.7]{Riehl}, \cite[section A.5]{Hazratpour}, and
\cite{PowerPasting} for the details and the precise terminology. For
example, in
%
% (riep 5 "6.1._kan-extensions")
% (rie "6.1._kan-extensions")
%
%D diagram 2-cat-2
%D 2Dx 100 +25 +25 +20 +25 +25 +20 +25 +25
%D 2D 100 A1 B1 C1
%D 2D / \ / \ / \\
%D 2D +25 A0 ---- A2 B0 ---- B2 C0 ---- C2
%D 2D
%D ren A0 A1 A2 ==> \catA \catB \catC
%D ren B0 B1 B2 ==> \catA \catB \catC
%D ren C0 C1 C2 ==> \catA \catB \catC
%D
%D ((
%D A0 A1 -> .plabel= a F
%D A1 A2 -> .curve= _10pt .plabel= m R
%D A1 A2 -> .curve= ^20pt .plabel= a G
%D A0 A2 -> .plabel= b H
%D A0 A2 midpoint relplace -4 -8 \Dn{T}
%D A1 A2 midpoint relplace 4 -2 \Dn{U}
%D
%D B0 B2 -> .curve= ^50pt .plabel= a GF
%D B0 B2 -> .curve= ^25pt .plabel= m RF
%D B0 B2 -> .plabel= b H
%D B0 B2 midpoint relplace 0 -21 \Dn{UF}
%D B0 B2 midpoint relplace 0 -7 \Dn{T}
%D
%D C0 C2 -> .curve= ^45pt .plabel= a GF
%D C0 C2 -> .plabel= b H
%D C0 C2 midpoint relplace 0 -12 \Dn{T·UF}
%D
%D A2 B0 midpoint relplace 0 -12 =
%D B2 C0 midpoint relplace 0 -12 =
%D ))
%D enddiagram
%D
$$\pu
\slowdiag{2-cat-2}
$$
%
we used ``whiskering'' and then ``vertical composition''.
We can use internal views to lower the level of abstraction of the
diagrams above. If we draw the images of an object $A∈\catA$ by the
functors and natural transformations we get:
%
%D diagram 2-cat-2-internal-view
%D 2Dx 100 +20 +20 +30 +20 +20 +30 +20 +20
%D 2D 100 A1 B1 C1
%D 2D / |\ / |\ / |\
%D 2D +10 / \ A2 / \ B2 / \ C2
%D 2D +15 | A3 | B3 | C3
%D 2D +15 A0 ---- A4 B0 ---- B4 C0 ---- C4
%D 2D
%D ren A0 A1 A2 A3 A4 ==> A FA GFA RFA HA
%D ren B0 B1 B2 B3 B4 ==> A FA GFA RFA HA
%D ren C0 C1 C2 C3 C4 ==> A FA GFA RFA HA
%D
%D (( A0 A1 |->
%D A1 A2 |-> .curve= ^5pt
%D A1 A3 |-> .curve= _10pt
%D A0 A4 |->
%D A2 A3 -> .plabel= r UFA
%D A3 A4 -> .plabel= r TA
%D
%D B0 B2 |-> .curve= ^40pt
%D B0 B3 |-> .curve= ^20pt
%D B0 B4 |->
%D B2 B3 -> .plabel= r UFA
%D B3 B4 -> .plabel= r TA
%D
%D C0 C2 |-> .curve= ^40pt
%D C0 C4 |->
%D C2 C4 -> .plabel= r \sm{TA∘UFA\\=(T·UF)A}
%D
%D A4 B0 midpoint relplace 4 -12 =
%D B4 C0 midpoint relplace 4 -12 =
%D ))
%D enddiagram
%D
$$\pu
\slowdiag{2-cat-2-internal-view}
$$
Note that this process of taking a ``pasting diagram'' and looking at
its internal view --- in which many names become longer and some nodes
are duplicated --- is the opposite of what people usually do in the
literature: they usually go from pasting diagrams to string diagrams,
in which most names are omitted. See \cite{MarsdenCTUSD} and
\cite[section A.5]{Hazratpour}.
% (find-books "__cats/__cats.el" "marsden-ctusd")
% (find-books "__cats/__cats.el" "hazratpour")
\newpage
% _ __ _
% | |/ /__ _ _ __ _____ _| |_ ___
% | ' // _` | '_ \ / _ \ \/ / __/ __|
% | . \ (_| | | | | | __/> <| |_\__ \
% |_|\_\__,_|_| |_| \___/_/\_\\__|___/
%
% «kan-extensions» (to ".kan-extensions")
% Orig: (favp 45 "kan-extensions")
% (fava "kan-extensions")
% sec:
\subsection{Kan extensions}
\label{kan-extensions}
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 192) "Proposition 6.1.5")
% (find-riehlcctext (+ 18 192) "Proposition 6.1.5")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 236) "3. The Kan Extension")
Kan extensions are usually drawn using 2-cells (\cite[definition
6.1.1]{Riehl}), but they can also be drawn as adjunctions
(\cite[proposition 6.1.5]{Riehl}, \cite[section X.3]{CWM2}). Let's see
how to draw them in both ways at the same time in a way that makes the
translation clear. Here is the diagram:
%
%D diagram kan-1
%D 2Dx 100 +35
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +20 A2 - A3
%D 2D |
%D 2D +20 A4
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> GF ∀G
%D ren A2 A3 ==> RF R{:=}\Ran_FH
%D ren A4 ==> H
%D ren B0 B1 ==> \catC^\catA \catC^\catB
%D ren C0 C1 ==> \catA \catB
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l UF
%D A1 A3 -> .plabel= r ∃!U
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l T
%D A0 A4 -> .slide= -20pt .plabel= l ∀V
%D B0 B1 <- sl^ .plabel= a ∘F
%D B0 B1 -> sl_ .plabel= b \Ran_F
%D C0 C1 -> .plabel= a F
%D ))
%D enddiagram
%D
%D diagram kan-2-cells-1
%D 2Dx 100 +25 +25 +20 +25 +25 +20 +25 +25
%D 2D 100 A1 B1 C1
%D 2D / \ / \ / \\
%D 2D +25 A0 ---- A2 B0 ---- B2 C0 ---- C2
%D 2D
%D ren A0 A1 A2 ==> \catA \catB \catC
%D
%D (( A0 A1 -> .plabel= a F
%D A1 A2 -> .curve= _10pt .plabel= m R
%D A1 A2 -> .curve= ^20pt .plabel= a ∀G
%D A0 A2 -> .plabel= b H
%D A0 A2 midpoint relplace -4 -8 \Dn{T}
%D A1 A2 midpoint relplace 2 -3 \Dn{∃!U}
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-1}
\qquad
\quad
\slowdiag{kan-2-cells-1}
$$
%
We will consider right Kan extensions only.
Fix $F:\catA→\catB$ and a category $\catC$. We have a functor
$(∘F):\catC^\catB→\catC^\catA$. Suppose that it has a right adjoint,
$(∘F)⊣\Ran_F$. For each natural transformation $H:\catA→\catC$ its
image by $\Ran_f$, $R:=\Ran_FH$, is a natural transformation
$R:\catB→\catC$. We have:
%
$$\begin{array}{rcl}
(∘F) &⊣& \Ran_H \\
\Hom_{\catC^\catA}((∘F)-,-) &≅& \Hom_{\catC^\catB}(-,\Ran_F-), \\
\Hom_{\catC^\catA}((∘F)G,H) &≅& \Hom_{\catC^\catB}(G,\Ran_FH), \\
\Hom_{\catC^\catA} (G∘F,H) &≅& \Hom_{\catC^\catB}(G,\Ran_FH), \\
\Hom_{\catC^\catA}(GF,H) &≅& \Hom_{\catC^\catB}(G,R) \\
\end{array}
$$
%
and if we substitute $[G := R]$ in $\Hom_{\catC^\catB}(G,R)$ and we
transpose $\id_R$ to the left we obtain a morphism $T:RF→H$. The pair
$(R,H)$ obeys a certain universal property, that we will call
``Ran-ness'':
%
%$$∀G:\catB→\catC. \;\; ∀V:GF→H. \;\; ∃!U:G→R. \;\; (T·UF)=V.$$
$$∀G. \; ∀V. \; ∃!U. \; (T·UF)=V.$$
The usual way of defining right Kan extensions is by starting with the
functors $F:\catA→\catB$ and $H:\catA→\catC$ and then saying that a
pair $(R,T)$ is {\sl a} right Kan extension of $H$ along $F$ iff it
obeys Ran-ness; the functor $\Ran_F$ and the adjunction come later.
See \cite{Riehl}, section 6.1.
Note that we don't draw the `$∀V:GF→H$' in the right half of the
diagram --- it would overwrite the rest.
\newpage
% _ _ _ _
% / \ | | | ___ ___ _ __ ___ ___ _ __ | |_ ___
% / _ \ | | | / __/ _ \| '_ \ / __/ _ \ '_ \| __/ __|
% / ___ \| | | | (_| (_) | | | | (_| __/ |_) | |_\__ \
% /_/ \_\_|_| \___\___/|_| |_|\___\___| .__/ \__|___/
% |_|
%
% «all-concepts» (to ".all-concepts")
% Orig: (favp 46 "all-concepts")
% (fava "all-concepts")
% sec:
\subsection{All concepts are Kan extensions}
\label{all-concepts}
Both \cite{CWM2} and \cite{Riehl} have sections called ``All concepts
are Kan extensions'' --- section X.7 in \cite{CWM2} and 6.5 in
\cite{Riehl}. Now that we have a favorite way of drawing right Kan
extensions we can use it to draw diagrams for 1) binary products in
$\Set$ are right Kan extensions, 2) limits are right Kan extensions
and 3) left adjoints are right Kan extensions. Here they are.
\def\bu{{•}}
\def\bubu{{••}}
\begin{enumerate}
\item Let $\bubu$ be the discrete category with two objects, $\bu$ be
the discrete category with one object, and $!:\bubu→\bu$ be the
unique functor from $\bubu$ to $\bu$. Then:
%
%D diagram kan-binary-prods
%D 2Dx 100 +40
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +20 A2 - A3
%D 2D |
%D 2D +20 A4
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> GF ∀G
%D ren A2 A3 ==> RF R{:=}\Ran_FH
%D ren A4 ==> H
%D ren B0 B1 ==> \Set^\bubu \Set^•
%D ren C0 C1 ==> \bubu •
%D
%D ren A0 A1 ==> (X,X) ∀X
%D ren A2 A3 ==> (Y{×}Z,Y{×}Z) Y{×}Z
%D ren A4 ==> (Y,Z)
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l (h,h)
%D A1 A3 -> .plabel= r ∃!h
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l (π,π')
%D A0 A4 -> .slide= -40pt .plabel= l ∀(f,g)
%D B0 B1 <- sl^ .plabel= a Δ:=(∘!)
%D B0 B1 -> sl_ .plabel= b \lim:=\Ran_!
%D C0 C1 -> .plabel= a !
%D ))
%D enddiagram
%D
%D diagram kan-2-cells-binary-prods
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D / \
%D 2D +30 A0 ---- A2
%D 2D
%D ren A0 A1 A2 ==> \catA \catB \catC
%D ren A0 A1 A2 ==> \bubu \bu \Set
%D
%D ((
%D A0 A1 -> .plabel= a !
%D A1 A2 -> .curve= _10pt .plabel= m Y×Z
%D A1 A2 -> .curve= ^20pt .plabel= a ∀X
%D A0 A2 -> .plabel= b (Y,Z)
%D A0 A2 midpoint relplace -6 -8 \Dn{(π,π')}
%D A1 A2 midpoint relplace 2 -5 \Dn{∃!h}
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-binary-prods}
\qquad
\quad
\slowdiag{kan-2-cells-binary-prods}
$$
\item Let $\catI$ be a finite index category --- for example, $\catI =
\psm{&&1 \\ &&↓ \\ 2&→&3}$ --- and let $\catC$ be a category with
finite limits. A functor $D:\catI→\catC$ is a diagram of shape
$\catI$ in $\catC$. Let's denote by $\bm1$ the discrete category
with a single object --- the name `$\bm1$' is more standard than
`$•$'. Then:
%
%D diagram kan-prods
%D 2Dx 100 +40
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +20 A2 - A3
%D 2D |
%D 2D +20 A4
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> ΔC ∀C
%D ren A2 A3 ==> RF R{:=}\Ran_FH
%D ren A4 ==> H
%D ren B0 B1 ==> \catC^\catI \catC^{\bm1}
%D ren C0 C1 ==> \catI \bm1
%D
%D ren A0 A1 ==> ΔX ∀X
%D ren A2 A3 ==> Δ\lim_{\catI}D \lim_{\catI}D
%D ren A4 ==> D
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l Δf
%D A1 A3 -> .plabel= r ∃!f
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l ε
%D A0 A4 -> .slide= -30pt .plabel= l ∀γ
%D B0 B1 <- sl^ .plabel= a Δ:=(∘!)
%D B0 B1 -> sl_ .plabel= b \lim:=\Ran_!
%D C0 C1 -> .plabel= a !
%D ))
%D enddiagram
%D
%D diagram kan-2-cells-prods
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D / \
%D 2D +30 A0 ---- A2
%D 2D
%D ren A0 A1 A2 ==> \catI \bm1 \catC
%D
%D ((
%D A0 A1 -> .plabel= a !
%D A1 A2 -> .curve= _10pt .plabel= m \lim_{\catI}D
%D A1 A2 -> .curve= ^20pt .plabel= a ∀X
%D A0 A2 -> .plabel= b D
%D A0 A2 midpoint relplace -4 -8 \Dn{ε}
%D A1 A2 midpoint relplace 2 -5 \Dn{∃!f}
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-prods}
\qquad
\quad
\slowdiag{kan-2-cells-prods}
$$
\newpage
\item Left adjoints are right Kan extensions. If
%
$$\catB \two/<-`->/<200>^L_R \catA$$
%
is an adjunction, then $(L,ε)$ is a right Kan extension of $\id_\catB$
along $R$. In a more compact notation, $L:=\Ran_R \id_\catB$ --- but
in this case we only know the action of $\Ran_R$ on the object
$\id_\catB$, and we don't know if this $\Ran_R$ can be extended to a
``real'' functor whose domain is the whole of $\catB^\catB$. The
diagram is:
%
%D diagram kan-adjoints
%D 2Dx 100 +40
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +20 A2 - A3
%D 2D |
%D 2D +20 A4
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> GR ∀G
%D ren A2 A3 ==> LR L{:=}\Ran_R\id_\catB
%D ren A4 ==> \id_\catB
%D ren B0 B1 ==> \catB^\catB \catB^\catA
%D ren C0 C1 ==> \catB \catA
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l UR
%D A1 A3 -> .plabel= r ∃!U
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l ε
%D A0 A4 -> .slide= -20pt .plabel= l ∀V
%D B0 B1 <- sl^ .plabel= a (∘R)
%D B0 B1 -> sl_ .plabel= b \Ran_R
%D C0 C1 -> .plabel= a R
%D ))
%D enddiagram
%D
%D diagram kan-2-cells-adjoints
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D / \
%D 2D +30 A0 ---- A2
%D 2D
%D ren A0 A1 A2 ==> \catB \catA \catB
%D
%D ((
%D A0 A1 -> .plabel= a R
%D A1 A2 -> .curve= _10pt .plabel= m L
%D A1 A2 -> .curve= ^20pt .plabel= a ∀G
%D A0 A2 -> .plabel= b \id_\catB
%D A0 A2 midpoint relplace -4 -8 \Dn{ε}
%D A1 A2 midpoint relplace 2 -5 \Dn{∃!U}
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-adjoints}
\qquad
\quad
\slowdiag{kan-2-cells-adjoints}
$$
To show that this works we have to prove that $∀V.∃!U.(ε·UR=V)$. We
will do that by ``inverting the equation $ε·UR=V$'':
%
%D diagram kan-adjoints-solving-U
%D 2Dx 100 +20 +20 +20 +25 +20 +20 +20
%D 2D _________ ____ _________ ____
%D 2D | || | | || |
%D 2D 100 A0 - A1 - A2 - A3 = B0 - B1 B2 - B3
%D 2D |__________| |__________|
%D 2D
%D 2D ||
%D 2D _________ ____
%D 2D | || |
%D 2D +50 C0 - C1 - C2 C3
%D 2D |__________|
%D 2D
%D 2D
%D ren A0 A1 A2 A3 ==> \catA \catB \catA \catB
%D ren B0 B1 B2 B3 ==> \catA \catB \catA \catB
%D ren C0 C1 C2 C3 ==> \catA \catB \catA \catB
%D
%D (( A0 A1 -> .plabel= b L
%D A1 A2 -> .plabel= b R
%D A2 A3 -> .plabel= b L
%D A0 A2 -> .curve= ^25pt .plabel= a \id_A
%D A2 A3 -> .curve= ^24pt .plabel= a G
%D A1 A3 -> .curve= _25pt .plabel= b \id_B
%D A0 A2 midpoint relplace 0 -8 \Dn{η}
%D A2 A3 midpoint relplace 0 -6 \Dn{U}
%D A1 A3 midpoint relplace 0 7 \Dn{ε}
%D
%D A3 B0 midpoint relplace 0 0 =
%D
%D B0 B1 -> .plabel= b L
%D # B1 B2 -> .plabel= b R
%D B2 B3 -> .plabel= b L
%D B0 B2 -> .curve= ^25pt .plabel= a \id_A
%D B2 B3 -> .curve= ^24pt .plabel= a G
%D B1 B3 -> .curve= _25pt .plabel= b \id_B
%D B2 B3 midpoint relplace 0 -6 \Dn{U}
%D B1 B2 midpoint relplace 1 2 \Dn{\id_L}
%D
%D B3 relplace 20 0 =\;U
%D
%D A1 C2 midpoint relplace 0 2 \veq
%D
%D C0 C1 -> .plabel= b L
%D C1 C2 -> .plabel= b R
%D # C2 C3 -> .plabel= b L
%D C0 C2 -> .curve= ^25pt .plabel= a \id_A
%D C2 C3 -> .curve= ^24pt .plabel= a G
%D C1 C3 -> .curve= _25pt .plabel= b \id_B
%D C0 C2 midpoint relplace 0 -8 \Dn{η}
%D C2 C3 midpoint relplace 0 2 \Dn{V}
%D
%D C3 relplace 25 0 =\;VL·η
%D ))
%D enddiagram
%D
$$\pu
\slowdiag{kan-adjoints-solving-U}
$$
%
The solution in $U:=VL·Gη$.
% (riep 5 "6.1._kan-extensions")
% (rie "6.1._kan-extensions")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 233) "X. Kan Extensions")
% (find-cwm2page (+ 13 248) "7. All Concepts Are Kan Extensions")
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 209) "6.5. All concepts")
\end{enumerate}
% _ __ __ _
% | |/ /__ _ _ __ / _| ___ _ __ _ __ ___ _ _| | __ _
% | ' // _` | '_ \ | |_ / _ \| '__| '_ ` _ \| | | | |/ _` |
% | . \ (_| | | | | | _| (_) | | | | | | | | |_| | | (_| |
% |_|\_\__,_|_| |_| |_| \___/|_| |_| |_| |_|\__,_|_|\__,_|
%
% «kan-formula» (to ".kan-formula")
% Orig: (favp 38 "kan-formula")
% (fava "kan-formula")
% sec:
\subsection{A formula for Kan extensions}
\label{kan-formula}
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 236) "3. The Kan Extension")
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 193) "6.2. A formula for Kan extensions")
\def\piAHSet {\ton{π} \catA \ton{H} \Set}
\def\piAHSetmini{\xton{H∘π} \Set}
\def\pdiag #1{\left(\diag{#1}\right)}
The sections X.3 of \cite{CWM2} and 6.2 of \cite{Riehl} discuss a
formula for calculating Kan extensions, that defines $\Ran_FH$ as the
functor whose action on objects is:
%
$$B \mapsto \Lim(B{↓}F \piAHSet),$$
%
and its action on morphisms is ``obvious'' in the sense of Section
\ref{to-deserve-a-name}. I found this formula totally impossible to
understand until I finally found a way to visualize what it ``meant''.
For each object $B∈\catB$ the functor $B{↓}F \piAHSetmini$ can be
regarded as a diagram in $\Set$ whose shape is the shape of the comma
category $B{↓}F$. If $\catA$ and $\catB$ are finite preorder categories
and $F$ is an inclusion then $B{↓}F$ can ``inherit its shape'' from
$\catA$; inclusions of preorders are ``toy examples'' ``for
children'', but they give us some intuition to start with, and they
can help us understand the formal version that can handle more general
cases.
These are the diagrams for $\Ran_F$ as a right adjoint --- note that
we use $\Set$ instead of $\catC$ to make things less abstract,
%
% (favp 45 "kan-extensions")
% (fava "kan-extensions")
%
%D diagram kan-1
%D 2Dx 100 +35
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +25 A2 - A3
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> GF G
%D ren A2 A3 ==> H \Ran_FH
%D ren B0 B1 ==> \Set^\catA \Set^\catB
%D ren C0 C1 ==> \catA \catB
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l V
%D A1 A3 -> .plabel= r U
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 |->
%D A3 relplace 20 0 =R
%D B0 B1 <- sl^ .plabel= a ∘F
%D B0 B1 -> sl_ .plabel= b \Ran_F
%D C0 C1 -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-1}
\qquad
\begin{array}{l}
RB = \\
(\Ran_FH)B = \\
\Lim(B{↓}F \piAHSet) \\
\end{array}
$$
%
and here are some diagrams to help us understand the comma category
$B{↓}F$ --- in the compact notation its objects have names like
$(A,β)$, but in the more visual notation they are L-shaped diagrams:
%
%D diagram CommaObj
%D 2Dx 100 +20
%D 2D 100 \A
%D 2D
%D 2D +15 \B \C
%D 2D
%D # ren ==>
%D
%D (( \A \C -> .plabel= r \f
%D \B \C |->
%D ))
%D enddiagram
%D
\pu
\def\CommaObj#1#2#3#4{
\def\A{#1}
\def\f{#4}
\def\B{#2} \def\C{#3}
\left(\diag{CommaObj}\right)
}
%
\def\kancommaobj#1#2#3{\psm{  \\ #2 \\}}
%
%D diagram kan-comma
%D 2Dx 100 +20 +55 +45 +30 +25
%D 2D 100 A1
%D 2D +20 A2 - A3 C0 E0 - E1 - E2
%D 2D +20 A4 - A5 C1 E3 - E4 - E5
%D 2D
%D 2D +15 B0 - B1 D0 F0 - F1 - F2
%D 2D
%D ren A1 A2 A3 A4 A5 ==> B A FA A' FA'
%D ren B0 B1 ==> \catA \catB
%D ren D0 ==> B{↓}F
%D ren E0 E1 E2 ==> (A,β) A HA
%D ren E3 E4 E5 ==> (A',β') A' HA'
%D ren F0 F1 F2 ==> B{↓}F \catA \Set
%D
%D (( A1 A3 -> .plabel= r β
%D A2 A3 |->
%D A2 A4 -> .plabel= l α
%D A3 A5 -> .plabel= r Fα
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D A1 A5 -> .slide= 20pt .plabel= r \sm{β'=\\Fα∘β}
%D B0 B1 -> .plabel= a F
%D
%D C0 xy+= 0 -20
%D C1 xy+= 0 -5
%D C0 .tex= \CommaObj{B}{A}{FA}{β} BOX
%D C1 .tex= \CommaObj{B}{A'}{FA'}{β'} BOX
%D C0 C1 -> .plabel= l α
%D D0 place
%D
%D E0 E1 |-> E1 E2 |->
%D E0 E3 -> .plabel= l α
%D E1 E4 -> .plabel= m α
%D E2 E5 -> .plabel= r Hα
%D E0 E4 harrownodes nil 20 nil |->
%D E1 E5 harrownodes nil 20 nil |->
%D E3 E4 |-> E4 E5 |->
%D F0 F1 -> .plabel= a π
%D F1 F2 -> .plabel= a H
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-comma}
$$
\newpage
\def\kancommaobj#1#2#3{\psm{  \\ #2 \\}}
Let's see an example.
%D diagram Kan_catA
%D 2Dx 100 +15
%D 2D 100 1 2
%D 2D +15 3 4
%D 2D +15 5 6
%D 2D
%D # ren 1 2 3 4 5 6 ==> 1' 2' 3' 4' 5' 6'
%D
%D (( 2 6 ->
%D 5 6 ->
%D
%D ))
%D enddiagram
%D
%D diagram Kan_catB
%D 2Dx 100 +15
%D 2D 100 1 2
%D 2D +15 3 4
%D 2D +15 5 6
%D 2D
%D ren 1 2 3 4 5 6 ==> 1' 2' 3' 4' 5' 6'
%D
%D (( 1 2 ->
%D 1 3 -> 2 4 ->
%D 3 4 ->
%D 3 5 -> 4 6 ->
%D 5 6 ->
%D ))
%D enddiagram
%D
%D
%D
%D diagram Kan_1'_down_F
%D 2Dx 100 +30
%D 2D 100 A1
%D 2D +15
%D 2D +15 A4 A5
%D 2D
%D ren A1 ==> \kancommaobj{1'}{2}{F2}
%D ren A4 A5 ==> \kancommaobj{1'}{5}{F5} \kancommaobj{1'}{6}{F6}
%D
%D (( A1 A5 ->
%D A4 A5 ->
%D ))
%D enddiagram
%D
%D diagram Kan_3'_down_F
%D 2Dx 100 +30
%D 2D 100 A1
%D 2D +15
%D 2D +15 A4 A5
%D 2D
%D ren A1 ==> \ph{\kancommaobj{3'}{2}{F2}}
%D ren A4 A5 ==> \kancommaobj{3'}{5}{F5} \kancommaobj{3'}{6}{F6}
%D
%D (( A1 place
%D A4 A5 ->
%D ))
%D enddiagram
%D
%D
%D
%D diagram Kan_1'_H
%D 2Dx 100 +20
%D 2D 100 A1
%D 2D +15
%D 2D +15 A4 A5
%D 2D
%D ren A1 ==> H_2
%D ren A4 A5 ==> H_5 H_6
%D
%D (( A1 A5 ->
%D A4 A5 ->
%D ))
%D enddiagram
%D
%D diagram Kan_3'_H
%D 2Dx 100 +20
%D 2D 100 A1
%D 2D +15
%D 2D +15 A4 A5
%D 2D
%D ren A1 ==> \ph{H_2}
%D ren A4 A5 ==> H_5 H_6
%D
%D (( A1 place
%D A4 A5 ->
%D ))
%D enddiagram
%D
\pu
If $\catA \ton{F} \catB$ is the inclusion $\pdiag{Kan_catA} →
\pdiag{Kan_catB}$,
\msk
then
$1'{↓}F = \pdiag{Kan_1'_down_F}$ and
$3'{↓}F = \pdiag{Kan_3'_down_F}$,
\msk
and $(1'{↓}F \piAHSetmini) = \pdiag{Kan_1'_H}$
and $(3'{↓}F \piAHSetmini) = \pdiag{Kan_3'_H}$;
\msk
so $R(1') = \Lim(1'{↓}F \piAHSetmini) = H_2 ×_{H_6} H_5$,
and $R(3') = \Lim(3'{↓}F \piAHSetmini) = H_5$.
We can follow the same pattern to calculate $R(2')$, $R(4')$, $R(5')$,
$R(6')$.
The square of the adjunction becomes this, in this particular case:
%
%D diagram Kan_A-shaped
%D 2Dx 100 +20
%D 2D 100 2
%D 2D +20
%D 2D +20 5 6
%D 2D
%D ren 2 5 6 ==> \A \B \C
%D
%D (( 2 6 ->
%D 5 6 ->
%D ))
%D enddiagram
%D
%D diagram Kan_B-shaped
%D 2Dx 100 +30
%D 2D 100 1 2
%D 2D +20 3 4
%D 2D +20 5 6
%D 2D
%D ren 1 2 3 4 5 6 ==> \A \B \C \D \E \F
%D
%D (( 1 2 ->
%D 1 3 -> 2 4 ->
%D 3 4 ->
%D 3 5 -> 4 6 ->
%D 5 6 ->
%D ))
%D enddiagram
%D
\pu
\def\KanAShaped#1#2#3{
\def\A{#1}
\def\B{#2}
\def\C{#3}
\pdiag{Kan_A-shaped}
}
\def\KanBShaped#1#2#3#4#5#6{
\def\A{#1}
\def\B{#2}
\def\C{#3}
\def\D{#4}
\def\E{#5}
\def\F{#6}
\pdiag{Kan_B-shaped}
}
%
%D diagram kanadjsquare-generic
%D 2Dx 100 +25
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +25 A2 - A3
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> GF G
%D ren A2 A3 ==> H \Ran_FH
%D ren B0 B1 ==> \Set^\catA \Set^\catB
%D ren C0 C1 ==> \catA \catB
%D
%D (( A0 A1 <-|
%D A0 A2 -> # .plabel= l V
%D A1 A3 -> # .plabel= r U
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 |->
%D A3 relplace 20 0 =R
%D # B0 B1 <- sl^ .plabel= a ∘F
%D # B0 B1 -> sl_ .plabel= b \Ran_F
%D # C0 C1 -> .plabel= a F
%D ))
%D enddiagram
%D
%D diagram kanadjsquare-example
%D 2Dx 100 +70
%D 2D 100 A0 A1
%D 2D
%D 2D +65 A2 A3
%D 2D
%D (( A0 .tex= \KanAShaped{G_2}{G_5}{G_6} BOX
%D A1 .tex= \KanBShaped{G_1}{G_2}{G_3}{G_4}{G_5}{G_6} BOX
%D A2 .tex= \KanAShaped{H_2}{H_5}{H_6} BOX
%D A3 .tex= \KanBShaped{H_2{×_{H_6}}H_5}{H_2}{H_5}{H_6}{H_5}{H_6} BOX
%D ))
%D (( A0 A1 <-|
%D A0 A2 ->
%D A1 A3 ->
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 |->
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{kanadjsquare-generic}
\qquad
\diag{kanadjsquare-example}
$$
\newpage
% _____ _ _ _
% | ___| _ _ __ ___| |_ ___ _ __ ___ __ _ ___ ___ | |__ (_)___
% | |_ | | | | '_ \ / __| __/ _ \| '__/ __| / _` / __| / _ \| '_ \| / __|
% | _|| |_| | | | | (__| || (_) | | \__ \ | (_| \__ \ | (_) | |_) | \__ \
% |_| \__,_|_| |_|\___|\__\___/|_| |___/ \__,_|___/ \___/|_.__// |___/
% |__/
% «functors-as-objects» (to ".functors-as-objects")
% Orig: (favp 50 "functors-as-objects")
% (fava "functors-as-objects")
% sec:
\subsection{Functors as objects \DONE}
\label{functors-as-objects}
One way to treat a diagram in $\Set$ like this
%
%D diagram evil-presheaf
%D 2Dx 100 +20 +20
%D 2D 100 A0
%D 2D / \
%D 2D +20 A1 A2
%D 2D \ /
%D 2D +20 A3
%D 2D |
%D 2D +20 A4
%D 2D
%D ren A0 A1 A2 A3 A4 ==> \{24,25\} \{1\} \{2,3\} \{1\} \{0,1\}
%D
%D (( A0 A1 ->
%D A0 A2 -> .plabel= r \sm{24↦2\\25↦2}
%D A1 A3 ->
%D A2 A3 ->
%D A3 A4 -> .plabel= r 1↦1
%D ))
%D enddiagram
%D
\pu
$$
F \qquad := \qquad \diag{evil-presheaf}
$$
%
as a functor is to think that that diagram is an abbreviation --- it
is just the upper-right part of a diagram like this,
%
%R local kite =
%R 1/ 1 \
%R |2 3|
%R | 4 |
%R \ 5 /
%R MixedPicture.__index.
%R arrows = function (mp, w) return (mp.ar or mp.zha):arrows(w) end
%R kite:tozmp({zdef="kitewitharrows", meta="p", scale="20pt"})
%R :addcells()
%R :addarrows()
%R :output()
\pu
% $$\zha{kitewitharrows}$$
%
%D diagram evil-presheaf-as-functor
%D 2Dx 100 +75
%D 2D 100 A0 A1
%D 2D
%D 2D +50 A2 A3
%D 2D
%D ren A0 ==> \zha{kitewitharrows}
%D ren A2 A3 ==> \catK \Set
%D
%D (( A1 .tex= \left(\diag{evil-presheaf}\right) BOX
%D A0 A1 |->
%D A2 A3 -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
\diag{evil-presheaf-as-functor}
$$
%
where we add the extra hint that the index category $\catK$ is exactly
the kite-shaped preorder category drawn above the ``$\catK$''.
The convention (CFSh) says that the image by a functor of a diagram is
a diagram with the same shape, so according to that convention we have
$F(1) = \{24,25\}$, $F(4→5) = (\{1\} \ton{1↦1} \{0,1\})$, and so
on; so the upper right part of the diagram above {\sl defines} $F$.
Note that the single `$↦$' above the $\catK \ton{F} \Set$ stands for
several `$↦$'s, one for each object and one for each morphism, and
note that $F$ is an object of $\Set^\catK$.
% ____ __ __ __ _ _ _ _
% / ___| \/ |___ / _| ___ _ __ ___| |__ (_) | __| |_ __ ___ _ __
% | | _| |\/| / __| | |_ / _ \| '__| / __| '_ \| | |/ _` | '__/ _ \ '_ \
% | |_| | | | \__ \ | _| (_) | | | (__| | | | | | (_| | | | __/ | | |
% \____|_| |_|___/ |_| \___/|_| \___|_| |_|_|_|\__,_|_| \___|_| |_|
%
% «gms-for-children» (to ".gms-for-children")
% Orig: (favp 38 "gms-for-children")
% (fava "gms-for-children")
% sec:
\subsection{Geometric morphisms for children \DONE}
\label{gms-for-children}
Let $\catA$ and $\catB$ be these preorder categories, and let
$f:\catA→\catB$ be the inclusion functor from $\catA$ to $\catB$:
%
$$
A := \pshAargs2345
\qquad
B := \pshBargs123456
$$
The left half of the diagram below is the standard definition of a
geometric morphism $f$ from a topos $\calE$ to a topos $\calF$. A
geometric morphism $f:\calE→\calF$ is actually an adjunction $f^*⊣f_*$
plus the guarantee that $f^*:\calE \ot \calF$ preserves limits, which
is a condition slightly weaker than requiring that $f^*$ has a left
adjoint. When that left adjoint exists it is denoted by $f^!$, and we
say that $f^!⊣f^*⊣f_*$ is an {\sl essential geometric morphism}. The
only non-standard thing about the diagram at the left below is that is
contains an internal view of the adjunction $f^*⊣f_*$.
%
$$
\diag{gm-for-adults}
\qquad
\def\LG{\pshAargs{G_2}{G_3}{G_4}{G_5}}
\def\G {\pshBargs{G_1}{G_2}{G_3}{G_4}{G_5}{G_6}}
\def\H {\pshAargs{H_2}{H_3}{H_4}{H_5}}
\def\RH{\pshBargs{H_2{×_{H_4}}H_3}{H_2}{H_3}{H_4}{H_5}{1}}
\diag{gm-for-children}
$$
The right half of the diagram is a particular case of the left half.
Its lower line, $\catA \ton{f} \catB$, does not exist in the left
half. The inclusion functor $f$ induces adjunctions $f^!⊣f^*⊣f_*$ as
this,
%
%D diagram essential-GM-small
%D 2Dx 100 +35
%D 2D 100 A B
%D 2D
%D 2D +20 A0 B0
%D 2D
%D ren A B ==> \Set^\catA \Set^\catB
%D ren A0 B0 ==> \catA \catB
%D
%D (( A B -> sl^^ .plabel= a f^!
%D A B <- .plabel= m f^*
%D A B -> sl__ .plabel= b f_*
%D A0 B0 -> .plabel= a f
%D ))
%D enddiagram
%D
$$\pu
\diag{essential-GM-small}
$$
%
where $f^*$ is easy to define and $f^!$ and $f_*$ not so much --- the
standard way to define $f^!$ and $f_*$ is by Kan extensions.
The big square in the upper part of the diagram is an internal view of
the adjunction $f^*⊣f_*$, with the functors $f^*G$, $G$, $H$, and
$f_*H$ being displayed as their internal views. We can choose the sets
$G_1, \ldots, G_6$ and the morphisms between them arbitrarily, so this
is an internal view of an arbitrary functor $G:\catB→\Set$; and the
same for $H$.
The arrow $f^*G \mapsot G$ can be read as a definition for the action
of $f^*$ on objects --- it just erases some parts of the diagram ---
and the arrow $H \mapsto f_*H$ can be read as a definition for the
action of $f_*$ on objects --- $f_*$ ``reconstructs'' $H_1$ and $H_6$
in a certain natural way. It is easy to reconstruct the actions of
$f^*$ and $f_*$ on morphisms from just what is shown, and to
reconstruct the two directions of the bijection.
The big diagram above can be used 1) to convince categorists who are
not seasoned toposophers that this diagrammatic language can make some
difficult categorical concepts more accessible, and 2) as a starting
point to generate diagrams ``for children'' for several parts of the
Elephant (\cite{Elephant1}), and even to prove new theorems on
toposes. For more on (1), see \cite{OchsLucatelli} and
\cite{OchsVGMS2018}; for (2), see \cite{MDE}.
% «reading-the-elephant» (to ".reading-the-elephant")
% Orig: (favp 52 "reading-the-elephant")
% (fava "reading-the-elephant")
% sec: 7.14
% «how-to-name-this-language» (to ".how-to-name-this-language")
% Orig: (favp 54 "how-to-name-this-language")
% (fava "how-to-name-this-language")
% sec: 8
% __ ___ _ _ _ _
% \ \ / / |__ _ _ ( | )_ __ ___ _ _ ___ ___ _ ____ _____( | )
% \ \ /\ / /| '_ \| | | | V V| '_ ` _ \| | | | / __/ _ \| '_ \ \ / / __|V V
% \ V V / | | | | |_| | | | | | | | |_| | | (_| (_) | | | \ V /\__ \
% \_/\_/ |_| |_|\__, | |_| |_| |_|\__, | \___\___/|_| |_|\_/ |___/
% |___/ |___/
%
% «why-my-conventions» (to ".why-my-conventions")
% Orig: (favp 54 "why-my-conventions")
% (fava "why-my-conventions")
% sec: 9
% \section{Why ``my conventions''? \DONE}
% \label{why-my-conventions}
% \standout{TODO:} redo, rewrite, move to the introduction.
% \msk
% I learned CT as an autodidact in a totally disorganized way. In the
% first years I just read, or rather {\sl tried} to read, everything
% that was available in my university's library, trying to locate the
% parts that could be useful to my main interest at that time, that was
% Non-Standard Analysis and how to do something similar to NSA but using
% filter-powers instead of ultrapowers...
% It was only after that that I realized that I had to learn how to {\sl
% write}. I remember one time spending a whole evening on an exercise
% of the beginning of \cite{LambekScott} that says just ``prove that for
% categories $\catA$, $\catB$, and $\catC$ we have $\catA^{\catB×\catC}
% ≅ (\catA^\catB)^\catC$'' --- the full proof had lots of parts, and I
% saw that I didn't know how to organize them in a neat way... also, the
% proofs given in books and articles just state the main parts and
% pretend that the rest is obvious, and in the case of
% $\catA^{\catB×\catC} ≅ (\catA^\catB)^\catC$ there were no ``main
% parts'', so I had to learn how to write down a proof in full, and this
% was a new style to me...
% Even now, many years after that, I still have the sensation that I had
% to improvise practically everything in my ways --- both the
% ``algebraic'' way and the ``diagrammatic'' way --- of writing
% categorical proofs, and that I still don't know even a tiny fraction
% of the techniques for writing that people learn when they take CT
% courses and they have opportunities to discuss exercises with other
% students and with TAs and more senior people...
% \msk
% {\sl The ``my conventions'' in the title of this text, and my use of
% the first person everywhere, are a way to stress that I still don't
% know enough about other people's private languages for CT, and that
% this is an attempt to gain access to other private languages,
% diagrammatic or not... I am especially interested in how people
% write when they turn their level-of-detail knob to a very high
% position.}
% It is difficult to publish material about diagrammatic languages
% that are more for {\sl visualition} and {\sl intuition} (see
% \cite{KromerSlides}) than for {\sl proving things}. The handwritten
% notes in \cite{MacLaneNotes} for a course given by MacLane taken by
% one of his students indicate that when he wasn't constrained by what
% could be printed easily he would use several kinds of diagrams that
% are not in \cite{CWM2}. I guess that Freyd and Scedrov have
% experimented with many variants of the languages in \cite{Freyd76}
% and \cite{FreydScedrov} that they never published...
% ____ _ _ _ _
% | _ \ ___| | __ _| |_ ___ __| | __ _____ _ __| | __
% | |_) / _ \ |/ _` | __/ _ \/ _` | \ \ /\ / / _ \| '__| |/ /
% | _ < __/ | (_| | || __/ (_| | \ V V / (_) | | | <
% |_| \_\___|_|\__,_|\__\___|\__,_| \_/\_/ \___/|_| |_|\_\
%
% «related-and-unrelated» (to ".related-and-unrelated")
% (misp 59 "related-and-unrelated")
% (misa "related-and-unrelated")
% sec: 9
% Orig: (favp 55 "related-and-unrelated")
% (fava "related-and-unrelated")
% sec: 10
%
\section{Related and unrelated work \DONE}
\label{related-and-unrelated}
% (find-books "__cats/__cats.el" "coecke")
% (find-books "__cats/__cats.el" "coecke-newstrup")
% (find-books "__cats/__cats.el" "marsden-ctusd")
% (find-books "__cats/__cats.el" "selinger-surveygl")
The diagrammatic language that I described here seems to be unrelated
to the ones in \cite{CoeckePQP} and \cite{CoeckeNewStruP} --- that
describe {\sl lots} of diagrammatic languages --- and also unrelated
to \cite{MarsdenCTUSD}. We lower the level of abstraction --- see for
example Section \ref{2-category-of-cats} --- while they (usually)
raise it.
% (find-books "__cats/__cats.el" "caccamo-winskel")
I've taken an approach that is the opposite of \cite{CaccamoWinskel}
and \cite{CaccamoPhD}. Cáccamo and Winskel define a derivation system
that can only construct functors, natural transformations, etc, that
obey the expected naturality conditions, while we allow some kinds of
sloppinesses, like constructing something that looks like a functor
and pretending that it is a functor when it may not be. When I started
working on this diagrammatic language I had a companion derivation
system for it; \cite[Section 14]{IDARCT} mentions it briefly, but it
doesn't show the introduction rules that create (proto)functors and
(proto)natural transformations and that allow being sloppy (``in the
syntactical world''). That derivation system was incomplete in all
senses --- it even had ``rules'' that I knew how to apply in
particular cases but I didn't know how to formalize.
% (find-books "__phil/__phil.el" "corfield")
% (find-books "__cats/__cats.el" "kromer")
% (find-books "__cats/__cats.el" "kromer-slides")
% (find-books "__cats/__cats.el" "cheng-morally")
Some of my excuses for allowing one to pretend that a functor is a
functor and leaving the verification to a second stage come from
\cite{ChengMorally}. I learned a {\sl lot} on how mathematicians use
intuition and diagrams from \cite{Kromer} --- \cite{KromerSlides} is a
great summary --- and \cite{Corfield}, and they have helped me to
identify which characteristics of my diagrammatic language are very
unusual and may be new, and that deserve to be presented in detail.
% (find-idarctpage 19 "14. Preservations, Frobenius, Beck-Chevalley")
% (find-idarcttext 19 "14. Preservations, Frobenius, Beck-Chevalley")
Many of the first ideas for my diagrammatic language appeared when I
was reading \cite{SeelyBeck}, \cite{SeelyLCCC}, \cite{SeelyPLC},
\cite{Jacobs}, and \cite{SeelyDiff} and trying to draw the ``missing
diagrams'' in those papers in both the original notation and in the
``archetypal case'' (\cite[Section 16]{IDARCT}).
Many of the later ideas appeared when I was trying to understand
sheaves using a certain approach ``for children'' (\cite{PH2}): I
learned how to draw diagrams showing a Grothendieck topology, its
corresponding Lawvere-Tierney topology, and its corresponding nucleus
{\sl in particular cases}, and I knew that {\sl there had to be a way}
(in the sense of \cite{ChengMorally}) to ``lift'' these diagrams of
the correspondences in particular cases to a diagram of the
correspondences in the general case... the details of this ``lifting''
were hard to formalize, but missing details started to become clear
when I required the diagrams to be translatable to a pseudocode that
could be translated to Agda. At this moment \cite{PH2} is still
incomplete, but some of the ideas in DL were motivated by its
conceptual holes.
% (p2ap 27 "7._toposes")
% (p2aa "7._toposes")
% (find-idarctpage 23 "16. Archetypal Models")
% (find-idarcttext 23 "16. Archetypal Models")
% (find-books "__cats/__cats.el" "fong-spivak")
% (find-books "__cats/__cats.el" "milewski-ctfp")
% (find-books "__cats/__cats.el" "perrone")
% (find-books "__cats/__cats.el" "sobocinski")
% end of body
% «ifluatex-2» (to ".ifluatex-2")
% (find-dn6 "output.lua" "write_dnt_file")
%L write_dnt_file("2022on-the-missing.dnt")
\pu
% «references» (to ".references")
% (misp 60 "references")
% (misa "references")
% Orig: (favp 58 "references")
% (fava "references")
\printbibliography
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% _____ _
% | ____|_ __ __| |
% | _| | '_ \ / _` |
% | |___| | | | (_| |
% |_____|_| |_|\__,_|
%
% ----------------------------------------
% «save-body» (to ".save-body")
% For: (find-LATEX "2022ochs-meteor1.tex")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
pat = "\n%% beginning of body\n(.-)%% end of body"
fname_in = "~/LATEX/2022on-the-missing.tex"
fname_out = "~/LATEX/2022ochs-meteor1-body.tex"
bigstr = ee_readfile(fname_in)
body = bigstr:match(pat)
= #bigstr, #body
ee_writefile(fname_out, body)
-- (find-tkdiff "2022on-the-missing.tex" "2022ochs-meteor1-body.tex")
% «extract-cites» (to ".extract-cites")
% (find-angg "LUA/bib.lua" "meteor")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
fname = "~/LATEX/2022on-the-missing.tex"
bigstr = ee_readfile(fname)
bigstr2 = bigstr:gsub("\n%%[^\n]*", "")
for a,b in bigstr2:gmatch("(\\cite{(.-)})") do
printf("%-20s %s\n", b, a)
end
for a,b,c in bigstr2:gmatch("(\\cite%[(.-)%]{(.-)})") do
aa = a:gsub("%s+", " ")
printf("%-20s %s\n", c, aa)
end
% _____ _
% |_ _|__ __| | ___
% | |/ _ \ / _` |/ _ \
% | | (_) | | (_| | (_) |
% |_|\___/ \__,_|\___/
%
% «TODO» (to ".TODO")
% Trebor: https://mail.google.com/mail/u/0/#inbox/FMfcgzGtwqFHBBKrWsvPTVMDJsnNSvzh
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% «make-arxiv» (to ".make-arxiv")
% (find-LATEX "2020clops-and-tops.tex" "arxiv")
% (find-build-for-arxiv-links "2022on-the-missing")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/LATEX/
#export PATH=/usr/local/texlive/2016/bin/x86_64-linux:$PATH
#export PATH=/usr/local/texlive/2019/bin/x86_64-linux:$PATH
export PATH=/usr/local/texlive/2020/bin/x86_64-linux:$PATH
#export PATH=/usr/local/bin:$PATH
which biber
biber --version
make -f 2019.mk STEM=2022on-the-missing veryclean
lualatex 2022on-the-missing.tex
biber 2022on-the-missing
pdflatex -record 2022on-the-missing.tex
# (find-LATEXfile "2022on-the-missing.fls" "biblatex/")
cd ~/LATEX/
flsfiles-zip 2022on-the-missing.fls 2022on-the-missing.zip
rm -rfv /tmp/2022on-the-missing.zip
rm -rfv /tmp/edrx-latex/
cd /tmp/
cp -v ~/LATEX/2022on-the-missing.zip .
mkdir /tmp/edrx-latex/
unzip -d /tmp/edrx-latex/ /tmp/2022on-the-missing.zip
cd /tmp/edrx-latex/
pdflatex 2022on-the-missing.tex
pdflatex 2022on-the-missing.tex
cp -v 2022on-the-missing.pdf /tmp/
# (find-pdf-page "/tmp/edrx-latex/2022on-the-missing.pdf")
# (find-pdf-text "/tmp/edrx-latex/2022on-the-missing.pdf")
# (find-fline "/tmp/edrx-latex/")
# (find-fline "/tmp/edrx-latex/2022on-the-missing.bbl")
# (find-fline "/tmp/edrx-latex/2022on-the-missing.bbl" "version")
# (find-fline "/usr/local/texlive/")
# (find-fline "/usr/local/texlive/" "2019")
# (find-fline "/tmp/2022on-the-missing.zip")
# Package biblatex Warning: File '2022on-the-missing.bbl' is wrong format version
# - expected 3.1.
% «make» (to ".make")
% (to "defs-slowdiag")
% (find-LATEX "catsem-slides.bib")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
# (find-LATEXfile "2019.mk")
make -f 2019.mk STEM=2022on-the-missing veryclean
make -f 2019.mk STEM=2022on-the-missing pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "mis"
% End: