Warning: this is an htmlized version!
The original is across this link, and the conversion rules are here. |

% (find-angg "LATEX/2009unilog-abs0.tex") % (find-dn4ex "edrx08.sty") % (find-angg ".emacs.templates" "s2008a") % (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009unilog-abs0.tex && latex 2009unilog-abs0.tex")) % (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009unilog-abs0.tex && pdflatex 2009unilog-abs0.tex")) % (eev "cd ~/LATEX/ && Scp 2009unilog-abs0.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/") % (defun d () (interactive) (find-dvipage "~/LATEX/2009unilog-abs0.dvi")) % (find-dvipage "~/LATEX/2009unilog-abs0.dvi") % (find-pspage "~/LATEX/2009unilog-abs0.pdf") % (find-pspage "~/LATEX/2009unilog-abs0.ps") % (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2009unilog-abs0.ps 2009unilog-abs0.dvi") % (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2009unilog-abs0.ps 2009unilog-abs0.dvi && ps2pdf 2009unilog-abs0.ps 2009unilog-abs0.pdf") % (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi") % (find-pspage "~/LATEX/tmp.ps") % (ee-cp "~/LATEX/2009unilog-abs0.pdf" (ee-twupfile "LATEX/2009unilog-abs0.pdf") 'over) % (ee-cp "~/LATEX/2009unilog-abs0.pdf" (ee-twusfile "LATEX/2009unilog-abs0.pdf") 'over) \documentclass[oneside]{book} \usepackage[latin1]{inputenc} \usepackage{edrx08} % (find-dn4ex "edrx08.sty") %L process "edrx08.sty" -- (find-dn4ex "edrx08.sty") \input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex") \begin{document} \input 2009unilog-abs0.dnt %*% (eedn4-51-bounded) %Index of the slides: %\msk % To update the list of slides uncomment this line: %\makelos{tmp.los} % then rerun LaTeX on this file, and insert the contents of "tmp.los" % below, by hand (i.e., with "insert-file"): % (find-fline "tmp.los") % (insert-file "tmp.los") \widemtos \def\sof#1{\{\,#1\,\}} \def\sst#1#2{\{\,#1\;|\;#2\,\}} \def\ssst#1#2{\{\,#1\;||\;#2\,\}} \def\psst#1#2{(\,#1\;||\;#2\,)} \def\psst#1#2{(#1\;||\;#2)} \def\dsst#1#2{#1\;||\;#2} \def\dsst#1#2{#1||#2} \def\Sub{¯{Sub}} {\bf Downcasing Types} Proto-abstract, 2009nov04 \bsk When we represent a category $\catC$ in Type Theory it becomes a 7-uple: $(\catC_0, \Hom_\catC, \id_\catC, ¢_\catC; Ð{assoc}_\catC, Ð{idL}_\catC, Ð{idR}_\catC)$, where the first four components are ``structure'' and the last three are ``properties''. We can define a ``protocategory'', $\catC^-$, as a 4-uple $(\catC_0, \Hom_\catC, \id_\catC, ¢_\catC)$ --- just the ``syntactical part'' of $\catC$, leaving out the ``logical part'' --- and we can do the same for functors, natural transformations, adjunctions, isos, limits, and so on. We can take many constructions and proofs from the ``real world'' --- where entities have both their ``syntactical'' and their ``logical'' parts --- and project them onto the ``syntactical world'' --- by keeping only their syntactical parts. The projections can be seen as the ``syntactical skeletons'' of the real entities, and they are especially amenable to diagrammatic representation. There is a simple way to attribute a precise meaning to each entity --- nodes, arrows, etc --- in each such diagrammatic representations, and we will show how to formalize two such diagrams --- the proof of the Yoneda lemma and the definition of monadic functor --- in Coq. For most applications in Categorical Semantics one further trick is needed: ``downcasing types'' --- for example, a morphism $f: A \to B$ is ``downcased'' to $a \mto b$. In a hyperdoctrine, if $P$ is an object over $B×C$, then $P$ ``is'' a subset $\ssst{(b,c)}{P(b,c)}$ of $B×C$. The downcasing of $P$ is $\psst{b,c}{P(b,c)}$, and the Beck-Chevalley Condition for $\forall$ says that the natural morphism from $f^* \Pi_{\pi_{BC}} P$ to $\Pi_{\pi_{AC}} (f×C)^* P$ should be an iso... in the downcasing, this becomes $\psst{a}{ýc.P(fa,c)} \mto \psst{a}{ýc.P(fa,c)}$... however, if we give a unique tag to each node and arrow and define the BCC morphism by a diagram showing its construction, then the BCC morphism becomes an iso between the two objects that ``are'' the same {\sl in the archetypal hyperdoctrine}, $\Sub(\Set)$. Roughly, what is the happening is the following: the formal definition of hyperdoctrine generalizes {\sl some} of the structure of $\Sub(\Set)$; with our way of interpreting diagrams we can define all this structure diagrammatically, in a notation that suggests that we are in $\Sub(\Set)$ (we say: ``in the archetypical case''), and then we can ``lift'' these definitions to diagrams with the same two-dimensional structure, but in any of the standard notations. Several categorical theorems become quite clear when we find an archetypical diagram for their (proto-)proofs, and then we lift that to standard notation; one example is $\_\_\_$. % (find-books "__cats/__cats.el" "jacobs") \bsk [Note for the referees: this paper is not about proving new theorems --- it is just about formalizing a language that might make old theorems clearer, and that might help constructing dictionaries between standard notations, and with formalizing categorical proofs in proof assistants. I would like to be able to characterize, for example, when a proof done in the ``syntactical world'' can be lifted to the ``real world'' --- but this looks as a distant goal at the moment. My guess is that a good first step towards that would be to formalize the realtion between the ``real world'' and the ``syntactical world'' in terms of the language of institutions --- but for that I would have try to have first a notion of proto-institution and (maybe) an archetype for institutions, and I haven't had the time to learn enough about institutions yet...] %*\end{document} % Local Variables: % coding: raw-text-unix % ee-anchor-format: "«%s»" % End: