% (find-LATEX "2020institutions.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020institutions.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2020institutions.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020institutions.pdf"))
% (defun e () (interactive) (find-LATEX "2020institutions.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020institutions"))
% (find-pdf-page   "~/LATEX/2020institutions.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020institutions.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020institutions.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020institutions.pdf
%               file:///tmp/2020institutions.pdf
%           file:///tmp/pen/2020institutions.pdf
% http://angg.twu.net/LATEX/2020institutions.pdf
% (find-LATEX "2019.mk")

% «.title-page»				(to "title-page")
% «.comma-category»			(to "comma-category")
% «.indexed-cats-and-fibrations»	(to "indexed-cats-and-fibrations")
% «.typing-insts»			(to "typing-insts")
% «.drawing-insts-1»			(to "drawing-insts-1")
% «.drawing-insts-2»			(to "drawing-insts-2")
% «.drawing-insts-3»			(to "drawing-insts-3")
% «.drawing-insts-4»			(to "drawing-insts-4")

\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb}                 % (find-es "tex" "colorweb")
%\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-es "tex" "geometry")
% (find-latexgeomtext "total={6.5in,8.75in},")
%\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}
%
\usepackage[backend=biber,
   style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-u.bib}  % (find-LATEX "catsem-u.bib")
%
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")





%  ____        __     
% |  _ \  ___ / _|___ 
% | | | |/ _ \ |_/ __|
% | |_| |  __/  _\__ \
% |____/ \___|_| |___/
%                     
% «defs»  (to ".defs")

\def\dnito{\lhookdownarrow}
\def\Ords{\mathsf{Ords}}

\def\psmi  #1#2{  \psm {#1 \\ \dnito \\ #2}}
\def\pmati #1#2{  \pmat{#1 \\ \dnito \\ #2}}
\def\pmatin#1#2#3{\pmat{#1 \\ \dnito & #3 \\ #2}}
\def \matin#1#2#3{ \mat{#1 \\ \dnito & #3 \\ #2}}

\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\calU{\mathcal{U}}

\def\C{\mathbb{C}}

\def\Cat{\mathbf{Cat}}
\def\Sig{\mathsf{Sig}}
\def\Sen{\mathsf{Sen}}
\def\Mod{\mathsf{Mod}}
\def\mfr{\mathfrak}




\setlength{\parindent}{0pt}


%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% «title-page»  (to ".title-page")

% (find-books "__cats/__cats.el" "diaconescu")



{\setlength{\parindent}{0em}
\footnotesize

Notes on Razvan Diaconescu's

``Institution-independent Model Theory'' (Birkhäuser, 2008)

\url{http://www.springer.com/birkhauser/mathematics/book/978-3-7643-8707-5}
\ssk

These notes are at:

\url{http://angg.twu.net/LATEX/2020institutions.pdf}

}

\bsk
\bsk



% «comma-category»  (to ".comma-category")
% (find-diaconescupage (+ 11 11) "comma category")
% (find-diaconescutext (+ 11 11) "comma category")

\subsection*{Comma categories}

(Page 11):

%D diagram ??
%D 2Dx     100 +25 +20
%D 2D  100         B1
%D 2D
%D 2D  +20 A0  B2  B3
%D 2D
%D 2D  +20 A1  B4  B5
%D 2D
%D 2D  +15 A2  C0  C1
%D 2D
%D ren A0 A1 A2 ==> (f,B) (f',B') A/\calU
%D ren    B1 ==> A
%D ren B2 B3 ==> B  \calU(B)
%D ren B4 B5 ==> B' \calU(B')
%D ren C0 C1 ==> \C' \C
%D
%D (( A0 A1  -> .plabel= l h
%D    A2 place
%D    B1 B3  -> .plabel= r f
%D    B2 B3 |->
%D    B2 B4  -> .plabel= l h
%D    B3 B5  -> .plabel= r \calU(h)
%D    B4 B5 |->
%D    B1 B5  -> .slide= 25pt .plabel= r f'
%D    C0 C1  -> .plabel= a \calU
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

The construction of the functor $C \mapsto C/R$, that we will use in
page 45:
%
%D diagram ??
%D 2Dx     100  +20 +35  +25 +20
%D 2D  100                   E1
%D 2D                         |
%D 2D  +20                   E3
%D 2D                         |
%D 2D  +20     B0 - B1  E4 - E5
%D 2D          |     |  |     |
%D 2D  +20     B2 - B3  E6 - E7
%D 2D
%D 2D  +15 A0  C0 - C1  F0 - F1
%D 2D      |
%D 2D  +15 A1  D0 - D1
%D 2D
%D ren             E1 ==>                        C'
%D ren             E3 ==>                        C
%D ren    B0 B1 E4 E5 ==>   (γ;f,D)  (f,D)    D  RD
%D ren    B2 B3 E6 E7 ==>  (γ;f',D') (f',D')  D' RD'
%D ren A0 C0 C1 F0 F1 ==> \Cat  C'/R C/R  \catB \catA
%D ren A1 D0 D1       ==> \catA^\op C' C
%D
%D (( A0 A1  <- .plabel= l (-/R)
%D    B0 B1 <-|
%D    B0 B2  -> .plabel= l δ
%D    B1 B3  -> .plabel= r δ
%D    B2 B3 <-|
%D    B0 B3 harrownodes nil 20 nil <-|
%D    C0 C1 <-|
%D    D0 D1  -> .plabel= a γ
%D    E1 E3  -> .plabel= r γ
%D    E3 E5  -> .plabel= r f
%D    E4 E5 |->
%D    E4 E6  -> .plabel= l δ
%D    E5 E7  -> .plabel= r Rδ
%D    E6 E7 |->
%D    E3 E7  -> .slide= 20pt .plabel= r f'
%D    E4 E7 harrownodes nil 20 nil |->
%D    F0 F1  -> .plabel= a R
%D
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\newpage



% «indexed-cats-and-fibrations»  (to ".indexed-cats-and-fibrations")
% (find-diaconescupage (+ 11 20) "2.5 Indexed Categories and Fibrations")
% (find-diaconescutext (+ 11 20) "2.5 Indexed Categories and Fibrations")

\section*{2.5. Indexed Categories and Fibrations}

(Page 20):

The Grothendieck category $B^♯$ of $B: I^\op → \Cat$:

%D diagram ??
%D 2Dx     100 +20 +30 +25 +15 +20
%D 2D  100     B0          F0
%D 2D
%D 2D  +20     B2  B3  E0      F1
%D 2D
%D 2D  +15 A0  C0  C1
%D 2D
%D 2D  +15 A1  D0  D1  E1  G0  G1
%D 2D
%D ren     B0         F0    ==>            Σ            〈i,Σ〉
%D ren     B2 B3  E0     F1 ==>       B(u)(Σ') Σ'  B^♯     〈i',Σ'〉
%D ren A0  C0 C1            ==> \Cat  B(i)  B(i')
%D ren A1  D0 D1  E1  G0 G1 ==> I^\op   i     i'   I     i  i'
%D
%D (( A0 A1  <- .plabel= l B
%D    B0 B2  -> .plabel= r φ
%D    B2 B3 <-|
%D    C0 C1 <-  .plabel= a B(u)
%D    D0 D1 ->  .plabel= a   u
%D    E0 E1 -> .plabel= r p
%D    F0 F1 -> .plabel= r 〈u,φ〉
%D    G0 G1 -> .plabel= a u
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


\newpage

% (find-diaconescupage (+ 10 45) "3.4 Institutions as Functors")
% (find-diaconescutext (+ 10 45) "3.4 Institutions as Functors")

\section*{3.4. Institutions as functors}

(Page 45):

\def\SS#1{\Set(#1,2)}
\def\SB#1{[#1{→}2]}


A room is a triple $(S,M,R)$ where:
%
$\pmat{S \text{ is a set,} \\ 
       M \text{ is a category,} \\
       R: |M| → \SS{S}}
$.

\ssk

A room morphism $(s,m):(S',M',R')→(S,M,R)$ is:
%
%D diagram room-morphism-1
%D 2Dx     100 +45
%D 2D  100 A0  A1
%D 2D
%D 2D  +10 B0  B1
%D 2D
%D 2D  +20 B2  B3
%D 2D
%D 2D  +10 C0  C1
%D 2D
%D 2D  +20 D0  D1
%D 2D
%D ren A0 A1 ==>  M'   M
%D ren B0 B1 ==> |M'| |M|
%D ren B2 B3 ==> \SB{S'} \SB{S}
%D ren C0 C1 ==> S'   S
%D ren D0 D1 ==> (S',M',R') (S,M,R)
%D
%D (( A0 A1 -> .plabel= a m
%D    B0 B1 -> .plabel= a |m|
%D    B0 B2 -> .plabel= l R'
%D    B1 B3 -> .plabel= r R
%D    B2 B3 -> .plabel= a (s;-)
%D    C0 C1 <- .plabel= a s
%D    D0 D1 -> .plabel= a (s,m)
%D ))
%D enddiagram
%D
%D diagram room-morphism-2
%D 2Dx     100 +25 +20 +25
%D 2D  100         A1
%D 2D              |  \
%D 2D  +25         |   A3
%D 2D              v    |
%D 2D  +15 A4 |--> A5   |
%D 2D        \       \  v
%D 2D  +25     A6 |--> A7
%D 2D
%D 2D  +20 B0 ---> B1
%D 2D
%D ren A1 A3 ==> |M'| |M|
%D ren A4 A6 ==>  S'   S
%D ren A5 A7 ==> \SB{S'} \SB{S}
%D ren B0 B1 ==> \Set^\op \Set
%D
%D (( A1 A3 -> .plabel= a |m|
%D    A4 A6 <- .plabel= l s
%D    A5 A7 -> .plabel= m (s;-)
%D
%D    A1 A5 -> .plabel= r R'
%D    A3 A7 -> .plabel= r R
%D
%D    A4 A5 |->
%D    A6 A7 |->
%D
%D    A4 A7 harrownodes nil 20 nil |->
%D    B0 xy+= 10 0
%D    B1 xy+= 10 0
%D    B0 B1 -> .plabel= a \SS-
%D ))
%D enddiagram
%D
$$\pu
  \diag{room-morphism-1}
  \qquad
  \diag{room-morphism-2}
$$

% (find-diaconescupage (+ 10 45) "3.4 Institutions as Functors")
% (find-diaconescutext (+ 10 45) "3.4 Institutions as Functors")



A room morphism is a morphism in the Grothendieck category blah:

%D diagram ??
%D 2Dx     100 +35 +55 +45 +30 +30
%D 2D  100     B0          F0
%D 2D
%D 2D  +20     B2  B3  E0      F1
%D 2D
%D 2D  +15 A0  C0  C1
%D 2D
%D 2D  +20 A1  D0  D1  E1  G0  G1
%D 2D
%D ren     B0         F0    ==>          (R',S')                       (M',(R',S'))
%D ren     B2 B3  E0     F1 ==>         (|m|;R,S) (R,S)       ((-)/\SS-)^♯   (M,(R,S))
%D ren A0  C0 C1            ==> \Cat^\op |M'|/\SS-  |M|/\SS-
%D ren A1  D0 D1  E1  G0 G1 ==> \Cat      M'         M        \Cat      M' M
%D
%D (( A0 A1  <- .plabel= m (-)/\SS-
%D    B0 B2  -> .plabel= l s
%D    B2 B3 <-|
%D    C0 C1 <-  # .plabel= a B(u)
%D    D0 D1 -> .plabel= a m
%D    E0 E1 -> .plabel= r p
%D    F0 F1 -> .plabel= r (m,s)
%D    G0 G1 -> .plabel= a m
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$











%D diagram ??
%D 2Dx     100  +35 +55  +40 +35
%D 2D  100                   E1
%D 2D                         |
%D 2D  +20                   E3
%D 2D                         |
%D 2D  +20     B0 - B1  E4 - E5
%D 2D          |     |  |     |
%D 2D  +20     B2 - B3  E6 - E7
%D 2D
%D 2D  +20 A0  C0 - C1  F0 - F1
%D 2D      |
%D 2D  +15 |   D0 - D1
%D 2D      |
%D 2D  +15 A1  D2 - D3
%D 2D
%D ren          E1 ==> |M'|
%D ren          E3 ==> |M|
%D ren B0 B1 E4 E5 ==> (|m|;R,\,S)   (R,S)    S  \Set(S,2)
%D ren B2 B3 E6 E7 ==> (|m|;R',\,S') (R',S')  S' \Set(S',2)
%D ren C0 C1 F0 F1 ==> |M'|/\Set(-,2) |M|/\Set(-,2) \Set^\op \Set
%D ren D0 D1       ==> |M'| |M|
%D ren D2 D3       ==>  M'   M
%D ren A0 A1       ==> \Cat \Cat^\op
%D
%D (( A0 A1  <- .plabel= m (|-|)/\Set(-,2)
%D    B0 B1 <-|
%D    B0 B2  <- .plabel= l s
%D    B1 B3  <- .plabel= r s
%D    B2 B3 <-|
%D    C0 C1 <-|
%D    D0 D1  -> .plabel= a |m|
%D    D2 D3  -> .plabel= a  m
%D    E1 E3  -> .plabel= r |m|
%D    E3 E5  -> .plabel= r R
%D    E4 E5 |->
%D    E4 E6  <- .plabel= l s
%D    E5 E7  -> .plabel= r (s;-)
%D    E6 E7 |->
%D    E3 E7  -> .slide= 30pt .plabel= r R'
%D    F0 F1  -> .plabel= a \Set(-,2)
%D
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$



\newpage

%  _____            _             
% |_   _|   _ _ __ (_)_ __   __ _ 
%   | || | | | '_ \| | '_ \ / _` |
%   | || |_| | |_) | | | | | (_| |
%   |_| \__, | .__/|_|_| |_|\__, |
%       |___/|_|            |___/ 
%
% «typing-insts»  (to ".typing-insts")

{\bf Typing institutions}

$$\begin{array}{rclcrcl}
  \Sig & 𝐭{is} & 𝐭{a category} \\
  \Sen & :     & \Sig → \Set \\
  \Mod & :     & \Sig → \Cat^\op \\
     ⊨ & :     & ? \\
     ⊨ & :     & (Σ:|\Sig|) → \Pts(|\Mod(Σ)|×\Sen(Σ)) \\
  \end{array}
$$
  
$$\begin{array}{rclcrcl}
  Σ   &∈& |\Sig| \\
  ⊨_Σ &⊆& |\Mod(Σ)|×\Sen(Σ) \\
  ⊨_Σ &∈& \Pts(|\Mod(Σ)|×\Sen(Σ)) \\
    ⊨ &∈& (Σ:|\Sig|) → \Pts(|\Mod(Σ)|×\Sen(Σ)) \\
    ⊨ &∈& ΠΣ⠆|\Sig|.\Pts(|\Mod(Σ)|×\Sen(Σ)) \\
  \end{array}
$$


\newpage

%  ____                     _               _ 
% |  _ \ _ __ __ ___      _(_)_ __   __ _  / |
% | | | | '__/ _` \ \ /\ / / | '_ \ / _` | | |
% | |_| | | | (_| |\ V  V /| | | | | (_| | | |
% |____/|_|  \__,_| \_/\_/ |_|_| |_|\__, | |_|
%                                   |___/     
%
% «drawing-insts-1»  (to ".drawing-insts-1")

{\bf Drawing institutions (1)}

%D diagram inst-def-internal-1
%D 2Dx     100  +30
%D 2D  100 A0   A1
%D 2D
%D 2D  +30 A2   A3
%D 2D
%D ren A0 A1 ==> \Mod(Σ) ⊨_Σ
%D ren A2 A3 ==>      Σ  \Sen(Σ)
%D
%D (( A2 A0 |->
%D    A2 A1 |->
%D    A2 A3 |->
%D ))
%D enddiagram
%D
%D diagram inst-def-external-1
%D 2Dx     100  +30
%D 2D  100 A0   A1 
%D 2D
%D 2D  +30 A2   A3 
%D 2D
%D ren A0 A1 ==> \Cat^\op ?
%D ren A2 A3 ==> \Sig \Set
%D
%D (( A2 A0 -> .plabel= l \Mod
%D    A2 A1 -> .plabel= r ⊨
%D    A2 A3 -> .plabel= b \Sen
%D ))
%D enddiagram
%D
%D diagram inst-def-external-2
%D 2Dx     100  +50
%D 2D  100 A0   A1 
%D 2D
%D 2D  +30 A2   A3 
%D 2D
%D ren A0 A1 ==> \Cat^\op \Pts(|\Mod(Σ)×\Sen(Σ)|)
%D ren A2 A3 ==> (Σ:\Sig) \Set
%D
%D (( A2 A0 -> .plabel= l \Mod
%D    A2 A1 -> .plabel= r ⊨
%D    A2 A3 -> .plabel= b \Sen
%D ))
%D enddiagram
%D
$$\pu
  \begin{array}{ccc}
    \diag{inst-def-external-1} \phantom{mmmmmmmm}
    &
    \hspace{-30pt}
    \diag{inst-def-internal-1}
    \\ \\
    \diag{inst-def-external-2}
  \end{array}
$$



\newpage

%  ____                     _               ____  
% |  _ \ _ __ __ ___      _(_)_ __   __ _  |___ \ 
% | | | | '__/ _` \ \ /\ / / | '_ \ / _` |   __) |
% | |_| | | | (_| |\ V  V /| | | | | (_| |  / __/ 
% |____/|_|  \__,_| \_/\_/ |_|_| |_|\__, | |_____|
%                                   |___/         
%
% «drawing-insts-2»  (to ".drawing-insts-2")

{\bf Drawing institutions (2)}

% (find-books "__cats/__cats.el" "gaina-kowalski")
% (find-fraissehintpage 3)

Gaina-Kowalski, p.3:

%D diagram ??
%D 2Dx      100       +20    +30        +45
%D 2D  100                  ModU <----| U
%D 2D                         |         |
%D 2D                         |   <--|  |
%D 2D                         v         v
%D 2D  +30                  ModV <----| V
%D 2D
%D 2D  +20  \Cat^\op  \Cat  ModSi <-- ModSi'
%D 2D        ^
%D 2D      Mod|
%D 2D         |                 \phi
%D 2D  +20  \Sig             Si ------> Si'
%D 2D
%D ren U ModU ==> \mfr{U'} \Mod(\mfr{U'})
%D ren V ModV ==> \mfr{V'} \Mod(\mfr{V'})
%D ren ModSi ModSi' ==> \Mod(Σ) \Mod(Σ')
%D ren    Si    Si' ==>      Σ       Σ'
%D
%D (( ModU U ModV V
%D    @ 0 @ 1 <-|
%D    @ 0 @ 2 ->
%D    @ 1 @ 3 ->
%D    @ 2 @ 3 <-|
%D    @ 0 @ 3 harrownodes nil 20 nil <-|
%D ))
%D ((  \Sig \Cat^\op -> .plabel= l \Mod
%D          \Cat         place
%D    ModSi   ModSi' <- .plabel= a \Mod(φ)
%D       Si      Si' -> .plabel= a      φ
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\newpage

%  ____                     _               _____ 
% |  _ \ _ __ __ ___      _(_)_ __   __ _  |___ / 
% | | | | '__/ _` \ \ /\ / / | '_ \ / _` |   |_ \ 
% | |_| | | | (_| |\ V  V /| | | | | (_| |  ___) |
% |____/|_|  \__,_| \_/\_/ |_|_| |_|\__, | |____/ 
%                                   |___/         
%
% «drawing-insts-3»  (to ".drawing-insts-3")

{\bf Drawing institutions (3)}

%D diagram ??
%D 2Dx      100       +30       +45
%D 2D  100            e |-----> e'
%D 2D
%D 2D  +25  \Set   SenSi --> SenSi'
%D 2D         ^
%D 2D     \Sen|
%D 2D         |         \phi
%D 2D  +20  \Sig     Si ------> Si'
%D 2D
%D ren e'           ==> \Sen(φ)(e)
%D ren SenSi SenSi' ==> \Sen(Σ) \Sen(Σ')
%D ren    Si    Si' ==>      Σ       Σ'
%D
%D (( e e' |->
%D    \Sig \Set -> .plabel= l \Sen
%D    SenSi SenSi' -> .plabel= a \Sen(φ)
%D    Si Si' -> .plabel= a \phi
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


\newpage

%  ____                     _               _  _   
% |  _ \ _ __ __ ___      _(_)_ __   __ _  | || |  
% | | | | '__/ _` \ \ /\ / / | '_ \ / _` | | || |_ 
% | |_| | | | (_| |\ V  V /| | | | | (_| | |__   _|
% |____/|_|  \__,_| \_/\_/ |_|_| |_|\__, |    |_|  
%                                   |___/          
%
% «drawing-insts-4»  (to ".drawing-insts-4")


{\bf Drawing institutions (4)}


%D diagram ??
%D 2Dx      100       +20     +25        +45     +40       +40
%D 2D  100  \Cat^\op  \Cat   ModSi <-- ModSi'    U <-----| U'
%D 2D
%D 2D  +25  \Set             SenSi --> SenSi'    e |-----> e'
%D 2D         ^
%D 2D         |
%D 2D         |                   \phi
%D 2D  +25  \Sig              Si ------> Si'
%D 2D
%D ren ModSi ModSi' ==> \Mod(Σ) \Mod(Σ')
%D ren SenSi SenSi' ==> \Sen(Σ) \Sen(Σ')
%D ren    Si    Si' ==>      Σ       Σ'
%D ren           e' ==>         \Sen(φ)(e)
%D ren     U     U' ==> \Mod(φ)(\mfr{U}')  \mfr{U}'
%D
%D (( \Sig \Set     -> .plabel= r \Sen
%D    \Sig \Cat^\op -> .slide= 10pt .plabel= l \Mod
%D         \Cat  place
%D    ModSi ModSi' <- .plabel= a \Mod(φ)
%D    SenSi SenSi' -> .plabel= a \Sen(φ)
%D    Si Si' -> .plabel= a \phi
%D ))
%D (( U U'  e e'
%D    @ 0 @ 1 <-|
%D    @ 0 @ 2  -> .plabel= l ⊨_Σ
%D    @ 1 @ 3  -> .plabel= r ⊨_{Σ'}
%D    @ 2 @ 3 |->
%D    @ 0 @ 3 harrownodes nil 20 nil <-> sl_ .plabel= a \text{adj}
%D    
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{0.8}{$
  \diag{??}
  $}
$$






\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-tla: "inst"
% End:
