% (find-LATEX "2021yoneda.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2021yoneda.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2021yoneda.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page      "~/LATEX/2021yoneda.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2021yoneda.pdf"))
% (defun e () (interactive) (find-LATEX "2021yoneda.tex"))
% (defun u () (interactive) (find-latex-upload-links "2021yoneda"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2021yoneda.pdf"))
%          (code-eec-LATEX "2021yoneda")
% (find-pdf-page   "~/LATEX/2021yoneda.pdf")
% (find-sh0 "cp -v  ~/LATEX/2021yoneda.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2021yoneda.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2021yoneda.pdf
%               file:///tmp/2021yoneda.pdf
%           file:///tmp/pen/2021yoneda.pdf
% http://angg.twu.net/LATEX/2021yoneda.pdf
% (find-LATEX "2019.mk")
% (find-lualatex-links "2021yoneda")

% «.page-1»	(to "page-1")

\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=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{edrx21}               % (find-LATEX "edrx21.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex            % (find-LATEX "edrx21chars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%\input 2017planar-has-defs.tex    % (find-LATEX "2017planar-has-defs.tex")
%
%\usepackage[backend=biber,
%   style=alphabetic]{biblatex}            % (find-es "tex" "biber")
%\addbibresource{catsem-slides.bib}        % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "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

% «page-1»  (to ".page-1")
% (y21p 1 "page-1")
% (y21a   "page-1")


%D diagram Yoneda-functors
%D 2Dx     100  +30
%D 2D  100      A1
%D 2D            |
%D 2D  +25 A2 - A3
%D 2D      |     |
%D 2D  +25 A4 - A5
%D 2D      |     |
%D 2D  +25 A6 - A7
%D 2D      |     |
%D 2D  +25 A8 - A9
%D 2D
%D 2D  +15 B0 - B1
%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 A8 A9 ==> F RF
%D ren B0 B1 ==> \catB \catA
%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    A6 A8  -> .plabel= l m
%D    A7 A9  -> .plabel= r Rm
%D    A6 A9 harrownodes nil 20 nil |->
%D    A8 A9 |->
%D
%D    A1 A5  -> .slide=  20pt .plabel= r h
%D    A1 A7  -> .slide=  35pt .plabel= r ℓ
%D    A2 A6  -> .slide= -15pt .plabel= l k
%D
%D    B0 B1  -> .plabel= a R
%D ))
%D enddiagram
%D
$$\pu
  \diag{Yoneda-functors}
$$



\sa{catB(C,idD)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catB(C,\id_D) \\
    = λf.\;\id_D∘f \\
    = λf.\;f \\
    = \id_{\catB(C,D)} \\
  \end{array}
  $}
  }

\sa{catB(C,g)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catB(C,g) \\
    = λf.\;g∘f \\
  \end{array}
  $}
  }
\sa{catB(C,m)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catB(C,m) \\
    = λk.\;m∘k \\
  \end{array}
  $}
  }
\sa{catB(C,mog)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    (λk.\;m∘k)∘(λf.\;g∘f) \\
    = λf.\;((λk.\;m∘k)∘(λf.\;g∘f))(f) \\
    = λf.\;(λk.\;m∘k)((λf.\;g∘f)(f)) \\
    = λf.\;(λk.\;m∘k)(g∘f) \\
    = λf.\;m∘(g∘f) \\
    = λf.\;(m∘g)∘f \\
    = \catB(C,m∘g) \\
  \end{array}
  $}
  }




%D diagram Yoneda-functor-left
%D 2Dx     100   +30  +55   +30
%D 2D  100 LA0 - LA1  LB0 - LB1
%D 2D      |       |  |     |
%D 2D  +25 |       |  LB2 - LB3
%D 2D      |       |  |     |
%D 2D  +25 LA2 - LA3  LB4 - LB5
%D 2D
%D 2D  +15 LC0 - LC1  LD0 - LD1
%D 2D
%D ren LA0 LA1 ==> D \catB(C,D)
%D ren LA2 LA3 ==> D \catB(C,D)
%D ren LB0 LB1 ==> D \catB(C,D)
%D ren LB2 LB3 ==> E \catB(C,E)
%D ren LB4 LB5 ==> F \catB(C,F)
%D ren LC0 LC1 ==> \catB \Set
%D ren LD0 LD1 ==> \catB \Set
%D
%D (( LA0 LA1 |->
%D    LA0 LA2  -> .plabel= l \id_D
%D    LA1 LA3  -> .plabel= r \ga{catB(C,idD)}
%D    LA0 LA3 harrownodes nil 20 nil |->
%D    LA2 LA3 |->
%D
%D    LB0 LB1 |->
%D    LB0 LB2  -> .plabel= l g
%D    LB1 LB3  -> .plabel= r \ga{catB(C,g)}
%D    LB0 LB3 harrownodes nil 20 nil |->
%D    LB2 LB3 |->
%D    LB2 LB4  -> .plabel= l m
%D    LB3 LB5  -> .plabel= r \ga{catB(C,m)}
%D    LB2 LB5 harrownodes nil 20 nil |->
%D    LB4 LB5 |->
%D
%D    LB0 LB4  -> .slide= -15pt .plabel= l m∘g
%D    LB1 LB5  -> .slide=  60pt .plabel= r \ga{catB(C,mog)}
%D
%D    LC0 LC1 -> .plabel= a \catB(C,-)
%D    LD0 LD1 -> .plabel= a \catB(C,-)
%D ))
%D enddiagram
%D
$$\pu
  \diag{Yoneda-functor-left}
$$


\sa{catA(A,RidD)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catA(A,R\id_D) \\
    = λh.\;R\id_D∘h \\
    = λh.\;\id_{RD}∘h \\
    = λh.\;h \\
    = \id_{\catA(A,RD)} \\
  \end{array}
  $}
  }

\sa{catA(A,Rg)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catA(A,Rg) \\
    = λh.\;Rg∘h \\
  \end{array}
  $}
  }
\sa{catA(A,Rm)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catA(A,Rm) \\
    = λℓ.\;Rm∘ℓ \\
  \end{array}
  $}
  }
\sa{catA(A,R(log))}{
  \scalebox{0.7}{$
  \begin{array}{l}
    (λℓ.\;Rm∘ℓ)∘(λh.\;Rg∘h) \\
    = λh.\;((λℓ.\;Rm∘ℓ)∘(λh.\;Rg∘h))(h) \\
    = λh.\;(λℓ.\;Rm∘ℓ)((λh.\;Rg∘h)(h)) \\
    = λh.\;(λℓ.\;Rm∘ℓ)(Rg∘h) \\
    = λh.\;Rm∘(Rg∘h) \\
    = λh.\;(Rm∘Rg)∘h \\
    = \catA(A,R(m∘g)) \\
  \end{array}
  $}
  }





%D diagram Yoneda-functor-right
%D 2Dx     100   +30  +55   +30
%D 2D  100 RA0 - RA1  RB0 - RB1
%D 2D      |       |  |     |
%D 2D  +25 |       |  RB2 - RB3
%D 2D      |       |  |     |
%D 2D  +25 RA2 - RA3  RB4 - RB5
%D 2D
%D 2D  +15 RC0 - RC1  RD0 - RD1
%D 2D
%D ren RA0 RA1 ==> D \catA(A,RD)
%D ren RA2 RA3 ==> D \catA(A,RD)
%D ren RB0 RB1 ==> D \catA(A,RD)
%D ren RB2 RB3 ==> E \catA(A,RE)
%D ren RB4 RB5 ==> F \catA(A,RF)
%D ren RC0 RC1 ==> \catB \Set
%D ren RD0 RD1 ==> \catB \Set
%D
%D (( RA0 RA1 |->
%D    RA0 RA2  -> .plabel= l \id_D
%D    RA1 RA3  -> .plabel= r \ga{catA(A,RidD)}
%D    RA0 RA3 harrownodes nil 20 nil |->
%D    RA2 RA3 |->
%D
%D    RB0 RB1 |->
%D    RB0 RB2  -> .plabel= l g
%D    RB1 RB3  -> .plabel= r \ga{catA(A,Rg)}
%D    RB0 RB3 harrownodes nil 20 nil |->
%D    RB2 RB3 |->
%D    RB2 RB4  -> .plabel= l m
%D    RB3 RB5  -> .plabel= r \ga{catA(A,Rm)}
%D    RB2 RB5 harrownodes nil 20 nil |->
%D    RB4 RB5 |->
%D
%D    RB0 RB4  -> .slide= -15pt .plabel= l m∘g
%D    RB1 RB5  -> .slide=  60pt .plabel= r \ga{catA(A,R(log))}
%D
%D    RC0 RC1 -> .plabel= a \catA(A,R-)
%D    RD0 RD1 -> .plabel= a \catA(A,R-)
%D ))
%D enddiagram
%D
$$\pu
  \diag{Yoneda-functor-right}
$$




\newpage

New diagrams for the Yoneda Lemma.

See M-x fav for the old ones.


%D diagram ??
%D 2Dx     100 +30  +50 +35  +40  +35
%D 2D  100          A1
%D 2D                |
%D 2D  +25     A2 - A3
%D 2D          |     |
%D 2D  +25     A4 - A5
%D 2D          |     |
%D 2D  +25     A6 - A7
%D 2D          |     |
%D 2D  +25     A8 - A9
%D 2D
%D 2D  +15     B0 - B1
%D 2D                 
%D 2D  +20 C0  D0 - D1  F0 - F1   F1r
%D 2D      |   |     |  |    F3a
%D 2D  +25 C1  D2 - D3  F2 - F3   F3r
%D 2D                   F2b  F3b
%D 2D  +15     E0 - E1
%D 2D
%D 2D  +20
%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 A8 A9 ==> F RF
%D ren B0 B1 ==> \catB \catA
%D ren C0 C1 ==> D E
%D ren D0 D1 ==> \catB(C,D) \catA(A,RD)
%D ren D2 D3 ==> \catB(C,E) \catA(A,RE)
%D ren E0 E1 ==> \catB(C,-) \catA(A,R-)
%D
%D newnode: F3a at: @F3+v(0,-8)  .TeX= Rg∘(Rf∘η)
%D newnode: F2b at: @F2+v(0,8)   .TeX= h
%D newnode: F3b at: @F3+v(0,8)   .TeX= Rh∘η
%D # newnode: F1r at: @F1+v(10,0)
%D # newnode: F3r at: @F3+v(10,0)
%D
%D ren F0 F1 F2 F3 ==> f Rf∘η g∘f R(g∘f)∘η
%D ren F1r F3r     ==> k Rg∘k
%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    A6 A8  -> .plabel= l g
%D    A7 A9  -> .plabel= r Rg
%D    A6 A9 harrownodes nil 20 nil |->
%D    A8 A9 |->
%D
%D    A1 A5  -> .slide=  20pt .plabel= r k
%D    A2 A6  -> .slide= -15pt .plabel= l h
%D
%D    B0 B1  -> .plabel= a R
%D
%D    C0 C1  -> .plabel= l g
%D    D0 D1  -> .plabel= a \sm{TC=\\λf.(Rf∘η)}
%D    D0 D2  -> .plabel= l \sm{\catB(C,g)=\\λf.(g∘f)}
%D    D1 D3  -> .plabel= r \sm{\catA(A,Rg)=\\λk.(Rg∘k)}
%D    D2 D3  -> .plabel= a \sm{TD=\\λh.(Rh∘η)}
%D    E0 E1  -> .plabel= a T
%D
%D    F0 F1 |-> F1 F3a |->
%D    F0 F2 |-> F2 F3 |->
%D    F2b F3b |->  F1r F3r |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

$$T_0 = (λC.λf.(Rf∘η)) = (λD.λh.(Rh∘η))$$

% (favp 33 "basic-example-full")
% (fava    "basic-example-full")



\newpage





%D diagram ??
%D 2Dx     100  +45
%D 2D  100      A1
%D 2D            |
%D 2D  +25 A2 - A3
%D 2D
%D 2D  +15 B0 - B1
%D 2D  +10 C0 - C1
%D 2D  +10 D0 - D1
%D 2D
%D ren    A1 ==>    A
%D ren A2 A3 ==> B RB
%D ren B0 B1 ==> \id (TB)(\id)
%D ren C0 C1 ==> \catB(B,B) \catA(A,RB)
%D ren D0 D1 ==> \catB(B,-) \catA(A,R-)
%D
%D (( A1 A3 -> .plabel= r η
%D    A2 A3 |->
%D    B0 B1 |-> 
%D    C0 C1  -> .plabel= a TB 
%D    D0 D1  -> .plabel= a T
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

% (favp 31 "basic-example-bij")
% (fava    "basic-example-bij")




%\printbibliography

\GenericWarning{Success:}{Success!!!}  % Used by `M-x cv'

\end{document}

%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% <make>

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2021yoneda veryclean
make -f 2019.mk STEM=2021yoneda pdf

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