Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% (find-angg "LATEX/2016-2-LA-cats.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2016-2-LA-cats.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2016-2-LA-cats.pdf"))
% (defun e () (interactive) (find-LATEX "2016-2-LA-cats.tex"))
% (defun u () (interactive) (find-latex-upload-links "2016-2-LA-cats"))
% (find-xpdfpage "~/LATEX/2016-2-LA-cats.pdf")
% (find-sh0 "cp -v  ~/LATEX/2016-2-LA-cats.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2016-2-LA-cats.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2016-2-LA-cats.pdf
%               file:///tmp/2016-2-LA-cats.pdf
%           file:///tmp/pen/2016-2-LA-cats.pdf
% http://angg.twu.net/LATEX/2016-2-LA-cats.pdf
%
% «.composition»	(to "composition")
% «.lateral-inverses»	(to "lateral-inverses")
% «.multiple-inverses»	(to "multiple-inverses")
% «.no-inverses»	(to "no-inverses")
% «.products»		(to "products")
% «.exponentials»	(to "exponentials")

\documentclass[oneside]{book}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%\usepackage{tikz}
%
\usepackage{edrx15}               % (find-angg "LATEX/edrx15.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-dn4ex "edrxheadfoot.tex")
%
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\begin{document}

\catcode`\^^J=10
\directlua{dednat6dir = "dednat6/"}
\directlua{dofile(dednat6dir.."dednat6.lua")}
\directlua{texfile(tex.jobname)}
\directlua{verbose()}
\directlua{output(preamble1)}
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
\def\pu{\directlua{pu()}}

% \directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
% %L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end

\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\textstyle #2}}
\def\subf#1{\underbrace{#1}_{}}
\def\p{\phantom{(}}

\def\cur{\operatorname{cur}}
\def\uncur{\operatorname{uncur}}
\def\app{\operatorname{app}}
\def\ren{\operatorname{ren}}

\defâ{\&}

\def\namedfunction#1#2#3#4#5{
  \begin{array}{rrcl}
    #1: & #2 & â & #3 \\
        & #4 & â & #5 \\
  \end{array}
  }




%                                      _ _   _             
%   ___ ___  _ __ ___  _ __   ___  ___(_) |_(_) ___  _ __  
%  / __/ _ \| '_ ` _ \| '_ \ / _ \/ __| | __| |/ _ \| '_ \ 
% | (_| (_) | | | | | | |_) | (_) \__ \ | |_| | (_) | | | |
%  \___\___/|_| |_| |_| .__/ \___/|___/_|\__|_|\___/|_| |_|
%                     |_|                                  
%
% «composition» (to ".composition")
% (lac162p 1 "composition")

Composition

(is associative)

%L mapstos_1 = function (str)
%L     local n, latex = 0, ""
%L     for d in str:gmatch("%d") do
%L       latex = latex .. format("%d \\mapsto %d \\\\\n", n, d)
%L       n = n + 1
%L     end
%L     return latex
%L   end
%L 
%L mapstos_2 = function (str)
%L     local latex = ""
%L     for a,b in str:gmatch("(%d)(%d)") do
%L       latex = latex .. format("%d \\mapsto %d \\\\\n", a, b)
%L     end
%L     return latex
%L   end
\pu

\def\mapsb #1{\sm{\expr{mapstos_1("#1")}}}
\def\mapsab#1{\sm{\expr{mapstos_2("#1")}}}

% \bsk

%D diagram ??
%D 2Dx     100   +35   +35  +35   +35   +35  
%D 2D  100 A --> B          a --> b          
%D 2D            |                |          
%D 2D            v                v          
%D 2D  +35       C --> D          c --> d    
%D 2D
%D ren  a b     ==>  \{1,2\} \{3,4\}
%D ren    c d   ==>          \{5,6\} \{7,8\} 
%D (( A B -> .plabel= a f
%D    B C -> .plabel= m g
%D    C D -> .plabel= b h
%D    A C -> .plabel= l (gâf=)\;\;f;g
%D    B D -> .plabel= r g;h\;\;(=hâg)
%D    
%D    a b -> .plabel= a \mapsab{13,24}
%D    b c -> .plabel= m \mapsab{36,45}
%D    c d -> .plabel= b \mapsab{57,67}
%D    a c ->  b d ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\bsk

%D diagram composition-1
%D 2Dx     100   +30   +30   +30
%D 2D  100 D <-- C <-- B <-- A
%D 2D
%D (( D A <- .plabel= a (hâg)âf .slide= 22pt
%D    D B <- .plabel= a  hâg    .slide= 10pt
%D    D C <- .plabel= m h   C B <- .plabel= m g  B A <- .plabel= m f
%D    C A <- .plabel= b    gâf  .slide= -10pt
%D    D A <- .plabel= b hâ(gâf) .slide= -22pt
%D ))
%D enddiagram
%D
%
$$\begin{array}{rcl}
  ((hâg)âf)(a) &=& (hâg)(f(a)) \\
               &=& h(g(f(a))) \\
               &=& h((gâf)(a)) \\
               &=& (hâ(gâf))(a) \\[5pt]
  ((hâg)âf)(a) &=& (hâ(gâf))(a) \\[5pt]
  (hâg)âf &=& hâ(gâf) \\
  \end{array}
  \qquad
  \Diag{composition-1}
$$


\bsk
\bsk

Identities:

If $f:AâB$ then $\id_A;f = f = f;\id_B$ 

%D diagram ??
%D 2Dx     100   +35   +35  +35   +35   +35  
%D 2D  100 A --> B          a --> b          
%D 2D            |                |          
%D 2D            v                v          
%D 2D  +35       C --> D          c --> d    
%D 2D
%D ren  A B     ==>  A  A
%D ren    C D   ==>     B  B
%D ren  a b     ==>  \{1,2\} \{1,2\}
%D ren    c d   ==>          \{3,4\} \{3,4\} 
%D (( A B -> .plabel= a \id_A
%D    B C -> .plabel= m f
%D    C D -> .plabel= b \id_B
%D    A C -> .plabel= l f\;=\;\id_A;f
%D    B D -> .plabel= r f;\id_B\;=\;f
%D    
%D    a b -> .plabel= a \mapsab{11,22}
%D    b c -> .plabel= m \mapsab{13,24}
%D    c d -> .plabel= b \mapsab{33,44}
%D    a c ->  b d ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\bsk
\bsk

% «lateral-inverses» (to ".lateral-inverses")

A theorem about lateral inverses:

If $f;g = \id$ and $g;h=\id$ then $f=h$

%D diagram ??
%D 2Dx     100   +35   +35  +35   +35   +35  
%D 2D  100 A --> B          a --> b          
%D 2D            |                |          
%D 2D            v                v          
%D 2D  +35       C --> D          c --> d    
%D 2D
%D ren  A B     ==>  B  A
%D ren    C D   ==>     B  A
%D ren  a b     ==>  \{1,2\} \{1,2\}
%D ren    c d   ==>          \{3,4\} \{3,4\} 
%D (( A B -> .plabel= a f
%D    B C -> .plabel= m g
%D    C D -> .plabel= b h
%D    A C -> .plabel= l \id_B\;=\;f;g
%D    B D -> .plabel= r \id_A\;=\;g;h
%D    
%D #   a b -> .plabel= a \mapsab{11,22}
%D #   b c -> .plabel= m \mapsab{13,24}
%D #   c d -> .plabel= b \mapsab{33,44}
%D #   a c ->  b d ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
  \qquad
  \begin{array}{rcl}
  \multicolumn {3}{c} {(f;g);h = \id_B;h = h} \\
  \multicolumn {3}{c} {f;(g;h) = f;\id_A = f} \\[5pt]
  f &=& f;\id_A \\
    &=& f;(g;h) \\
    &=& (f;g);h \\
    &=& \id_B;h \\
    &=& h
  \end{array}
$$



\newpage

% «multiple-inverses» (to ".multiple-inverses")
% (lac162p 2 "multiple-inverses")

Multiple inverses

%L forths["->>"] = function () pusharrow("->>") end

%D diagram ??
%D 2Dx     100   +35   +35   +35
%D 2D  100 A --> B     D
%D 2D            |     |
%D 2D            v     v
%D 2D  +35       C     E --> F
%D 2D
%D ren  A B  D     ==> \{1,2\} \{3,4,5\}   \{5,6\}
%D ren    C  E F   ==>          \{1,2\}   \{7,8,9\} \{5,6\}
%D (( A B >-> sl^ .plabel= a ?  A B >-> sl_ .plabel= b ?
%D    B C ->> .plabel= r \mapsab{31,42,52}
%D    A C  -> .plabel= l \id
%D
%D    D E ->> .plabel= l \mapsab{57,68}
%D    E F >-> sl^ .plabel= a ? E F >-> sl_ .plabel= b ?
%D    D F  -> .plabel= r \id
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\bsk
\bsk

\def\frown{=(}

% «no-inverses» (to ".no-inverses")

No inverses

%D diagram ??
%D 2Dx     100   +35   +35  +10   +35   +35
%D 2D  100 A --> B          E --> F
%D 2D            |                |
%D 2D            v                v
%D 2D  +35       C --> D          G --> H
%D 2D
%D ren  A B    E F     ==> \{3,4,5\} \{1,2\}           \{8,9\} \{5,6,7\}
%D ren    C D    G H   ==>          \{3,4,5\} \{1,2\}           \{8,9\} \{5,6,7\}
%D (( A B  -> .plabel= a \frown
%D    B C >-> .plabel= m \mapsab{13,24}
%D    A C  -> .plabel= l \id
%D    C D ->> sl^ C D ->> sl_
%D    B D -> .plabel= r \id
%D
%D    E G  -> .plabel= l \id
%D    E F >-> sl^ E F >-> sl_
%D    F G ->> .plabel= m \mapsab{58,69,79}
%D    G H  -> .plabel= b \frown
%D    F H  -> .plabel= r \id
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

%D diagram ??
%D 2Dx     100   +35   +35
%D 2D  100 A --> B
%D 2D            |
%D 2D            v
%D 2D  +35       C --> D
%D 2D
%D ren  A B     ==> \{4,5,6\} \{1,2,3\}
%D ren    C D   ==>           \{4,5,6\} \{1,2,3\} 
%D (( A B -> .plabel= a \frown
%D    B C -> .plabel= m \mapsab{14,25,35}
%D    C D -> .plabel= r \frown
%D    A C -> .plabel= l \id
%D    B D -> .plabel= r \id
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


\bsk
\bsk
\bsk

% «products» (to ".products")
% (lac162p 2 "products")

{\bf Products}

Property: $âf,g.â!h.(f=h;Ï\;â\;g=h;Ï')$

Solution: $h=»a:A.(f(a),g(a))$

Bijection: $(f,g)âh$

$(â)$: $»(f,g).(»a:A.(f(a),g(a)))$

$(â)$: $»h.((h;Ï),(h;Ï'))$

\bsk


%D diagram product-ABC
%D 2Dx     100    +45    +45
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +45 B <-- BxC --> C
%D 2D
%D ren    A      ==>    A
%D ren B BxC C   ==> B BÃC C
%D
%D (( A  B  -> .plabel= l f
%D    A BxC -> .plabel= m h
%D    A  C  -> .plabel= r g
%D    B BxC <- .plabel= b Ï\mathstrut
%D    BxC C -> .plabel= b Ï'
%D ))
%D enddiagram
%D
%D diagram product-explicit
%D 2Dx     100    +45    +45
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +45 B <-- BxC --> C
%D 2D
%D ren    A      ==>                      \{1,2\}
%D ren B BxC C   ==> \{3,4\}  \csm{(3,5),(3,6),\\(4,5),(4,6)}  \{5,6\} 
%D
%D (( A  B  -> .plabel= l \mapsab{13,24}
%D    A BxC -> .plabel= m \midmap
%D    A  C  -> .plabel= r \mapsab{15,26}
%D    B BxC <- .plabel= b Ï\mathstrut
%D    BxC C -> .plabel= b Ï'
%D ))
%D enddiagram
%D
$$\pu
  \def\midmap{\sm{1â(3,5)\\2â(4,6)}}
  %
  \diag{product-ABC}
  \qquad
  \diag{product-explicit}
$$




\newpage

% «exponentials» (to ".exponentials")
% (lac162p 3 "exponentials")

{\bf Exponentials}

Bijection: $fâg$

$(â)$ (``currying''): $g := \cur f := »a:A.»b:B.f(a,b)$

$(â)$ (``uncurrying''): $f := \uncur g := »(a,b):AÃB.((g(a))(b))$

\bsk

%D diagram exponentials-ABC
%D 2Dx      100     +45
%D 2D  100 AxB <--| A
%D 2D       |       |
%D 2D       |  <->  |
%D 2D       v       v
%D 2D  +50  C |--> B->C
%D 2D
%D ren AxB A    ==>  AÃB  A
%D ren C B->C   ==>   C  B{â}C
%D (( AxB A  <-| .plabel= a »A.(AÃB)
%D    C B->C |-> .plabel= b »C.(B{â}C)
%D    AxB C   -> .plabel= l f
%D    A B->C  -> .plabel= r g
%D    A C  harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
%D diagram exponentials-explicit
%D 2Dx      100     +60
%D 2D  100 AxB <--| A
%D 2D       |       |
%D 2D       |  <->  |
%D 2D       v       v
%D 2D  +50  C |--> B->C
%D 2D
%D ren AxB A    ==> \csm{(1,3),(1,4)\\(2,3),(2,4)}  \{1,2\}
%D ren C B->C   ==> \{5,6\} \csm{\fu55,\fu56,\\\fu65,\fu66}
%D (( AxB A <-|
%D    C B->C |->
%D    AxB C   -> .plabel= l \sm{(1,3)â5\\(1,4)â6\\(2,3)â6\\(2,4)â5}
%D    A B->C  -> .plabel= r \sm{1â\fu56\\2â\fu65}
%D    A C  harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\pu
  \def\fu#1#2{\csm{(3,#1),\\(4,#2)}}
  \diag{exponentials-ABC}
  \diag{exponentials-explicit}
$$


\bsk
\bsk

Properties: $\cur \uncur f = f$, \; $\uncur \cur g = g$

where: $fÃf' := \ang{Ï;f,\,Ï';f'}$, \; $\uncur g := (gÃ\id);\ev$

solving type equations:

\bsk

%:*"* *
%:
%:
%:  Ï   f    Ï'  f'     Ï:AÃ?âA   f:AâB     Ï':?ÃA'âA'  f':A'âB' 
%:  -----    ------    ------ ------------    ---------------------
%:   Ï;f     Ï';f'      Ï;f:AÃ?âB                Ï';f':?ÃA'âB'     
%:  ----------------     ---------------------------------------- 
%:  \ang{Ï;f,\,Ï';f'}        \ang{Ï;f,\,Ï';f'}:AÃA'âBÃB'
%:  ------------------\ren    ----------------------------\ren
%:       fÃf'                      fÃf':AÃA'âBÃB'
%:
%:       ^fxf'_1                    ^fxf'_2
%:
%:
%:  g  \id           g:Aâ(B{â}C)  \id:?â?     
%:  ------           ----------------------     
%:  gÃ\id   \ev      gÃ\id:AÃ?â(B{â}C)Ã?    \ev:(B{â}C)ÃBâC
%:  -----------      -----------------------------------------
%:  (gÃ\id);\ev                (gÃ\id);\ev:AÃ?âC
%:  -----------\ren            ------------------
%:    \uncur"g                     \uncur"g:AÃ?âC
%:
%:    ^uncur_g_1                   ^uncur_g_2
%:
\pu
$$\ded{fxf'_1} \qquad \ded{fxf'_2}$$

$$\ded{uncur_g_1} \qquad \ded{uncur_g_2}$$




\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-anchor-format:     "«%s»"
% End: