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