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

\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")

\def\respcomp{\mathsf{respcomp}}
\def\respids {\mathsf{respids}}
\def\sqcond  {\mathsf{sqcond}}
\def\Te {T_\eta}
\def\Tez{(T_\eta)_0}
\def\eTe{\eta_{T_\eta}}
\def\TeT{T_{\eta_T}}




%L forths["<."]  = function () pusharrow("<.") end

%D diagram Y0-main-names
%D 2Dx     100  +40
%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 - C1
%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 ==> \catB(C,-) \catA(A,R-)
%D
%D (( A1 A3  -> .plabel= r η
%D    A2 A3 |->
%D    A2 A4  -> .plabel= l f
%D    A3 A5  -> .plabel= r Rf
%D    A2 A5 harrownodes nil 20 nil |->
%D    A4 A5 |->
%D    A4 A6  -> .plabel= l g
%D    A5 A7  -> .plabel= r Rg
%D    A4 A7 harrownodes nil 20 nil |->
%D    A6 A7 |->
%D    A6 A8  -> .plabel= l h
%D    A7 A9  -> .plabel= r Rh
%D    A6 A9 harrownodes nil 20 nil |->
%D    A8 A9 |->
%D
%D    A2 A6  -> .slide= -15pt .plabel= l k
%D    A1 A5  -> .slide=  20pt .plabel= r ℓ
%D    A1 A7  -> .slide=  35pt .plabel= r m
%D
%D    B0 B1  -> .plabel= a R
%D
%D    C0 C1  -> .plabel= a T
%D  # C0 C1  <. .plabel= b T^{-1} .slide= -5pt
%D ))
%D enddiagram
\pu

\def\ColorOpt#1{{\color{brown} #1}}
\def\opt#1{\ColorOpt{\{} #1 \ColorOpt{\}}}
\def\s{\;\;\;\;\;\;\;}

%\sa{B(C,-).identity}{
%  \begin{array}{ll}
%    \catB(C,-).\text{identity}    & \text{is:} \\ [5pt]
%    %
%    ∀D. \; \catB(C,-)._1 \; (\catB.\id \; \opt{D})  \\
%    \s   = \Set.\id \; \opt{\catB(C,-)._0 \; D}, & \text{that is:} \\[5pt]
%    %
%    ∀D. \; \catB(C,\id_D)     \\
%    \s   = λf.\, \id_D ∘_\catB f  \\
%    \s   = λf.\,  f         \\
%    \s   = \id_{\catB(C,D)} \\
%  \end{array}
%  }
%\sa{A(A,R-).identity}{
%  \begin{array}{ll}
%    \catA(A,R-).\text{identity}    & \text{is:} \\ [5pt]
%    %
%    ∀D. \; \catA(A,R-)._1 \; (\catB.\id \; \opt{D})  \\
%    \s   = \Set.\id \; \opt{\catA(A,R-)._0 \; D}, & \text{that is:} \\[5pt]
%    %
%    ∀D. \; \catA(A,R(\id_D))         \\
%    \s   = λℓ.\, \id_{RD} ∘_\catA ℓ  \\
%    \s   = λℓ.\, ℓ                   \\
%    \s   = \id_{\catA(C,D)}          \\
%  \end{array}
%  }

\sa{Y0 constructions}{
  \begin{array}{rcl}
        \catA &\text{is}& \text{a small category} \\
        \catB &\text{is}& \text{a small category} \\
            R &:& \catB \to \catA \\
            A &∈& \catA \\
            C &∈& \catB \\[5pt]
              %
     B(C,-)   &:& \catB \to \Set  \\
     B(C,-)_0 &=& λD.\,\catB(C,D) \\
     B(C,-)_1 &=& λg.\,λf.\,g∘f   \\[5pt]
              %
    A(A,R-)   &:& \catB \to \Set   \\
    A(A,R-)_0 &=& λD.\,\catA(A,RD) \\
    A(A,R-)_1 &=& λg.\,λℓ.\,Rg∘ℓ   \\[5pt]
              %
            η &:& A \to RC           \\
            T &:& B(C,-) \to A(A,R-) \\[5pt]
         %      %
         %  η_T &=& T(C)(\id_C)       \\
         % \Tez &=& λD. \, λf.\, Rf∘η \\
              %
      (T_0↦η) &=& λT_0.\,T_0(C)(\id_C)   \\
      (η↦T_0) &=& λη.\,λD. \, λf.\, Rf∘η \\
    \end{array}
  }

\sa{respids B(C,-)}{
  \begin{array}{ll}
    \respids_{\catB(C,-)} \quad \text{is:} \\ [5pt]
    %
    ∀D. \; \catB(C,\id_D)         \\
    \s   = λf.\, \id_D ∘_\catB f  \\
    \s   = λf.\,  f               \\
    \s   = \id_{\catB(C,D)}       \\
  \end{array}
  }
\sa{respids A(A,R-)}{
  \begin{array}{ll}
    \respids_{\catA(A,R-)} \quad \text{is:} \\ [5pt]
    %
    ∀D. \; \catA(A,R(\id_D))         \\
    \s   = λℓ.\, \id_{RD} ∘_\catA ℓ  \\
    \s   = λℓ.\, ℓ                   \\
    \s   = \id_{\catA(C,D)}          \\
  \end{array}
  }

\sa{respcomp B(C,-)}{
  \begin{array}{ll}
    \respcomp_{\catB(C,-)} \quad \text{is:} \\ [5pt]
    %
    ∀D,E,F,g,h.  \\
    \s   \catB(C,h) ∘_\Set \catB(C,g)  \\
    \s   = (λk.\,h ∘_\catB k) ∘_\Set (λf.g ∘_\catB f)    \\
    \s   = λf.\,h ∘_\catB (g ∘_\catB f)             \\
    \s   = λf.\,(h ∘_\catB g) ∘_\catB f             \\
    \s   = \catB(C,h ∘_\catB g)             \\
  \end{array}
  }

\sa{respcomp A(A,R-)}{
  \begin{array}{ll}
    \respcomp_{\catA(A,R-)} \quad \text{is:} \\ [5pt]
    %
    ∀D,E,F,g,h.  \\
    \s   \catA(A,Rh) ∘_\Set \catA(A,Rg)  \\
    \s   = (λk.\,h ∘_\catB k) ∘_\Set (λf.g ∘_\catB f)    \\
    \s   = λf.\,h ∘_\catB (g ∘_\catB f)             \\
    \s   = λf.\,(h ∘_\catB g) ∘_\catB f             \\
    \s   = \catA(A,h ∘_\catB g)             \\
  \end{array}
  }







$$\pu
  \diag{Y0-main-names}
  \qquad
  \ga{Y0 constructions}
$$

$$\ga{respids B(C,-)}
  \qquad
  \ga{respids A(A,R-)}
$$

$$\ga{respcomp B(C,-)}
  \qquad
  \ga{respcomp A(A,R-)}
$$

\newpage

\sa{sqcond Te}{
  \begin{array}{ll}
    \sqcond_{\Te} \quad \text{is:} \\ [5pt]
    %
    ∀D,E,g.  \\
    \s   \Tez(E) ∘_\Set \catB(C,g)  \\
    \s   = (λk.\,Rk ∘_\catA η) ∘_\Set (λf.\,g ∘_\catB f) \\
    \s   = (λf.\,R(g ∘_\catB f) ∘_\catA η) \\
    \s   = (λf.\,Rg ∘_\catA (Rf ∘_\catA η)) \\
    \s   = (λℓ.\,Rg∘ℓ) ∘_\Set (λf.\,Rf∘η) \\
    \s   = \catA(A,Rg) ∘_\Set \Tez(D) \\
  \end{array}
  }


\sa{eTe = e}{
  \begin{array}{ll}
    (\eTe = η) \quad \text{is:} \\ [5pt]
    %
    (T_0→η) ((η↦T_0) (η))                         \\
    = (T_0→η) ((λη.\,λD. \, λf.\, Rf∘η) (η))      \\
    = (T_0→η) (λD. \, λf.\, Rf∘η)                 \\
    = (λT_0.\,T_0(C)(\id_C)) (λD. \, λf.\, Rf∘η)  \\
    = (λD. \, λf.\, Rf∘η) (C) (\id_C)             \\
    = R \id_C ∘ η                                 \\
    = \id_{RC} ∘η                                 \\
    = η                                           \\
  \end{array}
  }


$$\diag{Y0-main-names}
  \qquad
  \ga{Y0 constructions}
$$

$$\ga{sqcond Te}
  \qquad
  \ga{eTe = e}
$$

\newpage

\sa{(TeT)_0 = T_0}{
  \begin{array}{ll}
    ((\TeT)_0 = T_0) \quad \text{is:} \\ [5pt]
    %
    (η↦T_0) ((T_0→η) (T_0))                       \\
    = (η↦T_0) ((λT_0.\,T_0(C)(\id_C)) (T_0))      \\
    = (η↦T_0) (T_0(C)(\id_C))                     \\
    = (λη.\,λD. \, λf.\, Rf∘η) (T_0(C)(\id_C))    \\
    = λD. \, λf. \, Rf∘(T_0(C)(\id_C))            \\
    = λD. \, λf. \, T_0(D)(f)                     \\
    = T_0                                         \\
  \end{array}
  }

$$\diag{Y0-main-names}
  \qquad
  \ga{Y0 constructions}
$$

$$\ga{(TeT)_0 = T_0}
$$

\newpage

{\bf Lemma: $Rf∘TC(\id_C) = TD(f)$.}

{\bf Formal proof:} if we apply $\sqcond_T$ to $f:D→C$ we get:
%
$$∀D.\,∀f.\,∀γ.\,Rf∘TC(γ) = TD(f∘γ)$$

and if we specialize $γ:=\id_C$ above and simplify a bit we get:
%
$$∀D.\,∀f.\,Rf∘TC(\id_C) = TD(f)$$


%D diagram lemma-diag-1
%D 2Dx     100  +40
%D 2D  100      A1
%D 2D            |
%D 2D  +20 A2 - A3
%D 2D      |     |
%D 2D  +20 A4 - A5
%D 2D      |     |
%D 2D  +20 A6 - A7
%D 2D
%D 2D  +15 B0 - B1
%D 2D
%D 2D  +20 C0 - C1
%D 2D
%D ren    A1 ==>    A
%D ren A2 A3 ==> C RC
%D ren A4 A5 ==> C RC
%D ren A6 A7 ==> D RD
%D ren B0 B1 ==> \catB \catA
%D ren C0 C1 ==> \catB(C,-) \catA(A,R-)
%D
%D (( A1 A3  -> # .plabel= r η
%D    A2 A3 |->
%D    A2 A4  -> .plabel= l \id_C
%D    A3 A5  -> .plabel= r R\id_C
%D    A2 A5 harrownodes nil 20 nil |->
%D    A4 A5 |->
%D    A4 A6  -> .plabel= l f
%D    A5 A7  -> .plabel= r Rf
%D    A4 A7 harrownodes nil 20 nil |->
%D    A6 A7 |->
%D
%D  # A2 A6  -> .slide= -15pt .plabel= l k
%D    A1 A5  -> .slide=  30pt .plabel= r T(C)(\id_C)
%D    A1 A7  -> .slide=  80pt .plabel= r \sm{T(D)(f∘\id_C)\\=T(D)(f)}
%D
%D    B0 B1  -> .plabel= a R
%D
%D    C0 C1  -> .plabel= a T
%D  # C0 C1  <. .plabel= b T^{-1} .slide= -5pt
%D ))
%D enddiagram

%D diagram Y0-NT-3
%D 2Dx     100 +25  +40 +30    +35 +30    +35 
%D 2D  100 A0  B0 - B1  D0 |-> D1  E0 |-> E1  
%D 2D  +17 |   |    |   |      D3' |      E3' 
%D 2D  +8  A1  B2 - B3  D2 |-> D3  E2 |-> E3  
%D 2D
%D 2D  +15     C0 - C1
%D 2D
%D ren A0 A1       ==> C D
%D ren B0 B1 B2 B3 ==> \catB(C,C) \catA(A,RC) \catB(C,D) \catA(A,RD)
%D ren C0 C1       ==> \catB(C,-) \catA(A,R-)
%D # ren D0 D1 D3'   ==> \id_C TC(\id_C) Rf∘(TC(\id_C))
%D # ren D2 D2' D3   ==> f∘\id_C f TD(f)
%D
%D ren D0 D1 D3'   ==> γ TC(γ) Rf∘TC(γ)
%D ren D2    D3    ==> f∘γ TD(f∘γ)
%D ren E0 E1 E3'   ==> \id_C TC(\id_C) Rf∘TC(\id_C)
%D ren E2    E3    ==> f TD(f)
%D
%D (( A0 A1 -> .plabel= l f
%D    B0 B1 -> .plabel= a TC
%D    B0 B2 -> .plabel= l \catB(C,f)
%D    B1 B3 -> .plabel= r \catA(A,Rf)
%D    B2 B3 -> .plabel= a TD
%D    C0 C1 -> .plabel= a T
%D    D0 D1 |-> D1 D3' |->
%D    D0 D2 |-> D2 D3 |->
%D    E0 E1 |-> E1 E3' |->
%D    E0 E2 |-> E2 E3 |->
%D ))
%D enddiagram
\pu


{\bf Diagrams:}
%
$$\diag{Y0-NT-3}
$$

$$\diag{lemma-diag-1}
$$


% (favp 31 "basic-example-bij")
% (fava    "basic-example-bij")
% (fava    "basic-example-bij" "Y0-NT-3")



%    identity     : ∀ {A} → D [ F₁ (C.id {A}) ≈ D.id ]
%    homomorphism : ∀ {X Y Z} {f : C [ X , Y ]} {g : C [ Y , Z ]} →
%                     D [ F₁ (C [ g ∘ f ]) ≈ D [ F₁ g ∘ F₁ f ] ]





% %L dofile "edrxtikz.lua"  -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua"  -- (find-LATEX "edrxpict.lua")
% \pu

%\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=2022yoneda-pseudocode veryclean
make -f 2019.mk STEM=2022yoneda-pseudocode pdf

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