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