|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
[lua:
PAREN3 = lambda("one, two, three", undollar [["\n($one,\n $two,\n $three)\n"]])
TABLE = lambda("text", undollar [["<table>$text\n</table>\n"]])
TR = lambda("text", undollar [["<tr>$text\n</tr>\n"]])
TD = lambda("bg, text", undollar [["<td>$text\n</td>\n"]])
TDBG = lambda("bg, text", undollar [["<td bgcolor=\"$bg\">$text\n</td>\n"]])
FG = lambda("bg, text", undollar [["<font bgcolor=\"$fg\">$text</font>\n"]])
BGBLOCK = lambda("bg, text", [[TABLE(TR(TDBG(bg, text)))]])
QUO = lambda("text", undollar [["\n<blockquote>\n$text\n</blockquote>\n"]])
MATHL = lambda("fname, text", [[HREF("math/"..fname, fname).." "..text]])
mathL = lambda("fname, text", [[HREF("math/"..fname, fname)]])
setgetargs(vargs1, "QUO")
setgetargs(vargs2, "TABLE TR TD TDBG FG BGBLOCK MATHL mathL")
-- print(2802, mathL, _GETARGS["mathL"])
-- (find-zsh "cd ~/LUA/; lua blogme.lua -o ~/TH/L/math-b.html -i math.blogme")
-- (find-shttpfile "www.schemers.org/index.html" "<font color=GREEN>")
-- (find-fline "~/TH/L/e/gtk.e.html" "td bgcolor")
--22FF22
-- (eev "edrxnetscape ~/TH/L/math.html &" nil)
-- (find-es "page" "math.th-files")
]
[htmlize [J Eduardo Ochs - Academic Research - Categories, NSA, the
"Typical Point Notation", and a language for skeletons of proofs] [J
(...quick notes added in 2001dec26; I still haven't had time to glue
the pieces together and make a coherent whole. The rest of the page is
older.)
[HLIST1 [J Some important online texts:]
[HLIST2 [J On Category Theory, plus some unclassified things:]
[HLIST2 [J Barr/Wells: Toposes, Triples, and Theories (1985):]
[LR http://www.cwru.edu/artsci/math/wells/pub/ttt.html]
]
[J Phil Scott: [LR http://linear.di.fc.ul.pt/handbook.ps Some
Aspects of Categories in Computer Science] (1998/2000; a
chapter of the "Handbook of Algebra")]
[HLIST2 [J [LR http://www.cl.cam.ac.uk/~amp12/ Pitts]: Categorical
Logic (2001):]
[LR http://citeseer.nj.nec.com/pitts01categorical.html]
[LR http://www.cl.cam.ac.uk/~amp12/papers/]
[LR ftp://ftp.cl.cam.ac.uk/papers/amp12/catl.ps.gz]
]
[J [LR http://www.mathematik.tu-darmstadt.de/~streicher/ Thomas
Streicher]'s notes on [LR
http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/fib.ps.gz
Fibered Categories à là Jean Bénabou] (1999)]
[J Wesley Phoa: [LR
http://www.lfcs.informatics.ed.ac.uk/reports/92/ECS-LFCS-92-208/ECS-LFCS-92-208.ps.gz
An Introduction to Fibrations, Topos Theory, the Effective Topos
and Modest Sets]]
[HLIST2 [J Caccamo/Hyland/[LR http://www.cl.cam.ac.uk/~gw104/ Winskel]:]
[J [LR http://www.brics.dk/~mcaccamo/catnotes.ps.gz
Lecture Notes in Category Theory [' [Draft]] (2001)]
[J [LR http://www.brics.dk/RS/01/27/BRICS-RS-01-27.dvi.gz
A Higher-Order Calculus for Categories]]
]
[LR http://www.math.unipd.it/~maietti/ Milly Maietti's home page]
[HLIST2 [J [LR
http://www.tcs.informatik.uni-muenchen.de/~mhofmann/papers.html
Martin Hofmann]: Syntax and Semantics of Dependent Types
(1997):]
[LR http://citeseer.nj.nec.com/hofmann97syntax.html]
]
[HLIST2 [Q Nordström/Petersson/Smith: Martin-Löf's Type Theory:]
[LR http://citeseer.nj.nec.com/1666.html]
]
[HLIST2 [J Mark P. Jones: First Class Polymorphism with Type
Inference (1997):]
[LR http://www.cse.ogi.edu/~mpj/pubs/popl97-fcp.dvi.gz]
]
]
[HLIST2 [J On Type Theory (mainly on the Calculus of Constructions):]
[HLIST2 [LR http://www.cs.kun.nl/~herman/pubs.html Herman Geuvers]'s...
[J PhD thesis, [LR http://www.cs.kun.nl/~herman/Proefschrift.ps.gz
"Logics and Type Systems"] (1993), and]
[LR http://www.cs.kun.nl/~herman/BRABasSNCC.ps.gz "A Short and
Flexible Proof of Strong Normalization for the Calculus of
Constructions"]
]
[HLIST2 [J Barendregt: Lambda Calculi with Types (1992):]
[LR http://citeseer.nj.nec.com/barendregt92lambda.html]
[LR ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z]
]
[J [LR http://www.dur.ac.uk/zhaohui.luo/ Zhaohui Luo]'s PhD thesis:
"[LR http://www.dur.ac.uk/~dcs0zl/THESIS90.dvi.gz An Extended
Calculus of Constructions]" (1990).]
[J [LR http://home.uleth.ca/~jonathan.seldin/publications.html
Jonathan Seldin]'s homepage]
[J [LR http://www.cs.chalmers.se/~coquand/ Thierry Coquand]'s homepage]
[J Barbanera/[LR http://www.di.unito.it/~stefano/ Berardi]: [LR
http://www.di.unito.it/~stefano/Barbanera-ProofIrrelevanceOutOf.ps
Proof-Irrelevance out of Excluded Middle and Choice in the
Calculus of Constructions]]
]
[HLIST2 [J On Parametricity:]
[HLIST2 [J Phil Wadler:]
[LR
http://www.research.avayalabs.com/user/wadler/topics/parametricity.html
Theorems for Free! (1989), The Girard-Reynolds Isomorphism
(2001)]
[LR http://www.research.avayalabs.com/user/wadler/topics/history.html
Proofs are Programs: 19th Century Logic and 21st Century Computing]
]
[HLIST2 [J John Reynolds:]
[LR http://www-2.cs.cmu.edu/~jcr/
On Functors Expressible in the Polymorphic Typed Lambda Calculus]
]
[HLIST2 [J Izumi Takeuti:]
[J [LR http://www.sato.kuis.kyoto-u.ac.jp/~takeuti/abs-e.html#param
An Axiomatic System of Parametricity] (1998)]
[J [LR http://www.sato.kuis.kyoto-u.ac.jp/~takeuti/abs-e.html#cube
The Theory of Parametricity in Lambda Cube] (draft)]
]
[HLIST2 [J Harry Mairson:]
[LR http://www.cs.brandeis.edu/~mairson/Papers/para.ps.gz
Outline of a Proof Theory of Parametricity]
]
]
[HLIST2 [J On Non-standard Analysis, SDG and friends:]
[LR http://members.tripod.com/PhilipApps/nonstandard.html
A page with many links on Non-Standard Analysis]
[HLIST2 [LR http://www.acsu.buffalo.edu/~wlawvere/ William Lawvere]:
[J [LR http://www.acsu.buffalo.edu/~wlawvere/SDG_Outline.pdf
Outline of Synthetic Differential Geometry] (1998)]
[J [LR http://www.acsu.buffalo.edu/~wlawvere/ToposMotion.pdf
Toposes of Laws of Motion] (1997)]
]
[J [LR http://www.math.uu.se/~jonase/ Jonas Eliasson] seems to be
working on the relation between toposes of filters and toposes of
ultrafilters; he makes reference to some [LR
http://www.math.uu.se/~palmgren/publicat.html papers by Erik
Palmgren] that are not on-line.]
[J [LR http://iml.univ-mrs.fr/~ehrhard/pub.html Thomas Ehrhard]:
[LR ftp://iml.univ-mrs.fr/pub/ehrhard/difflamb.ps.gz The
Differential Lambda-Calculus] (2001).]
[HLIST2 [LR http://home.imf.au.dk/kock/ Anders Kock]:
[J [LR http://www.tac.mta.ca/tac/volumes/1999/n10/n10.ps Aspects
of Fractional Exponent Functors] (1999, with G. Reyes)]
[J [LR ftp://ftp.imf.au.dk/pub/kock/ODE5.ps Fractional Exponent
Functors and Categories of Differential Equations] (1998, with
G. Reyes)]
]
[J [LR http://www.brics.dk/~butz/ Carsten Butz]: [LR
http://www.brics.dk/~butz/public_ftp/new_stuff/filter.ps.gz The
filter construction revisited]
]
]
]
[P Citeseer search: [LR http://citeseer.nj.nec.com/cs/]]
[P HPSearch: [LR http://hpsearch.uni-trier.de/]]
[P [LR http://www.cs.uu.nl/people/franka/ref Frank Atanassow's list of
online Programming Language Theory texts]]
[RULE]
[P News, 2002may17: I'm not having enough time to update this page --
I'm spending 8 months doing research at [LR http://www.math.mcgill.ca/
McGill University], working with [LR http://www.math.mcgill.ca/~rags/
Robert Seely], with a [LR http://www.capes.gov.br/ CAPES]'s [LR
http://www.capes.gov.br/Bolsas/Exterior/Doutorando.htm "Sandwich
PhD"] grant, and besides the academic side there are also hundreds of
things happening wite my on a personal level, I'm sort of leaving my
tadpole stage -- and my newest sets of notes are too messy, and many
important parts of them are not TeXed yet... but, just to give an idea
of what I've been working on, here's the abstract for a presentation
that I'll be giving at the [LR
http://cs.colgate.edu/faculty/mulry/FMCS2002/Web/FMCS2002.html
FMCS2002] in early June:]
[P --snip--snip--]
[P Title: A System of Natural Deduction for Categories]
[P We will present a logic (system DNC) whose terms represent
categories, objects, morphisms, functors, natural transformations,
sets, points, and functions, and whose rules of deduction represent
certain constructive operations involving those entities. Derivation
trees in this system only represent the "T-part" (for "terms" and
"types") of the constructions, not the "P-part" ("proofs" and
"propositions"): the rules that generate functors and natural
transformations do not check that they obey the necessary equations.
So, we can see derivations in this system either as constructions
happening in a "syntactical world", that should be related to the
"real world" in some way (maybe through meta-theorems that are yet
to be found), or as being just "skeletons" of the real
constructions, with the P-parts having been omitted for briefness.]
[P Even though derivations in DNC tell only half of the story, they
still have a certain charm: DNC terms represent "types", but a tree
represents a construction of a lambda-calculus term; there's a
Curry-Howard isomorphism going on, and a tree can be a visual help for
understanding how the lambda-calculus term works -- how the data flows
inside a given categorical construction. Also, if we are looking for a
categorical entity of a certain "type" we can try to express it as a
DNC term, and then look for a DNC "deduction" having it as its
"conclusion"; the deduction will give us a T-part, and we will
still have to go back to the standard language to supply a P-part, but
at least the search has been broken in two parts...]
[P The way to formalize DNC, and to provide a translation between
terms in its "logic" and the usual notations for Category Theory, is
based on the following idea. Take a derivation tree D in the Calculus
of Constructions, and erase all the contexts and all the typings that
appear in it; also erase all the deduction steps that now look
redundant. Call the new tree D'. If the original derivation, D, obeys
some mild conditions, then it is possible to reconstruct it -- modulo
exchanges and unessential weakenings in the contexts -- from D', that
is much shorter. The algorithm that does the reconstruction generates
as a by-product a "dictionary" that tells the type and the "minimal
context" for each term that appears in D'; by extending the language
that the dictionary can deal with we get a way to translate DNC terms
and trees -- and also, curiously, with a few tricks more, and with
some minimal information to "bootstrap" the dictionary, categorical
diagrams written in a DNC-like language.]
[P --snip--snip--]
[P I'll also be giving a slightly shorter version of that talk at the
[LR http://www.cms.math.ca/Events/summer02/ CMS Summer 2002 Meeting],
in mid-June.]
[P I believe that the essential details (i.e., the "T-part") of a
certain construction of a categorical model of the Calculus of
Constructions fit in a few DNC diagrams, but my work on that is far
from finished :(.]
[RULE]
[P I am currently finishing the second year of my PhD on Mathematics,
at PUC-Rio, in Rio de Janeiro, Brazil. My work revolves around trying
to explain two "facts":]
[P 1) Some Calculus proofs involving infinitesimals, that apparently
would need either Non-Standard Analysis or Synthetical Differential
Geometry ("NSA" and "SDG", from now on) to be formalized, can be
translated into completely formal standard proofs --- where the
arguments about infinitesimals become standard arguments about limits
and continuity --- via a ridiculously simple trick whose central step
is to reread the "skeleton" of the proof in a certain filter-power
of the standard universe, instead of using a ultrafilter-power. These
proofs are certainly happening in a fragment of the usual logic; but
which fragment?]
[P 2) Proofs in category theory often also admit "skeletons"; VERY
roughly, the "skeleton" of a proof is a tree or diagram that encodes
the way of constructing the intermediate objects used in the proof;
by squeezing these trees or diagrams just a bit we can derive some
"natural properties" of the intermediate objects, and the original
statement we wanted to prove turns out to be an easy consequence of
these natural properties... That is, each such proof can be reduced to
a construction plus some trivial checkings; once the construction is
given it is possible to say "then it is obvious that xxx happens",
and a reader (or an automated reasoning system, working on a small
search space) should be able to fill up the missing details very
quickly; that is, we will have a language where certain uses of "it
is obvious that ..." will have a formal meaning, and in this language
the skeletons of proofs [IT are], modulo the last "it is obvious
that", real proofs. Moreover: if we define an "easy" proof as being
a proof that admits a "decent" skeleton (this must be formalized, of
course) then what I hope to be able to claim is this: [IT a
significant part of topos theory is "easy"]. Corollary: a topos
semantics for the language with infinitesimals mentioned above is
"easy to understand", and basic topos theory can be presented in a
much simpler way; it certainly doesn't need to be the bugaboo that
students usually think it is.]
[P I know that these topics may sound at the same time too pretentious
and too basic -- especially the language for proofs in categories --,
but I think that I have a pretty good reason to work on that: I'm
using the typical point notation to simplify category theory for
myself... many important objects of topos theory can be named in
typical point notation just by their types, without having to be
preceded by long chains of definitions, and many questions about
natural objects become even more natural; for example, if we are told
that there is an adjunction between the functors L and R we may try to
write down the "names" of two morphisms aL->b and a->bR and then try
to see if they "carry the same information", i.e., if regarding them
as programs (think in lambda-calculus) we can convert one into
another, and back. Also, it must be possible to construct the units
and counits a->aLR and bRL->b of the adjunction "from nothing", and
so on. Note: I still don't have a good notation for terms (only for
types right now) and so it is generally better to use the standard
notation to reason about reductions; however in my notes (links below)
I have some examples of translations between TP and standard
notations, and of using the TP notation to draw diagrams.]
[P An example of a diagram extracted from the proof in TP notation
that a functor that is a right adjoint preserves limits (pullbacks in
this case, and yes, the explanations [IT are] missing).]
[IMAGE IMAGES/preslim.png (right adjoints preserve limits)]
[P [Q [J You can pick a copy of my notes on the "typical point
notation" from the links below (2001a was last updated in
2001jan30, 2001b in 2001mar07, 2001c in 2001may07):]]]
[P Be warned that these notes are in a quite preliminary form: some
sections end abruptly, others do not exist, and the formatting is very
bad. Nevertheless, the main ideas are quite clear (I hope!), at least
in 2001a and 2001c.]
[LIST1
[J [L math/2001a-dvi.tgz 2001a-dvi.tgz] (dvi plus .eps files)]
[J [L math/2001a-dvi.zip 2001a-dvi.zip] (dvi plus .eps files)]
[J [L math/2001a.ps.gz 2001a.ps.gz] (postscript, 600dpi)]
[J [L math/2001a-ps.zip 2001a-ps.zip] (postscript, 600dpi)]
]
[P You almost certainly don't want to download 2001b: it contains some
early notes about "basic topos theory being easy" and about natural
deduction in arbitrary categories and in topoi, but everything is
messy, obscure and wrong. If you print it I'll have to deny that I
wrote it; previewing is OK, though, but will probably be a waste of
time.]
[LIST1
[J [L math/2001b-dvi.tgz 2001b-dvi.tgz] (dvi plus .eps files)]
[J [L math/2001b-dvi.zip 2001b-dvi.zip] (dvi plus .eps files)]
[J [L math/2001b.ps.gz 2001b.ps.gz] (postscript, 600dpi)]
[J [L math/2001b-ps.zip 2001b-ps.zip] (postscript, 600dpi)]
]
[P 2001c contains the "real" notes about a system of natural
deduction for categories, and how we can use this system to define
what is a "syntactical" (or "easy") categorical proof; some
examples of things that have syntactical proofs are the Yoneda lemma
and the fact that a Set^C has exponentials and a classifier object.]
[LIST1
[J [L math/2001c-dvi.tgz 2001c-dvi.tgz] (dvi plus .eps files)]
[J [L math/2001c-dvi.zip 2001c-dvi.zip] (dvi plus .eps files)]
[J [L math/2001c.ps.gz 2001c.ps.gz] (postscript, 600dpi)]
[J [L math/2001c-ps.zip 2001c-ps.zip] (postscript, 600dpi)]
]
[P I'll be presenting a (much cleaner!) version of these ideas in July
5, at a meeting called [L http://www.inf.puc-rio.br/nd/program_i.html
Natural Deduction Rio 2001]. Here is the abstract (3 pages and a
bit):]
[LIST1
[J [L math/2001nd-abs.dvi.gz 2001nd-abs.dvi.gz] (dvi)]
[J [L math/2001nd-abs-dvi.zip 2001nd-abs-dvi.zip] (dvi)]
[J [L math/2001nd-abs.ps.gz 2001nd-abs.ps.gz] (postscript, 600dpi)]
[J [L math/2001nd-abs-ps.zip 2001nd-abs-ps.zip] (postscript, 600dpi)]
]
[P Coming soon: a bibliography and many more translations between the
typical point notation and the more usual ones (MacLane, [LR
http://www.cwru.edu/artsci/math/wells/pub/ttt.html Barr and Wells],
Goldblatt, Lambek and Scott). Some months ago I translated most of
chapter 0 of Lambek and Scott's book into an older form of the TP
notation and TeXed the diagrams; the result is mostly unreadable but
I'm hoping to reuse some diagrams later, especially from the part on
monads. If you are me then you may want the links: [mathL
tp-dvi.tar.gz]/[mathL tp-dvi.zip], [mathL tp-ps600.ps.tar.gz]/[mathL
tp-ps600.ps.zip].]
[RULE]
[P [IT (This is the older informal abstract; I will soon cannibalize
the good parts of it into the other and delete the rest.)]]
[QUO
[P [Q
There is a class of proofs involving infinitesimals -- and this
class is large enough to be interesting, as it contains most
"straightforward calculations with infinitesimals" -- that can be
translated to standard proofs in terms of continuity and limits via
a surprisingly simple trick: reread these proofs in $Set^F$ (the
power of the standard universe by a filter, instead of using an
ultrafilter), with $F$ being a filter of (maybe punctured)
neighbourhoods of the "zero" point of a certain topological space;
then instead of choosing arbitrary infinitesimals where the
statements say "for all infinitesimals $epsilon_1$, $epsilon_2$,
...", take only the "natural" (or "universal") infinitesimals
induced by the filter $F$; then reread that in $Set$, which is
trivial because a filter-power by a filter of neighbourhoods can be
easily described in elementary terms.
]]
[P [Q
This works because these proofs are happening in a fragment of the
logic of $Set^F$ that "doesn't notice" the non-two-valuedness of
the logic of $Set^F$; and what is even more interesting is that we
can put these proofs in a form --- a sort of Curry-Howard
isomorphism for calculus with infinitesimals --- that depicts in a
nice way and in tree form the constructions and logical steps
involved, and that can be considered as the "skeletons" of the
proofs; these skeletons can be not only used to translate the proofs
to several more usual languages, but also to discover how to relax
hypotheses ("this function can be just $C^4$ instead of $C^infty$",
for example) and also lets us suppress most parameters of functions
(as they can be inferred from the tree) and discuss coherence
questions for Calculus and Differential Geometry (like "in this
situation all natural ways to obtain $dw/dx$ are equivalent"); if
this system can be made to work in full strength then we should hope
to be able someday to devise an algorithm that would understand the
notation that physicists and applied mathematicians use, and to
convert it to skeleton form or to put back the omitted variables.
]]
[P [Q
Then comes the categorical side of these ideas.
]]
[P [Q
What are the precise syntax, the logical properties and the
interesting semantics of the system where these proofs with
infinitesimals lie? I don't have any good answer for these questions
right now, but it seemed that the natural way to go was to pick some
interesting examples and try to interpret them on a topos; I started
to create a sort of notation of typical points for categories --
mainly to let me get more intuition about how things work on a topos
-- and it turned out that many categorical concepts could be
expressed very elegantly in this notation, as the language is built
from the start to make easy to express things like "then there is
exactly one natural arrow from x to y"; also, statements in that
language lead to diagrams quite easily, and I have a strong
impression (based on tests with friends) that this language is very
good for dydactical purposes; an algorithm to translate from this
language to the usual ones and back would then be useful not only to
formalize skeletons of proofs with infinitesimals via a categorical
setting, but also to discuss skeletons of categorical proofs.
]]
]
[RULE]
[P (Sorry for any incorrections, I will fix them as soon as I can...)]
[P]
[J The next block contains links to older texts in portuguese.]
[RULE]
[P (Aviso: [Q eu gerei os ".ps"s em 600 dpi e só usei gzip e tar pra
comprimir e empacotar, se alguém precisar de outra resolução ou de
pacotes feitos de outra maneira, mande um mail.])]
[P Minha [MYLBYTES math/tese-mestr.tgz tese de mestrado] (apresentada
e defendida em abril de 99) [Q é sobre formalizar
"demonstrações-rabisco" envolvendo infinitesimais; em termos mais
conhecidos, ela trata de lambda-cálculo, categorias, dedução natural,
intuicionismo, isomorfismo de Curry-Howard... enfim, tudo o que é
necessário para levar um matemático a entender análise não-standard
através de sistemas de tipos, e a ver o que está por trás de uma certa
tradução entre uma versão de análise não-standard que usa filtros no
lugar de ultrafiltros e análise convencional. Como eu não consegui
completar a tempo os últimos capítulos (ambiciosíssimos - eu ainda
estou pesquisando parte do material que eu imaginava que iria pôr
neles), que são sobre topoi, sobre "onde nós gostaríamos de chegar" e
sobre análise não-standard, eles tiveram que virar umas espécies de
apêndices com anotações informais, mas mesmo assim a tese foi muito
bem aceita. Dê uma olhada pra entender por quê!]]
[P [MYLBYTES math/slides-mestr.tgz [Q As transparências que eu usei na
defesa da tese de mestrado.]]]
[P [MYLBYTES math/00feb24.dvi [Q As transparências que eu usei na
minha apresentação no Encontro de Lógica da UFF, em 24 de fevereiro de
2000, sobre o mesmo assunto, mas com ênfase na tradução de contas
semi-standard (i.e., "não-standard com filtros") para standard.]]]
[P [MYLBYTES math/99sep25.dvi [Q Notação mais curta para as regras
de lógica linear, abreviando os contextos muito mais do que o
normal.]] [Q (Usei os símbolos do Troelstra pros conectivos)]]
[RULE]
[HLIST1 [Q A few links:]
[LR http://xxx.lanl.gov/]
[LR http://hypatia.dcs.qmw.ac.uk/]
[LR http://citeseer.nj.nec.com/]
[LR http://theory.stanford.edu/~selinger/people.html]
[LR http://saturn.umh.ac.be/~maesa/nicolas.htm [Q Le petit Nicolas en thèse]]
]
]]]
[#
# [P I've been writing some notes in English about all that I've been
# studying on the \"Typical Point Notation\" -- a system that started as
# a sort of Curry-Howard isomorphism for differential calculus, and that
# gave as by-products: 1) a fragment of non-standard analysis where
# filters suffice (instead of requiring ultrafilters) and where
# translation to standard analysis is immediate, and 2) a notation for
# categories in which coherence conditions become very easy to state and
# many important concepts can be expressed very elegantly.]
#
# [P I have split my notes in two parts: one part is about the
# \"Calculus\" side (which includes non-standard analysis with filters)
# and the other is about the \"Categories\" side. You can get them (both
# parts) by downloading any one of the four files below:]
#
# [LIST2
# [MATHL tp-dvi.tar.gz (~ 69720 bytes)]
# [MATHL tp-dvi.zip (~ 128041 bytes)]
# [MATHL tp-ps600.ps.tar.gz (~ 163027 bytes)]
# [MATHL tp-ps600.ps.zip (~ 162774 bytes)]
# ]
#
# [P They correspond to the version of [FG purple November 6, 2000]].
#
# [P Be aware that this material is not yet ready to be announced at any
# serious place: there are some sections that have been fully written
# and that should be very clear (I hope) but there are others that at
# this moment are just horrible drafts. Please preview on your screen
# before printing.]
]