% (find-LATEX "2020abramsky-tzevelekos.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020abramsky-tzevelekos.tex" :end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2020abramsky-tzevelekos.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020abramsky-tzevelekos.pdf"))
% (defun e () (interactive) (find-LATEX "2020abramsky-tzevelekos.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020abramsky-tzevelekos"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page   "~/LATEX/2020abramsky-tzevelekos.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020abramsky-tzevelekos.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020abramsky-tzevelekos.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020abramsky-tzevelekos.pdf
%               file:///tmp/2020abramsky-tzevelekos.pdf
%           file:///tmp/pen/2020abramsky-tzevelekos.pdf
% http://angg.twu.net/LATEX/2020abramsky-tzevelekos.pdf
% (find-LATEX "2019.mk")

% «.univs-define-adjunctions»	(to "univs-define-adjunctions")
% «.kleisli»			(to "kleisli")

\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{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")
\begin{document}

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



{\setlength{\parindent}{0em}
\footnotesize

Notes on Samson Abramsky and Nikos Tzevelekos's

"Introduction to Categories and Categorical Logic" (2011):

\url{https://arxiv.org/abs/1102.1313}

\url{https://arxiv.org/pdf/1102.1313.pdf}

\ssk

These notes are at:

\url{http://angg.twu.net/LATEX/2020abramsky-tzevelekos.pdf}

}


\bsk
\bsk

\section*{1.5.2. Universal Arrows and Adjoints}
% (find-abramskyticclpage 46 "1.5.2 Universal Arrows and Adjoints")
% (find-abramskyticcltext 46 "1.5.2 Universal Arrows and Adjoints")

\newpage

% «univs-define-adjunctions»  (to ".univs-define-adjunctions")
% (find-abramskyticclpage 48 "Proposition 69 (Universals define adjunctions)")
% (find-abramskyticcltext 48 "Proposition 69 (Universals define adjunctions)")

(P.48):

Proposition 69: universals define adjunctions.

Let $G:\calD→\calC$ and suppose that we have an operation $C \mapsto
(FC, η_C)$ that returns universal arrows. Then we can define an
adjunction $(F, G, Θ)$ from that:
%
%D diagram univs-define-adjunctions-1
%D 2Dx     100 +25 +20 +40 +25 +30 +25
%D 2D  100     A1
%D 2D           | \
%D 2D  +20 A2  A3  \       C1      E1
%D 2D      |        |       |       |
%D 2D  +20 |       A5  C2  C3  E2  E3
%D 2D      |        |  |    |  |    |
%D 2D  +25 A6 ---- A7  C4  C5  E4  E5
%D 2D
%D 2D  +20 B0 ---- B1  D0  D1  F0  F1
%D 2D
%D ren A1 A2 A3   A5 A6 A7  B0 B1 ==> C FC GFC   C' FC' GFC' \calD \calC
%D ren C1 C2 C3 C4 C5       D0 D1 ==> C FC GFC   D GD        \calD \calC
%D ren E1 E2 E3 E4 E5       F0 F1 ==> C FC GFC   D GD        \calD \calC
%D
%D (( A1 A3  -> .plabel= l η_C
%D    A2 A3 |->
%D    A5 A7  -> .plabel= r η_{C'}
%D    A6 A7 |->
%D
%D    A1 A5  -> .plabel= r f     # .curve= ^10pt
%D    A2 A6  -> .plabel= l \sm{Ff:=\\\widehat{η_{C'}∘f}}
%D    B0 B1  -> .plabel= a G
%D    A2 A5 harrownodes nil 20 nil <-| sl_ .plabel= a F
%D
%D    C1 C3  -> .plabel= l η_C
%D    C2 C3 |->
%D    C2 C4  -> .plabel= l \sm{Θ_{C,D}(f):=\\\hat{f}}
%D    C4 C5 |->
%D    C1 C5  -> .slide= 15pt .plabel= r f
%D    C2 C5 harrownodes nil 20 nil <-| sl^ .plabel= a Θ_{C,D}
%D    D0 D1  -> .plabel= a G
%D
%D    E1 E3  -> .plabel= l η_C
%D    E2 E3 |->
%D    E2 E4  -> .plabel= l h
%D    E4 E5 |->
%D    E1 E5  -> .slide= 15pt .plabel= r \sm{Θ_{C,D}^{-1}(h):=\\Gh∘η_C}
%D    E2 E5 harrownodes nil 20 nil |-> sl_ .plabel= b Θ_{C,D}^{-1}
%D    F0 F1  -> .plabel= a G
%D ))
%D enddiagram
%D
$$\pu
  \diag{univs-define-adjunctions-1}
$$

\bsk

%D diagram univs-define-adjunctions-2
%D 2Dx     100 +25 +50
%D 2D  100 A0  A1
%D 2D      |    |
%D 2D  +25 A2  A3  C0
%D 2D      |    |
%D 2D  +25 A4  A5  C1
%D 2D      |    |
%D 2D  +25 A6  A7
%D 2D
%D 2D  +20 B0  B1
%D 2D
%D ren A0 A1   A2 A3   A4 A5   A6 A7 ==> FA' A' FA A B GB B' GB'
%D ren B0 B1 ==> \calD \calC
%D ren C0 C1 ==> A GFA
%D
%D (( A0 A1 <-|
%D    A2 A3 <-|
%D    A4 A5 |->
%D    A6 A7 |->
%D    B0 B1 <-- sl^ .plabel= a F
%D    B0 B1  -> sl_ .plabel= b G
%D
%D    C0 C1 -> .plabel= r η_A
%D
%D    A0 A2 -> .plabel= l Fg:=\widehat{η_A∘g}
%D    A1 A3 -> .plabel= r g
%D    A2 A4 -> .plabel= l \sm{Θ_{A,B}(f):=\hat{f}\\k}
%D    A3 A5 -> .plabel= r \sm{f\\Θ_{A,B}^{-1}(k):=Gk∘η_A}
%D    A4 A6 ->
%D    A5 A7 ->
%D
%D    A0 A3 harrownodes nil 20 nil <-|     .plabel= a F
%D    A2 A5 harrownodes nil 20 nil <-| sl^ .plabel= a Θ_{A,B}
%D    A2 A5 harrownodes nil 20 nil |-> sl_ .plabel= b Θ_{A,B}^{-1}
%D ))
%D enddiagram
%D
$$\pu
  \diag{univs-define-adjunctions-2}
  \qquad
  \begin{array}{l}
    \pmat{F, \\ G, \\ Θ, \\ Θ^{-1}} \;\; :=
    \\ \\ 
    \pmat{\pmat{C↦FC \\
                (f:C→C') ↦ η_{C'}∘f
               } \\
          G, \\
          λC.λD.λ(f:C→GD).\hat{f}, \\
          λC.λD.λ(h:FC→D).Gh∘η_C   \\
         }
  \end{array}
$$




% (find-abramskyticclpage 50 "Proposition 70 (Adjunctions define universals)")
% (find-abramskyticcltext 50 "Proposition 70 (Adjunctions define universals)")



% (find-books "__cats/__cats.el" "abramsky-tzevelekos")
% (find-abramskyticclpage 42 "1.5 Universality and Adjoints")
% (find-abramskyticclpage 43 "1.5.1 Adjunctions for Posets")

% (find-abramskyticclpage 52 "1.5.3 Limits and Colimits")
% (find-abramskyticclpage 53 "1.5.4 Exponentials")
% (find-abramskyticclpage 55 "1.5.5 Exercises")


\newpage

% «kleisli»  (to ".kleisli")
% (find-abramskyticclpage 89 "1.8.3 The Kleisli Construction")





\end{document}

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

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

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