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

% «.ls-deriv»			(to "ls-deriv")
% «.pavlovic-quantifiers»	(to "pavlovic-quantifiers")
% «.seely-plc»			(to "seely-plc")
% «.seely-plc-trees»		(to "seely-plc-trees")
% «.seely-plc-trees-dnc»	(to "seely-plc-trees-dnc")
% «.local-set-theories»		(to "local-set-theories")
% «.local-set-theories-2»	(to "local-set-theories-2")
% «.notes-seelyhyp»		(to "notes-seelyhyp")
% «.luo»			(to "luo")

\documentclass[oneside]{book}
\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")
\begin{document}

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

% %L dofile "edrxtikz.lua"  -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua"  -- (find-LATEX "edrxpict.lua")
% \pu

% (find-dednat6 "dednat6/block.lua" "TexLines")
\directlua{tf:processuntil(texlines:nlines())}

%:|-⊢
%:|->↦



Index of the slides:
\msk
% To update the list of slides uncomment this line:
\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\tocline {Quantifiers in Pavlovic's thesis} {2}
\tocline {A derivation from Lambek/Scott} {3}
\tocline {Seely's PLC paper} {4}
\tocline {Seely's PLC paper: trees} {5}
\tocline {Seely's PLC paper: trees, in DNC} {6}
\tocline {Local set theories} {7}
\tocline {Local set theories (1)} {8}
\tocline {Notes on reading SeelyHyp} {9}



\setlength{\parindent}{0em}

\newpage
% --------------------
% «pavlovic-quantifiers»  (to ".pavlovic-quantifiers")
% (s "Quantifiers in Pavlovic's thesis" "pavlovic-quantifiers")
\myslide {Quantifiers in Pavlovic's thesis} {pavlovic-quantifiers}

\def𝐬#1{{\color{red}#1}}

The rules $𝐫IΠ, 𝐫EΠ, 𝐫IΣ, 𝐫EΣ$, as they appear in Pavlovi\v c:

%:
%:        [X:P:\DD']
%:       ============
%:       𝐬{q}:Q:\DD''
%:   --------------------𝐫IΠ\DD'\DD''
%:   𝐬{λX.q}:ΠX⠆P.Q:\DD''
%:
%:   ^pav-IProd
%:
%:
%:   𝐬p:P:\DD'   𝐬r:ΠX⠆P.Q(𝐬X):\DD''
%:   -------------------------------𝐫EΠ\DD'\DD''
%:       𝐬{rp}:Q𝐬{[X:=p]}:\DD''
%:
%:       ^pav-EProd
%:
%:                 [X:P:\DD']
%:                 ==========
%:   𝐬{p:P:\DD'}     Q:\DD'     𝐬{q:Q(p):\DD''}
%:   ------------------------------------------𝐫IΣ\DD'\DD''
%:     𝐬{\ang{p,q}}:ΣX⠆P.Q:\DD'
%:
%:     ^pav-ISum
%:
%:                           [X:P:\DD']
%:                         ===============
%:                         [𝐬Y:Q(X):\DD'']
%:                     ==========================
%:   𝐬r:ΣX⠆P.Q:\DD''   𝐬{s(X,Y)}:S(\ang{X,Y}):\DD
%:   --------------------------------------------𝐫EΣ\DD'\DD''
%:        𝐬{ν(r,(X,Y).s)}:S(𝐬r):\DD
%:
%:        ^pav-ESum
%:
$$\ded{pav-IProd}$$

$$\ded{pav-EProd}$$

$$\ded{pav-ISum}$$

$$\ded{pav-ESum}$$

\msk

The same rules, but with a DNC-ish choice of letters:

%:    [b:B:Θ']
%:    ========
%:    𝐬c:C:Θ''
%:  -----------------𝐫IΠΘ'Θ''
%:  𝐬{λb.c}:Πb⠆B.C:Θ''
%:
%:  ^pav-IProd-abc
%:
%:  b':B:Θ'  f:Πb⠆B.C(b):Θ''
%:  -------------------------𝐫EΠΘ'Θ''
%:    fb:C[b:=b']:Θ''
%:
%:    ^pav-EProd-abc
%:
%:          [b:B:Θ']
%:          ========
%:  b':B:Θ'   C:Θ'     c:C(b'):Θ''
%:  ------------------------------𝐫IΣΘ'Θ''
%:     \ang{b',c}:Σb⠆B.C:Θ'
%:
%:     ^pav-ISum-abc
%:
%:                           [b:B:Θ']
%:                         ===============
%:                         [𝐬c:C(b):Θ'']
%:                     ==========================
%:   𝐬p:Σb⠆B.C:Θ''   𝐬{d(b,c)}:D(\ang{b,c}):Θ'''
%:   --------------------------------------------𝐫EΣΘ'Θ''
%:        𝐬{ν(p,(b,c).d)}:D(𝐬p):Θ'''
%:
%:        ^pav-ESum-abc
%:
$$\ded{pav-IProd-abc}$$

$$\ded{pav-EProd-abc}$$

$$\ded{pav-ISum-abc}$$

$$\ded{pav-ESum-abc}$$


\newpage
% --------------------
% «ls-deriv»  (to ".ls-deriv")
% (s "A derivation from Lambek/Scott" "ls-deriv")
\myslide {A derivation from Lambek/Scott} {ls-deriv}


Lambek/Scott, p.131:

%:  ∀_{x∈A}\phi(x)|-∀_{x∈A}\phi(x)        ∃_{x∈A}\phi(x)|-∃_{x∈A}\phi(x)
%:  ------------------------------(2.4)   ------------------------------(2.4')
%:    ∀_{x∈A}\phi(x)|-_x\phi(x)           \phi(x)|-_x∃_{x∈A}\phi(x)
%:    -------------------------------------------------------------(1.2)
%:              ∀_{x∈A}\phi(x)|-_x∃_{x∈A}\phi(x)
%:              --------------------------------(1.4)
%:               ∀_{x∈A}\phi(x)|-∃_{x∈A}\phi(x)
%:  
%:               ^LS-p131
%:
$$\ded{LS-p131}$$

%:         a;∀b.P|-∀b.P        a;∃b.P|-∃b.P
%:         ------------(∀𝐫E)   ------------(∃𝐫I)
%:         a,b;∀b.P|-P         a,b;P|-∃b.P
%:         -----------------------------
%:  a|-b       a,b;∀b.P|-∃b.P
%:  -------------------------(𝐫s)
%:       a;∀b.P|-∃b.P
%:  
%:       ^LS-p131-dnc
%:
$$\ded{LS-p131-dnc}$$

\newpage
% --------------------
% «seely-plc»  (to ".seely-plc")
% (s "Seely's PLC paper" "seely-plc")
\myslide {Seely's PLC paper} {seely-plc}

(1.1.1. {\sl Orders}) 1 and $Ω$ are orders; if $A$ and $B$ are orders,
then $A×B$ and $Ω^A$ are also orders.

(1.1.2. {\sl Operators}) In the following, ``$σ∈A$'' means $σ$ is an
operator of order $A$; the rest of the arity is left unspecified for
simplicity.

For each order, there is a countable set of variable operators (called
``indeterminates'').

$*∈1$. $⊤∈Ω$.

If $σ, τ ∈ Ω$, then $σ∧τ$ and $σ→τ∈Ω$.

If $σ∈Ω$ and $\aa$ is an indeterminate of order $A$, then $Σ\aa∈A·σ$
and $Π\aa∈A·σ∈Ω$.
 
($×I$) If $σ∈A$, $τ∈B$, then $\ang{σ,τ}∈A×B$.

($×E$) If $σ∈A×B$, then $π_1σ∈A$, $π_2σ∈B$.

($PI$) If $\aa$ is an indeterminate of order $A$ and $σ∈Ω$, then
$[\aa∈A:σ]∈Ω^A$.

($PE$) If $τ∈A$, $σ∈Ω^A$, then $σ(τ)∈Ω$.

{\textsc{Definition} 1.1.3.} A type is an operator of order $Ω$.

(1.1.4. {\sl Terms}) In the following, ``$a∈τ$'' means $a$ is a term
of type $τ$; the rest of the arity is left unspecified for simplicity.

For each type, there is a countable set of variable terms (called
``variables'').

($⊤I$) $*∈⊤$.

($→I$) If $a∈τ$, $x$ a variable of type $σ$, then $λx∈σ·a∈σ→τ$.

($→E$) If $a∈σ→τ$, $b∈σ$, then $a(b)∈τ$.

($∧I$) If $a∈σ$, $b∈τ$, then $\ang{a,b}∈σ∧τ$.

($∧E$) If $a∈σ∧τ$, then $π_1a∈σ$ $π_2a∈τ$.

($ΣI$) If $\aa$is an indeterminate of order $A$, $σ∈Ω$, $τ∈A$, then
$I_{Σ\aa·σ,τ}∈σ[τ/\aa]→Σ\aa∈A·σ$. When clear from the context, we
shall denote this term by $I_τ$, or even by $I$; in particular, if
$b∈σ[τ/\aa]$, then $I(b)∈Σ\aa∈A·σ$.

($ΣE$) In $a∈σ→ρ$, $\aa$ an indeterminate of order $A$ which is not
free in $ρ$ nor in the type of any free variable in $a$, then
$𝐛V\aa∈A·a∈(Σ\aa∈A·σ)→ρ$.

($ΠI$) If $a∈σ$, $\aa$ an indeterminate of order $A$ which is not free
in the type of any free variable in $a$, then
$\Lambda\aa∈A·a∈Π\aa∈A·σ$.

($ΠE$) If $a∈Π\aa∈A·\aa$, $τ∈A$, then $a\{τ\}∈σ[τ/\aa]$, where
$σ[τ/\aa]$ is $σ$ with $τ$ replacing $\aa$.



\newpage
% --------------------
% «seely-plc-trees»  (to ".seely-plc-trees")
% (s "Seely's PLC paper: trees" "seely-plc-trees")
\myslide {Seely's PLC paper: trees} {seely-plc-trees}


%:<\langle 
%:>\rangle 
%:&\&

%:  ---   
%:  Ω:Θ
%:  
%:  ^Omega
%:  
%:  ---    ---   
%:  1:Θ    *:1   
%:  
%:  ^1     ^*1
%:  
%:  ---    ---
%:  ⊤:Ω    *:⊤
%:  
%:  ^T     ^*T
%:  
%:  A:Θ  B:Θ  σ:A  τ:B   σ:A×B   σ:A×B   
%:  --------  ---------  ------  ------  
%:   A×B:Θ    <σ,τ>:A×B  π_1σ:A  π_2σ:B  
%:  
%:   ^x       ^xI        ^xE1    ^xE2
%:  
%:   A:Θ          σ:Ω         τ:A  σ:A->Ω
%:  ------   --------------   -----------
%:  A->Ω:Θ   [\aa∈A:σ]:A->Ω     σ(τ):Ω
%:  
%:  ^->      ^->I               ^->E
%:  
%:  σ:Ω  τ:Ω  a:σ  b:τ    a:σ∧τ    a:σ∧τ 
%:  --------  ---------   ------   ------
%:    σ∧τ:Ω   <a,b>:σ∧τ   π_1a:σ   π_2a:τ
%:  
%:    ^and    ^andI       ^andE1   ^andE2
%:  
%:  σ:Ω  τ:Ω     a:τ       b:σ  a:σ→τ
%:  --------  ----------   ----------
%:    σ→τ:Ω   λx∈σ·a:σ→τ     a(b):τ
%:  
%:    ^imp    ^impI          ^impE
%:  
%:     σ:Ω          σ:Ω    τ:A               a:σ→ρ          
%:  ----------  -------------------   ----------------------
%:  Σ\aa∈A·σ:Ω  I:σ[τ/\aa]→Σ\aa∈A·σ   𝐛V\aa∈A·a:(Σ\aa∈A·σ)→ρ
%:  
%:  ^sum        ^sumI                 ^sumE
%:  
%:     σ:Ω              a:σ               τ:A  a:Π\aa∈A·\aa
%:  ----------  -----------------------   -----------------
%:  Π\aa∈A·σ:Ω  \Lambda\aa∈A·a:Π\aa∈A·σ    a\{τ\}:σ[τ/\aa] 
%:  
%:  ^prod       ^prodI                     ^prodE
%:  
$$\begin{array}{ccc}
  \ded{Omega}   \\ \\
  \ded{1} & \ded{*1}   \\ \\
  \ded{T} & \ded{*T}   \\ \\
  \ded{x} & \ded{xI} & \ded{xE1} \qquad \ded{xE2}   \\ \\
  \ded{->} & \ded{->I} & \ded{->E}   \\ \\
  \ded{and} & \ded{andI} & \ded{andE1} \qquad \ded{andE2}   \\ \\
  \ded{imp} & \ded{impI} & \ded{impE}   \\ \\
  \end{array}
$$

$$\begin{array}{ccccc}
  \ded{sum}  && \ded{sumI}  && \ded{sumE}   \\ \\
  \ded{prod} && \ded{prodI} && \ded{prodE}   \\ \\
  \end{array}
$$


\newpage
% --------------------
% «seely-plc-trees-dnc»  (to ".seely-plc-trees-dnc")
% (s "Seely's PLC paper: trees, in DNC" "seely-plc-trees-dnc")
\myslide {Seely's PLC paper: trees, in DNC} {seely-plc-trees-dnc}


%:  ---   
%:  Ω:Θ
%:  
%:  ^d.Omega
%:  
%:  ---      ---   
%:  1:Θ      *:1   
%:  
%:  ^d.1     ^d.*1
%:  
%:  ------    -------
%:  ω[⊤]:Ω    ⊤:ω[T]⊤
%:  
%:  ^d.T      ^d.*T
%:  
%:  A   B  a   b   a,b       a,b   
%:  -----  -----   ---       ---  
%:   A×B    a,b     a         b  
%:  
%:   ^d.x   ^d.xI   ^d.xE1    ^d.xE2
%:  
%:   A         ω[P]      a  a|->ω[P]
%:  ------   --------    -----------
%:  A->Ω     a|->ω[P]       ω[P]
%:  
%:  ^d.->    ^d.->I         ^d.->E
%:  
%:  ω[P]  ω[Q]  P  Q     P&Q        P&Q 
%:  ----------  ----     ---        ---
%:    ω[P&Q]     P&Q      P          Q
%:  
%:    ^d.and     ^d.andI  ^d.andE1   ^d.andE2
%:  
%:  ω[P]  ω[Q]   Q      P  P→Q
%:  ----------  ---     ------
%:    ω[P→Q]    P→Q       Q
%:  
%:    ^d.imp    ^d.impI   ^d.impE
%:  
%:    ω[P]   a,b|-ω[P]   a|-b   a|-ω[Q]   a,b;⊤|-P→Q          
%:  -------  ----------------   --------------------
%:  ω[∃b.P]    a|-P→(∃b.P)           a;⊤|-(∃b.P)→Q
%:  
%:  ^d.sum     ^d.sumI               ^d.sumE
%:  
%:    ω[P]   a|-ω[P]  a,b;P|-Q   b  ∀b.P
%:  -------  -----------------   -------
%:  ω[∀b.P]     a;P|-∀b.Q          b 
%:  
%:  ^d.prod     ^d.prodI           ^d.prodE
%:  
$$\begin{array}{ccc}
  \ded{d.Omega}   \\ \\
  \ded{d.1} & \ded{d.*1}   \\ \\
  \ded{d.T} & \ded{d.*T}   \\ \\
  \ded{d.x} & \ded{d.xI} & \ded{d.xE1} \qquad \ded{d.xE2}   \\ \\
  \ded{d.->} & \ded{d.->I} & \ded{d.->E}   \\ \\
  \ded{d.and} & \ded{d.andI} & \ded{d.andE1} \qquad \ded{d.andE2}   \\ \\
  \ded{d.imp} & \ded{d.impI} & \ded{d.impE}   \\ \\
  \end{array}
$$

$$\begin{array}{ccccc}
  \ded{d.sum}  && \ded{d.sumI}  && \ded{d.sumE}   \\ \\
  \ded{d.prod} && \ded{d.prodI} && \ded{d.prodE}   \\ \\
  \end{array}
$$


\newpage
% --------------------
% «local-set-theories»  (to ".local-set-theories")
% (s "Local set theories" "local-set-theories")
\myslide {Local set theories} {local-set-theories}

{%\myttchars
\footnotesize
\begin{verbatim}
(T1)  |-*

(T2)  a|-a

      a|-b  b|->c
(T3)  -----------
        a|-c

      a|-b_1 ... a|-b_n
(T4)  -----------------
      a|-(b_1,...,b_n)

      a|-(b_1,...,b_n)
(T5)  -----------------
          a|-b_i

      a,b|-ω[P]
(T6)  ---------
      a|-{b|P}

      a|-b  a|-b'
(T7)  -----------
      a|-ω[b=b']

      a|-b  a|-{b|P}
(T8)  --------------
       a|-ω[b∈{b|P}]


(L1)  P<=>Q := ω[P]=ω[Q]
(L2)      ⊤ := *=*
(L3)    P∧Q := (ω[P],ω[Q])=(ω[⊤],ω[⊤])
(L4)    P→Q := (P∧Q)<=>P
(L5)   ∀b.P := {b|P}={b|⊤}
(L6)      ⊥ := ∀ω[P].P
(L7)     ¬P := P→⊥
(L8)    P∨Q := ∀ω[R].(((P→R)∧(Q→R))→R)
(L9)   ∃b.P := ∀ω[Q]. ...
\end{verbatim}
}


\newpage
% --------------------
% «local-set-theories-2»  (to ".local-set-theories-2")
% (s "Local set theories (1)" "local-set-theories-2")
\myslide {Local set theories (1)} {local-set-theories-2}


{%\myttchars
\footnotesize
\begin{verbatim}
(Tautology)     P|-P
(Unity)         |-*'=*
(Equality)      b'=b''|-c[b:=b']=c[b:=b'']
(Products)      |-π<b,c>=b
                |-π'<b,c>=c
                |-<π(b,c),π'(b,c)>=(b,c)
(Comprehension) |-b∈{b|P}<=>P


                  P|-R
(Thinning)        ------
                  P,Q|-R

                  a;P|-Q   a;P,Q|-R
(Cut)             -----------------
                       a;P|-R

                    a,b;P|-Q   a|-b'
(Subst)           --------------------
                  a;P[b:=b']|-Q[b:=b']

                  a,b;P|-b∈{b|Q}<=>b∈{b|R}
(Extensionality)  ------------------------
                    a;P|-{b|Q}<=>{b|R}

                  P,Q|-R   P,R|-Q
(Equivalence)     ---------------
                     P|-Q<=>R
\end{verbatim}
}



\newpage
% --------------------
% «notes-seelyhyp»  (to ".notes-seelyhyp")
% (s "Notes on SeelyHyp" "notes-seelyhyp")
\myslide {Notes on reading SeelyHyp} {notes-seelyhyp}


  %
% (eedn4a-bounded)
% (find-ragshyppage (+ -504 513))
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")

\def\eqdef{\overset{\text{def}}{=}}

SeelyHyp, \S4:

(5') (i) For $t: X \to Y$, $\phi$ over $X$, we define

$Σ_t \phi \eqdef ∃\xi (t\xi = y ∧ \phi(\xi))$,

$Π_t \phi \eqdef ∀\xi (t\xi = y → \phi(\xi))$,

%:               tx=y∧\cc(x)
%:               -----------(∧E)
%:                  [\cc(x)]       tx=y∧\cc(x)
%:                  :::::::P       -----------(∧E)
%:                  \phi(x)          tx=y
%:                  ---------------------(∧I)
%:                           tx=y∧\phi(x)
%:                           ---------------------(∃I)
%:  ∃\xi(t\xi=y∧\cc(\xi))    ∃\xi(t\xi=y∧\phi(\xi))
%:  ---------------------------------------------(∃E)
%:                   ∃\xi(t\xi=y∧\phi(\xi))
%:
%:                   ^xii
%:
$$\ded{xii}$$


\bsk

For $f: A \to B$, define:

$Σ_f \ssst{a}{P(a)} \quad \eqdef \quad \ssst{b}{∃a.(f(a)=b \;\&\; P(a))}$

$Π_f \ssst{a}{P(a)} \quad \eqdef \quad \ssst{b}{∀a.(f(a)=b \;→\; P(a))}$


%:               		 [f(a)=b∧P(a)]^1      
%:                               ---------------(∧E)
%:           [f(a)=b∧P(a)]^1	     P(a)         
%:           ---------------(∧E)     ::::         
%:                  f(a)=b           Q(a)         
%:                  ---------------------(∧I)
%:                  un         f(a)=b∧Q(a)
%:                           ---------------(∃I)
%:  ∃a.(f(a)=b∧P(a))         ∃a.(f(a)=b∧Q(a))
%:  ---------------------------------------------(∃E)
%:                   ∃a.(f(a)=b∧Q(a))
%:
%:                   ^xiii
%:
$$\ded{xiii}$$


\newpage
% --------------------
% «luo»  (to ".luo")
% (s "Luo's ECC" "luo")
\myslide {Luo's ECC} {luo}

\def\Type{\mathit{Type}}
\def\Prop{\mathit{Prop}}

% (fooi "\Type_j" "Θ_j")

%:  
%:  ---------------(Ax)                     -------(Ax)
%:  |-\Prop:\Type_0                         |-Ω:Θ_0
%:  
%:  ^luo-Ax                                 ^luo-Ax-dnc
%:  
%:     \GG|-A:\Type_j			      a|-B:Θ_j					
%:  ----------------------(C)		    -----------(C)			
%:  \GG,x⠆A|-\Prop:\Type_0		    a,b|-Ω:Θ_0
%:  					    							
%:  ^luo-C				    ^luo-C-dnc						
%:  					    							
%:    \GG|-\Prop:\Type_0		      a|-Ω:Θ_0				
%:  ------------------------(T)		    ---------------------(T)				
%:  \GG|-\Type_j:\Type_{j+1}		    \GG|-Θ_j:Θ_{j+1}				
%:  					    							
%:  ^luo-T				    ^luo-T-dnc
%:  					    							
%:  \GG,x⠆A,\GG'|-\Prop:\Type_0		    a,b,c|-Ω:Θ_0				
%:  ---------------------------(var)	    ------------(var)			
%:       \GG,x⠆A,\GG'|-x⠆A		      a,b,c|-b				
%:  					    							
%:       ^luo-var			      ^luo-var-dnc					
%:  					    							
%:  \GG,x⠆A|-P:\Prop                        a,b|-ω[P]:Ω                                 
%:  -----------------(Π1)                   -------------(Π1)                           
%:  \GG|-Πx⠆A.P:\Prop                       a|-ω[∀b.P]:Ω                                        
%:                                                                                              
%:  ^luo-prod1                              ^luo-prod1-dnc
%:  					    							
%:  \GG|-A:\Type_j  \GG,x⠆A|-B:\Type_j	    a|-B:Θ_j  a,b|-C:Θ_j			
%:  ----------------------------------(Π2)  ----------------------(Π2)		
%:       \GG|-Πx⠆A.B:\Type_j		         a|-Πb⠆B.C:Θ_j				
%:                                                                                          
%:       ^luo-prod2			         ^luo-prod2-dnc					
%:                                                                                          
%:  \GG,x⠆A|-M:B                            a,b|-c:C                                    
%:  ------------------(λ)                   ------------------(λ)                               
%:  \GG|-λx⠆A.M:Πx⠆A.B                      a|-λb.c:Πb⠆B.C                                      
%:                                                                                          
%:  ^luo-lambda                             ^luo-lambda-dnc
%:                                                                                              
%:  \GG|-M:Πx⠆A.B  \GG|-N:A                 a|-(b|->c)  a|-b                            
%:  -----------------------(app)            -----------------------(app)                        
%:     \GG|-MN:[N/x]B                          a|-c                                     
%:                                                                                              
%:     ^luo-app                                ^luo-app-dnc
%:                                                                                              
%:  \GG|-A:\Type_j  \GG,x⠆A|-B:\Type_j      a|-B:Θ_j  a,b|-C:Θ_j                        
%:  ----------------------------------(Σ)   --------------------(Σ)             
%:     \GG|-Σx⠆A.B:\Type_j                     a|-Σb⠆B.C:Θ_j                            
%:                                                                                              
%:     ^luo-sum                                ^luo-sum-dnc
%:
%:  \GG|-M:A  \GG|-N:[M/x]B  \GG,x:A|-B:\Type_j
%:  -------------------------------------------(pair)
%:    \GG|-\mathbf{pair}_{Σx⠆A.B}(M,N):Σx⠆A.B
%:
%:    ^luo-pair
%:
%:  \GG|-M:Σx⠆A.B                            a|-(b,c):Σb⠆B.C           
%:  -------------(π1)                        -------------(π1)         
%:  \GG|-π_1(M):A                            a|-b:B            
%:                                                                      
%:  ^luo-pi1                                 ^luo-pi1-dnc
%:                                                                      
%:       \GG|-M:Σx⠆A.B                       a|-(b,c):Σb⠆B.C           
%:  -----------------------(π2)              ---------------(π2)
%:  \GG|-π_2(M):[π_1(M)/x]B                  a|-c:C    
%:
%:  ^luo-pi2                                 ^luo-pi2-dnc
%:
%:  \GG|-M:A   \GG|-A':\Type_j
%:  --------------------------(A{\preceq}A')
%:     \GG|-M:A'
%:
%:     ^luo-preceq
%:
$$\ded{luo-Ax}$$
$$\ded{luo-C}$$
$$\ded{luo-T}$$
$$\ded{luo-var}$$
$$\ded{luo-prod1}$$
$$\ded{luo-prod2}$$
$$\ded{luo-lambda}$$
$$\ded{luo-app}$$
$$\ded{luo-sum}$$
$$\ded{luo-pair}$$
$$\ded{luo-pi1}$$
$$\ded{luo-pi2}$$
$$\ded{luo-preceq}$$

\newpage

$$\ded{luo-Ax-dnc}$$
$$\ded{luo-C-dnc}$$
$$\ded{luo-T-dnc}$$
$$\ded{luo-var-dnc}$$
$$\ded{luo-prod1-dnc}$$
$$\ded{luo-prod2-dnc}$$
$$\ded{luo-lambda-dnc}$$
$$\ded{luo-app-dnc}$$
$$\ded{luo-sum-dnc}$$
% $$\ded{luo-pair-dnc}$$
$$\ded{luo-pi1-dnc}$$
$$\ded{luo-pi2-dnc}$$
% $$\ded{luo-preceq-dnc}$$








\end{document}

 (eepitch-shell)
 (eepitch-kill)
 (eepitch-shell)
cp -v ~/LATEX/2008notations.tex /tmp/o
~/LUA/texcatcodes.lua -trans /tmp/o /tmp/o2
# (find-fline "~/LATEX/2008notations.tex")
# (find-fline "/tmp/o2")
# (find-fline "~/LUA/texcatcodes.lua")

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