% (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: