|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: