|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2019newton-slides.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019newton-slides.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019newton-slides.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019newton-slides.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2019newton-slides; makeindex 2019newton-slides"))
% (defun e () (interactive) (find-LATEX "2019newton-slides.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019newton-slides"))
% (setq revert-without-query '("pdf$"))
% (find-pdf-page "~/LATEX/2019newton-slides.pdf")
% (find-sh0 "cp -v ~/LATEX/2019newton-slides.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019newton-slides.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019newton-slides.pdf
% file:///tmp/2019newton-slides.pdf
% file:///tmp/pen/2019newton-slides.pdf
% http://angg.twu.net/LATEX/2019newton-slides.pdf
%
% (find-TH "math-b" "2019-newton")
% «.defs» (to "defs")
% «.title-page» (to "title-page")
% «.introduction» (to "introduction")
% «.introduction-2» (to "introduction-2")
% «.functions-and-names» (to "functions-and-names")
% «.lambda» (to "lambda")
% «.internal-diagrams» (to "internal-diagrams")
% «.internal-diagrams-in-cats» (to "internal-diagrams-in-cats")
% «.BCC» (to "BCC")
% «.what-to-understand» (to "what-to-understand")
% «.parallel-diagrams» (to "parallel-diagrams")
% «.parallel-diagrams-lfc» (to "parallel-diagrams-lfc")
% «.example-in-topos» (to "example-in-topos")
% «.example-in-topos-2» (to "example-in-topos-2")
% «.see-them-as-lambda-terms» (to "see-them-as-lambda-terms")
% «.yoneda-1» (to "yoneda-1")
% «.yoneda-2» (to "yoneda-2")
% «.idris-ct» (to "idris-ct")
% «.skeletons-1» (to "skeletons-1")
% «.skeletons-2» (to "skeletons-2")
% «.skeletons-3» (to "skeletons-3")
% «.the» (to "the")
% «.term-search» (to "term-search")
% «.term-search-2» (to "term-search-2")
% «.int-ext-gen-part» (to "int-ext-gen-part")
\documentclass[oneside]{book}
\usepackage[colorlinks,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\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
%
\usepackage{edrx15} % (find-LATEX "edrx15.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
%
% (find-es "tex" "geometry")
\usepackage[paperwidth=11.5cm, paperheight=9.5cm,
%total={6.5in,4in},
%textwidth=4in, paperwidth=4.5in,
%textheight=5in, paperheight=4.5in,
%a4paper,
top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
]{geometry}
%
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% %L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
% \pu
% (find-TH "math-b" "2019-newton")
% (nea)
% ____ __
% | _ \ ___ / _|___
% | | | |/ _ \ |_/ __|
% | |_| | __/ _\__ \
% |____/ \___|_| |___/
%
% «defs» (to ".defs")
% (find-LATEX "edrx15.sty" "colors-2019")
\long\def\ColorRed #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray #1{{\color{GrayLight}#1}}
\long\def\ColorGray #1{{\color{black!30!white}#1}}
\def\respcomp{\mathsf{respcomp}}
\def\respids {\mathsf{respids}}
\def\sqcond {\mathsf{sqcond}}
\setlength{\parindent}{0em}
% _____ _ _ _
% |_ _(_) |_| | ___ _ __ __ _ __ _ ___
% | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
% | | | | |_| | __/ | |_) | (_| | (_| | __/
% |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
% |_| |___/
%
% «title-page» (to ".title-page")
% (nesp 1 "title-page")
% (nes "title-page")
\thispagestyle{empty} % (find-es "tex" "thispagestyle")
\begin{center}
\begin{tabular}{c}
{\Large {\bf On two tricks to make}} \\[1pt]
{\Large {\bf Category Theory fit in}} \\[1pt]
{\Large {\bf less mental space:}} \\[1pt]
{\Large {\bf missing diagrams and}} \\[1pt]
{\Large {\bf skeletons of proofs}} \\[1pt]
% \ColorGray{(talk @ EmacsConf 2019; short version)}
\\
A talk at the ``Creativity 2019'' conference \\
in honor of Newton da Costa's 90th birthday \\
Rio de Janeiro, december 11, 2019 \\
\\
By: Eduardo Ochs \\[4pt]
\scriptsize {\tt \color{DarkRed}eduardoochs@gmail.com} \\[-3pt]
\scriptsize \url{http://angg.twu.net/math-b.html#2019-newton} \\
\end{tabular}
\end{center}
\newpage
\noedrxfooter % (find-LATEX "edrxheadfoot.tex")
% ___ _ _ _ _
% |_ _|_ __ | |_ _ __ ___ __| |_ _ ___| |_(_) ___ _ __
% | || '_ \| __| '__/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \
% | || | | | |_| | | (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__|_| \___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%
% «introduction» (to ".introduction")
% (nesp 2 "introduction")
% (nes "introduction")
{\bf Introduction}
Most texts in Category Theory (``CT'' from here on)
are full of expressions like this:
\msk
``Let's write $(A×)$ for \ColorRed{the} functor that takes
each object $B$ to $A×B$''
\msk
I was absolutely fascinated by this ``\ColorRed{the}''.
A functor --- say, $(A×)$ --- has an action on objects,
an action on morphisms, and guarantees, or proofs,
that it respects identities and compositions.
\msk
That ``\ColorRed{the} functor'' implies that the reader should be able
to figure out by himself the action on morphisms, i.e.,
the precise meaning for $(A×)f$ when $f:B→C$, and to
check that this $(A×)$ respects identities and compositions.
\newpage
% ___ _ _ _ _ ____
% |_ _|_ __ | |_ _ __ ___ __| |_ _ ___| |_(_) ___ _ __ |___ \
% | || '_ \| __| '__/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \ __) |
% | || | | | |_| | | (_) | (_| | |_| | (__| |_| | (_) | | | | / __/
% |___|_| |_|\__|_| \___/ \__,_|\__,_|\___|\__|_|\___/|_| |_| |_____|
%
% «introduction-2» (to ".introduction-2")
% (nesp 3 "introduction-2")
% (nes "introduction-2")
{\bf Introduction (2)}
Formally, a functor $(A×):\Set→\Set$
is a 4-uple:
\msk
\phantom{mmm}
$(A×) = ((A×)_0, (A×)_1, \respids_{(A×)}, \respcomp_{(A×)})$
\bsk
The ``\ColorRed{the}'' in
\msk
\phantom{m}
``$(A×)$ is \ColorRed{the} functor that takes each object $B$ to $A{×}B$''
\msk
suggests that learning CT transforms you in a certain way...
you become a person who can infer $(A×)_1$, $\respids_{(A×)}$,
and $\respcomp_{(A×)}$ from just $(A×)_0$...
\msk
...you become a person who can define functors in a very
compact way, and the other CT people will understand you.
\msk
\ColorRed{(I wanted to become like that when I'd grow up)}
\newpage
% __ ____
% \ \ / / /_ _____ _ __ __ _ _ __ ___ ___ ___
% \ \ /\ / / /\ \ /\ / / _ \ | '_ \ / _` | '_ ` _ \ / _ \/ __|
% \ V V / / \ V V / (_) | | | | | (_| | | | | | | __/\__ \
% \_/\_/_/ \_/\_/ \___/ |_| |_|\__,_|_| |_| |_|\___||___/
%
% «functions-and-names» (to ".functions-and-names")
% (nesp 4 "functions-and-names")
% (nes "functions-and-names")
{\bf Functions with and without names}
Consider this function:
%
$$\begin{array}{rrrcl}
f & : & \{1,2,3\} &→& \Z \\
& & a &↦& 10a \\
\end{array}
$$
%
It has a name: $f$.
\msk
There are two easy ways to work with
functions without names...
\newpage
% _ _ _
% | | __ _ _ __ ___ | |__ __| | __ _
% | | / _` | '_ ` _ \| '_ \ / _` |/ _` |
% | |__| (_| | | | | | | |_) | (_| | (_| |
% |_____\__,_|_| |_| |_|_.__/ \__,_|\__,_|
%
% «lambda» (to ".lambda")
% (nesp 5 "lambda")
% (nes "lambda")
{\bf Lambda notation}
\msk
\begin{tabular}{rl}
Way 1: & A function is a \ColorRed{set} of input-output pairs: \\
& $f = \{(1,10), (2,20), (3,30)\}$ \\[2pt]
& So: $\begin{array}[t]{rcl}
f(2) &=& \{(1,10), (2,20), (3,30)\} (2) \\
&=& 20
\end{array}
$ \\[8pt]
Way 2: & A function is a \ColorRed{program} in $λ$-notation: \\
& $f = (λa.10a)$ \\[2pt]
& So: $\begin{array}[t]{rcl}
f(2) &=& (λa.10·a) (2) \\
&=& (10·a)[a:=2] \\
&=& 10·2 \\
&=& 20 \\
\end{array}
$
\end{tabular}
\msk
Both ways drop some information:
name, codomain, and, in the case of $(λa.10·a)$, domain.
There is a also this notation: $(λa\ColorRed{{:}\{1,2,3\}}.10·a)$, that
includes the domain (a ``\ColorRed{type}''!), but we are in a hurry...
\newpage
% ___ _ _ _ _
% |_ _|_ __ | |_ ___ _ __ _ __ __ _| | __| (_) __ _ __ _ ___
% | || '_ \| __/ _ \ '__| '_ \ / _` | | / _` | |/ _` |/ _` / __|
% | || | | | || __/ | | | | | (_| | | | (_| | | (_| | (_| \__ \
% |___|_| |_|\__\___|_| |_| |_|\__,_|_| \__,_|_|\__,_|\__, |___/
% |___/
% «internal-diagrams» (to ".internal-diagrams")
% (nesp 6 "internal-diagrams")
% (nes "internal-diagrams")
% (oxap 4 "fig:internal-1")
% (oxa "fig:internal-1")
{\bf Internal diagrams}
\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
$\pu
\scalebox{0.94}{$
\begin{array}{rrcl}
\sqrt{\phantom{a}}: & \N &→& \R \\
& n &↦& \sqrt{n} \\
\end{array}
\qquad
\diag{second-blob-function}
$}
$
\bsk
The $n \; \diagxyto/|->/<200> \; \sqrt{n}$ shows how $\sqrt{\phantom{a}}$ acts on a generic element.
The $3 \; \diagxyto/|->/<200> \; \sqrt{3}$ shows how $\sqrt{\phantom{a}}$ acts on a particular element.
The $4 \; \diagxyto/|->/<200> \; 2$ shows how $\sqrt{\phantom{a}}$ acts on another element.
\newpage
% ___ _ _ _ _ _
% |_ _|_ __ | |_ __| (_) __ _ __ _ ___ (_)_ __ ___ __ _| |_ ___
% | || '_ \| __| / _` | |/ _` |/ _` / __| | | '_ \ / __/ _` | __/ __|
% | || | | | |_ | (_| | | (_| | (_| \__ \ | | | | | | (_| (_| | |_\__ \
% |___|_| |_|\__| \__,_|_|\__,_|\__, |___/ |_|_| |_| \___\__,_|\__|___/
% |___/
%
% «internal-diagrams-in-cats» (to ".internal-diagrams-in-cats")
% (nesp 7 "internal-diagrams-in-cats")
% (nes "internal-diagrams-in-cats")
{\bf Internal diagrams in categories}
Above: internal view \ColorRed{(without the blobs)}
Below: external view
% \msk
%D diagram cat-1
%D 2Dx 100 +35 +30 +35 +30 +35
%D 2D 100 A0 A1 B0 B1 C0 C1
%D 2D
%D 2D +35 A2 A3 B2 B3 C2 C3
%D 2D
%D 2D +20 A4 A5 B4 B5 C4 C5
%D 2D
%D ren A0 A2 A1 A3 A4 A5 ==> C D FC FD \catA \catB
%D ren B0 B2 B1 B3 B4 B5 ==> B C (A×)B (A×)C \Set \Set
%D ren C0 C2 C1 C3 C4 C5 ==> B C A{×}B A{×}C \Set \Set
%D
%D (( A0 A1 |-> .plabel= a F_0
%D A0 A2 -> .plabel= l g
%D A0 A3 harrownodes nil 20 nil |-> .plabel= a F_1
%D A1 A3 -> .plabel= r Fg
%D A2 A3 |-> .plabel= a F_0
%D A4 A5 -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
\diag{cat-1}
$$
\msk
Above $\catA$: objects and morphisms of $\catA$ (same for $\catB$)
Above $F$: the actions of $F$ on objs and morphisms
(Some conventions come from \ColorRed{fibrations})
\newpage
% ____ ____ ____
% | __ ) / ___/ ___|
% | _ \| | | |
% | |_) | |__| |___
% |____/ \____\____|
%
% «BCC» (to ".BCC")
% (nesp 8 "BCC")
% (nes "BCC")
{\bf The shape of Beck-Chevalley}
\def\BCCL{\mathsf{BCCL}}
%D diagram BCCL-std
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <====================== B1
%D 2D -\\ -\\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\> B2' ============== B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= f^{\prime*}P B1 .tex= P
%D B2 .tex= z^{\prime*}f^*Σ_zP B3 .tex= z^*Σ_zP
%D B4 .tex= Σ_{z'}f^{\prime*}P B5 .tex= Σ_zP
%D B6 .tex= f^*Σ_zP B7 .tex= Σ_zP
%D B2' .tex= f^{\prime*}z^*Σ_zP
%D B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D B0 B4 |-> B1 B5 |->
%D B2 B6 <-| B3 B7 <-|
%D B6 B7 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r \BCCL
%D B0 B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= X×_{Y}Z b1 .tex= Z b2 .tex= X b3 .tex= Y
%D b0 b1 -> .plabel= b f'
%D b0 b2 -> .plabel= l z'
%D b1 b3 -> .plabel= r z
%D b2 b3 -> .plabel= a f
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\pu
\diag{BCCL-std}
$$
\newpage
% __ ___ _ _ _
% \ \ / / |__ __ _| |_ | |_ _ __ _ _ _ _ _ __ __| |
% \ \ /\ / /| '_ \ / _` | __| | __| '__| | | | | | | | '_ \ / _` |
% \ V V / | | | | (_| | |_ | |_| | | |_| | | |_| | | | | (_| |
% \_/\_/ |_| |_|\__,_|\__| \__|_| \__, | \__,_|_| |_|\__,_|
% |___/
%
% «what-to-understand» (to ".what-to-understand")
% (nesp 9 "what-to-understand")
% (nes "what-to-understand")
{\bf What I was trying to understand}
Short answer: categorical semantics \ColorRed{should be} more intuitive
Part of the long answer: \ColorRed{hyperdoctrines} are important
but the \ColorRed{definition} of hyperdoctrine is super-hard...
\msk
A hyperdoctrine is a fibration $p:\bbE→\bbB$
over a base category $\bbB$ with finite products,
in which each fiber is cartesian-closed, and
in which every change-of-base functor $f^*$
has adjoints $Σ_f ⊣ f^* ⊣ Π_f$...
Also, all Beck-Chevalley maps and
all Frobenius maps in it are invertible
(yuck! Plus \ColorRed{lots} of details...)
\msk
What are the \ColorRed{intended semantics} of these operations?
Can I work in the \ColorRed{abstract definition} and in the
intended semantics \ColorRed{``in parallel''}?
\newpage
% ____ _ _ _ _ _
% | _ \ __ _ _ __ __ _| | | ___| | __| (_) __ _ __ _ ___
% | |_) / _` | '__/ _` | | |/ _ \ | / _` | |/ _` |/ _` / __|
% | __/ (_| | | | (_| | | | __/ | | (_| | | (_| | (_| \__ \
% |_| \__,_|_| \__,_|_|_|\___|_| \__,_|_|\__,_|\__, |___/
% |___/
%
% «parallel-diagrams» (to ".parallel-diagrams")
% (nesp 10 "parallel-diagrams")
% (nes "parallel-diagrams")
{\bf Parallel diagrams}
...what are the \ColorRed{intended semantics} of these operations?
Can I work in the \ColorRed{abstract definition} and in the
intended semantics \ColorRed{``in parallel''}?
\msk
Yes, if by ``in parallel'' we mean
``using diagrams with the same shape''.
An example:
%
%D diagram int-ext-gen-part
%D 2Dx 100 +35 +30 +35 +30 +35
%D 2D 100 A0 A1 B0 B1 C0 C1
%D 2D
%D 2D +35 A2 A3 B2 B3 C2 C3
%D 2D
%D 2D +20 A4 A5 B4 B5 C4 C5
%D 2D
%D ren A0 A2 A1 A3 A4 A5 ==> X Y FX FY \catA \catB
%D ren B0 B2 B1 B3 B4 B5 ==> B C (A×)B (A×)C \Set \Set
%D ren C0 C2 C1 C3 C4 C5 ==> B C A{×}B A{×}C \Set \Set
%D
%D (( A0 A1 |-> .plabel= a F_0
%D A0 A2 -> .plabel= l g
%D A0 A3 harrownodes nil 20 nil |-> .plabel= a F_1
%D A1 A3 -> .plabel= r Fg
%D A2 A3 |-> .plabel= a F_0
%D A4 A5 -> .plabel= a F
%D
%D B0 B1 |-> .plabel= a (A×)_0
%D B0 B2 -> .plabel= l f
%D B0 B3 harrownodes nil 20 nil |-> .plabel= a (A×)_1
%D B1 B3 -> .plabel= r (A×)f
%D B2 B3 |-> .plabel= a (A×)_0
%D B4 B5 -> .plabel= a (A×)
%D
%D C0 C1 |-> .plabel= a (A×)_0
%D C0 C2 -> .plabel= l f
%D C0 C3 harrownodes nil 20 nil |-> .plabel= a (A×)_1
%D C1 C3 -> .plabel= r λp.(πp,f(π'p))
%D C2 C3 |-> .plabel= a (A×)_0
%D C4 C5 -> .plabel= a (A×)
%D ))
%D enddiagram
%D
$$\pu
\scalebox{0.87}{$
\diag{int-ext-gen-part}
$}
$$
\newpage
% ____ _ _ _ _ _____ ____
% | _ \ __ _ _ __ __ _| | | ___| | | | | ___/ ___|
% | |_) / _` | '__/ _` | | |/ _ \ | | | | |_ | |
% | __/ (_| | | | (_| | | | __/ | | |___| _|| |___
% |_| \__,_|_| \__,_|_|_|\___|_| |_____|_| \____|
%
% «parallel-diagrams-lfc» (to ".parallel-diagrams-lfc")
% (nesp 11 "parallel-diagrams-lfc")
% (nes "parallel-diagrams-lfc")
% (vgmp 12 "parallel")
% (vgm "parallel")
{\bf Parallel diagrams - Logic for Children}
The main \ColorRed{techniques} discussed in the workshop
``Logic for Children'' (in the UniLog 2018, in Vichy )
involved parallel diagrams...
%
\def\tm #1#2{ \begin{tabular}{#1}#2\end{tabular}}
\def\ptm#1#2{\left (\begin{tabular}{#1}#2\end{tabular}\right )}
\def\smm#1#2{\sm{\text{#1}\\\text{#2}}}
%
$$\begin{array}{c}
\ptm{c}{particular \\ case \\ ``for children''}
\two/<-`->/<500>^{\smm{particularize}{(easy)}}_{\smm{generalize}{(hard)}}
\ptm{c}{general \\ case \\ ``for adults''}
\\
\\
\ptm{c}{intended \\ meaning}
\two/<--`-->/<500>
\ptm{c}{categorical \\ semantics}
\\
\\
\ptm{c}{internal $+$ \\ external}
\two/<--`-->/<500>
\ptm{c}{external \\ view}
\end{array}
$$
\newpage
% ____ __ __
% / ___| \/ |___
% | | _| |\/| / __|
% | |_| | | | \__ \
% \____|_| |_|___/
%
% «example-in-topos» (to ".example-in-topos")
% (nesp 12 "example-in-topos")
% (nes "example-in-topos")
{\bf An example from Topos Theory}
\ssk
In 2018 I was using these techniques ---
parallel diagrams, internal views,
particular cases, finite examples ``for children''
--- to understand things in Topos Theory...
\msk
I was super happy because with these techniques
I finally was able to understand some things
about toposes and sheaves, that before were
MUCH more abstract than my brain could handle...
\msk
..and I showed this figure, of a particular case
of a geometric morphism that induces a sheaf...
\msk
(This particular case is rich enough to give me
a lot of intuition about GMs and shaves)
\newpage
% ____ __ __ ____
% / ___| \/ |___ |___ \
% | | _| |\/| / __| __) |
% | |_| | | | \__ \ / __/
% \____|_| |_|___/ |_____|
%
% «example-in-topos-2» (to ".example-in-topos-2")
% (nesp 13 "example-in-topos-2")
% (nes "example-in-topos-2")
\phantom{.}
\vspace{-1.5cm}
% (vgsp 14 "first-gm")
% (vgs "first-gm")
%
%L sesw = {[" w"]="↙", [" e"]="↘"}
%
%R local B, F, RG = 3/ 1 \, 3/ F_1 \, 3/ !Gt \
%R | w e | | w e | | w e |
%R | 2 3 | |F_2 F_3 | |G_2 G_3 |
%R | e w e | | e w e | | e w e |
%R | 4 5 | | F_4 F_5| | G_4 G_5|
%R | e w | | e w | | e w |
%R \ 6 / \ F_6 / \ 1 /
%R
%R local A, G, LF = 3/ 2 3 \, 3/G_2 G_3 \, 3/F_2 F_3 \
%R | e w e | | e w e | | e w e |
%R \ 4 5 / \ G_4 G_5/ \ F_4 F_5/
%R
%R B :tozmp({def="pB", scale="7pt", meta="s p"}):addcells(sesw):output()
%R F :tozmp({def="pF", scale="7pt", meta="s p"}):addcells(sesw):output()
%R RG:tozmp({def="pRG", scale="7pt", meta="s p"}):addcells(sesw):output()
%R A :tozmp({def="pA", scale="7pt", meta="s p"}):addcells(sesw):output()
%R G :tozmp({def="pG", scale="7pt", meta="s p"}):addcells(sesw):output()
%R LF:tozmp({def="pLF", scale="7pt", meta="s p"}):addcells(sesw):output()
\def\Gt{G_2 {×_{G_4}} G_3}
\pu
%D diagram GM-children-big
%D 2Dx 100 +57
%D 2D 100 A0 A1
%D 2D
%D 2D +45 A2 A3
%D 2D
%D 2D +25 A4 A5
%D 2D
%D 2D +25 A6 A7
%D 2D
%D ren A0 A1 ==> \pLF \pF
%D ren A2 A3 ==> \pG \pRG
%D ren A4 A5 ==> \Set^\catA \Set^\catB
%D ren A6 A7 ==> \pA \pB
%D
%D (( A0 A1 <-|
%D A2 A3 |->
%D A0 A2 ->
%D A1 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 -> sl^ .plabel= a f
%D
%D ))
%D enddiagram
%D
%D diagram GM-general
%D 2Dx 100 +35
%D 2D 100 A0 A1
%D 2D
%D 2D +25 A2 A3
%D 2D
%D 2D +15 A4 A5
%D 2D
%D ren A0 A1 ==> f^*F F
%D ren A2 A3 ==> G f_*G
%D ren A4 A5 ==> \calF \calE
%D
%D (( A0 A1 <-
%D A2 A3 ->
%D A0 A2 ->
%D A1 A3 ->
%D A0 A3 harrownodes nil 20 nil <->
%D A4 A5 <- sl^ .plabel= a f^*
%D A4 A5 -> sl_ .plabel= b f_*
%D
%D ))
%D enddiagram
%D
$$\pu
\resizebox{!}{105pt}{$
\begin{array}{ccc}
\diag{GM-children-big}&
\qquad
\qquad&
\diag{GM-general}\\
\\
\text{(for children; inclusion, sheaf)}&&
\text{(for adults)}\\
\end{array}
$}
$$
\newpage
% _ _ _ _ _ _
% _ __ __ _ _ __ __ _| | | ___| | | | __ _ _ __ ___ | |__ __| | __ _
% | '_ \ / _` | '__/ _` | | |/ _ \ | | |/ _` | '_ ` _ \| '_ \ / _` |/ _` |
% | |_) | (_| | | | (_| | | | __/ | | | (_| | | | | | | |_) | (_| | (_| |
% | .__/ \__,_|_| \__,_|_|_|\___|_| |_|\__,_|_| |_| |_|_.__/ \__,_|\__,_|
% |_|
%
% «see-them-as-lambda-terms» (to ".see-them-as-lambda-terms")
% (nesp 14 "see-them-as-lambda-terms")
% (nes "see-them-as-lambda-terms")
I felt that I had some techniques for creating
``the right (finite) examples'', and these examples
could give me/us a lot of intuition on Topos Theory...
\msk
That was quite nice, but then I started to ask:
what \ColorRed{exactly} is this ``intuition''?
What \ColorRed{kinds} of knowledge are transferred
between parallel diagrams?
\msk
My first answer was:
in two parallel diagrams $A$ and $B$
with entities $A_1, \ldots, A_n$, $B_1, \ldots, B_n$,
the relations between the entities in $A$
and the correpondent entities in $B$
are the same \ColorRed{if we see these entities as $λ$-terms}.
\msk
So: {\bf let's study this!} $↑$
\newpage
% __ __ _
% \ \ / /__ _ __ ___ __| | __ _
% \ V / _ \| '_ \ / _ \/ _` |/ _` |
% | | (_) | | | | __/ (_| | (_| |
% |_|\___/|_| |_|\___|\__,_|\__,_|
%
% «yoneda-1» (to ".yoneda-1")
% (nesp 15 "yoneda-1")
% (nes "yoneda-1")
{\bf Formalizing the Yoneda Lemma in $λ$-calculus}
See: \url{http://angg.twu.net/math-b.html#notes-yoneda}
% (nyop 24 "changing-R-to-Bto-2")
% (nyo "changing-R-to-Bto-2")
%D diagram yoneda-2-curve
%D 2Dx 100 +40
%D 2D 100 A
%D 2D |
%D 2D v
%D 2D +25 C |-> RC
%D 2D
%D 2D +20 F1 -> F2
%D 2D |
%D 2D v
%D 2D +25 F3
%D 2D
%D ren A ==> 1
%D ren F1 F2 F3 ==> (C{→}\_) (1{→}R\_) R
%D
%D (( C RC |->
%D A RC -> .plabel= r γ
%D F1 F2 -> .plabel= b T
%D F1 F2 midpoint A RC midpoint <-> .curve= ^14pt
%D F2 F3 <->
%D F1 F3 -> .plabel= l T'
%D ))
%D enddiagram
%
%D diagram yoneda-3-curve
%D 2Dx 100 +45
%D 2D 100 A
%D 2D |
%D 2D v
%D 2D +25 C |-> RC
%D 2D
%D 2D +20 F1 -> F2
%D 2D |
%D 2D v
%D 2D +25 F3
%D 2D
%D ren A RC ==> 1 (B{→}C)
%D ren F1 F2 F3 ==> (C{→}\_) (1{→}(B{→}\_)) (B{→}▁)
%D
%D (( C RC |->
%D A RC -> .plabel= r γ
%D F1 F2 -> .plabel= b T
%D F1 F2 midpoint A RC midpoint <-> .curve= ^14pt
%D F2 F3 <->
%D F1 F3 -> .plabel= l T'
%D ))
%D enddiagram
%
\pu
$$
\resizebox{!}{60pt}{$
\diag{yoneda-2-curve}
\qquad
\diag{yoneda-3-curve}
$}
$$
\newpage
% __ __ _ ____
% \ \ / /__ _ __ ___ __| | __ _ |___ \
% \ V / _ \| '_ \ / _ \/ _` |/ _` | __) |
% | | (_) | | | | __/ (_| | (_| | / __/
% |_|\___/|_| |_|\___|\__,_|\__,_| |_____|
%
% «yoneda-2» (to ".yoneda-2")
% (nesp 16 "yoneda-2")
% (nes "yoneda-2")
{\bf Formalizing the Yoneda Lemma in $λ$-calculus (2)}
\msk
%D diagram yoneda-R-5+
%D 2Dx 100 +40
%D 2D 100 A
%D 2D |
%D 2D v
%D 2D +25 C |-> RC
%D 2D
%D 2D +20 F1 -> F2
%D 2D |
%D 2D v
%D 2D +25 F3
%D 2D
%D ren F1 F2 F3 ==> (C{→}\_) (A{→}R\_) \phantom{R}
%D
%D (( C RC |-> A RC -> .plabel= r γ
%D F1 F2 -> .plabel= a T
%D F3 place
%D ))
%D enddiagram
\pu
\resizebox{0.92\textwidth}{!}{%
$\cdiag{yoneda-R-5+}
\quad
\begin{array}[c]{l}
A∈\catA \\
C∈\catC \\
R:\catA→\catC \\
γ:A→RC \\
\ColorRed{γ := TC(\id_C)} \\[5pt]
%
(C{→}\_): \catC→\Set \\
(C{→}\_)_0(D) = \Hom_\catC(C,D) \\
(C{→}\_)_1(h) = λg.(g;h) \\[5pt]
%
(A{→}R\_): \catC→\Set \\
(A{→}R\_)_0(D) = \Hom_\catA(A,RD) \\
(A{→}R\_)_1(h) = λδ.(δ;Rh) \\[5pt]
%
T: (C{→}\_) → (A{→}R\_) \\
% \ColorRed{T_0(D) := λg.(γ;Rg)} \\
\end{array}
$}
\newpage
% _ _ _ _
% (_) __| |_ __(_)___ ___| |_
% | |/ _` | '__| / __|_____ / __| __|
% | | (_| | | | \__ \_____| (__| |_
% |_|\__,_|_| |_|___/ \___|\__|
%
% «idris-ct» (to ".idris-ct")
% (nesp 17 "idris-ct")
% (nes "idris-ct")
{\bf Categories, functors, NTs, etc, in Idris-ct}
\ssk
I decided to grow up,
and instead of only writing the formalizations
of my diagrams as $λ$-terms ``\ColorRed{by hand}''
in a system of $λ$-calculus with dependent types,
as I've been doing for ages ---
\msk
I would finally learn a language with dependent types
that doubles as a proof assistant: \ColorRed{Idris} ---
and I would implement my Yoneda --- or at least
its translation to $λ$-terms --- in Idris, on top
of its library for Category Theory, \ColorRed{Idris-ct}...
\newpage
% ____ _ _ _ _
% / ___|| | _____| | ___| |_ ___ _ __ ___ / |
% \___ \| |/ / _ \ |/ _ \ __/ _ \| '_ \/ __| | |
% ___) | < __/ | __/ || (_) | | | \__ \ | |
% |____/|_|\_\___|_|\___|\__\___/|_| |_|___/ |_|
%
% «skeletons-1» (to ".skeletons-1")
% (nesp 18 "skeletons-1")
% (nes "skeletons-1")
{\bf Skeletons (1)}
Remember that a functor $(A×):\Set→\Set$
is a 4-uple:
\msk
\phantom{m}
$(A×) = ((A×)_0, (A×)_1; \respids_{(A×)}, \respcomp_{(A×)})$
\msk
The components before the `;'
don't mention equalities of morphisms,
the components after the `;' do.
If we drop the components after the `;' we get
\msk
\phantom{m}
$(A×) = ((A×)_0, (A×)_1)$
\msk
A ``\ColorRed{proto-functor}''.
It is possible to do something similar for
(proto)categories, (proto)isos, (proto)NTs,
(proto)adjunctions, (proto)fibrations,
(proto)hyperdoctrines...
\newpage
% ____ _ _ _ ____
% / ___|| | _____| | ___| |_ ___ _ __ ___ |___ \
% \___ \| |/ / _ \ |/ _ \ __/ _ \| '_ \/ __| __) |
% ___) | < __/ | __/ || (_) | | | \__ \ / __/
% |____/|_|\_\___|_|\___|\__\___/|_| |_|___/ |_____|
%
% «skeletons-2» (to ".skeletons-2")
% (nesp 19 "skeletons-2")
% (nes "skeletons-2")
{\bf Skeletons (2)}
Most constructions and proofs in Category Theory
can be done first on the proto-things and then
``lifted'' to the real things.
\msk
The constructions with only the proto-parts are
easier and very visual, and they work as ``\ColorRed{skeletons}''
for the real constructions and proofs.
\msk
I published this idea in a paper in Logica Universalis,
``Internal Diagrams and Archetypal Reasoning in
Category Theory'' (2013), but no one paid any attention.
(Link: \url{http://angg.twu.net/math-b.html\#idarct})
\msk
I created a \ColorRed{modified version} of Idris-ct
that defines protocats, protofunctors, etc, instead of
cats, functors, etc, and I'm translating my Yoneda \ColorRed{to it}!
\newpage
% ____ _ _ _ _____
% / ___|| | _____| | ___| |_ ___ _ __ ___ |___ /
% \___ \| |/ / _ \ |/ _ \ __/ _ \| '_ \/ __| |_ \
% ___) | < __/ | __/ || (_) | | | \__ \ ___) |
% |____/|_|\_\___|_|\___|\__\___/|_| |_|___/ |____/
%
% «skeletons-3» (to ".skeletons-3")
% (nesp 20 "skeletons-3")
% (nes "skeletons-3")
{\bf Skeletons (3)}
The diagrams on which I'm working can be treated
as ``skeletons'' of categorical constructions/proofs
in at least two senses.
\msk
1) The ``proto-things'' of the previous slides.
2) They can help us with the ``the''s.
\newpage
% _____ _
% |_ _| |__ ___
% | | | '_ \ / _ \
% | | | | | | __/
% |_| |_| |_|\___|
%
% «the» (to ".the")
% (nesp 21 "the")
% (nes "the")
{\bf ``The''}
``Let's denote by $(A×)$ \ColorRed{the} functor that takes
each object $B$ to $A{×}B$''
\msk
This means that the \ColorRed{action of objects} of $(A×)$,
$(A×)_0$, is $B ↦ A{×}B$... $(A×)_0 = λB.(A{×}B)$.
The \ColorRed{action of morphisms} of $(A×)$,
$(A×)_1$, is not obvious. % What is $(A×)_1 f$?
\msk
Why do the books on CT say ``$(A×)$ is \ColorRed{the}
functor that takes each object $B$ to $A{×}B$''?
\msk
Answer: because \ColorRed{there is a way} to find
\ColorRed{a natural meaning} for $(A×)_1$!
For logicians: \ColorRed{find a proof} of $(B→C)→(A∧B→A∧C)$
and then apply Curry-Howard to obtain $λp.(πp,f(π'p))$.
For CS'ers: \ColorRed{find a term} of \ColorRed{type} $(B→C)→(A{×}B→A{×}C)$.
\newpage
% _____ _
% |_ _|__ _ __ _ __ ___ ___ ___ __ _ _ __ ___| |__
% | |/ _ \ '__| '_ ` _ \ / __|/ _ \/ _` | '__/ __| '_ \
% | | __/ | | | | | | | \__ \ __/ (_| | | | (__| | | |
% |_|\___|_| |_| |_| |_| |___/\___|\__,_|_| \___|_| |_|
%
% «term-search» (to ".term-search")
% (nesp 22 "term-search")
% (nes "term-search")
% (ntyp 52 "obvious-term")
% (nty "obvious-term")
{\bf Finding a term of type such-and-such}
Suppose that we know a function $f:A→B$ and a set $C$.
Then ``$f$ \ColorRed{induces} a function $(f{×}C):A{×}C→B{×}C$
\ColorRed{in a natural way}''.
\msk
How do we discover the function that
``\ColorRed{deserves the name}'' $(f{×}C)$?
\msk
Trick: ``\ColorRed{in a natural way}'' usually means
``using only the operations from $λ$-calculus'', (!!!!!!!)
i.e., ``a $λ$-term''.
%:
%: f⠆A{→}B
%: ===============
%: (f{×}C)⠆A{×}C{→}B{×}C
%:
%: ^obvious-1
%:
%: A{→}B
%: =============
%: A{×}C{→}B{×}C
%:
%: ^obvious-2
%:
%:
%: [A{×}C]^1
%: ---------
%: A A{→}B [A{×}C]^1
%: -------------- ---------
%: B C
%: -----------------
%: B{×}C
%: -------------1
%: A{×}C{→}B{×}C
%:
%: ^obvious-3
%:
%: [p⠆A{×}C]^1
%: ---------
%: πp⠆A f⠆A{→}B [p⠆A{×}C]^1
%: ------------------- -----------
%: f(πp)⠆B π'p⠆C
%: ---------------------------
%: (f(πp),π'p)⠆B{×}C
%: -------------1
%: (λp⠆A{×}C⠆(f(πp),π'p))⠆A{×}C{→}B{×}C
%:
%: ^obvious-4
%:
\pu
$$\ded{obvious-1}
\quad ⇒ \quad
\ded{obvious-2}
\quad ⇒ (...)
$$
% «term-search-2» (to ".term-search-2")
% (nesp 23 "term-search-2")
% (nes "term-search-2")
$\begin{array}{c}
\ded{obvious-2}
\quad ⇒ \quad
\ded{obvious-3}
\\
\\
\quad ⇒ \quad
\ded{obvious-4}
\\
\\
\quad ⇒ \quad
(f{×}C) := (λp⠆A{×}C⠆(f(πp),π'p))
\end{array}
$
\newpage
% ___ _ __ _ __ _
% |_ _|_ __ | |_ / /____ _| |_ __ _ ___ _ __ / / __ __ _ _ __| |_
% | || '_ \| __| / / _ \ \/ / __| / _` |/ _ \ '_ \ / / '_ \ / _` | '__| __|
% | || | | | |_ / / __/> <| |_ | (_| | __/ | | |/ /| |_) | (_| | | | |_
% |___|_| |_|\__/_/ \___/_/\_\\__| \__, |\___|_| |_/_/ | .__/ \__,_|_| \__|
% |___/ |_|
%
% «int-ext-gen-part» (to ".int-ext-gen-part")
% (nesp 24 "int-ext-gen-part")
% (nes "int-ext-gen-part")
{\bf Internal/external, generic/particular}
%D diagram int-ext-gen-part
%D 2Dx 100 +35 +30 +35 +30 +35
%D 2D 100 A0 A1 B0 B1 C0 C1
%D 2D
%D 2D +35 A2 A3 B2 B3 C2 C3
%D 2D
%D 2D +20 A4 A5 B4 B5 C4 C5
%D 2D
%D ren A0 A2 A1 A3 A4 A5 ==> X Y FX FY \catA \catB
%D ren B0 B2 B1 B3 B4 B5 ==> B C (A×)B (A×)C \Set \Set
%D ren C0 C2 C1 C3 C4 C5 ==> B C A{×}B A{×}C \Set \Set
%D
%D (( A0 A1 |-> .plabel= a F_0
%D A0 A2 -> .plabel= l g
%D A0 A3 harrownodes nil 20 nil |-> .plabel= a F_1
%D A1 A3 -> .plabel= r Fg
%D A2 A3 |-> .plabel= a F_0
%D A4 A5 -> .plabel= a F
%D
%D B0 B1 |-> .plabel= a (A×)_0
%D B0 B2 -> .plabel= l f
%D B0 B3 harrownodes nil 20 nil |-> .plabel= a (A×)_1
%D B1 B3 -> .plabel= r (A×)f
%D B2 B3 |-> .plabel= a (A×)_0
%D B4 B5 -> .plabel= a (A×)
%D
%D C0 C1 |-> .plabel= a (A×)_0
%D C0 C2 -> .plabel= l f
%D C0 C3 harrownodes nil 20 nil |-> .plabel= a (A×)_1
%D C1 C3 -> .plabel= r λp.(πp,f(π'p))
%D C2 C3 |-> .plabel= a (A×)_0
%D C4 C5 -> .plabel= a (A×)
%D ))
%D enddiagram
%D
$$\pu
\scalebox{0.87}{$
\diag{int-ext-gen-part}
$}
$$
$(A×)f$ is \ColorRed{some} function with this type:
$(A×)f: A{×}B→A{×}C$.
With some practice we can find a good candidate!
$(A×)f := λp.(πp,f(π'p))$
\msk
\ColorRed{(Not just practice! ${=})$)}
% \newpage
% (Time's over! Thank you!)
% (vgmp 12 "parallel")
% (vgm "parallel")
% (vgsp 14 "first-gm")
% (vgs "first-gm")
% (neap)
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "nes"
% End: