[INCLUDE TH/speedbar.blogme]
[SETFAVICON dednat4/dednat4-icon.png]
[# SETFAVICON IMAGES/forthsun.png]
[#
(defun c () (interactive) (find-blogme3-sh0-if "math-b"))
(defun u () (interactive) (find-blogme-upload-links "math-b"))
;; http://anggtwu.net/math-b.html
;; file:///home/edrx/TH/L/math-b.html
;; «sec»
;; A variant of:
;; (find-blogme3 "anggdefs.lua" "sec")
(defun bsec (tag h head) (insert (bsec0 tag h head)))
(defun bsec0 (tag h head)
(ee-template0 "
[#
# «.{tag}»\t\t(to \"{tag}\")
# {(ee-S `(bsec ,tag ,h ,head))}
# (find-math-b-links \"{tag}\" \"{<}fnamestem{>}\")
#]
[sec «{tag}» (to \".{tag}\")
{h} {head}]
"))
#]
[lua: LR = R ]
[lua:
require "defs-2022" -- (find-blogme3 "defs-2022.lua")
short_:add [[
]]
]
[SETHEADSTYLE [LUCIDA]]
[lua: load_TARGETS()
loada2html()
def [[ RIGHTFIG 2 target,img "![](\"$img\")
" ]]
def [[ Sub 2 A,n IT(A).."$n" ]]
require "sexp" -- (find-blogme3 "sexp.lua")
]
[# 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) ]]
]
[#
# «.2025-ebl» (to "2025-ebl")
# «.2024-panic-t» (to "2024-panic-t")
# «.2022-ebl» (to "2022-ebl")
# «.2022-md» (to "2022-md")
# «.2021-groth-tops» (to "2021-groth-tops")
# «.2021-excuse-tt» (to "2021-excuse-tt")
# «.clops-and-tops» (to "clops-and-tops")
# «.favorite-conventions» (to "favorite-conventions")
# «.notes-on-notation-2020» (to "notes-on-notation-2020")
# «.2020-tallinn» (to "2020-tallinn")
# «.2020-classifier» (to "2020-classifier")
# «.2019-newton» (to "2019-newton")
# «.2019-viipl» (to "2019-viipl")
# «.missing-diagrams-elephant» (to "missing-diagrams-elephant")
# «.notes-yoneda» (to "notes-yoneda")
# «.intro-tys-lfc» (to "intro-tys-lfc")
# «.ebl2019-five-appls» (to "ebl2019-five-appls")
# «.ebl2019-mesa» (to "ebl2019-mesa")
# «.wld-2019» (to "wld-2019")
# «.tug-2018» (to "tug-2018")
# «.logic-for-children-unilog-2018» (to "logic-for-children-unilog-2018")
# «.visualizing-gms-unilog-2018» (to "visualizing-gms-unilog-2018")
# «.zhas-for-children-2» (to "zhas-for-children-2")
# «.notes-on-notation» (to "notes-on-notation")
# «.ebl-2017» (to "ebl-2017")
# «.lclt» (to "lclt")
# «.zhas-for-children» (to "zhas-for-children")
# «.istanbul» (to "istanbul")
# «.sheaves-for-children» (to "sheaves-for-children")
# «.sheaves-on-zdags» (to "sheaves-on-zdags")
# «.internal-diags-in-ct» (to "internal-diags-in-ct")
# «.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 The best things here are marked like [STANDOUT [' [this]]].]
[# 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/
GF => http://www.dpmms.cam.ac.uk/people/g.lima/
]
[_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://anggtwu.net/LATEX/2009unilog-abs1.pdf
(find-angg "LATEX/2009unilog-abs1.tex")
unilog2010-slides => http://anggtwu.net/LATEX/2010unilog-current.pdf
unilog2010-slides.dvi => http://anggtwu.net/LATEX/2010unilog-current.dvi
(find-angg "LATEX/2010unilog-current.tex")
unilog2010-1.dvi => http://anggtwu.net/LATEX/2010unilog-2010jun21.dvi
unilog2010-1.pdf => http://anggtwu.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
_local-copies -> (find-eevarticlesection "local-copies")
_local-copies -> http://anggtwu.net/eev-intros/find-psne-intro.html
local-copies -> eev-intros/find-psne-intro.html
#]
######################################## #]
[_TARGETS
Kock-axdiff => http://www.mscand.dk/issue.php?year=1977&volume=40
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://anggtwu.net/LATEX/2009unilog-abs1.pdf
(find-angg "LATEX/2009unilog-abs1.tex")
unilog2010-slides => http://anggtwu.net/LATEX/2010unilog-current.pdf
unilog2010-slides.dvi => http://anggtwu.net/LATEX/2010unilog-current.dvi
(find-angg "LATEX/2010unilog-current.tex")
unilog2010-1.dvi => http://anggtwu.net/LATEX/2010unilog-2010jun21.dvi
unilog2010-1.pdf => http://anggtwu.net/LATEX/2010unilog-2010jun21.pdf
ashes => http://en.wikipedia.org/wiki/Eyjafjallaj%C3%B6kull#2010_eruptions
]
[WITHINDEX
[_TARGETS
.emacs.papers -> (find-angg ".emacs.papers")
local-copies -> http://anggtwu.net/eev-intros/find-psne-intro.html
]
[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 [R eev-intros/find-psne-intro.html local copies] of)
online papers with the functions defined in my [_ .emacs.papers]
file.]
[P Note: I use [R dednat6.html Dednat6] to draw most of my diagrams.
[BR] The LaTeX source of my PDFs is always available - or should be.
[BR] To download the LaTeX source of a PDF called [TT foo.pdf] try:
[BR] [TT wget http://anggtwu.net/LATEX/foo.tgz]
[BR] [TT wget http://anggtwu.net/LATEX/foo.zip]
[BR] then unpack it and run [TT lualatex foo.tex].
[BR] If neither the [TT .tgz] not the [TT .zip] are online, [R
contact.html get in touch]!
]
]]
[br]
[br ----------------------------------------]
[#
# (bsec "2025-ebl" "H2" "Adapting Lean tutorials to the Brazilian case (2025)")
# (find-math-b-links "2025-ebl" "2025adapting-lean-tuts")
#]
[sec «2025-ebl» (to ".2025-ebl")
H2 Adapting Lean tutorials to the Brazilian case (2025)]
[P My submission to the EBL 2025.
[BR] [R http://anggtwu.net/LATEX/2025ebl-abs.pdf Abstract.]
[BR] [R http://anggtwu.net/LATEX/2025adapting-lean-tuts.pdf Slides (unrevised).]
]
[br ----------------------------------------]
[#
# (bsec "2024-panic-t" "H2" "Panic! At Equalities (Versão Teresópolis) (2024)")
# (find-math-b-links "2024-panic-t" "2024panic-teresopolis")
#]
[sec «2024-panic-t» (to ".2024-panic-t")
H2 Panic! At Equalities (Versão Teresópolis) (2024)]
[P [RIGHTFIG http://anggtwu.net/LATEX/2024panic-teresopolis.pdf
IMAGES/2024panic-teresopolis.png]
This was my presentation at the "Retiro de Teresópolis" in
2024jun18. The "Retiro" doesn't have a page yet, but it was
organized by the same people who organized [R
2021aulas-por-telegram.html these meetings]. My presentation was in
Portuguese and with slides in Portuguese, and it was mainly about
the techniques that I've been using to teach Calculus 2 ([R
2024.1-C2.html page], [R
http://anggtwu.net/LATEX/2024-1-C2-Tudo.pdf PDFzão]) to the
students of Rio das Ostras, that usually arrive at the course
without knowing how to manipulate expressions.
]
[P [R http://anggtwu.net/LATEX/2024panic-teresopolis.pdf Slides].]
[br ----------------------------------------]
[#
# (bsec "2022-ebl" "H2" "On a way to visualize some Grothendieck Topologies (2022)")
# (find-math-b-links "2022-ebl" "2022ebl-abs")
# (find-math-b-links "2022-ebl" "2022ebl")
#]
[sec «2022-ebl» (to ".2022-ebl")
H2 On a way to visualize some Grothendieck Topologies (2022)]
[P My presentation at the [R https://ebl2021.ufba.br/ XX EBL] (sep/2022).
[R http://anggtwu.net/LATEX/2022ebl.pdf Slides],
[R LATEX/2022ebl.tex.html LaTeX source],
[R http://anggtwu.net/LATEX/2022ebl-abs.pdf abstract].
[BR] See my "[R #2021-groth-tops Grothendieck Topologies for Children]" (2021).]
[br ----------------------------------------]
[#
# (bsec "2022-md" "H2" "On the missing diagrams in Category Theory (2022) ")
# (find-math-b-links "2022-md" "2022on-the-missing")
# Tweet by Bruno Gavranovic:
# https://twitter.com/bgavran3/status/1518490598675824642
#]
[sec «2022-md» (to ".2022-md")
H2 On the missing diagrams in Category Theory (2022) ]
[P [NAME md] [# «md»
#]
[STANDOUT [' [MD]]]
This is a rewrite of [R #favorite-conventions [' [FavC]]].
Its abstract is:
]
[P [RIGHTFIG http://anggtwu.net/LATEX/2022on-the-missing.pdf
IMAGES/2022on-the-missing.png]
Most texts on Category Theory are written in a very terse style, in
which people pretend a) that all concepts are visualizable, and b)
that the readers can reconstruct the diagrams that the authors had
in mind based on only the most essential cues. As an outsider I
spent years believing that the techniques for drawing diagrams were
part of the oral culture of the field, and that the insiders could
read texts on CT reconstructing the "missing diagrams" in them line
by line and paragraph by paragraph, and drawing for each page of
text a page of diagrams with all the diagrams that the authors had
omitted. My belief was wrong: there are lots of conventions for
drawing diagrams scattered through the literature, but that unified
diagrammatic language did not exist. In this chapter I will show an
attempt to reconstruct that (imaginary) language for missing
diagrams: we will see an extensible diagrammatic language, called
DL, that follows the conventions of the diagrams in the literature
of CT whenever possible and that seems to be adequate for drawing
"missing diagrams" for Category Theory. Our examples include the
"missing diagrams" for adjunctions, for the Yoneda Lemma, for Kan
extensions, and for geometric morphisms, and how to formalize them
in Agda.]
[P This was published as a
[R https://link.springer.com/referenceworkentry/10.1007/978-3-030-68436-5_41-1
chapter]
of this book:
[R https://link.springer.com/referencework/10.1007/978-3-030-68436-5
Handbook of Abductive Cognition].
[# https://meteor.springer.com/abductivecognition #]
[BR] The current ("first-person") version is [R
http://anggtwu.net/LATEX/2022on-the-missing.pdf here].
[BR] The version on Arxiv (also "first-person") is here:
[R https://arxiv.org/pdf/2204.10630.pdf PDF],
[R https://arxiv.org/abs/2204.10630 abstract].
[BR] The technical report "On the missing diagrams in Category
Theory: Agda code" will be at [R
http://anggtwu.net/LATEX/2022on-the-missing-agda.pdf this
link].]
[P The version accepted into the "Handbook of Abductive Cognition" is
drier and shorter: it is not in the first person, it has a much
shorter introduction, and it doesn't have the [R
http://anggtwu.net/LATEX/2022on-the-missing.pdf#page=42 chapter]
that shows extensions of the diagrammatic language. I think that
the first-person version is much better. =/]
[br ----------------------------------------]
[#
# (bsec "2021-groth-tops" "H2" "Grothendieck Topologies for Children (2021)")
# (find-math-b-links "2021-groth-tops" "2021groth-tops-children")
#]
[sec «2021-groth-tops» (to ".2021-groth-tops")
H2 Grothendieck Topologies for Children (2021)]
[P [RIGHTFIG http://anggtwu.net/LATEX/2021groth-tops-children.pdf
IMAGES/2021-groth-tops.png]
The paper "Planar Heyting Algebras for Children" ([R
#zhas-for-children-2 here]) showed how to use Planar Heyting
Algebras to visualize the truth-values and the operations of
Propositional Calculus in certain toposes; the "...for children" of
its title means: "we will start from some motivating examples ('for
children') that are easy to visualize, and then go the general case
('for adults') - [IT but there are precise techniques for working
on the case 'for children' and on the case 'for adults' in
parallel]". These techniques are described in detail [R
#favorite-conventions here].
In these notes we will use these techniques to visualize
Grothendieck topologies - first in the "archetypal" case of the
canonical topology on a certain finite topological space, and then
we will generalize that to arbitrary Grothendieck topogies on
certain finite posets. that we will treat as "ex-topologies".]
[P The PDF is [R http://anggtwu.net/LATEX/2021groth-tops-children.pdf
here], but it is a mess. I rewrote most of the important ideas
cleanly [R #clops-and-tops here].]
[P I give two informal talks on that, both in Portuguese, [R
https://sites.google.com/view/teoriadascategoriaseaplicacoes/home?authuser=0
here].
[BR] The first one was in may 17, 2021, and was a bit messy. [R
https://sites.google.com/view/teoriadascategoriaseaplicacoes/semin%C3%A1rios-passados?authuser=0
Recording].
[BR] The second one was in june 7, 2021, and was much better. [R
https://youtu.be/e5WuosPuyq8 Youtube], better quality [R
https://sites.google.com/view/teoriadascategoriaseaplicacoes/semin%C3%A1rios-passados?authuser=0
recording].
[BR] [R
http://anggtwu.net/LATEX/2021groth-tops-children-slides.pdf
slides].
]
[br ----------------------------------------]
[#
# (bsec "2021-excuse-tt" "H2" "Category Theory as An Excuse to Learn Type Theory (2021)")
# (find-math-b-links "2021-excuse-tt" "2021excuse")
# (find-math-b-links "2021-excuse-tt" "2021excuse-abs")
#]
[sec «2021-excuse-tt» (to ".2021-excuse-tt")
H2 Category Theory as An Excuse to Learn Type Theory (2021) ]
[P [RIGHTFIG http://anggtwu.net/LATEX/2021excuse.pdf
IMAGES/2021-excuse-tt.png]
The organizers of the "[R https://encontrocategorico.mat.br/
Encontro Brasileiro em Teoria das Categorias]" invited me to give a
50-minute talk there. My talk was on the [R
https://encontrocategorico.mat.br/programacao/ thursday], 28
january 2021. The abstract for my talk is [R
http://anggtwu.net/LATEX/2021excuse-abs.pdf here], and the slides
are [R http://anggtwu.net/LATEX/2021excuse.pdf here]. The
recording is [R https://www.youtube.com/watch?v=8WLcVb1rU1Y#t=7m40s
here] [COLOR red (in Portuguese)].]
[br ----------------------------------------]
[#
# (bsec "clops-and-tops" "H2" "Each closure operator induces a topology and vice-versa (2020/2021) ")
# (find-math-b-links "clops-and-tops" "2020clops-and-tops")
#]
[sec «clops-and-tops» (to ".clops-and-tops")
H2 Each closure operator induces a topology and vice-versa (2020/2021) ]
[P [RIGHTFIG http://anggtwu.net/LATEX/2020clops-and-tops.pdf
IMAGES/2020clops-and-tops.png]
[STANDOUT [' [Clops&Tops]]]
One of the main prerequisites for understanding sheaves on
elementary toposes is the proof that a (Lawvere-Tierney) topology
on a topos induces a closure operator on it, and vice-versa. That
standard theorem is usually presented in a relatively brief way,
with most details being left to the reader, and with no hints on
how to visualize some of the hardest axioms and proofs.]
[P These notes are, on a first level, an attempt to present that
standard theorem in all details and in a visual way, following the
conventions [R #favorite-conventions below]; in particular, some
properties, like stability by pullbacks, are always drawn in the
same "shape".]
[P [RIGHTFIG http://anggtwu.net/LATEX/2020clops-and-tops.pdf#page=39
IMAGES/2020clops-and-tops-4-2-small.png]
On a second level these notes are also an experiment on doing these
proofs on "archetypal cases" in ways that makes all the proofs easy
to lift to the "general case". Our first archetypal case is a
"topos with inclusions". This is a variant of the "toposes with
canonical subobjects" from section 2.15 of [<]Lambek/Scott 86[>];
all toposes of the form Set^C, where C is a small category, are
toposes with inclusions, and when we work with toposes with
inclusions concepts like subsets and intersections are very easy to
formalize. We do all our proofs on the correspondence between
closure operators and topologies in toposes with inclusions, and
then we show how to lift all our proofs to proofs that work on any
topos. Our second archetypal case is toposes of the form Set^D,
where D is a finite two-column graph. We show a way to visualize
all the Lawvere-Tierney topologies on toposes of the form Set^D,
and we define formally a way to "add visual intuition to a proof
about toposes"; this is related to the several techniques for doing
"Category Theory for children" that are explained in the first
sections of [<][R #favorite-conventions FavC][>].]
[P The [R http://anggtwu.net/LATEX/2020clops-and-tops.pdf PDF] of the
current version (2021jul26). [R https://arxiv.org/abs/2107.11301
Arxiv].
[BR] Older versions: [R
http://anggtwu.net/LATEX/2020clops-and-tops-20201124.pdf 2020nov24].
[BR] See also: "[R
http://anggtwu.net/LATEX/2021lindenhovius-j-to-X.pdf On a formula
that is not in Grothendieck Topologies in Posets']" ([R
https://arxiv.org/abs/2107.08501 Arxiv]).
]
[br ----------------------------------------]
[#
# (bsec "favorite-conventions" "H2" "On my favorite conventions for drawing the missing diagrams in Category Theory (2020) ")
# (find-math-b-links "favorite-conventions" "2020favorite-conventions")
#]
[sec «favorite-conventions» (to ".favorite-conventions")
H2 On my favorite conventions for drawing the missing diagrams in Category Theory (2020) ]
[P [RIGHTFIG http://anggtwu.net/LATEX/2020favorite-conventions.pdf
IMAGES/2020favorite-conventions.png]
[STANDOUT [' [FavC]]]
I used to believe that my conventions for drawing diagrams for
categorical statements could be written down in one page or less,
and that the only tricky part was the technique for reconstructing
objects "from their names"... but then I found out that this is not
so.]
[P This is an attempt to explain, with motivations and examples, all
the conventions behind a certain diagram, called the "Basic
Example" in the text. Once the conventions are understood that
diagram becomes a "skeleton" for a certain lemma related to the
Yoneda Lemma, in the sense that both the statement and the proof of
that lemma can be reconstructed from the diagram. The last sections
discuss some simple ways to extend the conventions; we see how to
express in diagrams the ("real") Yoneda Lemma and a corollary of
it, how to define comma categories, and how to formalize the
diagram for "geometric morphism for children" mentioned in section
1.]
[P People in CT usually only share their ways of visualizing things
when their diagrams cross some threshold of of mathematical
relevance - and this usually happens when they prove new theorems
with their diagrams, or when they can show that their diagrams can
translate calculations that used to be huge into things that are
much easier to visualize. The diagrammatic language that I present
here lies below that threshold - and so it is a "private"
diagrammatic language, that I am making public as an attempt to
establish a dialogue with other people who have also created their
own private diagrammatic languages.]
[P [R http://anggtwu.net/LATEX/2020favorite-conventions.pdf PDF], [R
https://arxiv.org/abs/2006.15836 arxiv].
The non-arxiv PDF is better - it has colors and hyperlinks.
[BR] See [R #2022-md [' [MD]]] for a rewritten version of these notes.
]
[br ----------------------------------------]
[#
# (bsec "notes-on-notation-2020" "H2" "Notes on Notation (2020)")
# (find-math-b-links "notes-on-notation-2020" "{fnamestem}")
#]
[sec «notes-on-notation-2020» (to ".notes-on-notation-2020")
H2 Notes on Notation (2020)]
[P In 2020 I decided to test [R #favorite-conventions my conventions]
for drawing [R #missing-diagrams-elephant missing diagrams] by drawing
some of the diagrams that are "missing" in several texts and seeing if
I always get diagrams that are easy to translate into Idris. These are
messy notes for personal use, but if you have your own conventions I'd
love to see them - please [R contact.html get in touch].
[BR] More ""s mean more interesting.
]
[lua:
def [[ noo 3 pdfurl,sexp,longname R(pdfurl,longname) ]]
]
[P [noo http://anggtwu.net/LATEX/2020abramsky-tzevelekos.pdf (abtp)
Abramsky/Tzevelekos],
[BR] [noo http://anggtwu.net/LATEX/2020awodey.pdf (awop)
Awodey's book],
[BR] [noo http://anggtwu.net/LATEX/2020badiou-low.pdf (blop)
Badiou's "Logics of Worlds"],
[BR] [noo http://anggtwu.net/LATEX/2020badiou-mt.pdf (bmtp)
Badiou's "Mathematics of The Transcendental"],
[BR] [noo http://anggtwu.net/LATEX/2020barrwellsctcs.pdf (ctcp)
Barr/Wells's CTCS],
[BR] [noo http://anggtwu.net/LATEX/2020bell-lst.pdf (lstp)
Bell's "Toposes and Local Set Theories"],
[BR] [noo http://anggtwu.net/LATEX/2020institutions.pdf (instp)
Diaconescu's "Institutions..."],
[BR] [noo http://anggtwu.net/LATEX/2020jacobs.pdf (jacp)
Jacobs's "Categorical Logic and Type Theory"],
[BR] [noo http://anggtwu.net/LATEX/2020kockdiff.pdf (kdip)
Kock's "A Simple Axiomatics for Differentiation"],
[BR] [noo http://anggtwu.net/LATEX/2020lambek86.pdf (l86p)
Lambek86],
[BR] [noo http://anggtwu.net/LATEX/2020lawvere-adjfo.pdf (ladp)
Lawvere's "Adjointness in Foundations" (1969)],
[BR] [noo http://anggtwu.net/LATEX/2020lawvere-equahyp.pdf (leqp)
Lawvere's "Equality in Hyperdoctrines" (1970)],
[BR] [noo http://anggtwu.net/LATEX/2020macdonaldsobral.pdf (mdsp)
MacDonald/Sobral],
[BR] [noo http://anggtwu.net/LATEX/2020cwm.pdf (cwmp)
MacLane's CWM],
[BR] [noo http://anggtwu.net/LATEX/2020maclane-moerdijk.pdf (mmop)
MacLane/Moerdijk's "Sheaves in Geometry and Logic"],
[BR] [noo http://anggtwu.net/LATEX/2020mclarty.pdf (larp)
McLarty's "Elementary Categories, Elementary Toposes"],
[BR] [noo http://anggtwu.net/LATEX/2020genericfigures.pdf (gefp)
Reyes*2/Zolfaghari's "Generic Figures..."],
[BR] [noo http://anggtwu.net/LATEX/2020riehl.pdf (riep)
Riehl's "Categories in Context"],
[BR] [noo http://anggtwu.net/LATEX/2020seelyhyp.pdf (shyp)
Seely's "Hyperdoctrines..."],
[BR] [noo http://anggtwu.net/LATEX/2020seelylccc.pdf (slcp)
Seely's "LCCCs and Type Theory"],
[BR] [noo http://anggtwu.net/LATEX/2020dialectica.pdf (vdpp)
Valeria de Paiva's "The Dialectica Categories"]
]
[br ----------------------------------------]
[#
# (bsec "2020-tallinn" "H2" "What kinds of knowledge do we gain by doing CT in several levels of abstraction in parallel? (2020)")
# (find-math-b-links "2020-tallinn" "2020tallinn-abstract")
# (taap)
#]
[sec «2020-tallinn» (to ".2020-tallinn")
H2 What kinds of knowledge do we gain by doing CT in several levels of abstraction in parallel? (2020)]
[P A talk that I submitted to [R
http://www.diagrams-conference.org/2020/ Diagram 2020]. Its short
abstract is:]
[NARROW [P
Concepts and proofs in Category Theory are usually presented in a
very abstract way, in which the diagrams, the motivating examples
and the low-level details are mostly omitted and left as exercises
for the reader. Here we will discuss how to work in this more
abstract level and in less abstract levels at the same time, using
parallel diagrams and transfering some information from the more
abstract diagram to the less abstract one and back - and we will
show formally, using type systems, what we gain by working in two
levels of abstraction in parallel.
]]
[P Its "real", 4-page abstract is [R
http://anggtwu.net/LATEX/2020tallinn-abstract.pdf here].]
[br ----------------------------------------]
[# ######################################## #]
[#
# (bsec "2020-classifier" "H2" "Notes about classifiers and local operators in a Set^(P,A) (2020)")
# (find-math-b-links "2020-classifier" "2019classifier")
#]
[sec «2020-classifier» (to ".2020-classifier")
H2 Notes about classifiers and local operators in a Set^(P,A) (2020)]
[P
In the last section of [R #zhas-for-children-2 Planar Heyting
Algebras for Children 2: Local Operators, J-Operators, and
Slashings] ([R http://anggtwu.net/LATEX/2020J-ops-new.pdf PDF])
I wrote that the proofs that my definitions for Ω and [IT
j] "work as expected" are "routine". Well, they are only routine
if you know some techniques... these notes [COLOR red will]
discuss these techniques and show all the calculations, but they
are currently in a [COLOR red very] preliminary form.
[BR] The [R http://anggtwu.net/LATEX/2019classifier.pdf PDF].
]
[# ######################################## #]
[br ----------------------------------------]
[#
# (bsec "2019-newton" "H2" "On two tricks to make Category Theory fit in less mental space")
# (find-math-b-links "2019-newton" "2019newton-slides")
# (find-math-b-links "2019-newton" "2019newton-abs")
# (nesp)
#]
[sec «2019-newton» (to ".2019-newton")
H2 On two tricks to make Category Theory fit in less mental space (2019)]
[P A talk at the [R
https://sites.google.com/view/creativity2019/welcome Creativity
2019] in Rio de Janeiro, in the workshop on [R
https://sites.google.com/view/creativity2019/workshops/formal-logic-and-foundations-of-mathematics
formal logic and foundations].
Its full title was "On two tricks to make Category Theory fit in
less mental space: missing diagrams and skeletons of proofs", and
the abstract that I submitted is [R
http://anggtwu.net/LATEX/2019newton-abs.pdf here].
[BR] [STANDOUT [' [LessMS]]]
[R http://anggtwu.net/LATEX/2019newton-slides.pdf Slides].
[# The slides are [R http://anggtwu.net/LATEX/2019newton-slides.pdf
here]. #]
]
[br ----------------------------------------]
[#
# (bsec "2019-viipl" "H2" "Using Planar Heyting Algebras to develop visual intuition about IPL (2019)")
# 1st: (find-math-b-links "2019-viipl" "2019ilha-grande-slides")
# 2nd: (find-math-b-links "2019-viipl" "2019seminario-hermann")
# (sehp)
#]
[sec «2019-viipl» (to ".2019-viipl")
H2 Using Planar Heyting Algebras to develop visual intuition about IPL (2019)]
[P
[RIGHTFIG http://anggtwu.net/LATEX/2019seminario-hermann.pdf
IMAGES/2019-viipl.png]
Two presentations with the same title in two small events.
[BR] The first one was in 2019aug19 at the "Jornadas de Mirantão"
at [R http://www.meioambiente.uerj.br/campus/campusilhagrande.htm
Ilha Grande], and in it I alternated between its [R
http://anggtwu.net/LATEX/2019ilha-grande-slides.pdf slides] and
my [R http://anggtwu.net/LATEX/2019logicday.pdf slides] for the
[R #wld-2019 World Logic Day 2019].
[BR] The second one was in 2019sep10 at the "Seminário do [R
http://www-di.inf.puc-rio.br/~hermann/ Hermann]" at PUC-Rio, and
in it I alternated between its [R
http://anggtwu.net/LATEX/2019seminario-hermann.pdf slides] and
the [R http://anggtwu.net/LATEX/2017planar-has-1.pdf Planar
Heyting Algebras for Children] paper (see [R #zhas-for-children-2
here]).
[BR] I did not prepare abstracts for them.
]
[br ----------------------------------------]
[#
# (bsec "missing-diagrams-elephant" "H2" "On some missing diagrams in the Elephant (2019)")
# (find-math-b-links "missing-diagrams-elephant" "2019oxford-abs")
# (find-math-b-links "missing-diagrams-elephant" "2019elephant-poster")
# (oxap)
# (elzp)
#]
[sec «missing-diagrams-elephant» (to ".missing-diagrams-elephant")
H2 On some missing diagrams in the Elephant (2019) ]
[P
[RIGHTFIG http://anggtwu.net/LATEX/2019oxford-abs.pdf
IMAGES/oxford2019.png]
[STANDOUT [' [MDE]]] This is a 12-page [R
http://anggtwu.net/LATEX/2019oxford-abs.pdf extended abstract]
(also [R http://anggtwu.net/LATEX/2019oxford-abs-noc.pdf here]
with darker fonts) that I submitted to [R
http://www.cs.ox.ac.uk/ACT2019/ ACT2019], that happened in Oxford
in july 2019. The extended abstract's abstract is:]
[NARROW
[P Imagine two category theorists, Aleks and Bob, who both think
very visually and who have exactly the same background. One day
Aleks discovers a theorem, [Sub T 1], and sends an e-mail, [Sub E
1], to Bob, stating and proving [Sub T 1] in a purely algebraic
way; then Bob is able to reconstruct by himself Aleks's diagrams
for [Sub T 1] exactly as Aleks has thought them. We say that Bob
has reconstructed the "missing diagrams" in Aleks's e-mail.]
[P Now suppose that Carol has published a paper, [Sub P 2], with a
theorem [Sub T 2]. Aleks and Bob both read her paper
independently, and both pretend that she thinks diagrammatically
in the same way as them. They both "reconstruct the missing
diagrams" in [Sub P 2] in the same way, even though Carol has
never used those diagrams herself.]
[P Here we will reconstruct, in the sense above, some of the
"missing diagrams" in two factorizations of geometric morphisms
in section A4 of Johnstone's "Sketches of an Elephant", and also
some "missing examples". Our criteria for determining what is
"missing" and how to fill out the holes are essentially the ones
presented in the "Logic for Children" workshop at the UniLog
2018; they are derived from a certain [IT definition] of
"children" that turned out to be especially fruitful.]
]
[P My submission was not accepted to become a talk, only to the [R
http://www.cs.ox.ac.uk/ACT2019/preproceedings/ACT%202019%20programme.pdf
poster session] (on tuesday 16/july).
[BR] The [R http://anggtwu.net/LATEX/2019elephant-poster.pdf PDF of
the poster]. I wrote [COLOR brown [BF INCOMPLETE]] at the bottom
of it by hand when I hanged it to the wall.
[BR] The poster makes reference to these papers, notes, and slides:
]
[UL [LI [BF PH1] ("Planar Heyting Algebras for Children"): [R
http://anggtwu.net/LATEX/2017planar-has-1.pdf PDF], [R
#zhas-for-children-2 more info].]
[LI [BF PH2] ("Planar Heyting Algebras for Children 2: Local
Operators"): [R http://anggtwu.net/LATEX/2020J-ops-new.pdf
PDF], [R #zhas-for-children-2 more info].]
[LI [BF NYo] ("Notes on the Yoneda Lemma"): [R
http://anggtwu.net/LATEX/2019notes-yoneda.pdf PDF], [R
#notes-yoneda more info].]
[LI [BF MDE] ("On some missing diagrams in the Elephant"): [R
http://anggtwu.net/LATEX/2019oxford-abs.pdf PDF] of the
extended abstract.]
[LI [BF IDARCT] ("Internal Diagrams and Archetypal Reasoning in
Category Theory"): [R
http://anggtwu.net/LATEX/idarct-preprint.pdf PDF], [R #idarct
more info].]
]
[P See the "[R #zhas-for-children-2 Planar Heyting Algebras for
Children]" series.]
[br ----------------------------------------]
[#
# (bsec "notes-yoneda" "H2" "Notes on the Yoneda Lemma")
# (find-math-b-links "notes-yoneda" "2019notes-yoneda")
# (nyo)
# (nyop)
#]
[sec «notes-yoneda» (to ".notes-yoneda")
H2 Notes on the Yoneda Lemma (2019/2020)]
[P [RIGHTFIG http://anggtwu.net/LATEX/2019notes-yoneda
IMAGES/yoneda-2019.png]
[STANDOUT [' [NYo]]]
[R http://anggtwu.net/LATEX/2020notes-yoneda.pdf Slides],
My plan [COLOR red was] to make a video from this, but I got stuck...
[BR] Then some friends asked me to present this to them in Portuguese
[BR] by Zoom in 2020may29, and they [R
https://www.youtube.com/watch?v=MiSeA-WahQU recorded] it. Then I
got [COLOR red unstuck] -
[BR] and I wrote the paper "[R #favorite-conventions On my favorite
conventions...]"
[BR] and declared these slides [COLOR red obsolete].
[BR]
[BR] The full title of the slides is:
]
[NARROW [P
[BF A diagram for the Yoneda Lemma]
[BR] (In which each node and arrow can be
[BR] interpreted precisely as a "[R
https://en.wikipedia.org/wiki/Lambda_calculus#Lambda_terms
term]",
[BR] and most of the interpretations are
[BR] "obvious"; plus dictionaries!!!)
]]
[P I am [IT trying] to implement this in a proof assistant -
[BR] on top of Jannis Limpberg's [R
https://limperg.de/posts/2018-07-27-yoneda.html work] or on [R
https://github.com/statebox/idris-ct idris-ct] -
[BR] but I am progressing slowly! Help, please!!!
[BR] Here is [R IDRIS/Tut.idr.html my eev-ized version] of the [R
http://docs.idris-lang.org/en/latest/tutorial/ Idris tutorial].
[BR]
[BR] Older versions of the slides:
[R http://anggtwu.net/LATEX/2019notes-yoneda.pdf 2020-04-05],
[R http://anggtwu.net/LATEX/2019notes-yoneda-2019-06-01.pdf
2019-06-01].
[BR]
[BR] If you don't know the Yoneda Lemma well
[BR] then start by these blog posts:
[R https://www.math3ma.com/blog/the-yoneda-embedding E],
[R https://www.math3ma.com/blog/the-yoneda-lemma L].
]
[br ----------------------------------------]
[#
# (bsec "intro-tys-lfc" "H2" "An introduction to type systems (and to the \"Logic for Children\" project) (2019)")
# (find-math-b-links "intro-tys-lfc" "2019notes-types")
# (nty)
# (ntyp)
#]
[sec «intro-tys-lfc» (to ".intro-tys-lfc")
H2 An introduction to type systems (and to the "Logic for Children" project) (2019)]
[P
[RIGHTFIG http://anggtwu.net/LATEX/2019notes-types.pdf
IMAGES/intro-tys-lfc.png]
This is going to be a series of [COLOR red videos], but I am still
working on the slides... work in progress!
[BR] [COLOR red Preliminary mini-abstract:] once we learn a bit of
type systems - the [R https://en.wikipedia.org/wiki/Lambda_cube
Barendregt Cube] and [R
https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation
BHK]; the [R
https://en.wikipedia.org/wiki/Calculus_of_constructions Calculus
of Constructions] is not really needed - we can use the
techniques of the "Logic for Children" project to build diagrams
for categorical concepts in a way in which every node and arrow
in these diagrams can be interpreted precisely as a lambda term;
moreover, we can create "dictionaries" based on those diagrams
that help us translate between several standard notations found
in the literature - and help us read the standard literature.
[BR] Links to some of the slides (work in progress!):
[BR] 1. [STANDOUT [' [NTy]]] [R
http://anggtwu.net/LATEX/2019notes-types.pdf An
introduction to Type Theory] (40% ready).
[BR] 2. [R http://anggtwu.net/LATEX/2019notes-yoneda.pdf Notes on the
Yoneda Lemma] (90% ready; moved to the item above)
]
[P I almost gave a presentation about the part on types at [R
https://pt.foursquare.com/v/instituto-de-filosofia-e-ci%C3%AAncias-sociais-ifcs/4e68dc877d8bef8fc4a2b86a/photos
IFCS] in 2019jun18, but Jean-Yves Beziau forgot to pick up the
projector from the secretary's drawer in the morning... she left
everything locked, went out for lunch and only returned many, many
hours later.]
[br ----------------------------------------]
[#
# (bsec "ebl2019-five-appls" "H2" "Five applications of the \"Logic for Children\" project to Category Theory (2019)")
# (find-math-b-links "ebl2019-five-appls" "2019ebl-five-appls")
#]
[sec «ebl2019-five-appls» (to ".ebl2019-five-appls")
H2 Five applications of the "Logic for Children" project to Category Theory (2019)]
[P A talk that I gave at the [R https://ebl2019.ci.ufpb.br/ EBL2019]
in 2019may09. Its abstract is [R
http://anggtwu.net/LATEX/2019ebl-abs.pdf here]. My plans for this
talk were very ambitious: I wanted to present the main ideas,
motivations and constructions of [R #zhas-for-children-2 PHAfC 1, 2
and 3] and [R #logic-for-children-unilog-2018 Logic for Children] in
20 minutes, with lots of figures... but when it was my turn to present
all the people who knew a bit of Category Theory were in another room,
attending a session with technical talks, and I did not have the 5 or
6 slides that I [IT could] have made my talk more accessible to an
audience of philosophers. I failed miserably.]
[R http://anggtwu.net/LATEX/2019ebl-five-appls.pdf Slides.]
[br ----------------------------------------]
[#
# (bsec "ebl2019-mesa" "H2" "Ensinando Matemática Discreta para calouros com português muito ruim (2019)")
# (find-math-b-links "ebl2019-mesa" "2019ebl-mesa-slides")
#]
[sec «ebl2019-mesa» (to ".ebl2019-mesa")
H2 Ensinando Matemática Discreta para calouros com português muito ruim (2019)]
[P [NAME ebl2019-m] I organized a round table about how to teach Logic
to undergraduates in the [R https://ebl2019.ci.ufpb.br/ EBL2019].
[BR]
Its abstracts are [R
http://anggtwu.net/LATEX/2019ebl-mesa-disc-logica-grad.pdf here]
(in Portuguese). It happened in 2019may06.
[BR]
The slides of my talk - about a way to teach Discrete Mathematics
to freshmen who speak and write Portuguese very badly - are [R
http://anggtwu.net/LATEX/2019ebl-mesa-slides.pdf here] (about 70%
in English).
]
[br ----------------------------------------]
[#
# (bsec "wld-2019" "H2" "How to almost teach Intuitionistic Logic to Discrete Mathematics Students (2019) ")
# (find-math-b-links "wld-2019" "2019logicday")
#]
[sec «wld-2019» (to ".wld-2019")
H2 How to almost teach Intuitionistic Logic to Discrete Mathematics Students (2019) ]
[P [RIGHTFIG http://anggtwu.net/LATEX/2019logicday.pdf
IMAGES/entrada-PURO.jpg]
A talk in the [R http://www.logicauniversalis.org/wld World Logic
Day] - 2019jan14 - in [R
http://www.logicauniversalis.org/wld-rio-de-janeiro Rio de
Janeiro], about:
[BR] 1) my approach to teaching [R 2018.2-MD.html Discrete Mathematics] to the students
that we get nowadays,
[BR] 2) my [R #lclt course] without prerequisites on lambda-calculus
and intuitionistic logic, and
[BR] 3) how this fits at the base of the [R
#logic-for-children-unilog-2018 Logic for Children] project.
[# This is related to the "[R #ebl2019-five-appls Five
Applications...]" talk and to the [R #ebl2019-mesa round table]
above. #]
[BR] [R http://anggtwu.net/LATEX/2019logicday.pdf Slides.]
]
[br ----------------------------------------]
[#
# (bsec "tug-2018" "H2" "Dednat6: an extensible (semi-)preprocessor for LuaLaTeX")
# (find-math-b-links "tug-2018" "2018tugboat-rev1")
#]
[sec «tug-2018» (to ".tug-2018")
H2 Dednat6: an extensible (semi-)preprocessor for LuaLaTeX ]
[P [RIGHTFIG http://anggtwu.net/LATEX/2018tug-dednat6.pdf
IMAGES/tug-2018.png]
A talk at [R https://www.tug.org/tug2018/ TUG2018], in Rio de
Janeiro, in [R https://tug.org/tug2018/program.html 2018jul20] about
the [R dednat6.html package] that I use to typeset several kinds of
diagrams.
[BR] Its full title is "Dednat6: an extensible (semi-)preprocessor for
LuaLaTeX that understands diagrams in ASCII art".
[BR] 2018-12-31: Official page: [R http://anggtwu.net/dednat6.html]
[BR] 2018-10-29: [COLOR red Revised version] of the article about
Dednat6 to [R https://www.tug.org/tugboat/ TUGboat]. [R
http://anggtwu.net/LATEX/2018tugboat-rev1.pdf PDF], [R
http://anggtwu.net/LATEX/2018tugboat-rev1.tgz source]; [R
https://tug.org/TUGboat/tb39-3/tb123ochs-dednat.pdf published] in
[R http://www.tug.org/TUGboat/Contents/contents39-3.html TUGBoat
39:3].
[BR] 2018-10-16: Original version of the article about Dednat6 to
TUGboat: [R http://anggtwu.net/LATEX/2018tugboat.pdf PDF], [R
http://anggtwu.net/LATEX/2018tugboat.tgz source]. Has some [IT
very] ugly line breaks.
[BR] 2018-07-20: First day of the [R https://www.tug.org/tug2018/
Conference]. [R https://tug.org/tug2018/program.html Program], [R
http://anggtwu.net/LATEX/2018tug-dednat6.pdf my slides] and a [R
https://www.youtube.com/watch?v=CjQKbxwtQ-o video] of my
presentation (without me jumping to point to things).
[BR] 2018-05-08: [R http://anggtwu.net/LATEX/2018tug-dednat6-abs.pdf
Abstract] submitted to the conference.
]
[br ----------------------------------------]
[#
# (bsec "logic-for-children-unilog-2018" "H2" "Logic for Children (workshop at UniLog 2018) ")
# (find-math-b-links "logic-for-children-unilog-2018" "2018vichy-video")
# (find-math-b-links "logic-for-children-unilog-2018" "2017vichy-workshop")
#]
[sec «logic-for-children-unilog-2018» (to ".logic-for-children-unilog-2018")
H2 Logic for Children (workshop at UniLog 2018) ]
[P [RIGHTFIG http://anggtwu.net/LATEX/2018vichy-video.pdf
IMAGES/vichy-video-pentominos.png]
I organized (with [R
https://cmuc.mat.uc.pt/rdonweb/person/ppgeral.do?idpessoa=1331
Fernando Lucatelli]) a workshop called "Logic for Children" that
happened at the [R http://www.uni-log.org/vichy2018 UniLog 2018] in
Vichy, France, in june 24, 2018.
[BR]
[STANDOUT [' [LFCV]]] I made a [R https://youtu.be/v2QGtteAqUk
video] to advertise the workshop. It was based on [R
http://anggtwu.net/LATEX/2018vichy-video.pdf these slides]. I took
the pentomino image from [R
http://puzzler.sourceforge.net/docs/pentominoes.html here].
[BR]
[STANDOUT [' [LFC]]] [R logic-for-children-2018.html Here] is its
[COLOR red unofficial page], that has [COLOR red lots] of links and
resources.
[BR]
[R http://www.uni-log.org/wk6-CHI.html Here] is the official page
of the workshop.
[BR]
[R http://anggtwu.net/LATEX/2017vichy-workshop.pdf Here] is its
original description and call for papers in PDF form.
]
[br ----------------------------------------]
[#
# (bsec "visualizing-gms-unilog-2018" "H2" "Visualizing Geometric Morphisms (talk at UniLog 2018)")
# (find-math-b-links "visualizing-gms-unilog-2018" "2018vichy-vgms-slides")
#]
[sec «visualizing-gms-unilog-2018» (to ".visualizing-gms-unilog-2018")
H2 Visualizing Geometric Morphisms (talk at UniLog 2018)]
[P [RIGHTFIG http://anggtwu.net/LATEX/2018vichy-vgms-slides.pdf
IMAGES/2018vichy-vgms.png]
A talk given at the workshop "[R
http://www.uni-log.org/wk6-CAT.html Categories and Logic]" in the
[R http://www.uni-log.org/vichy2018 UniLog 2018] in june 22, 2018.
[BR]
Its subtitle was "An application of the "[R
#logic-for-children-unilog-2018 Logic for Children]" project to
Category Theory".
[BR]
[R http://anggtwu.net/LATEX/2017visualizing-gms.pdf Abstract].
[BR]
[STANDOUT [' [VGM]]]
[R http://anggtwu.net/LATEX/2018vichy-vgms-slides.pdf Slides].
]
[br ----------------------------------------]
[#
# (bsec "zhas-for-children-2" "H2" "Planar Heyting Algebras for Children (2017)")
# (find-math-b-links "zhas-for-children-2" "2017planar-has-1")
# (find-math-b-links "zhas-for-children-2" "2019J-ops")
# (find-math-b-links "zhas-for-children-2" "2020J-ops-new")
# (find-math-b-links "zhas-for-children-2" "2021planar-HAs-2")
#]
[sec «zhas-for-children-2» (to ".zhas-for-children-2")
H2 Planar Heyting Algebras for Children (2017-) ]
[P [RIGHTFIG http://anggtwu.net/LATEX/2017planar-has-1.pdf
IMAGES/planar-has-2CGs.png]
Finite planar Heyting Algebras ("ZHA"s) are very good tools for
teaching Heyting Algebras [COLOR brown and Intuitionistic
Propositional Logic] to "children"; "children" here means "people
without mathematical maturity", in the sense that they are not able
to understand structures that are too abstract straight away, they
need particular cases first.]
[P This is going to be a series of three papers.]
[NARROW
[P [STANDOUT [<]PH1[>]] The [R
http://anggtwu.net/LATEX/2017planar-has-1.pdf first paper],
called "[COLOR red Planar Heyting Algebras for Children]", is
about intuitionistic logic and ZHAs, and about the relation
between ZHAs and topological semantics. It has been tested on real
"children" - sophomore CS students! - and it was published in the
[R http://www.sa-logic.org/start1.html South American Journal of
Logic], [R http://www.sa-logic.org/sajl-51.html vol.5, no.1].]
[# http://www.sa-logic.org/start1.html
#]
[# The first version of it that I submitted is [R
http://anggtwu.net/LATEX/2017planar-has-1-v1.pdf here] - it was
rejected by the referees. #]
[# PH2: #]
[P [STANDOUT [<]PH2[>]] [RIGHTFIG
http://anggtwu.net/LATEX/2021planar-HAs-2.pdf
IMAGES/planar-has-qms.png] The [R
http://anggtwu.net/LATEX/2021planar-HAs-2.pdf second paper],
called "[COLOR red Planar Heyting Algebras for Children 2:
J-Operators, Slashings, and Nuclei]", is about a way to visualize
nuclei on ZHAs; nuclei are the basis for building sheaves. There
is a version of it on arxiv, as [R
https://arxiv.org/abs/2001.08338 arXiv:2001.08338], and the
current version is [R
http://anggtwu.net/LATEX/2021planar-HAs-2.pdf here]. I am
rewriting some of its sections (for the n-th time).]
[# PH3: #]
[P [STANDOUT [<]PH3[>]] The third paper - with [R
http://reh.math.uni-duesseldorf.de/~arndt/ Peter Arndt], about
tools for visualizing some of the material about geometric
morphisms and sheaves in section A4 of Johnstone's [IT Sketches of
an Elephant] - is still in gestation, but the extended abstract
called "[R #missing-diagrams-elephant On some missing diagrams in
the Elephant]" ([R http://anggtwu.net/LATEX/2019oxford-abs.pdf
PDF]) - that I submitted to the [R http://www.cs.ox.ac.uk/ACT2019/
ACT2019] contains many of the ideas that will be on it.]
]
[br]
[P Related:
[BR] "[R #favorite-conventions On my favorite conventions...]" - a
broad view of the "for children" project, with concrete examples
(2020). [COLOR red Start by this!]
[BR] "[R #visualizing-gms-unilog-2018 Visualizing geometric
morphisms]" - my talk about the third paper at the
UniLog2018.
[BR] "[R #logic-for-children-unilog-2018 Logic for Children]"
- a workshop that I organized at the UniLog2018.
[R http://anggtwu.net/logic-for-children-2018.html Page],
[R https://youtu.be/v2QGtteAqUk video],
[R http://anggtwu.net/LATEX/2018vichy-video.pdf slides].
[BR] When I present this to "real" children who don't know
lambda notation we go through [R
http://anggtwu.net/LATEX/2018-1-LA-material.pdf this
material] first.
]
[#
I also gave a [R #visualizing-gms-unilog-2018 talk] about the
third paper in [R http://www.uni-log.org/vichy2018 UniLog2018];
its abstract is [R
http://anggtwu.net/LATEX/2017visualizing-gms.pdf here], and its
title is "Visualizing geometric morphisms".
[BR] [STANDOUT 2019nov26:] [R
http://anggtwu.net/LATEX/2020J-ops-new.pdf Here] is a draft
version of the second paper that is quite good. [R
http://anggtwu.net/LATEX/2017planar-has-2.pdf This old draft] is
very badly written.
[UL [LI The [R http://anggtwu.net/LATEX/2017planar-has-1.pdf first
paper] is about intuitionistic logic and ZHAs, and about the
relation between ZHAs and topological semantics; it has been
tested on real "children" (sophomore CS students!) and submitted.
[BR] [STANDOUT 2019jun03:] [R
http://anggtwu.net/LATEX/2017planar-has-1.pdf Here] is a version
with a much better introduction than the [R
http://anggtwu.net/LATEX/2017planar-has-1-v1.pdf first version]
that I submitted (and that was rejected).
]
[LI [RIGHTFIG http://anggtwu.net/LATEX/2020J-ops-new.pdf
IMAGES/planar-has-qms.png] The second paper is about a way to
visualize local operators on ZHAs; local operators are the base
for building sheaves.
[BR] [STANDOUT 2019nov26:] [R
http://anggtwu.net/LATEX/2019J-ops.pdf Here] is a draft version
of the second paper that is quite good. [R
http://anggtwu.net/LATEX/2017planar-has-2.pdf This old draft] is
very badly written.]
[LI The third paper - with [R
http://reh.math.uni-duesseldorf.de/~arndt/ Peter Arndt], about
tools for visualizing some of the material about geometric
morphisms and sheaves in section A4 of Johnstone's [IT Sketches of
an Elephant] - is still in gestation; see below.]
]
[P My submission to the [R http://www.cs.ox.ac.uk/ACT2019/ ACT2019],
"[R #missing-diagrams-elephant On some missing diagrams in the
Elephant]", is currently the best presentation of the material in
the third paper.
[BR]
I also gave a [R #visualizing-gms-unilog-2018 talk] about the third
paper in [R http://www.uni-log.org/vichy2018 UniLog2018]; its
abstract is [R http://anggtwu.net/LATEX/2017visualizing-gms.pdf
here], and its title is "Visualizing geometric morphisms".]
[P When I present this to "real" children who don't know lambda
notation we go through [R
http://anggtwu.net/LATEX/2018-1-LA-material.pdf this material]
first.]
[P [R http://anggtwu.net/LATEX/2017planar-has-1.pdf The first paper (revised version).]
[BR] [R http://anggtwu.net/LATEX/2020J-ops-new.pdf The second paper (working draft).]
[#
[BR] [R http://anggtwu.net/LATEX/2017planar-has-3.pdf The third paper (working draft).]
#]
[BR] Older drafts:
[# R http://anggtwu.net/LATEX/2017planar-has-1-v1.pdf The first paper (version submitted in 2017aug30).]
[R http://anggtwu.net/LATEX/2017planar-has.pdf 2017jun11],
[R http://anggtwu.net/LATEX/2016planar-has.pdf 2016dec18].
]
#]
[br ----------------------------------------]
[#
# (bsec "notes-on-notation" "H2" "Notes on notation (2017)")
#]
[sec «notes-on-notation» (to ".notes-on-notation")
H2 Notes on notation (2017)]
[P [RIGHTFIG http://anggtwu.net/LATEX/2017cwm.pdf IMAGES/2017cwm.png]
[IT "Different people have different measures for "mental space";
someone with a good algebraic memory may feel that an expression like
[<]...[>] is easy to remember, while I always think diagramatically,
and so what I do is that I remember this diagram [<]...[>] and I
reconstruct the formula from it."] ([R #idarct IDARCT])]
[P These are very informal notes showing my favourite ways to draw the
"missing diagrams" in MacLane's [R
https://en.wikipedia.org/wiki/Categories_for_the_Working_Mathematician
CWM], and my favourite choice of letters for them. Work in progress
changing often, contributions and chats welcome, etc. My plan is to do
something similar for parts of the [R
https://ncatlab.org/nlab/show/Elephant Elephant] next.]
[P [R http://anggtwu.net/LATEX/2017yoneda.pdf A skeleton for the Yoneda Lemma (PDF)].
[BR] [R http://anggtwu.net/LATEX/2017cwm.pdf Notes on notation: CWM (PDF)].
[BR] [R http://anggtwu.net/LATEX/2017elephant.pdf Notes on notation: Elephant (PDF)].
]
[br ----------------------------------------]
[#
# (bsec "ebl-2017" "H2" "IPL For Children and Meta-Children, or: How Archetypal Are ZHAs?")
#]
[sec «ebl-2017» (to ".ebl-2017")
H2 IPL For Children and Meta-Children, or: How Archetypal Are ZHAs? (2017)]
[P [RIGHTFIG http://anggtwu.net/LATEX/2017ebl-slides.pdf IMAGES/ebl2017.png]
This is a 20-minute talk that I gave in the
[R http://www.inf.ufg.br/ebl2017/ebl.html EBL2017] in 2017may09.
[BR] The full title is:
"Intuitionistic Propositional Logic For Children and Meta-Children,
or: How Archetypal Are Finite Planar Heyting Algebras?"
[BR] It is an introduction to the material in
[R #zhas-for-children-2 Planar Heyting Algebras for Children].
[BR] Abstract: [R http://anggtwu.net/LATEX/2017ebl-abs.pdf PDF].
[BR] Slides: [R http://anggtwu.net/LATEX/2017ebl-slides.pdf PDF]
[BR] Handouts: [R http://anggtwu.net/LATEX/2017ebl-handouts.pdf PDF].
]
[br ----------------------------------------]
[#
# (bsec "lclt" "H2" "Lambda-calculus, logics and translations (course, 2016-)")
#]
[sec «lclt» (to ".lclt")
H2 Lambda-calculus, logics and translations (course, 2016-)]
[P [RIGHTFIG http://anggtwu.net/LATEX/2018-1-LA-material.pdf
IMAGES/lclt.png] In 2016 I started giving a [IT very] introductory
course on lambda-calculus, types, intuitionistic propositional logic,
Curry-Howard, Categories, Lisp and Lua in the [R blergh.html campus]
where I work. The course is 2hs/week, has no prerequisites at all, has
no homework, and is usually attended by 2nd/3rd semester CompSci
students; they spend most of their time in class discussing and doing
exercises together in groups on a whiteboard.]
[P I have LaTeXed a part of the material; it's [R
http://anggtwu.net/LATEX/2018-1-LA-material.pdf here]. For
bibliography, images of the whiteboards, etc, go [R 2017.2-LA.html
here].]
[br ----------------------------------------]
[#
# (bsec "zhas-for-children" "H2" "Intuitionistic Logic for Children, or: Planar Heyting Algebras for Children (2015)")
#]
[sec «zhas-for-children» (to ".zhas-for-children")
H2 Intuitionistic Logic for Children, or: Planar Heyting Algebras for Children (2015)]
[P [RIGHTFIG http://anggtwu.net/LATEX/2015planar-has.pdf IMAGES/zhasforchildren.png]
Seminar notes, with lots of figures (all drawn with [R dednat6.html Dednat6]).
[BR] Not self-contained. Superseded by [R #zhas-for-children-2 this].
[BR] I never wrote a textual abstract for this, but the page 2 of the
[R http://anggtwu.net/LATEX/2015planar-has.pdf PDF] is a nice "One
page intro" with text and diagrams.
[BR]
[BR] [R http://anggtwu.net/LATEX/2015planar-has.pdf The PDF is here]
(and [R dednat6/tests/4.pdf here]).
[BR] Current version: 2015oct19b.
[BR] (First version: 2015sep24.)
]
[br ----------------------------------------]
[#
# (bsec "istanbul" "H2" "Logic and Categories, or: Heyting Algebras for Children (2015)")
#]
[sec «istanbul» (to ".istanbul")
H2 Logic and Categories, or: Heyting Algebras for Children (2015)]
[P [RIGHTFIG http://anggtwu.net/LATEX/2014istanbul-a.pdf IMAGES/new-girl-from-ipanema-mini.png]
A tutorial presented at the [R http://www.uni-log.org/start5.html
UniLog 2015] conference (Istanbul), 20-22/jun/2015.
[BR] Abstract: [R http://anggtwu.net/LATEX/2014istanbul-a.pdf PDF],
[R http://www.uni-log.org/t5-cat.html HTML].
[BR] Slides: [R http://anggtwu.net/LATEX/istanbul1.pdf PDF].
[BR] Handouts: [R http://anggtwu.net/LATEX/istanbul-handouts.pdf PDF].
[BR] Notes on a meaning for "for children": [R http://anggtwu.net/LATEX/2015children.pdf PDF].
]
[br ----------------------------------------]
[#
# (bsec "sheaves-for-children" "H2" "Sheaves for children (2014)")
#]
[NAME sfc]
[sec «sheaves-for-children» (to ".sheaves-for-children")
H2 Sheaves for children (2014)]
[P [RIGHTFIG http://anggtwu.net/LATEX/2014sfc-slides.pdf IMAGES/2014-evil-presheaf.png]
A 20-minute talk - [R http://anggtwu.net/LATEX/2014sfc-slides.pdf
here are its slides] - presented at the [R
http://www.uff.br/ebl/ebl_program.html XIV] [R http://www.uff.br/ebl/
EBL], on 2014apr09. Its [R
http://anggtwu.net/LATEX/2014sfc-abstract.pdf abstract]:]
[lua:
def [[ SUP 1 body "$body" ]]
def [[ catD 1 _ BF"D" ]]
def [[ Set 1 _ BF"Set" ]]
def [[ SetD 1 _ Set()..SUP(catD()) ]]
]
[NARROW
[P First-year university students - the ``children'' of the title
- often prefer to start from an interesting particular case, and
only then proceed to general statements. How can we make
intuitionistic logic, toposes, and sheaves accessible to them?]
[P Let [IT D] be a finite subset of N[SUP 2]. Draw arrows for all
the ``black pawns moves'' between points of [IT D], and let [catD]
be the poset generated by that graph; [catD] is what we call a
``ZDAG'', and [SetD] is a ``ZDAG-topos''. It turns out that the
truth-values of a [SetD] can be represented in a very nice way as
two-dimensional ASCII diagrams, and that all the operations leading
to sheaves and geometric morphisms can be understood via algorithms
on diagrams.]
[P In this talk we will present a computer library for performing
computations interactively on the truth-values of ZDAG-toposes. The
diagrams are rendered in ASCII by default, but there is a module
that typesets them in LaTeX.]
]
[P The second - and much longer - version of this talk (at the [R
http://www.rio-logic.org/seminar.html Seminário Carioca de
Lógica], 2014may19, 15:00, [R
http://maps.google.com/maps?f=q&q=Instituto+de+Filosofia+e+Ciencias+Sociais,+Rio+de+Janeiro
IFCS]) had [R http://anggtwu.net/LATEX/2014sfc-slides2.pdf these
slides] and [R http://anggtwu.net/LATEX/2014sfc-slides2h.pdf these
handouts], and was meant for much younger "children". The focus this
time was a visual characterization of the subsets of N[SUP 2] that are
Heyting Algebras, and how can we treat their points as truth-values,
and so how to interpret intuitionistic logic on them. I call these
subsets "ZHAs", the definitions and main theorems for them are in the
pages 20 to 27 of the [R http://anggtwu.net/LATEX/2014sfc-slides2.pdf
slides], and also at the [R
http://anggtwu.net/LATEX/2014sfc-slides2h.pdf handouts].]
[RULE ----------------------------------------]
[#
# (bsec "sheaves-on-zdags" "H2" "Sheaves on Finite DAGs may be Archetypal (2011)")
# (find-math-b-links "sheaves-on-zdags")
#]
[sec «sheaves-on-zdags» (to ".sheaves-on-zdags")
H2 Sheaves on Finite DAGs may be Archetypal (2011)]
[# (find-wdg40w3m "special/img.html" "The ALIGN attribute")
#]
[P [RIGHTFIG http://anggtwu.net/MINICATS/sheaves_for_children__1_to_7.pdf IMAGES/omega-kite.png]
Can the ideas of my article about "[R #internal-diags-in-ct internal
diagrams]" be used to present the basic concepts of toposes and
sheaves starting from simple, "archetypal" examples? I believe so, but
this is still a work in progress!]
[P Here are 7 pages of [IT very nice]
handwritten notes (titled "Sheaves for Children"):
[R MINICATS/sheaves_for_children__1_to_7.pdf pdf],
[R MINICATS/sheaves_for_children__1_to_7.djvu djvu].
They were written after discussions with Hugo Luiz Mariano and Claus
Akira Matsushige Horodynski in feb/2012, during a minicourse on CT in
Brasilia organized by Claus, with me and Hugo as lecturers...]
[P ...and [R LATEX/2011ebl-abs.pdf here] are some slightly older notes
- I submitted them, in a admittedly incomplete form, to the [R
http://www.cle.unicamp.br/ebl2011/ XVI EBL], with [R
LATEX/2011ebl-booklet-abs.pdf this abstract] - and then I did a bad
job at presenting them; [R LATEX/2011ebl-slides.pdf here] are the
slides, they cover only the first ideas =(.]
[P For the sake of completeness, here are some handwritten diagrams
describing Kan extensions in an (hopefully) archetypal case,
motivated by discussions with [R
https://ncatlab.org/nlab/show/Guilherme+Frederico+Lima G.F. Lima]:
[R SCANS/ochs_kan_2011apr02_1200dpi.djvu 1200dpi djvu],
[R SCANS/ochs_kan_2011apr02_600dpi.djvu 600dpi djvu],
[R SCANS/ochs_kan_2011apr02_600dpi.pdf 600dpi pdf].]
[RULE ----------------------------------------]
[#
# (bsec "internal-diags-in-ct" "H2" "Internal Diagrams in Category Theory (2010)")
# (find-math-b-links "internal-diags-in-ct" "internal-diags-in-ct")
# (find-math-b-links "idarct" "idarct-preprint")
# (find-math-b-links "idarct" "idarct")
#]
[NAME idarct]
[sec «internal-diags-in-ct» (to ".internal-diags-in-ct")
H2 Internal Diagrams in Category Theory (2010/2013) ]
[# https://link.springer.com/article/10.1007/s11787-013-0083-z
#]
[P [RIGHTFIG http://anggtwu.net/LATEX/idarct-preprint.pdf
IMAGES/idarct.png]
[STANDOUT [' [IDARCT]]]
A [R LATEX/idarct-preprint.pdf paper] that I published at [R
https://www.springer.com/journal/11787 [IT Logica Universalis]] in
its [R http://link.springer.com/journal/11787/7/3/page/1 special
issue on Categorical Logic] in 2013.
[BR] The [R
https://link.springer.com/article/10.1007/s11787-013-0083-z
published version] has some weirdly-sized figures and some ugly
page breaks. The [R LATEX/idarct-preprint.pdf preprint] is much
better.
[BR] Here is its abstract:]
[NARROW
[P We can regard operations that discard information, like
specializing to a particular case or dropping the intermediate steps
of a proof, as [IT projections], and operations that reconstruct
information as [IT liftings]. By working with several projections in
parallel we can make sense of statements like "[BF Set] is the
archetypal Cartesian Closed Category", which means that proofs about
CCCs can be done in the "archetypal language" and then lifted to
proofs in the general setting. The method works even when our
archetypal language is diagrammatical, has potential ambiguities, is
not completely formalized, and does not have semantics for all
terms. We illustrate the method with an example from hyperdoctrines
and another from synthetic differential geometry.]
]
[P This was my first "real" paper.]
[P For my talk at the UniLog 2010 ([R #unilog-2010 below]) I prepared
a HUGE [R http://anggtwu.net/LATEX/2010unilog-current.pdf set of
slides], and after chatting with several people at the conference I
understood that the best way to try to publish those ideas would be to
focus on the philosophical side and to leave out most technicalities
(e.g., fibrations)... so I wrote "Internal Diagrams in Category
Theory" and submitted it to LU. The referees told me to change some
things in it, including the title, and to split the paper in two.
Instead of splitting it I wrote some new sections to explain how its
two "halves" were connected, and this became "Internal Diagrams and
Archetypal Reasoning in Category Theory".]
[P I abandoned the idea of "downcasings" after some years - now I use
internal diagrams and particular cases. See [R #zhas-for-children-2
here] and [R logic-for-children-2018.html here].]
[# http://article.gmane.org/gmane.science.mathematics.categories/5991
#]
[P (2013) [R LATEX/idarct-preprint.pdf Internal Diagrams and
Archetypal Reasoning in Category Theory]
[BR] (2010) [R LATEX/2010diags.pdf Internal Diagrams in Category
Theory]
]
[RULE ----------------------------------------]
[#
# (bsec "unilog-2010" "H2" "Downcasing Types (at UniLog'2010)")
#]
[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 of 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].
[BR] First official release of the slides (2010jun21, 100 pages):
[__ unilog2010-1.pdf pdf].
[BR] Latest version of the slides (109 pages): [__
unilog2010-slides.dvi dvi], [__ unilog2010-slides pdf].
]
[# P I am still adding things to the set of slides that I prepared for
that presentation.]
[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]
]
[#
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
SetI/F→SetI/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.)]
[P Note (2010): [IT I still don't have the tools for formalizing this
idea completely.] As what I have is an "incomplete internal language",
the ideas in [R #internal-diags-in-ct this preprint] may help.]
[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]
[P I moved them to [R math-old-links.html this page].]
[RULE ---------------------------------------------------------------------]
[# (find-math-b-links "PhD" "NONE")
#]
[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 lots of holes) in August, 2003 and
presented the final version - filling out [IT some] 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!) #] (FEBF/UERJ), and also trying to finish a
very important Free Software project that I've been working on
since 1999 ([R index.html#eev GNU eev]).]
[P [BF The thesis] is in Portuguese and [IT you don't want to see it]. Really. =(
[# - 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 (2010/2013): [R #idarct this paper] has all the ideas from my
PhD thesis, plus some! It fills all the gaps from the thesis, and it
is quite well written =).]
[P News (October 2005): I gave 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://anggtwu.net/math/2001a.ps.gz
http://anggtwu.net/math/2001b.ps.gz
http://anggtwu.net/math/2001F.ps.gz
#]
[RULE ------------------------------------------------------------------]
[br ----------------------------------------]
[#
# (bsec "MsC" "H1" "MsC Thesis and related things ")
# (find-math-b-links "MsC" "../math/tesemestr")
#]
[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 [STANDOUT 2017set19]: update: since mid-2015 I'm using [R
dednat6.html Dednat6], LuaLaTeX and [R
https://www.ctan.org/pkg/pict2e?lang=en pict2e] for all my diagrams.]
[P My PhD thesis included lots of hairy categorical diagrams, and I
ended up writing a LaTeX preprocessor in Lua - called "dednat4.lua" -
to help me typeset them. Below are some examples of diagrams that I
have typeset with dednat4:]
[lua:
def [[ TABLE 1 text "\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"
]]
]
[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/downcasing_Ax.png]
[DIAGTEXT Downcasing A×
[BR] (three views)]
]
[# TD [IMG IMAGES/eqfib-trans.png]
[DIAGTEXT Proving transitivity
[BR] in an EqFibration
[BR] (slightly wrong)]
]
]
]
[P Note that dednat4 is obsolete, and that the diagrams above use an
obsolete notation - the notation for "downcasings" from [R #idarct
IDARCT]...]
[# dednat4/examples/eqfibs.metatex.html here #]
[# 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 [R
eev-intros/find-psne-intro.html 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 emacs-lisp-mode)
# End:
#]