% (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:

