Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% 3.tex: tests for dednat6.
% See: http://angg.twu.net/dednat6.html
%      http://angg.twu.net/dednat6/tests/3.tex.html
%      http://angg.twu.net/dednat6/tests/3.tex
%      http://angg.twu.net/dednat6/tests/3.pdf
%
% (defun c () (interactive) (find-sh "lualatex 3.tex"))
% (defun c () (interactive) (find-sh "lualatex --output-format=dvi 3.tex"))
% (defun d () (interactive) (find-xpdfpage "3.pdf"))
% (defun d () (interactive) (find-xdvipage "3.dvi"))
% (defun e () (interactive) (find-dn6 "tests/3.tex"))

\documentclass[oneside]{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
% \usepackage{amsfonts}
% \usepackage{amssymb}
% \usepackage{luacode}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")

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

\begin{document}

\catcode`\^^J=10
\directlua{dednat6dir = "../"}
\directlua{dofile(dednat6dir.."dednat6.lua")}
\directlua{require "abbrevs"}
\directlua{texfile(tex.jobname)}
% \directlua{quiet()}
\directlua{verbose()}
\directlua{output(preamble1)} % (find-dn6 "preamble6.lua" "preamble1")
\def\pu{\directlua{pu()}}
\pu

% From: \input ../../LATEX/istanbuldefs.tex  % (find-LATEX "istanbuldefs.tex")
\catcode`°=13 \def°{^\circ}
\catcode`Ξ»=13 \defΞ»{\lambda}
\catcode`×=13 \def×{\times}

\def\ang#1{\langle#1\rangle}

% A shorthand for matrices:
\def\mat #1{\begin       {matrix}#1\end{matrix}}
\def\pmat#1{\left (\begin{matrix}#1\end{matrix}\right)}
\def\bmat#1{\left [\begin{matrix}#1\end{matrix}\right]}
\def\cmat#1{\left\{\begin{matrix}#1\end{matrix}\right\}}
\def\sm #1{\begin       {smallmatrix}#1\end{smallmatrix}}
\def\psm#1{\left (\begin{smallmatrix}#1\end{smallmatrix}\right )}
\def\bsm#1{\left [\begin{smallmatrix}#1\end{smallmatrix}\right ]}
\def\csm#1{\left\{\begin{smallmatrix}#1\end{smallmatrix}\right\}}
% A trick for typesetting trees in \scriptsize:
\def\scri#1{\hbox{\scriptsize$#1$}}
\def\pded#1{\pmat{\ded{#1}}}
\def\pded#1{\pmat{\scri{\ded{#1}}}}




Some demos for dednat6: 3.tex
\par \url{http://angg.twu.net/dednat6/tests/3.tex}
\par \url{http://angg.twu.net/dednat6/tests/3.tex.html}
\par \url{http://angg.twu.net/dednat6/tests/3.pdf}

See:
\par \url{http://angg.twu.net/dednat6.html}



\medskip




%                     __    _                  __                _   
%  ___ _ __ ___       \ \  | |_ _____  __      \ \    ___  _   _| |_ 
% / __| '__/ __|  _____\ \ | __/ _ \ \/ /  _____\ \  / _ \| | | | __|
% \__ \ | | (__  |_____/ / | ||  __/>  <  |_____/ / | (_) | |_| | |_ 
% |___/_|  \___|      /_/   \__\___/_/\_\      /_/   \___/ \__,_|\__|
%                                                                    
\newsavebox{\myboxdedsrc}
\newsavebox{\myboxdedtex}
\newsavebox{\myboxdedout}
\newsavebox{\myboxdiagsrc}
\newsavebox{\myboxdiagtex}
\newsavebox{\myboxdiagout}

%D diagram T:F->G
%D 2Dx    100   +20  +20
%D 2D 100       A
%D 2D         / - \
%D 2D        /  |  \
%D 2D       v   v   v
%D 2D +25 FA ------> GA
%D 2D          TA
%D (( A FA -> A GA ->
%D    FA GA -> .plabel= b TA
%D    A FA GA midpoint |->
%D ))
%D enddiagram

%:                   P\&Q
%:                   ----
%:             P\&Q   Q  
%:             ----   :f 
%:  P\&Q        P     R  
%:    :(P\&)f   -------  
%:  P\&R          P\&R   
%:  
%:  ^t1           ^t2
%:  
\pu

\setbox0=\hbox{$\mat{\ded{t1} := \ded{t2}}$}
\savebox{\myboxdedout}{\copy0}

\setbox0=\hbox{$\diag{T:F->G}$}
\savebox{\myboxdiagout}{\copy0}

\setbox0=\hbox{%
\begin{minipage}[c]{5.2cm}
\par \verb!%D diagram T:F->G!
\par \verb!%D 2Dx    100   +20  +20!
\par \verb!%D 2D 100       A!
\par \verb!%D 2D         / - \!
\par \verb!%D 2D        /  |  \!
\par \verb!%D 2D       v   v   v!
\par \verb!%D 2D +25 FA ------> GA!
\par \verb!%D 2D          TA!
\par \verb!%D (( A FA -> A GA ->!
\par \verb!%D    FA GA -> .plabel= b TA!
\par \verb!%D    A FA GA midpoint |->!
\par \verb!%D ))!
\par \verb!%D enddiagram!
\par \verb!$$\pu \diag{T:F->G}$$!
\end{minipage}%
}
\savebox{\myboxdiagsrc}{\copy0}

\setbox0=\hbox{%
\begin{minipage}[c]{5.0cm}
\footnotesize
\par \verb!$$\defdiag{T:F->G}{!
\par \verb!   \morphism(300,0)/->/%!
\par \verb!    <-300,-375>[{A}`{FA};{}]!
\par \verb!   \morphism(300,0)/->/%!
\par \verb!    <300,-375>[{A}`{GA};{}]!
\par \verb!   \morphism(0,-375)|b|/->/%!
\par \verb!    <600,0>[{FA}`{GA};{TA}]!
\par \verb!   \morphism(300,0)/|->/%!
\par \verb!    <0,-375>[{A}`{\phantom{O}};{}]!
\par \verb!  }!
\par \verb!  \diag{T:F->G}!
\par \verb!$$!
\end{minipage}%
}
\savebox{\myboxdiagtex}{\copy0}


\setbox0=\hbox{%
\begin{minipage}[c]{5.2cm}
\par \verb!%:                   P\&Q!
\par \verb!%:                   ----!
\par \verb!%:             P\&Q   Q  !
\par \verb!%:             ----   :f !
\par \verb!%:  P\&Q        P     R  !
\par \verb!%:    :(P\&)f   -------  !
\par \verb!%:  P\&R          P\&R   !
\par \verb!%:  !
\par \verb!%:  ^t1           ^t2!
\par \verb!%:  !
\par \verb!$$\pu \ded{t1} := \ded{t2}$$!
\end{minipage}%
}
\savebox{\myboxdedsrc}{\copy0}

\setbox0=\hbox{%
\begin{minipage}[c]{5.7cm}
\footnotesize
\par \verb!$$!
\par \verb!\defded{t1}{!
\par \verb! \infer*[{(P\&)f}]{ \mathstrut P\&R }{!
\par \verb!  \mathstrut P\&Q } }!
\par \verb!\defded{t2}{!
\par \verb! \infer[{}]{ \mathstrut P\&R }{!
\par \verb!  \infer[{}]{ \mathstrut P }{!
\par \verb!   \mathstrut P\&Q } &!
\par \verb!  \infer*[{f}]{ \mathstrut R }{!
\par \verb!   \infer[{}]{ \mathstrut Q }{!
\par \verb!    \mathstrut P\&Q } } } }!
\par \verb!\ded{t1} := \ded{t2}!
\par \verb!$$!
\end{minipage}%
}
\savebox{\myboxdedtex}{\copy0}

%L forths["x+="] = function () ds:pick(0).x = ds:pick(0).x + getwordasluaexpr() end
%L forths["y+="] = function () ds:pick(0).y = ds:pick(0).y + getwordasluaexpr() end

%D diagram src-tex-out
%D 2Dx      100     +125    +20
%D 2D   100               diagout
%D 2D   +35 diagsrc
%D 2D   +40        diagtex
%D 2D
%D 2D   +80               dedout
%D 2D   +20 dedsrc
%D 2D   +60        dedtex
%D 2D
%D (( diagsrc .tex= \fbox{\usebox{\myboxdiagsrc}}
%D    diagtex .tex= \fbox{\usebox{\myboxdiagtex}}
%D    diagout .tex= \fbox{\usebox{\myboxdiagout}}
%D    dedsrc  .tex= \fbox{\usebox{\myboxdedsrc}}
%D    dedtex  .tex= \fbox{\usebox{\myboxdedtex}}   x+= -7
%D    dedout  .tex= \fbox{\usebox{\myboxdedout}}   x+= -17
%D    diagsrc diagtex ->  diagtex diagout ->
%D    dedsrc  dedtex  ->  dedtex  dedout  ->
%D ))
%D enddiagram
%D

$$\pu \diag{src-tex-out}$$






\newpage

%            _  _                  _   _
%   __ _  __| |(_)_   _ _ __   ___| |_(_) ___  _ __  ___
%  / _` |/ _` || | | | | '_ \ / __| __| |/ _ \| '_ \/ __|
% | (_| | (_| || | |_| | | | | (__| |_| | (_) | | | \__ \
%  \__,_|\__,_|/ |\__,_|_| |_|\___|\__|_|\___/|_| |_|___/
%            |__/
%
% Inspired by:
% (find-unilogcurr "" "adjs-to-cob-quants")
% (find-dvipage  "~/LATEX/2010unilog-current.dvi" 70 "adjs-to-cob-quants")
% http://angg.twu.net/math-b.html#internal-diags-in-ct
% http://angg.twu.net/LATEX/2010unilog-current.pdf (pp.71-73)

Our archetypal adjunctions: $L \dashv R$, $({\land}Q) \dashv (Q{\to})$, $({×}B) \dashv (B{\to})$.

%D diagram adjunction-0
%D 2Dx      100    +30
%D 2D  100 LA' <-| A'
%D 2D       |      |
%D 2D    Lf |  <-| | f
%D 2D       v      v
%D 2D  +30  LA <-| A
%D 2D       |      |
%D 2D    gb |  <-| | g
%D 2D     h |  |-> | h#
%D 2D       v      v
%D 2D  +30  B |-> RB
%D 2D       |      |
%D 2D     k |  |-> | Rk
%D 2D       v      v
%D 2D  +30 B' |-> RB'
%D 2D
%D (( LA' A' <-|
%D    LA  A  <-|
%D    B  RB  |->
%D    B' RB' |->
%D
%D    LA' LA -> .plabel= l Lf              A' A   -> .plabel= r f
%D    LA  B  -> .PLABEL= _(0.42) g^\flat   A  RB  -> .PLABEL= ^(0.42) g
%D    LA  B  -> .PLABEL= _(0.58) h         A  RB  -> .PLABEL= ^(0.58) h^\sharp
%D    B   B' -> .plabel= l k               RB RB' -> .plabel= r Rk
%D
%D    LA' A   harrownodes nil 20 nil <-|
%D    LA RB   harrownodes nil 20 nil <-| sl^
%D    LA RB   harrownodes nil 20 nil |-> sl_
%D     B RB'  harrownodes nil 20 nil |->
%D ))
%D enddiagram

%D diagram adjunction-and-imp
%D 2Dx      100    +30
%D 2D  100 LA' <-| A'
%D 2D       |      |
%D 2D    Lf |  <-| | f
%D 2D       v      v
%D 2D  +30  LA <-| A
%D 2D       |      |
%D 2D    gb |  <-| | g
%D 2D     h |  |-> | h#
%D 2D       v      v
%D 2D  +30  B |-> RB
%D 2D       |      |
%D 2D     k |  |-> | Rk
%D 2D       v      v
%D 2D  +30 B' |-> RB'
%D 2D
%D ren    LA' A'   ==>   ({\land}Q)P' P'
%D ren    LA  A    ==>   ({\land}Q)P  P
%D ren    B   RB   ==>   R  (Q{\to})R
%D ren    B'  RB'  ==>   R' (Q{\to})R'
%D
%D (( LA' A' <-|
%D    LA  A  <-|
%D    B  RB  |->
%D    B' RB' |->
%D
%D    LA' LA -> .plabel= l ({\land}Q)f     A' A   -> .plabel= r f
%D    LA  B  -> .PLABEL= _(0.42) g^\flat   A  RB  -> .PLABEL= ^(0.42) g
%D    LA  B  -> .PLABEL= _(0.58) h         A  RB  -> .PLABEL= ^(0.58) h^\sharp
%D    B   B' -> .plabel= l k               RB RB' -> .plabel= r (Q{\to})k
%D
%D    LA' A   harrownodes nil 20 nil <-|
%D    LA RB   harrownodes nil 20 nil <-| sl^
%D    LA RB   harrownodes nil 20 nil |-> sl_
%D     B RB'  harrownodes nil 20 nil |->
%D ))
%D enddiagram

%D diagram adjunction-prod-exp
%D 2Dx      100    +30
%D 2D  100 LA' <-| A'
%D 2D       |      |
%D 2D    Lf |  <-| | f
%D 2D       v      v
%D 2D  +30  LA <-| A
%D 2D       |      |
%D 2D    gb |  <-| | g
%D 2D     h |  |-> | h#
%D 2D       v      v
%D 2D  +30  B |-> RB
%D 2D       |      |
%D 2D     k |  |-> | Rk
%D 2D       v      v
%D 2D  +30 B' |-> RB'
%D 2D
%D ren    LA' A'   ==>   ({×}B)A' A'
%D ren    LA  A    ==>   ({×}B)A  A
%D ren    B   RB   ==>   C  (B{\to})C
%D ren    B'  RB'  ==>   C' (B{\to})C'
%D
%D (( LA' A' <-|
%D    LA  A  <-|
%D    B  RB  |->
%D    B' RB' |->
%D
%D    LA' LA -> .plabel= l ({×}B)\alpha     A' A   -> .plabel= r \alpha
%D    LA  B  -> .PLABEL= _(0.42) g^\flat    A  RB  -> .PLABEL= ^(0.42) g
%D    LA  B  -> .PLABEL= _(0.58) h          A  RB  -> .PLABEL= ^(0.58) h^\sharp
%D    B   B' -> .plabel= l \gamma           RB RB' -> .plabel= r (B{\to})\gamma
%D
%D    LA' A   harrownodes nil 20 nil <-|
%D    LA RB   harrownodes nil 20 nil <-| sl^
%D    LA RB   harrownodes nil 20 nil |-> sl_
%D     B RB'  harrownodes nil 20 nil |->
%D ))
%D enddiagram

$$\pu
  \diag{adjunction-0}
  \qquad
  \diag{adjunction-and-imp}
  \quad
  \diag{adjunction-prod-exp}
$$




%L abbrevs:add("&", "\\land ", "->", "\\to ")
%:
%:
%:                P'&Q <------| P'
%:    P'&Q          |           |
%:    -----         |           |
%:      P'  P'&Q    |           |   P'
%:      :f  ----    |           |   :f
%:      P    Q      |    <-|    |   P
%:      ------      |           |
%:        P&Q       |           |   ^f
%:                  |           |
%:        ^Lf       |           |
%:                  v           v
%:                 P&Q <------| P
%:                  |           |
%:          P&Q     |           |    P
%:          ---     |           |    :g
%:   P&Q     P      |    <-|    |   Q->R
%:   ---     :g     |           |
%:    Q     Q->R    |           |    ^g
%:    ----------    |           |
%:        R         |           |
%:                  |           |   P  [Q]^1
%:        ^gflat    |           |   --------
%:                  |           |    P&Q
%:                  |           |     :h
%:          P&Q     |           |     R
%:           :h     |           |    ----1
%:           R      |    |->    |    Q->R
%:                  |           |
%:           ^h     |           |    ^hsharp
%:                  |           |
%:                  v           v
%:                 R |-------> Q->R
%:                  |           |
%:                  |           |   [Q]^1  Q->R
%:                  |           |   -----------
%:            R     |           |      R
%:            :k    |           |      :k
%:            R'    |    |->    |      R'
%:                  |           |     ----
%:            ^k    |           |     Q->R'
%:                  |           |
%:                  |           |     ^Rk
%:                  v           v
%:                 R |-------> Q->R'
%:
\pu

%D diagram adjunction-and-imp-2
%D 2Dx      100    +40
%D 2D  100 LA' <-| A'
%D 2D       |      |
%D 2D    Lf |  <-| | f
%D 2D       v      v
%D 2D  +50  LA <-| A
%D 2D       |      |
%D 2D    gb |  <-| | g
%D 2D     h |  |-> | h#
%D 2D       v      v
%D 2D  +50  B |-> RB
%D 2D       |      |
%D 2D     k |  |-> | Rk
%D 2D       v      v
%D 2D  +50 B' |-> RB'
%D 2D
%D ren    LA' A'   ==>   P'{\land}Q P'
%D ren    LA  A    ==>    P{\land}Q P
%D ren    B   RB   ==>   R    Q{\to}R
%D ren    B'  RB'  ==>   R'   Q{\to}R'
%D
%D (( LA' A' <-|
%D    LA  A  <-|
%D    B  RB  |->
%D    B' RB' |->
%D
%D    LA' LA -> .plabel= l \Lf             A' A   -> .plabel= r \f
%D    LA  B  -> .PLABEL= _(0.42) \gb       A  RB  -> .PLABEL= ^(0.42) \g
%D    LA  B  -> .PLABEL= _(0.58) \h        A  RB  -> .PLABEL= ^(0.58) \hsharp
%D    B   B' -> .plabel= l \k              RB RB' -> .plabel= r \Rk
%D
%D    LA' A   harrownodes nil 20 nil <-|
%D    LA RB   harrownodes nil 20 nil <-| sl^
%D    LA RB   harrownodes nil 20 nil |-> sl_
%D     B RB'  harrownodes nil 20 nil |->
%D ))
%D enddiagram

$$\pu
  \def\Lf{\pded{Lf}    \;=:\; ({\land}Q)f}             \def\f{f}
  \def\gb{\pded{gflat} \;=:\; g^\flat}                 \def\g{g}
  \def\h{h}          \def\hsharp{h^\sharp  \;=:\; \pded{hsharp}}
  \def\k{k}          \def\Rk    {(Q{\to})k \;=:\; \pded{Rk}}
  %
  \diag{adjunction-and-imp-2}
$$



%D diagram adjunction-prod-exp-2
%D 2Dx      100    +30
%D 2D  100 LA' <-| A'
%D 2D       |      |
%D 2D    Lf |  <-| | f
%D 2D       v      v
%D 2D  +30  LA <-| A
%D 2D       |      |
%D 2D    gb |  <-| | g
%D 2D     h |  |-> | h#
%D 2D       v      v
%D 2D  +30  B |-> RB
%D 2D       |      |
%D 2D     k |  |-> | Rk
%D 2D       v      v
%D 2D  +30 B' |-> RB'
%D 2D
%D ren    LA' A'   ==>   A'{×}B A'
%D ren    LA  A    ==>    A{×}B A
%D ren    B   RB   ==>   C  B{\to}C
%D ren    B'  RB'  ==>   C' B{\to}C'
%D
%D (( LA' A' <-|
%D    LA  A  <-|
%D    B  RB  |->
%D    B' RB' |->
%D
%D    LA' LA -> .plabel= l \Lf             A' A   -> .plabel= r \f
%D    LA  B  -> .PLABEL= _(0.42) \gb       A  RB  -> .PLABEL= ^(0.42) \g
%D    LA  B  -> .PLABEL= _(0.58) \h        A  RB  -> .PLABEL= ^(0.58) \hsharp
%D    B   B' -> .plabel= l \k              RB RB' -> .plabel= r \Rk
%D
%D    LA' A   harrownodes nil 20 nil <-|
%D    LA RB   harrownodes nil 20 nil <-| sl^
%D    LA RB   harrownodes nil 20 nil |-> sl_
%D     B RB'  harrownodes nil 20 nil |->
%D ))
%D enddiagram

$$\pu
  \def\Lf{Ξ»p.(\alpha(πp),π'p)  \;=:\; ({×}B)\alpha}           \def\f{\alpha}
  \def\gb{Ξ»p.(g(πa))(π'p) \;=:\; g^\flat}                          \def\g{g}
  \def\h{h}                       \def\hsharp{h^\sharp  \;:=\; Ξ»a.Ξ»b.h(a,b)}
  \def\k{\gamma}           \def\Rk{(B{\to})\gamma \;:=\; Ξ»f.Ξ»b.\gamma(f(b))}
  %
  \diag{adjunction-prod-exp-2}
$$





\newpage

%  _  __                       _                 _                 
% | |/ /__ _ _ __     _____  _| |_ ___ _ __  ___(_) ___  _ __  ___ 
% | ' // _` | '_ \   / _ \ \/ / __/ _ \ '_ \/ __| |/ _ \| '_ \/ __|
% | . \ (_| | | | | |  __/>  <| ||  __/ | | \__ \ | (_) | | | \__ \
% |_|\_\__,_|_| |_|  \___/_/\_\\__\___|_| |_|___/_|\___/|_| |_|___/
%                                                                  

%L luarecteval [[
%L ra, rb = 2/        \, 2/  #1    \
%L           |#1  #2  |   |#2  #3  |
%L           |  #3  #4|   |  #4  #5|
%L           \        /   \    #6  /
%L ]]
%L ra:tomp({def="catAmicro", scale="2pt", meta="t p"}):addbullets():output()
%L rb:tomp({def="catBmicro", scale="2pt", meta="t p"}):addbullets():output()
%L ra:tomp({def="preshA#1#2#3#4",     scale="20pt", meta="p"}):addcells():addarrows():output()
%L rb:tomp({def="preshB#1#2#3#4#5#6", scale="20pt", meta="p"}):addcells():addarrows():output()

\def\Set{\mathbf{Set}}
\def\Lan{\mathsf{Lan}}
\def\Ran{\mathsf{Ran}}

Kan extensions: a general case and a particular case.


%D diagram Kan1
%D 2Dx     100     +40
%D 2D  100 C |---> LC
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +30 FD <--| D
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +30 E |---> RD
%D 2D
%D 2D  +20 SA <--- SB
%D 2D
%D 2D  +20 A ----> B
%D 2D
%D ren   C  LC ==> C      \Lan_{F}C
%D ren   FD D  ==> D∘F     D
%D ren   E  RD ==> E      \Ran_{F}C
%D ren   SA SB ==> \Set^A \Set^B
%D ren   A  B  ==> A       B
%D
%D (( C LC |->
%D    FD D <-|
%D    E RD |->
%D    SA SB -> sl^^ .plabel= a \Lan_{F}
%D    SA SB <-      .plabel= m ∘F
%D    SA SB -> sl__ .plabel= b \Ran_{F}
%D    A  B ->       .plabel= a F 
%D
%D    C FD ->  LC D ->
%D    FD E ->  D RD ->
%D
%D    C  D   harrownodes nil 20 nil |-> sl^
%D    C  D   harrownodes nil 20 nil <-| sl_
%D    FD RD  harrownodes nil 20 nil <-| sl^
%D    FD RD  harrownodes nil 20 nil |-> sl_
%D ))
%D enddiagram

\def\mypb#1#2#3#4{#1_#2{{×}_{#1_#3}}#1_#4}
\def\mypo#1#2#3#4{#1_#2{{+}_{#1_#3}}#1_#4}

%D diagram Kan2
%D 2Dx     100     +85
%D 2D  100 C |---> LC
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +75 FD <--| D
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +75 E |---> RD
%D 2D
%D 2D  +45 SA <--- SB
%D 2D
%D 2D  +45 A ----> B
%D 2D
%D ren   C  LC ==> \preshA{C_2}{C_3}{C_4}{C_5}   \preshB{0}{C_2}{C_3}{C_4}{C_5}{\mypo{C}435}
%D ren   FD D  ==> \preshA{D_2}{D_3}{D_4}{D_5}   \preshB{D_1}{D_2}{D_3}{D_4}{D_5}{D_6}
%D ren   E  RD ==> \preshA{E_2}{E_3}{E_4}{E_5}   \preshB{\mypb{E}243}{E_2}{E_3}{E_4}{E_5}{1}
%D ren   SA SB ==> \Set^{\catAmicro} \Set^{\catBmicro}
%D ren   A  B  ==> \preshA{2}{3}{4}{5}           \preshB{1}{2}{3}{4}{5}{6}
%D
%D (( C LC |->
%D    FD D <-|
%D    E RD |->
%D    SA SB -> sl^^ .plabel= a \Lan_{F}
%D    SA SB <-      .plabel= m ∘F
%D    SA SB -> sl__ .plabel= b \Ran_{F}
%D    A  B ->       .plabel= a F 
%D
%D    C FD ->  LC D ->
%D    FD E ->  D RD ->
%D
%D    C  D   harrownodes nil 20 nil |-> sl^
%D    C  D   harrownodes nil 20 nil <-| sl_
%D    FD RD  harrownodes nil 20 nil <-| sl^
%D    FD RD  harrownodes nil 20 nil |-> sl_
%D ))
%D enddiagram
%D
\pu
$$\diag{Kan1}
  \qquad
  \qquad
  \qquad
  \diag{Kan2}
$$


% \newpage









\end{document}


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