[INCLUDE TH/speedbar.blogme] [SETFAVICON dednat4/dednat4-icon.png] [# lua: print "Hello" ] [lua: LR = R ] [# (defun c () (interactive) (find-blogme3-sh0-if "math-b")) ;; http://angg.twu.net/math-b.html ;; file:///home/edrx/TH/L/math-b.html #] [lua: load_TARGETS() loada2html() ] [# lua: -- (find-blogme3file "elisp.lua") -- (find-blogme3file "anggdefs.lua") -- print(defs_as_lua()) -- print(_E4s_as_lua()) PP(_Es) PP(TGT('(find-angg "foo")')) PP(TGT('(find-TH "foo")')) PP(_G["-->"]('(find-TH "foo")')) ] [# (find-sh "lua50 ~/blogme/blogme.lua -o /tmp/math-b.blogme -i math-b.blogme") (find-efile "paren.el") (defun c () (interactive) (find-sh0-if "" " cd ~/TH/L/; cp ~/TH/math-b.blogme ~/TH/L/TH/math-b.blogme; lua51 ~/blogme3/blogme3.lua -o math-b.html -i TH/math-b.blogme ")) #] [# Eduardo Ochs - Academic Research - Categories, NSA, the "Typical Point Notation", and a language for skeletons of proofs #] [lua: def [[ __ 2 str,text _target[str] and HREF(_target[str], nilify(text) or str) or BG("red", str) ]] def [[ _ 1 body __(gsub(body, " ", "."), body) ]] ] [# # «.unilog-2010» (to "unilog-2010") # «.filter-infinitesimals» (to "filter-infinitesimals") # «.sheaves-for-ncs» (to "sheaves-for-ncs") # «.seminars-2007» (to "seminars-2007") # «.general-links» (to "general-links") # «.PhD» (to "PhD") # «.FMCS-2002» (to "FMCS-2002") # «.CMS-2002» (to "CMS-2002") # «.Natural-Deduction-Rio-2001» (to "Natural-Deduction-Rio-2001") # «.2001-UNICAMP» (to "2001-UNICAMP") # «.MsC» (to "MsC") # «.2000-UFF» (to "2000-UFF") # «.dednat4» (to "dednat4") #] [lua: -- (eev "firefox ~/TH/L/math.html &" nil) -- (find-es "page" "math.th-files") ] [# ------------------------------------------------------------------ #] [htmlize [J Eduardo Ochs - Academic Research - Categorical Semantics, Downcasing Types, Skeletons of Proofs, and a bit of Non-Standard Analysis] [P I'm currently living in a strange limbo between the academic world and the real world.] [_TARGETS Abadi => http://www.soe.ucsc.edu/~abadi/allpapers.html Abramsky => http://web.comlab.ox.ac.uk/oucl/work/samson.abramsky/pubsthematic.html Aczel => http://www.cs.man.ac.uk/~petera/papers.html Adamek => http://www.iti.cs.tu-bs.de/TI-INFO/adamek/adamek.html Altenkirch => http://www.cs.nott.ac.uk/~txa/ Aspinall => http://homepages.inf.ed.ac.uk/da/ Atanassow => http://homepages.cwi.nl/~atanasso/ Avigad => http://www.andrew.cmu.edu/user/avigad/papers.html Awodey => http://www.andrew.cmu.edu/user/awodey/ Baez => http://math.ucr.edu/home/baez/ Barendregt => http://www.cs.ru.nl/~henk/ Barr => http://www.math.mcgill.ca/barr/ Bauer => http://math.andrej.com/category/papers/ Beeson => http://michaelbeeson.com/research/papers/pubs.html Bell => http://publish.uwo.ca/~jbell/ Berardi => http://www.di.unito.it/~stefano/ Berg => http://www.mathematik.tu-darmstadt.de/~berg/ Birkedal => http://www.itu.dk/people/birkedal/ Blass => http://www.math.lsa.umich.edu/~ablass/ Blute => http://aix1.uottawa.ca/~rblute/ Brown => http://www.bangor.ac.uk/~mas010/publicfull.htm Bunge => http://www.math.mcgill.ca/~bunge/ Butz => http://www.itu.dk/~butz/ Caccamo => http://www.brics.dk/~mcaccamo/ Cockett => http://pages.cpsc.ucalgary.ca/~robin/ Coquand => http://www.cs.chalmers.se/~coquand/ Crosilla => http://www.maths.leeds.ac.uk/~pmtmlcr/ Dawson => http://cs.stmarys.ca/~dawson/papers.html DePaiva => http://www2.parc.com/isl/members/paiva/ <- (no) DePaiva => http://www.cs.bham.ac.uk/~vdp/ Diaconescu => http://www.imar.ro/~diacon/ Dosen => http://www.mi.sanu.ac.yu/~kosta/ Dybjer => http://www.cs.chalmers.se/~peterd/ Egger => http://www.mscs.dal.ca/~jegger/ Ehrhard => http://iml.univ-mrs.fr/~ehrhard/pub.html Escardo => http://www.cs.bham.ac.uk/~mhe/ Fiore => http://www.cl.cam.ac.uk/~mpf23/ Funk => http://www.math.uregina.ca/~funk/ Gaucher => http://www.pps.jussieu.fr/~gaucher/ Geuvers => http://www.cs.kun.nl/~herman/pubs.html Girard => http://iml.univ-mrs.fr/~girard/ Grandis => http://www.dima.unige.it/~grandis/rec.public_grandis.html Gurevich => http://research.microsoft.com/~gurevich/annotated.html Hasegawa => http://www.kurims.kyoto-u.ac.jp/~hassei/papers/index.html Hermida => http://maggie.cs.queensu.ca/chermida/ Hofmann => http://www.tcs.informatik.uni-muenchen.de/~mhofmann/papers.html Hofstra => http://www.mathstat.uottawa.ca/~phofstra/preprints.htm Honsell => http://users.dimi.uniud.it/~furio.honsell/Papers/list-papers.html Hyland => http://www.dpmms.cam.ac.uk/~martin/ Jacobs => http://www.cs.ru.nl/~bart/PAPERS/index.html Jardine => http://www.math.uwo.ca/~jardine/papers/ Jibladze => http://www.rmi.acnet.ge/~jib/ Joyal => http://www.professeurs.uqam.ca/pages/joyal.andre.htm Kock => http://home.imf.au.dk/kock/ Koslowski => http://www.iti.cs.tu-bs.de/TI-INFO/koslowj/RESEARCH/ Lack => http://www.maths.usyd.edu.au/u/stevel/ Lafont => http://iml.univ-mrs.fr/~lafont/ Lamarche => http://www.loria.fr/~lamarche/ Lambek => http://en.wikipedia.org/wiki/Joachim_Lambek Laurent => http://www.pps.jussieu.fr/~laurent/ Lawvere => http://www.acsu.buffalo.edu/~wlawvere/ Leinster => http://www.maths.gla.ac.uk/~tl/ Levy => http://www.cs.bham.ac.uk/~pbl/ Longo => http://www.di.ens.fr/users/longo/ Luo => http://www.cs.rhul.ac.uk/~zhaohui/ MPJones => http://web.cecs.pdx.edu/~mpj/pubs.html Maietti => http://www.math.unipd.it/~maietti/pubb.html Mairson => http://www.cs.brandeis.edu/~mairson/ Makkai => http://www.math.mcgill.ca/makkai/ Maltsiniotis => http://www.institut.math.jussieu.fr/~maltsin/ Marcos => http://www.dimap.ufrn.br/~jmarcos/ McLarty => http://www.colinmclarty.com/ Milner => http://www.cl.cam.ac.uk/~rm135/ Mislove => http://www.entcs.org/mislove.html Moerdijk => http://www.math.uu.nl/people/moerdijk/ Moggi => http://www.disi.unige.it/person/MoggiE/publications.html Negri => http://www.helsinki.fi/~negri/ Nelson => http://www.math.princeton.edu/~nelson/papers.html Niefield => http://www.math.union.edu/~niefiels/ Palmgren => http://www.math.uu.se/~palmgren/ Pare => http://www.mscs.dal.ca/~pare/publications.html Pastro => http://www.maths.mq.edu.au/~craig/ Pavlovic => http://www.kestrel.edu/home/people/pavlovic/ Petric => http://www.mi.sanu.ac.yu/~zpetric/ Phoa => http://www.margaretmorgan.com/wesley/ Pierce => http://www.cis.upenn.edu/~bcpierce/ Pitts => http://www.cl.cam.ac.uk/~amp12/ Plotkin => http://homepages.inf.ed.ac.uk/gdp/publications/ Porter => http://www.bangor.ac.uk/~mas013/ Pratt => http://boole.stanford.edu/pratt.html Pronk => http://www.mscs.dal.ca/Faculty/pronk.htm Queiroz => http://www.cin.ufpe.br/~ruy/ Regnier => http://iml.univ-mrs.fr/~regnier/ Reyes => http://po-start.com/reyes/ Reynolds => http://www.cs.cmu.edu/~jcr/ Rosebrugh => http://www.mta.ca/~rrosebru/ Rosolini => http://www.disi.unige.it/person/RosoliniG/biblio.html Sambin => http://www.math.unipd.it/~sambin/ Scedrov => http://www.cis.upenn.edu/~scedrov/ Schalk => http://www.cs.man.ac.uk/~schalk/ Schuster => http://www.mathematik.uni-muenchen.de/~pschust/ Scott => http://www.site.uottawa.ca/~phil/papers/ ScottD => http://www-2.cs.cmu.edu/~scott/ Seely => http://www.math.mcgill.ca/rags/ Seldin => http://www.cs.uleth.ca/~seldin/publications.shtml Selinger => http://www.mscs.dal.ca/~selinger/ Simmons => http://www.cs.man.ac.uk/~hsimmons/ Simpson => http://homepages.inf.ed.ac.uk/als/ Spitters => http://www.cs.ru.nl/~spitters/articles.html Street => http://www.maths.mq.edu.au/~street/ Streicher => http://www.mathematik.tu-darmstadt.de/~streicher/ Takeuti => http://www.sato.kuis.kyoto-u.ac.jp/~takeuti/index-e.html Taylor => http://www.monad.me.uk/ Tholen => http://www.math.yorku.ca/~tholen/research.htm VanOosten => http://www.math.uu.nl/people/jvoosten/ Vickers => http://www.cs.bham.ac.uk/~sjv/ VonPlato => http://www.helsinki.fi/~vonplato/ Wadler => http://homepages.inf.ed.ac.uk/wadler/ Weirich => http://www.seas.upenn.edu/~sweirich/publications.html Wells => http://www.case.edu/artsci/math/wells/home.html Wiedijk => http://www.cs.ru.nl/~freek/index.html Winskel => http://www.cl.cam.ac.uk/~gw104/ Wood => http://www.mscs.dal.ca/Faculty/rjwood.html Wraith => http://www.wra1th.plus.com/gcw/rants/math/index.html Yanofsky => http://www.sci.brooklyn.cuny.edu/~noson/ ] [_TARGETS Barendregt-lct => ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z Barendregt-lctCS => http://citeseer.nj.nec.com/barendregt92lambda.html Beck-thesis => http://www.tac.mta.ca/tac/reprints/articles/2/tr2abs.html Berardi-piemccc => http://www.di.unito.it/~stefano/Barbanera-ProofIrrelevanceOutOf.ps Blute-ctll => http://aix1.uottawa.ca/~rblute/catsurv.ps Butz-filter => http://www.brics.dk/~butz/public_ftp/new_stuff/filter.ps.gz Charity => http://pll.cpsc.ucalgary.ca/charity1/www/home.html Charity-manual => ftp://ftp.cpsc.ucalgary.ca/pub/projects/charity/literature/manuals/manual.ps.gz Charity-scd2 => ftp://ftp.cpsc.ucalgary.ca/pub/projects/charity/literature/papers_and_reports/dataII.ps.gz Ehrhard-difflamb => ftp://iml.univ-mrs.fr/pub/ehrhard/difflamb.ps.gz Eliasson => http://www.math.uu.se/~jonase/ Eliasson-thesis => http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.6032 Eliasson-thesis => http://www.math.uu.se/research/pub/FEliasson1.pdf Farmer-stt => http://www.cas.mcmaster.ca/sqrl/papers/sqrl18.ps.Z Geuvers-sncc => http://www.cs.kun.nl/~herman/BRABasSNCC.ps.gz Geuvers-thesis => http://www.cs.ru.nl/~herman/PUBS/Proefschrift.ps.gz Hofmann-lccc => http://www.dcs.ed.ac.uk/home/mxh/csl94.ps.gz Hofmann-ssdtCS => http://citeseer.nj.nec.com/hofmann97syntax.html Hofmann-thesis => http://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/index.html Hofmann-ttlccc => http://www.dcs.ed.ac.uk/home/mxh/csl94.ps.gz Jacobs-cltt => http://www.cs.ru.nl/~bart/PAPERS/index.html Kock-afef => http://www.tac.mta.ca/tac/volumes/1999/n10/n10.ps Kock-axdiff => http://www.mscand.dk/issue.php?year=1977&volume=40 Kock-fefcde => ftp://ftp.imf.au.dk/pub/kock/ODE5.ps Kock-sdg => http://home.imf.au.dk/kock/sdg99.pdf Kock-ttfact => http://www.dimap.ufrn.br/pipermail/logica-l/2006-August/000438.html Lawvere-sdgout => http://www.acsu.buffalo.edu/~wlawvere/SDG_Outline.pdf Lawvere-tlmotion => http://www.acsu.buffalo.edu/~wlawvere/ToposMotion.pdf Leinster-complex => http://www.arxiv.org/abs/math.CT/0212377 Leinster-sheaves => http://www.maths.gla.ac.uk/~tl/sheaves.pdf Lietz-msc => http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/lietz.ps.gz Luo-thesis => http://www.dur.ac.uk/~dcs0zl/THESIS90.dvi.gz MPJones-fcpoly => http://www.cse.ogi.edu/~mpj/pubs/popl97-fcp.dvi.gz MPJones-hmtypes => http://www.cse.ogi.edu/~mpj/pubs/haskwork95.dvi.gz Mairson-ptp => http://www.cs.brandeis.edu/~mairson/Papers/para.ps.gz NSA-links => http://members.tripod.com/PhilipApps/nonstandard.html Negri-ndnotes => http://www.helsinki.fi/~negri/prana.pdf Nordstrom-mltt => http://citeseer.nj.nec.com/1666.html Palmgren-bhk => http://www.math.uu.se/~palmgren/cbhk-mscs.ps Phoa-fttetms => http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ECS-LFCS-92-208.ps.gz Pitts-catlogic => ftp://ftp.cl.cam.ac.uk/papers/amp12/catl.ps.gz Pitts-catlogicCS => http://citeseer.nj.nec.com/pitts01categorical.html Plato-ndnotes => http://www.helsinki.fi/~negri/dresum.pdf Schalk-games => http://www.cs.man.ac.uk/~schalk/notes/intgam.ps.gz Schalk-modll => http://www.cs.man.ac.uk/~schalk/notes/llmodel.ps.gz Schalk-monads => http://www.cs.man.ac.uk/~schalk/notes/monads.ps.gz Scott-aspects => http://linear.di.fc.ul.pt/handbook.ps Seely-diff => http://www.math.mcgill.ca/rags/difftl/difftl.ps.gz Seely-lccc => http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf Seely-polcat => http://www.math.mcgill.ca/rags/games/games.ps.gz Simmons-sheaves => http://www.cs.man.ac.uk/~hsimmons/DOCUMENTS/PAPERSandNOTES/Omegasets.ps.gz Streicher-fibs => http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/FibLec.pdf.gz TAC-reprints => http://www.tac.mta.ca/tac/reprints/index.html TTT => http://www.cwru.edu/artsci/math/wells/pub/ttt.html Takeuti-asp => http://www.sato.kuis.kyoto-u.ac.jp/~takeuti/abs-e.html#param Takeuti-cube => http://www.sato.kuis.kyoto-u.ac.jp/~takeuti/abs-e.html#cube Taylor-pandt => http://www.monad.me.uk/stable/Proofs+Types.html Wadler-greynolds => http://www.research.avayalabs.com/user/wadler/topics/parametricity.html Wadler-pap => http://www.research.avayalabs.com/user/wadler/topics/history.html Wadler-tffree => http://www.research.avayalabs.com/user/wadler/topics/parametricity.html Yanofsky-diag => http://arxiv.org/abs/math.LO/0305282 UFF => http://www.uff.br/grupodelogica/ Cahiers => http://www.numdam.org/numdam-bin/feuilleter?j=CTGDC unilog2010-start => http://www.uni-log.org/start3.html unilog2010-catl => http://www.uni-log.org/ss3-CAT.html unilog2010-sched => http://dl.dropbox.com/u/1202739/fullschedule.html unilog2010-handbook => http://www.uni-log.org/handbook-unilog2010.pdf unilog2010-abs1 => http://angg.twu.net/LATEX/2009unilog-abs1.pdf (find-angg "LATEX/2009unilog-abs1.tex") unilog2010-slides => http://angg.twu.net/LATEX/2010unilog-current.pdf unilog2010-slides.dvi => http://angg.twu.net/LATEX/2010unilog-current.dvi (find-angg "LATEX/2010unilog-current.tex") unilog2010-1.dvi => http://angg.twu.net/LATEX/2010unilog-2010jun21.dvi unilog2010-1.pdf => http://angg.twu.net/LATEX/2010unilog-2010jun21.pdf ashes => http://en.wikipedia.org/wiki/Eyjafjallaj%C3%B6kull#2010_eruptions ] [# http://www.mscs.dal.ca/~selinger/ct2006/ http://www.mscs.dal.ca/~selinger/ct2006/index.html #] [WITHINDEX [_TARGETS .emacs.papers -> (find-angg ".emacs.papers") local-copies -> (find-eevarticlesection "local-copies") ] [NARROW [SMALL [P Note: I don't use this page very much myself, and so I don't usually notice when the links to papers stop working... 8-\ I always access (my [__ local-copies local copies] of) online papers with the functions defined in my [_ .emacs.papers] file.]]] [br] [sec «unilog-2010» (to ".unilog-2010") H2 Downcasing Types (at UniLog'2010)] [P I gave a talk about Downcasing Types at the [__ unilog2010-catl special session on Categorical Logic] of [__ unilog2010-start UNILOG'2010], on 2010apr22. Very few people attended - because the [__ ashes volcanic ashes] many people could not fly to Portugal, and from [__ unilog2010-handbook all these programmed talks] only [__ unilog2010-sched these] ended up happening. The abstract was:] [NARROW [P When we represent a category C in a type system it becomes a 7-uple, whose first four components - class of objects, Hom, id, composition - are "structure"; the other three components are "properties", and only these last three involve equalities of morphisms.] [P We can define a projection that keeps the "structure" and drops the "properties" part; it takes a category and returns a "proto-category", and it also acts on functors, isos, adjunctions, proofs, etc, producing proto-functors, proto-proofs, and so on.] [P We say that this projection goes from the "real world" to the "syntactical world"; and that it takes a "real proof", P, of some categorical fact, and returns its "syntactical skeleton", P-. This P- is especially amenable to diagrammatic representations, because it has only the constructions from the original P --- the diagram chasings have been dropped.] [P We will show how to "lift" the proto-proofs of the Yoneda Lemma and of some facts about monads and about hyperdoctrines from the syntactical world to the real world. Also, we will show how each arrow in our diagrams is a term in a precise diagrammatic language, and how these diagrams can be read out as definitions. The "downcased" diagrams for hyperdoctrines, in particular, look as diagrams about Set (the archetypical hyperdoctrine), yet they state the definition of an arbitrary hyperdoctrine, plus (proto-)theorems.] ] [P (A longer version of the abstract: [__ unilog2010-abs1 pdf].)] [P I am still adding things to the set of slides that I prepared for that presentation.] [P First official release of the slides (2010jun21, 100 pages): [# [__ unilog2010-1.dvi dvi],] [__ unilog2010-1.pdf pdf].] [P Latest version of the slides: [__ unilog2010-slides.dvi dvi], [__ unilog2010-slides pdf].] [HLIST3 [J Some related posts at cat-dist:] [R http://article.gmane.org/gmane.science.mathematics.categories/5906 2010jun01: Joyal on "=."] [R http://article.gmane.org/gmane.science.mathematics.categories/5909 2010jun01: Lumsdaine on p:E->C in DTT] ] [P (I will try to submit a part of that to [R http://article.gmane.org/gmane.science.mathematics.categories/5991 this CPF]...)] [# the full abstract is [__ unilog2010-abs1 here], and a shorter version of it appeared at the [__ unilog2010-handbook congress handbook]. a [__ unilog2010-slides set of slides], and in that sense the congress was perfect (8-\). I am still adding things to the slides, and now they're almost great [Q &] self-contained, and I am going to reuse them soon... #] [RULE ----------------------------------------] [sec «filter-infinitesimals» (to ".filter-infinitesimals") H2 Natural infinitesimals in filter-powers (2008)] [P "Purely calculational proofs" involving infinitesimals can be "lifted" from the non-standard universe (an ultrapower) to the "semi-standard universe" (a filter-power) through the quotient Set^I/F->Set^I/U; and after they've been moved to the right filter-power they can be translated very easily to standard proofs. I don't know how much of this idea is new, but I liked it so much that I wrote it down in some detail and asked for feedback in the [R http://www.mta.ca/~cat-dist/ Categories mailing list].] [P [IMG IMAGES/filterp-maps.png]] [P Preliminary version (2008jul13), including the message to the mailing list: [HREF LATEX/2008filterp.pdf pdf], [HREF LATEX/2008filterp.dvi dvi], [HREF LATEX/2008filterp-texsrc.tar.gz source].] [P A (long-ish) abstract for a presentation intended for undergrads: [HREF LATEX/2008filterp.pdf pdf], [HREF LATEX/2008filterp.tex.html source]. [BR] I presented that at the students' colloquium at [R http://www.mat.puc-rio.br/ PUC-Rio], on 2008aug20, 17:00-18:00hs. [BR] I will talk about it again at [R http://seminarios.impa.br/cgi-bin/SEMINAR_browse.cgi#hoje IMPA], on 2008sep17, 15:30 ([R http://seminarios.impa.br/pdfs/sem4284.pdf pdf]).] [# http://seminarios.impa.br/cgi-bin/SEMINAR_browse.cgi?mes_corrente=9&ano_corrente=2008] [P (News: Reinhard Boerger pointed me to later (post-1958) work by Laugwitz and Schmieden, and I got a copy of the "[R http://www.mathematik.uni-muenchen.de/~antipode/abstracts.html Reuniting the Antipodes]" [R http://www.amazon.com/Reuniting-Antipodes-Constructive-Nonstandard-Continuum/dp/1402001525/ book]; my current impression is that my result is not as trivial as I was afraid it could be. Homework-in-progress: several cleanups on the preliminary version above, and I'm trying - harder - to understand Moerdijk and Palmgren's sheaf models.)] [RULE ----------------------------------------] [sec «sheaves-for-ncs» (to ".sheaves-for-ncs") H2 Sheaves for Non-Categorists (2008)] [P This is another presentation that - [IT maybe after some clean-ups] - will be accessible to undergrads... The current version of the slides (far from ready, with lots of garbage and gaps!) is here: [HREF LATEX/2008graphs.pdf pdf], [HREF LATEX/2008graphs.tex.html source]. The presentation will be at the [R http://www.uff.br/grupodelogica/ Logic Seminar at UFF], on 2008sep04, 16:00-17:00hs.] [# Another one: "Lógica sobre grafos", PURO, terça, 30/set/2008. #] [P Here's an htmlized version of the abstract:] [NARROW [P Take a set of "worlds", W, and a directed acyclical graph on W, given by a relation R ⊂ W × W. Let's call the functions W → {0,1} "modal truth-values", and the R-non-decreasing functions W → {0,1} "intuitionistic truth-values". If we see W as a topological space with the order topology induced by R, the intuitionistic truth-values correspond to open sets.] [P The pair (O(W), ⊆) is a Heyting algebra --- meaning that we can interpret intuitionistic propositional logic on it --- and it is a (bigger) DAG, and so we can repeat the above process with it, to generate a (bigger) topological space (O(W), O(O(W))), which is the natural setting for talking about "covers", "saturated covers", and "unions of covers".] [P This presentation will be focused on understanding all these ideas (and more!), mainly in the case where W has three worlds forming a "V", and R has two arrows pointing downwards. The operation of "taking the union of a cover" turns out to be a particular case of a "Lawvere-Tierney modality"; the double negation is another LT-modality.] ] [# (find-LATEX "2008sheaves-abs1.tex") #] [RULE ----------------------------------------] [sec «seminars-2007» (to ".seminars-2007") H2 Seminar on downcasing types (nov/2007)] [# (find-angg ".emacs" "find-LTX") #] [P If you are going to attend my seminars at [R http://www.mat.puc-rio.br/disciplinas/MAT2210/ PUC] at November/2007 and want to take a peek at my notes (they are very incomplete at the moment, it goes without saying), they have just been split into several parts:] [LIST2 [R [--> (find-LTX "2007dnc-sets") ] 1. Downcasing Sets] [R [--> (find-LTX "2008typesystems") ] 2. Downcasing Type Systems] [R [--> (find-LTX "2008bcc") ] 3. Downcasing the Beck-Chevalley Condition] [R [--> (find-LTX "2008topos-str") ] 4. Downcasing the Structure of a Topos] [R [--> (find-LTX "2008comprcat") ] 5. Downcasing Comprehension Categories] [R [--> (find-LTX "2008hyp") ] 6. Notes about Hyperdoctrines] [R [--> (find-LTX "2008sheaves") ] 7. Notes about Sheaves] [J [R [--> (find-LTX "2008sdg") ] 8. Downcasing ring objects of line type] (as in [__ Kock-axdiff Kock77]; for SDG)] [R [--> (find-LTX "2008monads") ] 9. Notes about monads (and *-autonomous and differential categories)] [R [--> (find-LTX "2008notations") ] 10. Notes about the notation in several papers] [R [--> (find-LTX "2008kocknsext") ] 11. Notes about the notation in Kock & Mikkelsen's paper on ultrapowers] ] [# (find-LTX "2008filterp") (find-LTX "2008natded") (find-LTX "2008projeto") (find-LTX "2008projeto-puro") #] [# P I'm planning to finish the part on downcasing BCC soon, and to typeset it using [_ dednat4], and to include its slides in the dednat4 package as examples. I'm also planning to complete a few pendencies on dednat4 soon, and to release it "officially". The notes of downcasing BCC should be readable (when completed, of course) by anyone with some background in Category Theory independently of the other parts.] [P Bad news (?), dec/2007: the seminars will not happen - instead, I got a job at São Paulo, on computer stuff. I'll keep working on maths and on my personal free software projects in my spare time. If you find any of these things interesting, and want to discuss or to encourage me to finish something, get in touch!] [P 2008: I am giving a series of seminars at [_ UFF] to try to organize my ideas about downcasing types... here are links to some of TeXed slides (they are very preliminary, too. Should I be embarassed to provide links to these things? Well...):] [# (find-blogme3 "angglisp.lua" "find-LATEX") # (defun find-LATEX (stem) (find-pspage (format "~/LATEX/%s.pdf" stem))) # (find-sh "cd ~/LATEX/; ls *.pdf") # (find-angg "LATEX/") # not yet: (find-LATEX "2008filterp") # (find-LATEX "2008hyp") # (find-LATEX "2008sdg") # (find-LATEX "2008sheaves") # (find-LATEX "2008topos-str") #] [RULE ----------------------------------------] [sec «general-links» (to ".general-links") H2 General links] [LIST1 [R http://ncatlab.org/nlab/show/HomePage] [R http://liinwww.ira.uka.de/bibliography/ The Collection of Computer Science Bibliographies] [J [R http://citeseer.ist.psu.edu/ CiteSeer] (broken?)] [R http://citeseerx.ist.psu.edu/ CiteSeerX] [R http://dblp.uni-trier.de/ DBLP] [LR http://www.tac.mta.ca/tac/] [LR http://www.mta.ca/~cat-dist/] [R http://news.gmane.org/gmane.science.mathematics.categories] [__ Cahiers Cahiers de Topologie et Géométrie Différentielle Catégoriques] [R http://arxiv.org/list/math.CT/recent] [R http://arxiv.org/help/] [LR http://www.cs.uu.nl/people/franka/ref Frank Atanassow's list of online Programming Language Theory texts] [R http://arxiv.org/] [J [R http://www.aslonline.org/membership_outreach_indiv.html ASL] journals: [R http://www.jstor.org/action/showPublication?journalCode=jsymboliclogic JSL] and [R http://www.jstor.org/action/showPublication?journalCode=bullsymblogi BSL]] [R http://www.cs.nyu.edu/pipermail/fom/] [# http://www.cs.nyu.edu/pipermail/fom/2008-October/013131.html Pratt on intuitionism #] [R http://www.informatik.uni-trier.de/~ley/db/journals/] [LR http://guilde.jeunes-chercheurs.org/Alire/detente/petit-nicolas.htm Le petit Nicolas en thèse] [J The [R http://www.dimap.ufrn.br/pipermail/logica-l/ Brazilian mailing list on logic], and [R galdino.html some notes] on one of its most vocal members.] [R http://math.ucr.edu/home/baez/TWF.html] [R http://www.ams.org/mathweb/mi-books.html] [R http://onlinebooks.library.upenn.edu/webbin/book/callover?key=Q] ] [# http://hpsearch.uni-trier.de/] [# http://hypatia.dcs.qmw.ac.uk/] [# http://xxx.lanl.gov/] [HLIST1 [J Some articles and books that I'm reading:] [J [_ Blute], [_ Cockett] [Q &] [_ Seely]: [__ Seely-diff Differential Categories] (2005)] [J Notes by [__ Schalk Andrea Schalk]: [__ Schalk-monads monads], [__ Schalk-modll cat. models for LL], [__ Schalk-games games] ] [J Notes by [__ Simmons Harold Simmons], esp. this one about [__ Simmons-sheaves sheaves on omega-sets]] [J [_ Fiore], [_ Leinster]: [__ Leinster-complex Objects of Categories as Complex Numbers] (2002)] [J [_ Leinster]: [__ Leinster-sheaves A proof that sheaves do not belong to algebraic geometry] (2007)] [J J. L. [_ Bell]: A Primer of Infinitesimal Analysis (1998)] [J Eisenbud [Q &] Harris: The Geometry of Schemes] [J [_ Cockett] [Q &] [_ Seely]: [__ Seely-polcat Polarized Category Theory, Modules, and Game Semantics] (2004)] [HLIST2 [__ MPJones M. P. Jones]: [J [__ MPJones-hmtypes From Hindley-Milner Types to First-Class Structures] (1995)], [J [__ MPJones-fcpoly First Class Polymorphism with Type Inference] (1997)] ] [J Robin [_ Milner]: A Theory of Type Polymorphism in Programming (1978)] [J John Allen: Anatomy of Lisp (1978)] [J Bart [_ Jacobs]: Categorical Logic and Type Theory] [HLIST3 [J Papers about [_ Charity]:] [J its [__ Charity-manual manual],] [J [__ Charity-scd2 Strong Categorical Datatypes II].] ] ] (The next sections are links to online texts.) [HLIST1 [J Category Theory (in general):] [J [_ Barr]/[_ Wells]: [__ TTT Toposes, Triples, and Theories] (1985).] [J Phil [_ Scott]: [__ Scott-aspects Some Aspects of Categories in Computer Science] (1998/2000; a chapter of the "Handbook of Algebra")] [J Andy [_ Pitts]: [__ Pitts-catlogic Categorical Logic] (2001) ([__ Pitts-catlogicCS CS entry]) ] [J Noson [_ Yanofsky]'s [__ Yanofsky-diag paper about diagonal arguments] (2003)] ] [HLIST1 [J Fibrations:] [J Thomas [_ Streicher]'s [__ Streicher-fibs notes on Fibered Categories à là Jean Bénabou] (1999)] [J Wesley [_ Phoa]: [__ Phoa-fttetms An Introduction to Fibrations, Topos Theory, the Effective Topos and Modest Sets]] ] [#  ] [HLIST1 [J Monads:] [J [__ Schalk-monads Notes] by [__ Schalk Andrea Schalk]] [J [_ Blute]/[_ Scott]: [__ Blute-ctll Category Theory for Linear Logicians]] [J [__ Beck-thesis Jon Beck's thesis] and [_ TTT], from [__ TAC-reprints TAC reprints]] ] [HLIST1 [J Sheaves:] [J Notes by [__ Simmons Harold Simmons] on [__ Simmons-sheaves sheaves and omega-sets]] [J [__ Bell J.L. Bell: Toposes and Local Set Theories]] ] [HLIST1 [J Type Theory (mainly the Calculus of Constructions):] [HLIST2 [__ Geuvers Herman Geuvers]'s... [J PhD thesis, [__ Geuvers-thesis "Logics and Type Systems"] (1993), and] [__ Geuvers-sncc "A Short and Flexible Proof of Strong Normalization for the Calculus of Constructions"] ] [J [_ Barendregt]: [__ Barendregt-lct Lambda Calculi with Types (1992)] ([__ Barendregt-lctCS CS entry])] [J [__ Luo Zhaohui Luo]'s PhD thesis: "[__ Luo-thesis An Extended Calculus of Constructions]" (1990).] [J W.M.Farmer: [__ Farmer-stt The Seven Virtues of Simple Type Theory] (2003)] [J [__ Seldin Jonathan Seldin]'s homepage] [J [__ Coquand Thierry Coquand]'s homepage] [J Barbanera/[_ Berardi]: [__ Berardi-piemccc Proof-Irrelevance out of Excluded Middle and Choice in the Calculus of Constructions]] [__ Maietti Milly Maietti's home page] [J [__ Hofmann Martin Hofmann]: [__ Hofmann-thesis Extensional concepts in intensional type theory] (PhD thesis, 1995), [__ Hofmann-ssdtCS Syntax and Semantics of Dependent Types] (1997) ] [HLIST2 [J LCCCs:] [J [__ Seely R.A.G. Seely]: [__ Seely-lccc LCCCs and type theory] (1984)] [J [__ Hofmann Martin Hofmann]: [__ Hofmann-ttlccc On the interpretation of TT in LCCCs] (1994)] [J [__ Palmgren Erik Palmgren]: [__ Palmgren-bhk A categorical version of the BHK interpretation] (2004)] ] [__ Nordstrom-mltt Nordström/Petersson/Smith: Martin-Löf's Type Theory] [J [__ MPJones Mark P. Jones]: [__ MPJones-fcpoly First Class Polymorphism with Type Inference] (1997) ] ] [HLIST1 [J Parametricity:] [HLIST2 [__ Wadler Phil Wadler]: [J [__ Wadler-tffree Theorems for Free!] (1989),] [J [__ Wadler-greynolds The Girard-Reynolds Isomorphism] (2001)] [J [__ Wadler-pap Proofs are Programs: 19th Century Logic and 21st Century Computing]] ] [HLIST2 [__ Reynolds John Reynolds]: [LR http://www-2.cs.cmu.edu/~jcr/ On Functors Expressible in the Polymorphic Typed Lambda Calculus] ] [HLIST2 [__ Takeuti Izumi Takeuti]: [J [__ Takeuti-asp An Axiomatic System of Parametricity] (1998)] [J [__ Takeuti-cube The Theory of Parametricity in Lambda Cube] (draft)] ] [HLIST2 [__ Mairson Harry Mairson]: [__ Mairson-ptp Outline of a Proof Theory of Parametricity] ] ] [HLIST1 [J Non-standard Analysis, SDG and friends:] [__ NSA-links A page with many links on Non-Standard Analysis] [HLIST2 [__ Lawvere William Lawvere]: [J [__ Lawvere-sdgout Outline of Synthetic Differential Geometry] (1998)] [J [__ Lawvere-tlmotion Toposes of Laws of Motion] (1997)] ] [J Jonas Eliasson's [__ Eliasson-thesis thesis]; he makes reference to some [__ Palmgren papers by Erik Palmgren] that are not on-line.] [J [__ Ehrhard Thomas Ehrhard]: [__ Ehrhard-difflamb The Differential Lambda-Calculus] (2001).] [HLIST2 [__ Kock Anders Kock]: [J [__ Kock-axdiff A simple axiomatics for differentiation] (1977)] [J [__ Kock-sdg Synthetic Differential Geometry] (1981/2006)] [J [__ Kock-ttfact Topos-theoretic factorization of non-standard extensions] (1974, witk Mikkelsen; SLNM 369)] [J [__ Kock-afef Aspects of Fractional Exponent Functors] (1999, with [__ Reyes G. Reyes])] [J [__ Kock-fefcde Fractional Exponent Functors and Categories of Differential Equations] (1998, with [__ Reyes G. Reyes])] ] [J [__ Butz Carsten Butz]: [__ Butz-filter The filter construction revisited]] ] [HLIST1 [J Natural Deduction:] [J [_ Girard]/[_ Lafont]/[_ Taylor]: [__ Taylor-pandt Proofs and Types]] [__ Plato-ndnotes Jan von Plato's lecture notes] [__ Negri-ndnotes Sara Negri's lecture notes] ] [NAME grothendieck] [# «Grothendieck» # (find-angg ".emacs.papers" "grothendieck") #] [HLIST1 Grothendieck: [J Biographical article in Notices of the AMS, parts [LR http://www.ams.org/notices/200409/fea-grothendieck-part1.pdf 1] and [LR http://www.ams.org/notices/200410/fea-grothendieck-part2.pdf 2] (2004)] [J McLarty: [LR http://www.math.jussieu.fr/~leila/grothendieckcircle/mclarty1.pdf The Rising Sea: Grothendieck on simplicity and generality] (2003)] [R http://kolmogorov.unex.es/~navarro/res/] [R http://mapage.noos.fr/recoltesetsemailles/TdM.htm] ] [HLIST1 [J Etc (unclassified):] [R http://alessio.guglielmi.name/res/cos/PN/index.html] [R http://www.phil.cmu.edu/projects/ast/] [R http://www.phil.cmu.edu/projects/ast/Papers/bnotes.pdf] [R http://www.mat.ufmg.br/~elaine/] [R http://www.fields.utoronto.ca/programs/scientific/06-07/homotopy/courses/] ] [P Links to the home pages of some category theorists (and a few type theorists): [_ Abadi], [_ Abramsky], [_ Aczel], [_ Adamek], [_ Altenkirch], [_ Aspinall], [_ Atanassow], [_ Avigad], [_ Awodey], [_ Baez], [_ Barendregt], [_ Barr], [_ Bauer], [_ Beeson], [_ Bell], [_ Berardi], [_ Berg], [_ Birkedal], [_ Blass], [_ Blute], [_ Brown], [_ Bunge], [_ Butz], [_ Caccamo], [_ Cockett], [_ Coquand], [_ Crosilla], [_ Dawson], [_ DePaiva], [_ Diaconescu], [_ Dosen], [_ Dybjer], [_ Egger], [_ Ehrhard], [_ Escardo], [_ Fiore], [_ Funk], [_ Gaucher], [_ Geuvers], [_ Girard], [_ Grandis], [_ Gurevich], [_ Hasegawa], [_ Hermida], [_ Hofmann], [_ Hofstra], [_ Honsell], [_ Hyland], [_ Jacobs], [_ Jardine], [_ Jibladze], [_ Joyal], [_ Kock], [_ Koslowski], [_ Lack], [_ Lamarche], [_ Lambek], [_ Laurent], [_ Lawvere], [_ Leinster], [_ Levy], [_ Longo], [_ Luo], [_ MPJones], [_ Maietti], [_ Mairson], [_ Makkai], [_ Marcos], [_ McLarty], [_ Maltsiniotis], [_ Milner], [_ Mislove]; [_ Moerdijk], [_ Moggi], [_ Nelson], [_ Negri], [_ Niefield], [_ Palmgren], [_ Pare], [_ Pastro], [_ Pavlovic], [_ Petric], [_ Phoa], [_ Pierce], [_ Pitts], [_ Plotkin], [_ Porter], [_ Pratt], [_ Pronk], [_ Queiroz], [_ Regnier], [_ Reynolds], [_ Rosebrugh], [_ Rosolini], [_ Sambin], [_ Scedrov], [_ Schalk], [_ Schuster], [_ Scott], [_ ScottD], [_ Seely], [_ Seldin], [_ Selinger], [_ Simmons], [_ Simpson], [_ Spitters], [_ Street], [_ Streicher], [_ Taylor], [_ Tholen], [_ VanOosten], [_ Vickers], [_ Wadler], [_ Weirich], [_ Wells], [_ Wiedijk], [_ Winskel], [_ Wood], [_ Wraith], [_ Yanofsky].] [RULE ---------------------------------------------------------------------] [sec «PhD» (to ".PhD") H1 PhD and post-PhD research] [P I did both my MsC and my PhD (and also my graduation, by the way) at [LR http://www.mat.puc-rio.br/ the Department of Mathematics at PUC-Rio]. The Dept of Mathematics is a fantastic place - tiny, incredibly friendly, well-equipped, lots of research going on -, but (rant mode on) PUC-Rio is a private university, and most of the students from other departments were ultra-competitive rich kids who had never stepped out of the marble towers they live in. I used to find it very hard - very painful, even - to interact with them, and even to stand their looks, like if they were always trying to tag me as either a "winner" or a "loser", as if there weren't any other ways to live. Eeek! But these days are long gone now (rant mode off).] [P I spent the first eight months of 2002 at [LR http://www.math.mcgill.ca/ McGill University] in Montreal, doing research for my PhD thesis there, working with [LR http://www.math.mcgill.ca/~rags/ Robert Seely]... I was in a [LR http://www.capes.gov.br/Bolsas/Exterior/Doutorando.htm "Sandwich PhD"] program (thanks [LR http://www.capes.gov.br/ CAPES]!), which is something that lets us do part of the research abroad and then come back and finish (and defend) the thesis at our university of origin.] [P I defended my PhD thesis (with a few holes) in August, 2003 and presented the final version - filling out [IT most] of the gaps - in February, 2004. Then I spent most of 2004 teaching part-time in an university at the outskirts of Rio (the more realworldish job that I've ever had!), and also finishing a very important Free Software project that I've been working on since 1999 ([L index.html GNU eev]).] [P [BF The thesis] is in Portuguese and [IT you don't want to see it] - you want to see the slides that I'm working on (it's 2005mar12 as I write this), in which the method for interpreting diagrams and "lifting" them from Set to an arbitrary category with the adequate structure in explained in a really nice way. But if you are really anxious you can [HREF contact.html get in touch with me].] [P News (October 2005): I'm giving a series of talks about my PhD thesis at UFF (see [R http://www.uff.br/grupodelogica/]). Expect slides soon and articles not so soon, but as soon as possible.] [NAME FMCS-2002] [# «FMCS-2002» (to ".FMCS-2002") #] [P [BF This is the abstract for a talk] that I gave at the [LR http://cs.colgate.edu/faculty/mulry/FMCS2002/Web/FMCS2002.html FMCS2002] in June 8, 2002.] [NARROW [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 I also gave [BF a shorter version of that talk] at the [R http://www.cms.math.ca/Events/summer02/ CMS Summer 2002 Meeting], in [LR http://www.cms.math.ca/Events/summer02/sched.html#CP June 17].] [P Slides for the longer talk (45 minutes, 26+3 pages): [HREF math/2002fmcs.pdf pdf], [HREF math/2002fmcs.ps.gz ps], [HREF math/2002fmcs.dvi.gz dvi], [HREF math/2002fmcs-texsrc.tar.gz source].] [NAME CMS-2002] [# «CMS-2002» (to ".CMS-2002") #] [P Slides for the shorter talk (one week later, 15 minutes, 16+2 pages: [HREF math/2002cms.pdf pdf], [HREF math/2002cms.ps.gz ps], [HREF math/2002cms.dvi.gz dvi], [HREF math/2002cms-texsrc.tar.gz source].] [P [BF Fact:] all the essential details (i.e., the "T-part", as in the abstract above) of a certain construction of a categorical model of the Calculus of Constructions - and also of categorical models of several fragments of CC - can be expressed in (a few!) categorical diagrams using the DNC language. I'm currently (February/March 2005) preparing talks and articles about that.] [P] [# [BR] #] [NAME Natural-Deduction-Rio-2001] [# «Natural-Deduction-Rio-2001» (to ".Natural-Deduction-Rio-2001") #] [P [BF An older talk about Natural Deduction for Categories.] After using something like the DNC notation for years just because "it looked right", but without any good formal justification for it, in February 2001 I had the key idea: [IT there were rules of both discharge and introduction for the "connectives" for functors and natural transformations.] A few months after that (in July 5 2001, to be precise) I gave a talk about it at a meeting called [LR http://www.inf.puc-rio.br/nd/program_i.html Natural Deduction Rio 2001].] [P Abstract (3 pages and a bit): [R math/2001nd-abs.pdf pdf], [R math/2001nd-abs.ps.gz ps], [R math/2001nd-abs.dvi.gz dvi], [R math/2001nd-texsrc.tar.gz source]. ] [P Slides (16 slides): [R 2001ndsl.pdf pdf], [R 2001ndsl.ps.gz ps], [R 2001ndsl-dvi.tar.gz dvi+eps's], [R 2001ndsl-texsrc.tar.gz source]. ] [NAME 2001-UNICAMP] [# «2001-UNICAMP» (to ".2001-UNICAMP") #] [P [BF Another talk, even older, about Natural Deduction for Categories.] After finding the key idea that I mentioned above I arranged to give a (very informal) talk at the [R http://www.cle.unicamp.br/ Centro de [Q Lógica] e Epistemologia at UNICAMP]. It happened in April 25, 2001, and for it I had to assemble my personal notes into something that could be used as slides. The title was ""Set^C is a topos" has a syntactical proof".] [P The notes from which the slides were made: [R math/2001c.ps.gz ps], [R math/2001c-dvi.tar.gz dvi+eps's], [R math/2001c-texsrc.tar.gz source]. ] [# unlinked: http://angg.twu.net/math/2001a.ps.gz http://angg.twu.net/math/2001b.ps.gz http://angg.twu.net/math/2001F.ps.gz #] [RULE ------------------------------------------------------------------] [# H1 [NAME MsC MsC] Thesis and related things:] [sec «MsC» (to ".MsC") H1 MsC Thesis and related things] [# My [NAME MsC MsC] Thesis ("Tese de Mestrado") and related things:] [P [BF My master's thesis: "Categorias, Filtros e Infinitesimais Naturais"] (April, 1999). The thesis and the slides used in the defense are in Portuguese.] [P Thesis (7+116 pages): [R math/tesemestr.ps.gz ps], [R math/tesemestr.pdf pdf], [R math/tesemestr-dvi.tar.gz dvi+eps's], [R math/tesemestr-texsrc.tar.gz source]. ] [P Slides (15 slides): [R math/slidesmestr.ps.gz ps], [R math/slidesmestr.pdf pdf], [R math/slidesmestr-dvi.tar.gz dvi+eps's], [R math/slidesmestr-texsrc.tar.gz source]. ] [P The diagrams were made with [L [-> diaglib] diaglib] and the deduction trees with [L LATEX/dednat.icn.html dednat.icn].] [NAME 2000-UFF] [# «2000-UFF» (to ".2000-UFF") #] [P A few months after the defense (in February 24, 2000, to be precise) I gave a talk at UFF about a kind of "Nonstandard Analysis with Filters", and about skeletons of proofs. Slides (12 slides plus one page), in Portuguese: [R math/2000uff.pdf pdf], [R math/2000uff.ps.gz ps], [R math/2000uff-dvi.tar.gz dvi+eps's], [R math/2000uff-texsrc.tar.gz source]. ] [P My advisor at PUC: [HREF http://www.mat.puc-rio.br/~nicolau/ Nicolau Saldanha]] [RULE ------------------------------------------------------------------] [sec «dednat4» (to ".dednat4") H1 Typesetting categorical diagrams in LaTeX] [P My PhD thesis included lots of hairy categorical diagrams, and I ended up writing a [R dednat4.html LaTeX preprocessor] in Lua to help me typeset them. Currently (March 2005) I'm trying to pack that preprocessor and document it; its [R dednat4/README.html README] is still horribly incomplete. The source code for the examples below is [R dednat4/examples/eqfibs.metatex.html here].] [lua: def [[ TABLE 1 text "$text\n
\n" ]] def [[ TR 1 text "$text\n\n" ]] def [[ TD 1 text "$text\n\n" ]] def [[ TDcolspan 2 n,text "$text\n\n" ]] def [[ DIAGTEXT 1 text BR()..COLOR("red",text) ]] def [[ DIAGTEXT 1 text "
\n" ..text.."\n
\n" ]] ] [TABLE [TR [TDcolspan 3 [IMG IMAGES/preslim.png] [DIAGTEXT if a functor R has a left adjont [BR] then it preserves limits] ] ] [TR [TD [IMG IMAGES/lccc-bcc.png] [DIAGTEXT The Beck-Chevalley map [BR] in an LCCC] ] [TD [IMG IMAGES/lccc-frob.png] [DIAGTEXT The Frobenius map [BR] in an LCCC] ] [TD [IMG IMAGES/eqfib-trans.png] [DIAGTEXT Proving transitivity [BR] in an EqFibration [BR] (slightly wrong)] ] ] ] [RULE ----------------------------------------] [_TARGETS local.copies -> (find-TH "eev-article" "local-copies") .emacs.papers -> (find-angg ".emacs.papers") Xscreenshot-rect -> (find-angg "bin/Xscreenshot-rect") dednat4 -> (find-TH "dednat4") ] [P Technical information: this page was made with [_ blogme]; the source is [R TH/math-b.blogme here]. I access [_ local copies] of papers with the functions defined in my [_ .emacs.papers]. The diagrams were made by processing [IT this file] (oops, which?) with [_ dednat4], then viewing the resulting dvi file with xdvi and taking screenshots with [_ Xscreenshot-rect].] [# This is somewhat offtopic [moderator, feel free to delete the message], but things best done by machines should be done by machines. At http://validator.w3.org/checklink you enter a URL and it tells you about broken links. #] ] ] [# http://www.math.ubc.ca/people/faculty/cass/Euclid/byrne.html http://www.math.uchicago.edu/~shulman/exposition/ http://ncatlab.org/nlab/show/Mike+Shulman http://types10.mimuw.edu.pl/ #] [# # Local Variables: # coding: raw-text-unix # modes: (fundamental-mode blogme-mode) # End: #]