% Dednat6's "preamble1":
%
\def\diagxyto{\ifnextchar/{\toop}{\toop/>/}}
\def\to     {\rightarrow}
%
\def\defded#1#2{\expandafter\def\csname ded-#1\endcsname{#2}}
\def\ifdedundefined#1{\expandafter\ifx\csname ded-#1\endcsname\relax}
\def\ded#1{\ifdedundefined{#1}
    \errmessage{UNDEFINED DEDUCTION: #1}
  \else
    \csname ded-#1\endcsname
  \fi
}
\def\defdiag#1#2{\expandafter\def\csname diag-#1\endcsname{\bfig#2\efig}}
\def\defdiagprep#1#2#3{\expandafter\def\csname diag-#1\endcsname{{#2\bfig#3\efig}}}
\def\ifdiagundefined#1{\expandafter\ifx\csname diag-#1\endcsname\relax}
\def\diag#1{\ifdiagundefined{#1}
    \errmessage{UNDEFINED DIAGRAM: #1}
  \else
    \csname diag-#1\endcsname
  \fi
}
%
\newlength{\celllower}
\newlength{\lcelllower}
\def\cellfont{}
\def\lcellfont{}
\def\cell #1{\lower\celllower\hbox to 0pt{\hss\cellfont${#1}$\hss}}
\def\lcell#1{\lower\celllower\hbox to 0pt   {\lcellfont${#1}$\hss}}
%
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
\def\pu{\directlua{pu()}}
%
% End of preamble1.


\defded{comp}{   % In the "%:"-block in lines 60--69
 \infer[{1}]{ \mathstrut a\to c }{
  \infer[{}]{ \mathstrut c }{
   \infer[{}]{ \mathstrut b }{
    \mathstrut [a]^1 &
    \mathstrut a\to b } &
   \mathstrut b\to c } } }
\defdiag{adj}{   % In the "%D"-block in lines 79--97
  \morphism(0,0)/<-|/<375,0>[{LA}`{A};]
  \morphism(0,0)/->/<0,-375>[{LA}`{B};]
  \morphism(375,0)/->/<0,-375>[{A}`{RB};]
  \morphism(0,-375)/|->/<375,0>[{B}`{RB};]
  \morphism(37,-187)/<->/<300,0>[{\phantom{O}}`{\phantom{O}};]
  \morphism(0,-600)|a|/{@{<-}@<2.5pt>}/<375,0>[{\catB}`{\catA};{L}]
  \morphism(0,-600)|b|/{@{->}@<-2.5pt>}/<375,0>[{\catB}`{\catA};{R}]
}