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