% (find-angg "LATEX/2008notations.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008notations.tex && latex    2008notations.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008notations.tex && pdflatex 2008notations.tex"))
% (eev "cd ~/LATEX/ && Scp 2008notations.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008notations.dvi")
% (find-pspage  "~/LATEX/2008notations.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2008notations.ps 2008notations.dvi")
% (find-pspage  "~/LATEX/2008notations.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")

% «.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")

% Bater: Martin-Löf, Phoa, Reynolds, Wadler, Jacobs

\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08}       % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty"  -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex   % (find-dn4ex "edrxheadfoot.tex")
\begin{document}

\input 2008notations.dnt

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


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)    PQ := ýÏ[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}

% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End:
