% (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:
