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

% (find-angg "LATEX/2009unilog-abs1.tex") % (find-dn4ex "edrx08.sty") % (find-angg ".emacs.templates" "s2008a") % (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009unilog-abs1.tex && latex 2009unilog-abs1.tex")) % (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009unilog-abs1.tex && pdflatex 2009unilog-abs1.tex")) % (eev "cd ~/LATEX/ && Scp 2009unilog-abs1.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/") % (defun d () (interactive) (find-dvipage "~/LATEX/2009unilog-abs1.dvi")) % (find-dvipage "~/LATEX/2009unilog-abs1.dvi") % (find-pspage "~/LATEX/2009unilog-abs1.pdf") % (find-pspage "~/LATEX/2009unilog-abs1.ps") % (find-xpdfpage "~/LATEX/2009unilog-abs1.pdf") % (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2009unilog-abs1.ps 2009unilog-abs1.dvi") % (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -o 2009unilog-abs1.ps 2009unilog-abs1.dvi && ps2pdf 2009unilog-abs1.ps 2009unilog-abs1.pdf") % (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2009unilog-abs1.ps 2009unilog-abs1.dvi && ps2pdf 2009unilog-abs1.ps 2009unilog-abs1.pdf") % (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi") % (find-pspage "~/LATEX/tmp.ps") % (ee-cp "~/LATEX/2009unilog-abs1.pdf" (ee-twupfile "LATEX/2009unilog-abs1.pdf") 'over) % (ee-cp "~/LATEX/2009unilog-abs1.pdf" (ee-twusfile "LATEX/2009unilog-abs1.pdf") 'over) % (find-LATEX "2009unilog-dnc.tex") \documentclass[oneside]{book} \usepackage[latin1]{inputenc} \usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref") \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-abs1.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 {\bf Downcasing Types} (Abstract sent to UNILOG'2010) % http://www.uni-log.org/start3.html % http://www.uni-log.org/ss3-CAT.html Eduardo Ochs - LLaRC, PURO/UFF, Brazil eduardoochs@gmail.com \ssk For more details see: \url{http://angg.twu.net/LATEX/2009unilog-dnc.pdf} \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 call the ``structure'' components the ``syntactical part'', and the ``properties'' components the ``logical part''. A {\sl protocategory} is a 4-uple $(\catC_0, \Hom_\catC, \linebreak[1] \id_\catC, ¢_\catC)$ --- just the ``syntactical skeleton'' of what a category is, without the components that talk about equality of morphisms. By splitting at the right places the uples that represent functors, natural transformations, isos, adjunctions, limits, etc, we define proto-functors, proto-NTs, and so on. The operation that takes entities and returns the corresponding proto-entities behaves as a projection, and we say that it goes from the ``real world'' --- where everything has both a ``syntactical'' and a ``logical'' part --- to the ``syntactical world'', where only the syntactical parts have been kept. The opposite of to {\sl project} is to {\sl lift}. We may start with a proto-something, $s^-$, in the syntactical world, and try to lift it to an $s$ in the real world that projects into $s^-$. Meta-theorems about lifting are hard to obtain, but we know many interesting liftings --- each object $r$ of the (projectable fragment of the) real world projects to an proto-object $r^-$ that can be lifted back to $r$ --- and we can start by studying them to understand how liftings behave. % about lifting are hard to obtain, but each object of the % (projectable fragment of the) real world may be lifted by first % constructing its projection and then ``completing'' it using % information from the original object. Proto-objects --- even proto-proofs --- are especially amenable to being represented diagrammatically, and there is a simple way to attribute a precise meaning to each entity --- each node, arrow, etc --- appearing in these diagrams. We will show how to formalize two such diagrammatic proofs --- the Yoneda Lemma and one of the weakest monadicity theorems --- as terms in Coq. \def\Sub{\text{Sub}} \def\BCCL{f^* \Pi_{\pi_{BC}} P} \def\BCCR{\Pi_{\pi_{AC}} (f×C)^* P} \def\BCCS{\ssst{aİA}{ıcİC.P(fa,c)}} \def\psst#1#2{(#1\;||\;#2)} \def\psst#1#2{#1||#2} \def\bccp{\psst{a}{ıc.P(fa,c)}} \def\bcc{\psst{a}{ıc.P(fa,c)}} \def\bcca{\psst{a}{ıc.P}} \def\bccbc{\psst{b,c}{P}} For most applications in Categorical Semantics one further trick is needed: ``downcasing types'', that lets us name entities by what they represent in the ``archetypical case''. For example, in a hyperdoctrine, if $P$ is an object over $B×C$ and $f:A \to B$ then Beck-Chevalley Condition for `$\forall$' says that the natural morphism from $\BCCL$ to $\BCCR$ should be an iso. In the archetypical hyperdoctrine, $\Sub(\Set)$, $P$ ``is'' a subset $\sst{(b,c)İB×C}{P(b,c)}$ of $B×C$, and both $\BCCL$ and $\BCCR$ ``deserve the name'' $\sst{aİA}{ıcİC.\,P(fa,c)}$. The downcasing of $P$ is $\psst{b,c}{P}$, and the BCC map becomes a map $\bcca \mto \bcca$ that is not the identity, whose construction can be read out from a diagram. % \msk % in the notation coming from the ``archetypal hyperdoctrine'' % $\Sub(\Set)$ % In the downcasing, this becomes $\psst{a}{ıc.P(fa,c)} \mto % \psst{a}{ıc.P(fa,c)}$, which looks like an identity map; 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)$, i.e., ``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 ``archetypical diagrams'' for their (proto-)proofs, and then we lift those to standard notations; we will show some examples from Lawvere's ``Adjointness in Foundations'' (1969) and ``Equality in Hyperdoctrines'' (1970) papers. % (find-books "__cats/__cats.el" "jacobs") % (find-books "__cats/__cats.el" "borceux") % (find-angg ".emacs.papers" "barr") % (find-angg ".emacs.papers" "beck") % (find-angg "LATEX/2008hyp.tex") % (find-angg "LATEX/2008hyp.tex" "frob-for-equality-2") % (find-angg "LATEX/2008hyp.tex" "frob-for-equality-2" "EqTP-lawvere67") % (find-dvipage "~/LATEX/2008hyp.dvi" 34) % (find-pspage "~/LATEX/2008hyp.ps" 34) % (find-angg "LATEX/2009dnc-monads.tex") %*\end{document} % Local Variables: % coding: raw-text-unix % ee-anchor-format: "«%s»" % End: