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

% (find-angg "LATEX/2013idct-changes.tex") % (find-dn4ex "edrx08.sty") % (find-angg ".emacs.templates" "s2008a") % (defun c () (interactive) (find-zsh "cd ~/LATEX/ && latex 2013idct-changes.tex")) % (defun c () (interactive) (find-zsh "cd ~/LATEX/ && pdflatex 2013idct-changes.tex")) % (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2013idct-changes.tex && latex 2013idct-changes.tex")) % (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2013idct-changes.tex && pdflatex 2013idct-changes.tex")) % (defun d () (interactive) (find-xdvipage "~/LATEX/2013idct-changes.dvi")) % (eev "cd ~/LATEX/ && Scp 2013idct-changes.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/") % (find-xdvipage "~/LATEX/2013idct-changes.dvi") % (find-pspage "~/LATEX/2013idct-changes.ps") % (find-pspage "~/LATEX/2013idct-changes.pdf") % (find-xpdfpage "~/LATEX/2013idct-changes.pdf") % (find-evincepage "~/LATEX/2013idct-changes.pdf") % (find-zsh0 "cd ~/LATEX/ && dvipdf 2013idct-changes.dvi 2013idct-changes.pdf") % (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2013idct-changes.ps 2013idct-changes.dvi") % (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2013idct-changes.ps 2013idct-changes.dvi && ps2pdf 2013idct-changes.ps 2013idct-changes.pdf") % (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi") % (find-pspage "~/LATEX/tmp.ps") % (ee-cp "~/LATEX/2013idct-changes.pdf" (ee-twupfile "LATEX/2013idct-changes.pdf") 'over) % (ee-cp "~/LATEX/2013idct-changes.pdf" (ee-twusfile "LATEX/2013idct-changes.pdf") 'over) % (find-twusfile "LATEX/" "2013idct-changes") % http://angg.twu.net/LATEX/2013idct-changes.pdf \documentclass[oneside]{book} \usepackage[latin1]{inputenc} \usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref") \usepackage{breakurl} % (find-es "tex" "breakurl") \usepackage{edrx08} % (find-dn4ex "edrx08.sty") %L process "edrx08.sty" -- (find-dn4ex "edrx08.sty") \input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex") \begin{document} %\input {stem}.dnt % (find-angg ".emacs" "idct") % (find-idctpage 15 "12. Hyperdoctrines") { \footnotesize \setlength{\parindent}{0em} \par {\bf Extra sections for the} \par {\bf ``Internal Diagrams in Category Theory'' paper ---} \par {\bf part of a fuller set of changes, corrections, explanations ---} \par {\bf first version, 2013apr05} \par {\bf Eduardo Ochs, eduardoochs@gmail.com} \msk \par This: \url{http://angg.twu.net/LATEX/2013idct-changes.pdf} \par the paper: \url{http://angg.twu.net/LATEX/2013idct-changes.pdf} } \bsk \section*{11.50. Skeletons of proofs} Let's call the ``projected'' version of a mathematical object its ``skeleton''. The underlying idea in this paper is that for the {\sl right kinds} of projections, and for {\sl some kinds} of mathetical objects, it should be possible to reconstruct enough of the original object from its skeleton and few extra clues --- just like paleontologists can reconstruct from a fossil skeleton the look of an animal when it was alive. Now the irresistible questions are: which kinds of objects do have skeletons? What do these skeletons look like? How does the reconstruction process work, and how much of it can be performed by computers? When is it that the liftings become ambiguous, what kinds of hints are needed, and how should we specify them? And in what situations is this idea doomed to fail, because for each non-trivial way of separating the object's data into ``skeleton'' and ``non-skeleton'' something doesn't work? Answering all this in a general setting is obviously a daunting task. A first natural step, though, is to start from a handful of natural examples --- and then say: these are our archetypal examples of skeletons, projections, and liftings. How do we formalize and generalize what we got here? In the section [18.25. The syntactical world] we will sketch an approach that {\sl may} yield a reasonbably rich family of examples: namely, that on a sizeable fragment of Category Theory all definitions can be split into a {\sl structure} part plus {\sl properties}, and each theorem into a {\sl construction} plus an {\sl equational part}. A big part of Mathematics is definitions plus theorems --- and in that fragment of Category Theory these can be clearly split into a ``syntactical'' skeleton, with just the ``structures'' and ``constructions'', plus, on top of that, a reconstructible, ``equational'' flesh. We will call the system with just this skeleton the ``syntactical world''. It would be very hard to explain precisely the general ideas here before first showing a language on which they can make sense, so we will now look at some examples. We will have to use hyperdoctrines, even though they are weaker, less familiar, and harder to define than toposes; that's because of technical difficulties that we will discuss in section [18.75 The problem with toposes]. % (find-idctpage 15 "12. Hyperdoctrines") % \section*{18.25. Projecting out the equational part} % \section*{18.25. The real world and the syntactical world} \section*{18.25. The syntactical world} We can now explain our archetypal projection: the one from the ``real world'' to the ``syntactical world'' for a fragment of Category Theory, that we mentioned in section [11.50. Skeletons of proofs]. We have been avoiding all mentions to equations between morphisms --- for example, in the section [9. Adjunctions] we glossed over the usual standard requirement that $f^{\sharp\flat} = f$. That was deliberate. % (find-854 "" "abstract") \msk A category $\catC$ is a 7-uple, % $$\catC = (\catC_0, \Hom_\catC, \id_\catC, ¢_\catC; \assoc_\catC, \idL_\catC, \idR_\catC)$$ % where the three last components are assurances that the composition $¢_\catC$ is associative and that the identities behave as expected with respect to composition at the left and the right. These three last components are exactly the ones whose typings --- all this can be formalized in an adequate type system --- involve equalities of morphisms. By dropping them we get what we will call the {\sl proto-category} associated to $\catC$: % $$\catC^- = (\catC_0, \Hom_\catC, \id_\catC, ¢_\catC)$$ % The same idea can be applied to lots of categorical structures. We can define, in a similar way, proto-functors, proto-natural transformations, proto-isos, proto-adjunctions, proto-products, proto-terminals, proto-exponentials, proto-cartesian-closed categories, a proto-Yoneda lemma, proto-fibrations, and so on. Also, it turns out that many categorical proofs can be projected onto their corresponding ``proto-proofs'', by dropping all parts that involve equalities of morphisms --- and the resulting proto-proofs keep the {\it constructions} of the original proofs, but leave out the diagram chasings. This is explained in great detail, with many diagrams, at the course notes [\url{http://angg.twu.net/math-b.html\#unilog-2010}]. \section*{18.50. Formalizing diagrams in Type Theory} \def\f{} \def\g{{\ov}} We saw at sections [3. Downcased Types] and [7. Functors] how to make each downcased ``name'' stand for both a ``name'' and its ``meaning''. In our downcased categorical diagrams, each node and each arrow has a definite meaning as a categorical entity; so, let's consider each node and arrow in a downcased diagram a {\sl diagrammatical name}. Note that diagrammatic names are {\sl positional} --- in the sense that entities with the same apparent names but at different positions of a diagram are allowed to have different meanings. That happened, for example, in the diagram at p.22, where both $\f^*\g^*(\f^*Q)$ and $\f^*Q$ became $\ssst{a,b}{Qabb}$ --- abbreviated to a `$Qabb$' above an `$a,b$' --- in the downcasing. % (find-angg ".emacs" "idct") % (find-idctpage 22 "Qabb") % (find-idctfile "" "Frob-5") % --- objects, morphisms, categories, functors, etc, are ``entities''. \msk Now take any downcased diagram $D$, and draw two {\sl copies} of it, one above another, like this: % $$\begin{matrix} D \\ \dnto \\ D^- \end{matrix}$$ Let's take the positionality of names a step further. At the top diagram, $D$, all meanings are in the ``real world'', and are non-proto categorical entities. At the lower diagram, $D^-$, in the ``syntactical world'', each meaning is the proto-categorical entity corresponding to the non-proto entity above. For example, the meanings for an iso arrow `$a,b \bij b,a$' will be just a pair $(\ang{'_{AB},_{AB}}, \ang{'_{BA},_{BA}})$ in the syntactical world, but in the real world it will be this plus the assurances that both composites are identities. Suppose that we tag with a different number --- in light gray, say --- each node and each arrow in the diagram $D \to D^-$; for example, our two copies of `$a,b \bij b,a$' may get tagged as `$\bij_{2099}$' in the real-world diagram, and as `$\bij_{99}$' in the syntactical world. With this we get numerical suffixes that we can use for the corresponding terms, and in the formalization of that diagram in a proof assistant the terms {\tt flip\_AB\_99} and {\tt flip\_AB\_2099} will, by convention, stand for the proto-iso and for the iso respectively. \msk % An important point to notice is that each node and arrow in each of % our diagrams stands for a definite categorical entity --- objects, % morphisms, categories, functors, etc, are ``entities'' ---, and the % downcased language has been designed to let each diagram be a % blueprint for a formalization --- in a type system, and thus on % proof assistants --- of a construction. % At the lower % diagram, $D^-$, we will be at the syntactical world, and all meanings % will be proto-categorial entities; the corres % then in the lower copy, that we are calling $D^-$, each node or arrow % will stand for a proto-entity, and the corresponding node or arrow in % $D$ will stand for the corresponding non-proto-entity. This notation % is obviously positional: two different arrows with similar names, say, % `$a \mto b'$, at different positions in the full diagram will usually % stand for different objects in the formalization of the diagram in % Type Theory. A primitive way to implement this on proof assistants is % easy to describe: [example - $a \bij b \bij c$?] % ---------------------------------------- \section*{18.75 The problem with toposes} {\sl Elementary toposes} are very simple to define --- an elementary topos is just a CCC with pullbacks and a classifier object --- and it is well-known that they are exactly the categorical models for a certain (intuitionistic) fragment of Set Theory. Why did we have to resort to clumsy hyperdoctrines? % What are our reasons for using hyperdoctrines instead? The problem is that we can't define {\sl classifier object} without defining {\sl monic arrow} first; all my attempts to find a usable definition of ``proto-monic'' have failed rather miserably, so I can't rely on either ``proto-classifiers'' or ``proto-toposes''. This means that if I had to stick with toposes I wouldn't be able to apply the idea of ``projection into the syntactical world'' to the metatheory, i.e., to the categorical models for the polymorphic type theory needed to formalize the projection from the real world into the syntactical world. \msk [Todo: explain that the classifier object in a topos induces a hyperdoctrine structure on the underlying CCC, and it is that structure which is needed for interpreting first-order logic with equality there; the details are not as well-known as they should, and to add polymorphism we need to add extra structure which is even less familiar. I believe that these and other results in categorical semantics can become much more accessible with the use of diagrams in a downcased language, as in the sections [12. Hyperdoctrines] and [17. Objects of line type]; the diagrams for these semantics, translations, and their computer implementations are high-priority future work.] % ...is that there doesn't seem to be any good way to define what a % proto-monic should be, and thus the classifier object axiom is also % impossible... % % but hyperdoctrines (or them with a universal object for % polymorphism) are enough for 1st order logic... % A subtle point: topos % % split monics % % that should be interesting in i % % we can then use to study more general phenomena - namely, % % possible way to approach the % singleton map % metalanguage \end{document} % Local Variables: % coding: raw-text-unix % ee-anchor-format: "«%s»" % End: