[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") #] [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://angg.twu.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://angg.twu.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 Set

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