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

% «.basic-rules»	(to "basic-rules")
% «.strong-rules»	(to "strong-rules")


\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 2008lcccs.dnt

%*
% (eedn4-51-bounded)

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 {Basic rules} {2}
\tocline {Strong rules} {3}

\def\Eq{¯{Eq}}


\newpage
% --------------------
% «basic-rules»  (to ".basic-rules")
% (s "Basic rules" "basic-rules")
\myslide {Basic rules} {basic-rules}

% (find-jacobspage (+ 19 581) "10_  First order dependent type theory")
% (find-jacobspage (+ 19 585) "five basic rules of DTT")

Rules:
%:
%:  a|-b:B   a|-B=B'
%:  ----------------¯{conv}
%:       a|-b:B'
%:  
%:       ^conv
%:  
%:   a|-B           a|-b  a,b,c|-d
%:  ------¯{proj}   --------------¯{subst}
%:  a,b|-b            a,c|-d
%:  
%:  ^proj             ^subst
%:  
%:     a,b,b',c|-d               a|-B  a|-c
%:  ------------------¯{contr}   ----------¯{weak}
%:  a,b,\ov{c}|-\ov{d}             a,b|-c
%:  
%:  ^contr                         ^weak
%:  
%:    a,b,c,d|-e                       a|-*'
%:    ----------¯{exch}    ---   ---   -------
%:    a,c,b,d|-e           |-1   |-*   a|-*'=*
%:  
%:    ^exch                ^1    ^*    ^*=*
%:  
$$\ded{conv} \qquad \ded{proj} \qquad \ded{subst}$$

$$\ded{contr} \qquad \ded{weak} \qquad \ded{exch}$$

$$\ded{1} \qquad \ded{*} \qquad \ded{*=*}$$


Formation rules:
%:
%:    a,b|-C       a,b|-C      a|-B
%:  ---------å   ---------Æ   ---------------¯{Eq}
%:  a|-åb:B.C    a|-Æb:B.C    a,b,b'|-\Eq_B[b=b']
%:  
%:  ^Pi          ^Sigma       ^Eq
%:  
$$\ded{Pi} \qquad \ded{Sigma} \qquad \ded{Eq}$$

% (find-jacobspage (+ 19 586) "associated introduction and elimination rules")

Intros and elims:
%:  
%:   a,b|-c      a|-b  a|-b|->c
%:  --------ð    --------------¯{app}
%:  a|-b|->c         a|-c
%:  
%:  ^lambda          ^app
%:  
%:    a,b|-C               a,b,c|-d
%:  ------------¯{pair}    ----------¯{unpack.weak}
%:  a,b,c|-(b,c)           a,(b,c)|-d
%:  
%:  ^pair                  ^unpack.weak
%:  
%:     a|-B             a,b,b',c|-D    a,b,\ov{c}|-\ov{d}
%:  ----------¯{refl}   ---------------------------------¯{with.via.weak}
%:  a,b|-(b=b)                a,b,b',(b=b'),c|-d
%:  
%:  ^refl                     ^withvia.weak
%:  
$$\ded{lambda} \qquad \ded{app}$$
$$\ded{pair} \qquad \ded{unpack.weak}$$
$$\ded{refl} \qquad \ded{withvia.weak}$$

% (find-jacobspage (+ 19 587) "10.1.1. Example")

Example (10.1.1):
%:
%:                                              a,b'|-C_{b'}         a,b|-C_b
%:                                            ==================   ------------
%:                                 a|-\bb'    a,b,b',c_b|-C_{b'}   a,b,c_b|-c_b
%:                                =========   ---------------------------------
%:                                a,b|-\bb'   a,b,b',(b=b'),c_b|-c_{b'}
%:                                -----------------------------------
%:                         a|-\bb       a,b,(b=\bb'),c_b|-c_{\bb'}
%:                         ---------------------------------------
%:           a|-(\bb=\bb')     a,(\bb=\bb'),c_\bb|-c_{\bb'}
%:           ----------------------------------------------
%:  a|-c_\bb          a,c_\bb|-c_{\bb'}
%:  -----------------------------------
%:            a|-c_{\bb'}
%:  
%:            ^example-10.1.1
%:
$$\ded{example-10.1.1}$$


\newpage
% --------------------
% «strong-rules»  (to ".strong-rules")
% (s "Strong rules" "strong-rules")
\myslide {Strong rules} {strong-rules}

Strong rules:
%:  
%:  a,(b,c)|-D   a,b,c|-d
%:  ---------------------¯{unpack.strong}
%:     a,(b,c)|-d
%:  
%:     ^unpack.strong
%:  
%:  a,b,b',(b=b')|-C   a,b|-\ov{\ov{c}}
%:  -----------------------------------¯{with.via.strong}
%:       a,b,b',(b=b')|-c
%:  
%:       ^with.via.strong
%:  
$$\ded{unpack.strong}$$
$$\ded{with.via.strong}$$

Proposition: the strong rules are equivalent to:
%:  
%:  a|-(b,c)     a|-(b,c)
%:  --------    --------'
%:    a|-b        a|-c
%:  
%:    ^pi         ^pi'
%:  
%:  a|-(b=b')               a|-(b=b)'
%:  ---------¯{eq.ext}   ---------------¯{eq.refl}
%:  a|-b=b'              a|-(b=b)'=(b=b)
%:  
%:  ^eq.ext              ^eq.refl
%:  
$$\ded{pi} \qquad \ded{pi'}$$
$$\ded{eq.ext} \qquad \ded{eq.refl}$$

Proof 1:
%:  
%:    a,b|-C
%:   --------
%:   a,b,c|-c             a,b|-C
%:  ==========¯{unp.w}   --------
%:  a,(b,c)|-c           a,b,c|-c
%:  =============================
%:            a,(b,c)|-C          a,b,c|-c
%:            ----------------------------
%:            a,(b,c)|-c
%:  
%:            ^proof-1
%:
$$\ded{proof-1}$$



%*

\end{document}

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