% (find-LATEX "2020tallinn-abstract.tex")
% (find-LATEX "2020tallinn-abstract.bib")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020tallinn-abstract.tex" :end))
% (defun c () (interactive) (find-LATEXsh "pdflatex -record 2020tallinn-abstract.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2020tallinn-abstract.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020tallinn-abstract.pdf"))
% (defun e () (interactive) (find-LATEX "2020tallinn-abstract.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020tallinn-abstract"))
%
% (find-LATEXsh  "./dednat6load.lua -4 2020tallinn-abstract.tex")
% (find-LATEXfile                     "2020tallinn-abstract.dnt")
%
% (find-pdf-page   "~/LATEX/2020tallinn-abstract.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020tallinn-abstract.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020tallinn-abstract.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020tallinn-abstract.pdf
%               file:///tmp/2020tallinn-abstract.pdf
%           file:///tmp/pen/2020tallinn-abstract.pdf
% http://angg.twu.net/LATEX/2020tallinn-abstract.pdf
% (find-LATEX "2019.mk")

% «.links»		(to "links")
% «.title»		(to "title")
% «.first-diagrams»	(to "first-diagrams")
% «.make»		(to "make")

%\documentclass[oneside]{article}
\documentclass[runningheads]{llncs}                % (find-es "tex" "llncs")
\usepackage[colorlinks,urlcolor=DarkRed,citecolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%\usepackage{pict2e}
\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
%
\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 2019oxford-chars.tex       % (find-LATEX "2019oxford-chars.tex")
\input 2020tallinn-abstract.dnt   % (find-LATEX "2020tallinn-abstract.dnt")
%
\begin{document}

\def\directlua#1{}
\def\pu{}
%\catcode`\^^J=10
%\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

\def\resizediag#1#2#3{\resizebox{#1}{#2}{$\diag{#3}$}}
\def\squigbijy{-2.8}   % (find-LATEX "2017planar-has-defs.tex" "squigbijtest")

% «links»  (to ".links")
% http://www.diagrams-conference.org/2020/
% http://www.diagrams-conference.org/2020/index.php/calls/main-track/
% https://mail.google.com/mail/ca/u/0/#inbox/FMfcgxwGDDtFBVZprxqvvXQsPljWfkld
% (find-es "tex" "llncs")




%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% «title»  (to ".title")
% (find-LATEX "2019oxford-abs.tex" "title")

\title{What kinds of knowledge do we gain by doing Category Theory in
  several levels of abstraction in parallel?}

\titlerunning{What kinds of knowledge do we gain by...?}


% (find-es "tex" "llncs")
% (find-es "arxiv" "orcid")
% (find-llncsfile "samplepaper.tex" "\\author")
%\author{Eduardo Ochs\inst{1}\orcidID{0000-0003-3854-9181}}
\author{Eduardo Ochs\orcidID{0000-0003-3854-9181}}
%
\authorrunning{E. Ochs}
%
\institute{Universidade Federal Fluminense, Rio das Ostras, RJ, Brazil \\
           \email{eduardoochs@gmail.com}\\
           \url{http://angg.twu.net/math-b.html}}

\maketitle



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.

One way to make concepts of Category Theory totally formal is to
implement them on proof assistants. For example, the diagram below

% (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).")
%
% In a type system
% (find-math-b-links "notes-yoneda" "2019notes-yoneda")
% (nyop 7 "first-yoneda-diagram")
% (nyo    "first-yoneda-diagram")
%
%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= b T
%D    F3 place
%D    F1 F2 midpoint A RC midpoint <-> .curve= ^14pt
%D ))
%D enddiagram
%
\pu
$$\cdiag{yoneda-R-5+}
 \qquad
 \begin{array}[c]{l}
 A∈\catA \\
 C∈\catC \\
 R:\catA→\catC \\
 γ:A→RC \\[5pt]
 %
 (C{→}\_): \catC→\Set \\
 (C{→}\_)_0(D) = \Hom_\catC(C,D) \\
 (C{→}\_)_1(h) = λg.(g;h) \\[5pt]
 %
 (A{→}R\_): \catC→\Set \\
 (A{→}R\_)_0(D) = \Hom_\catA(A,RD) \\
 (A{→}R\_)_1(h) = λδ.(δ;Rh) \\[5pt]
 %
 T: (C{→}\_) → (A{→}R\_) \\[5pt]
 T_0(D) := λg.(γ;Rg) \\
 γ := TC(\id_C) \\
 \end{array}
$$
%
``is'' the Yoneda Lemma, as in \cite{Riehl}, Theorem 2.2.4, but in a
 slightly more general form and in a different notation: ours is
 $\Hom(\Hom(C,-),\Hom(A,R-)) ≅ \Hom(A,RC)$; the details are in
 \cite{OchsNotesOnYoneda}, and an implementation of it in Idris is
 underway.

If we erase the left half of the diagram above we get a ``skeleton''
for the Yoneda Lemma, in the sense of \cite{OchsIDARCT}, Sections 1
and 12: the full diagram including the right half can be reconstructed
from its left half with very few extra clues.

% (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 27 "19. The syntactical world")
% (find-idarcttext 27 "19. The syntactical world")

Let's say that a diagram is ``formal enough'' when its formalization
on a type system or on a proof assistant is very easy to obtain, as in
the example above --- or at least if it is easy to formalize it in a
type system if we work only in its ``syntactical part'', as discussed
in Sections 12 and 19 of \cite{OchsIDARCT}. All the diagrams that I am
going to present in this talk are ``formal enough'' in this sense.

Now look at the figure below:

% (oxap 4 "fig:internal-1")
% (oxa    "fig:internal-1")

% «internal-external»  (to ".internal-external")
% (ph1p 4 "internal-external")
% (ph1    "internal-external")
\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
%D diagram generic-adjunction
%D 2Dx     100  +30    +35  +25
%D 2D  100      LA <-| A    
%D 2D           |      |    
%D 2D           v      v    
%D 2D  +30 G    LB <-| B    I
%D 2D      |    |      |    |   
%D 2D      v    v      v    v   
%D 2D  +30 H    C |--> RC   J
%D 2D           |      |    
%D 2D           v      v    
%D 2D  +30      D |--> RD   
%D 2D                       
%D 2D  +20      E <==> F    
%D 2D
%D ren LA A ==> LA' A'
%D ren LB B ==> LA  A
%D ren C RC ==> B  RB
%D ren D RD ==> B' RB'
%D ren E F  ==> \catB \catA
%D ren G H  ==> LRB B
%D ren I J  ==> A RLA
%D
%D (( LA A <-| .plabel= a L_0
%D    LB B <-| .plabel= a L_0
%D    C RC |-> .plabel= b R_0
%D    D RD |-> .plabel= b R_0
%D
%D    LA  B harrownodes nil 20 nil <-| sl^ .plabel= a L_1
%D    LB RC harrownodes nil 20 nil <-| sl^ .plabel= a ♭
%D    LB RC harrownodes nil 20 nil |-> sl_ .plabel= b ♯
%D    C  RD harrownodes nil 20 nil |-> sl^ .plabel= b R_1
%D
%D    LA LB -> .plabel= l Lα
%D     A  B -> .plabel= r  α
%D    LB  C -> .plabel= l \sm{g^♭\\f}
%D     B RC -> .plabel= r \sm{g\\f^♯}
%D     C  D -> .plabel= l β
%D    RC RD -> .plabel= r Rβ
%D    E F <- sl^ .plabel= a L
%D    E F -> sl_ .plabel= b R
%D    G H -> .plabel= l εB
%D    I J -> .plabel= r ηA
%D ))
%D enddiagram
%D
%D diagram (xB)-|(B->)
%D 2Dx     100  +45    +35  +40
%D 2D  100      LA <-| A    
%D 2D           |      |    
%D 2D           v      v    
%D 2D  +30 G    LB <-| B    I
%D 2D      |    |      |    |   
%D 2D      v    v      v    v   
%D 2D  +30 H    C |--> RC   J
%D 2D           |      |    
%D 2D           v      v    
%D 2D  +30      D |--> RD   
%D 2D                       
%D 2D  +20      E <==> F    
%D 2D
%D ren LA A ==> A{×}C A
%D ren LB B ==> B{×}C B
%D ren C RC ==> D (C{→}D)
%D ren D RD ==> E (C{→}E)
%D ren E F  ==> \Set \Set
%D ren G H  ==> (C{→}D){×C} D
%D ren I J  ==> B (C→B{×}C)
%D ren I J  ==> B (C{→}(B{×}C))
%D
%D (( LA A <-| # .plabel= a ({×}B)_0
%D    LB B <-| # .plabel= a ({×}B)_0
%D    C RC |-> # .plabel= b (B{→})_0
%D    D RD |-> # .plabel= b (B{→})_0
%D
%D    LA  B harrownodes nil 20 nil <-| sl^ # .plabel= a L_1
%D    LB RC harrownodes nil 20 nil <-| sl^ .plabel= a ♭
%D    LB RC harrownodes nil 20 nil |-> sl_ .plabel= b ♯
%D    C  RD harrownodes nil 20 nil |-> sl^ # .plabel= b R_1
%D
%D    LA LB -> .plabel= l λp.(f(πp),π'p)
%D     A  B -> .plabel= r f
%D    LB  C -> .plabel= l \sm{λp.g(πp)(π'p)\\\phantom{mmmmmm}h}
%D     B RC -> .plabel= r \sm{g\phantom{mmmmm}\\λb.λc.h(b,c)}
%D     C  D -> .plabel= l k
%D    RC RD -> .plabel= r λf.λc.k(fc)
%D    E F <- sl^ .plabel= a ({×}C)
%D    E F -> sl_ .plabel= b (C{→})
%D    G H -> .plabel= l λp.(πp)(π'p)
%D    I J -> .plabel= r λb.λc.(b,c)
%D ))
%D enddiagram
%D
\begin{figure}[!htbp]
  \pu
  \centering
  $\begin{array}{c}
   \resizediag{!}{!}{second-blob-function}
   \qquad
   \resizediag{!}{!}{generic-adjunction}
   \\
   \\
   \resizediag{!}{!}{(xB)-|(B->)}
   \end{array}
  $
  \caption{Three cases of internal views and external views.}
  \label{fig:internal-external}
\end{figure}


It is composed of three subdiagrams, that we will call $\sm{AB\\C}$,
and each of them is made of {\sl external view} below and an {\sl
  internal view} above.

Diagram $A$ shows, below, the external view of the function $\N
\ton{\sqrt{\phantom{a}}} \R$, and above that its internal view --- in
which one of the arrows, $n \mapsto \sqrt{n}$, shows the action of
$\sqrt{\phantom{a}}$ on a generic element, and the other `$\mto$'
arrows, like $3 \mapsto \sqrt{3}$ and $4 \mapsto 2$, show substitution
instances of $n \mapsto \sqrt{n}$, maybe after some term reductions.
Compare this with, say, \cite{LawvereSchanuel}, \cite{Riehl},
\cite{FongSpivak} --- they use external and internal diagrams but they
don't make the distinction between `$\to$' and `$\mapsto$', and this
makes their diagrams hard to formalize.

Diagram $B$ shows the external view of a (generic) adjunction $L⊣R$,
and above it its internal view. The nodes and arrows above $\catB$ are
objects and morphisms in $\catB$, and similarly for the nodes and
arrows above $\catA$. The `$\mto$' arrows of the internal view are now
of three kinds: actions of functors on objects, actions of functors on
morphisms, and ``transpositions'' coming from the natural isomorphism
$\Hom(L-,-) ↔ \Hom(-,R-)$. Diagram $C$ is essentially the same as $B$,
but for a particular adjunction: $({×}B)⊣(B{→})$. Note how the
diagrams $B$ and $C$ have exactly the same shape --- but our diagrams
for internal views are much bigger than the corresponding external
views.

In this talk I will present, in a way accessible to non-specialists,
how to work with diagrams for generic cases and particular cases in
parallel and how to transfer knowledge from the general to the
particular {\sl and back} (as in \cite{OchsPH1} and
\cite{OchsACT2019}), how to build internal diagrams in slightly harder
cases than the example above (i.e., in monads!), and how to do the
opposite of the categorists' habit of ``getting rid of the variables''
(as in Part I of \cite{LambekScott}).

I know how to show {\sl formally}, using type systems and
$λ$-calculus, what kinds of knowledge and intutions we can obtain
easily, and almost automatically, by working at the same time in
parallel diagrams like: with $λ$-terms/without, general/particular,
and external/internal; but I don't know yet how describe these kinds
of knowledge and intuitions in terms that are less mathematical and
more philosophical, like for example what Ralf Krömer's did in his
book \cite{Kromer} and in its slides for his keynote talk in
\cite{OchsLucatelli}, available from the web page of the workshop ---
and this is one of my main reasons, or excuses, for trying to present
these ideas to non-mathematicians.


% (find-books "__cats/__cats.el" "lawvere-schanuel")
% (find-lawvereconcmathpage (+ 15  13) "internal diagram of a set")
% (find-THfile "logic-for-children-2018.blogme" "second-class")



% (find-books "__cats/__cats.el" "kromer-slides")
% (find-LATEX "2020tallinn-abstract.bib")


% (nesp 17 "idris-ct")
% (nes     "idris-ct")




%  _____ _          _         _ _                                     
% |  ___(_)_ __ ___| |_    __| (_) __ _  __ _ _ __ __ _ _ __ ___  ___ 
% | |_  | | '__/ __| __|  / _` | |/ _` |/ _` | '__/ _` | '_ ` _ \/ __|
% |  _| | | |  \__ \ |_  | (_| | | (_| | (_| | | | (_| | | | | | \__ \
% |_|   |_|_|  |___/\__|  \__,_|_|\__,_|\__, |_|  \__,_|_| |_| |_|___/
%                                       |___/                         
%
% «first-diagrams»  (to ".first-diagrams")
% (find-LATEX "2017planar-has-1.tex" "internal-external")





% (find-books "__cats/__cats.el" "lawvere-rosebrugh")
% (find-lawveresetsmathpage (+ 15   2) "internal diagram")



% internal/external
% generic/particular
% with lambda-terms/without
% proto/non-proto
% parallel diags to change notation
% internded semantics

% The series of papers \cite{OchsPH1}, \cite{OchsPH2}, and
% \cite{OchsACT2019} --- where \cite{OchsACT2019} can 


% Make obsolete notations more accessible
% Formalize categorical ideas (in two levels)



% (find-math-b-links "2019-newton" "2019newton-slides")



% Translation (in two steps - Kan extensions)
% (jopp 30 "kan-extensions")
% (jop     "kan-extensions")

% (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).")

% Monads:
% (nmop 4)
% (nmo)

% (find-books "__cats/__cats.el" "macdonald-sobral")

% (find-LATEXgrep "grep --color -nH --null -e second *.tex | grep -a class")
% (find-LATEXfile "2017vichy-workshop.tex" "second-class entities")



\bibliographystyle{splncs04}
\bibliography{2020tallinn-abstract}   % (find-LATEX "2020tallinn-abstract.bib")

% (find-es "tex" "bibtex-2017")
% (find-kopkadaly4page (+ 12 310) "\\bibliographystyle{style}")
% (find-kopkadaly4text (+ 12 310) "\\bibliographystyle{style}")



% \newpage

% \printbibliography


\end{document}


%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% «make»  (to ".make")

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019.mk")
make -f 2019.mk STEM=2020tallinn-abstract veryclean
lualatex 2020tallinn-abstract
bibtex   2020tallinn-abstract
lualatex 2020tallinn-abstract
lualatex 2020tallinn-abstract

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
make -f 2019.mk STEM=2020tallinn-abstract veryclean
./dednat6load.lua -4 2020tallinn-abstract.tex
pdflatex             2020tallinn-abstract
bibtex               2020tallinn-abstract
pdflatex             2020tallinn-abstract
pdflatex -record     2020tallinn-abstract

# (find-kopkadaly4page (+ 12 219) "9.3.2   Bibliography with BIBTEX")
# (find-kopkadaly4text (+ 12 219) "9.3.2   Bibliography with BIBTEX")
# (find-LATEXfile "" "2020tallinn-abstract")
# (find-LATEXfile "2020tallinn-abstract.bib")
# (find-LATEXfile "2020tallinn-abstract.bbl")
# (find-es "tex" "bibtex-test")

# (taap)
# (find-latex-upload-links "2020tallinn-abstract")


\end{document}

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