% (find-angg "LATEX/2019notes-monads-tys.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019notes-monads-tys.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019notes-monads-tys.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019notes-monads-tys.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2019notes-monads-tys; makeindex 2019notes-monads-tys"))
% (defun e () (interactive) (find-LATEX "2019notes-monads-tys.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019notes-monads-tys"))
% (find-xpdfpage "~/LATEX/2019notes-monads-tys.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019notes-monads-tys.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019notes-monads-tys.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019notes-monads-tys.pdf
%               file:///tmp/2019notes-monads-tys.pdf
%           file:///tmp/pen/2019notes-monads-tys.pdf
% http://angg.twu.net/LATEX/2019notes-monads-tys.pdf

% «.colors»			(to "colors")
% «.title-page»			(to "title-page")
%   «.diag:generic-adjunction»	(to "diag:generic-adjunction")
%   «.diag:prod-adj-exp»	(to "diag:prod-adj-exp")

\documentclass[oneside]{book}
\usepackage[colorlinks]{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-angg ".emacs.papers" "latexgeom")
\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

% «colors» (to ".colors")
% (find-angg ".emacs.papers" "xcolor")
\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\setofst#1#2{\{\,#1\;|\;#2\,\}}
\def\setofsc#1#2{\{\,#1\;;\;#2\,\}}

\setlength{\parindent}{0em}

\def\O{\mathcal{O}}
\def\T{\mathbf{T}}
\def\F{\mathbf{F}}

\def\Nat{\operatorname{Nat}}

% (find-LATEXfile "2017idarct.tex" "\\def\\sqcond")
\def\respcomp{\mathsf{respcomp}}
\def\respids {\mathsf{respids}}
\def\sqcond  {\mathsf{sqcond}}






%  _____ _ _   _                               
% |_   _(_) |_| | ___   _ __   __ _  __ _  ___ 
%   | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
%   | | | | |_| |  __/ | |_) | (_| | (_| |  __/
%   |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
%                      |_|          |___/      
%
% «title-page» (to ".title-page")
% (nyop 1 "title-page")
% (nyo    "title-page")

% (cl1p 1 "title-page")
% (cl1    "title-page")

\begin{tabular}[b]{c}
{\Large {\bf Notes on adjunctions and monads }}\\
{\Large { (and on how to interpret their }}\\
{\Large { diagrams in type systems) }}\\[2.5pt]
\scriptsize \ColorRed{Eduardo Ochs (UFF, Rio das Ostras, Brazil)} \\[-4pt]
\scriptsize \url{http://angg.twu.net/\#nmoooo?} \\
\\
%
$\begin{array}{ccc}
   \resizebox{!}{30pt}{$diag$} &
   % &
   \begin{array}[c]{l}
     T_0 := λD.λg.(γ;Rg) \\
     γ := TC(\id_C) \\
   \end{array}
 \end{array}
$ \\
%
\end{tabular}

\newpage

\noedrxfooter

% (find-books "__cats/__cats.el" "awodey")
% (find-awodeyctpage (+ 10 180)   "eta")


% «diag:generic-adjunction»  (to ".diag:generic-adjunction")
%
%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
$$\pu
  \diag{generic-adjunction}
$$

% «diag:prod-adj-exp»  (to ".diag:prod-adj-exp")
%
%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
$$\pu
  \diag{(xB)-|(B->)}
$$






\end{document}

% Local Variables:
% coding: utf-8-unix
% End: