[RULE ----------------------------------------] [# # (bsec "internal-diags-in-ct" "H2" "Internal Diagrams in Category Theory (2010)") #] [NAME idarct] [sec «internal-diags-in-ct» (to ".internal-diags-in-ct") H2 Internal Diagrams in Category Theory (2010)] [P A paper submitted to [R http://article.gmane.org/gmane.science.mathematics.categories/5991 [IT Logica Universalis]], and published in their [R http://link.springer.com/journal/11787/7/3/page/1 special issue on Categorical Logic in 2013], with a longer name: "[R LATEX/idarct-preprint.pdf Internal Diagrams and Archetypal Reasoning in Category Theory]". 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 The [R LATEX/idarct-preprint.pdf paper] was produced from the material that I created for the talk [R #unilog-2010 below]. The [R http://angg.twu.net/LATEX/2010unilog-current.pdf slides] covers much more ground, but the paper explains the ideas much more clearly. The revised version (2013), that has more sections and more words in the title: "[R LATEX/idarct-preprint.pdf Internal Diagrams and Archetypal Reasoning in Category Theory]" (if you prefer a [R LATEX/idarct-preprint.dvi .dvi], it needs this [R LATEX/frob-sketch.eps .eps]). The original version (just "Internal Diagrams in Category Theory", 2010) is [R LATEX/2010diags.pdf here].] [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 the [__ ashes volcanic ashes] many people could not fly to Portugal, and from [__ unilog2010-handbook all these programmed talks] only [__ unilog2010-sched these] ended up happening. The abstract was:] [NARROW [P When we represent a category C in a type system it becomes a 7-uple, whose first four components - class of objects, Hom, id, composition - are "structure"; the other three components are "properties", and only these last three involve equalities of morphisms.] [P We can define a projection that keeps the "structure" and drops the "properties" part; it takes a category and returns a "proto-category", and it also acts on functors, isos, adjunctions, proofs, etc, producing proto-functors, proto-proofs, and so on.] [P We say that this projection goes from the "real world" to the "syntactical world"; and that it takes a "real proof", P, of some categorical fact, and returns its "syntactical skeleton", P-. This P- is especially amenable to diagrammatic representations, because it has only the constructions from the original P --- the diagram chasings have been dropped.] [P We will show how to "lift" the proto-proofs of the Yoneda Lemma and of some facts about monads and about hyperdoctrines from the syntactical world to the real world. Also, we will show how each arrow in our diagrams is a term in a precise diagrammatic language, and how these diagrams can be read out as definitions. The "downcased" diagrams for hyperdoctrines, in particular, look as diagrams about Set (the archetypical hyperdoctrine), yet they state the definition of an arbitrary hyperdoctrine, plus (proto-)theorems.] ] [P (A longer version of the abstract: [__ unilog2010-abs1 pdf].)] [P First official release of the slides (2010jun21, 100 pages): [# [__ unilog2010-1.dvi dvi],] [__ unilog2010-1.pdf pdf].] [P 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 Set

\n" ..text.."\n |