Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% (find-angg "LATEX/2009-nd-in-hyps.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009-nd-in-hyps.tex && latex    2009-nd-in-hyps.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009-nd-in-hyps.tex && pdflatex 2009-nd-in-hyps.tex"))
% (eev "cd ~/LATEX/ && Scp 2009-nd-in-hyps.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2009-nd-in-hyps.dvi"))
% (find-dvipage "~/LATEX/2009-nd-in-hyps.dvi")
% (find-pspage  "~/LATEX/2009-nd-in-hyps.pdf")
% (find-pspage  "~/LATEX/2009-nd-in-hyps.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2009-nd-in-hyps.ps 2009-nd-in-hyps.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2009-nd-in-hyps.ps 2009-nd-in-hyps.dvi && ps2pdf 2009-nd-in-hyps.ps 2009-nd-in-hyps.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2009-nd-in-hyps.pdf" (ee-twupfile "LATEX/2009-nd-in-hyps.pdf") 'over)
% (ee-cp "~/LATEX/2009-nd-in-hyps.pdf" (ee-twusfile "LATEX/2009-nd-in-hyps.pdf") 'over)

% (find-LATEX "2009unilog-dnc.tex")
% (find-LATEX "2009unilog-dnc.tex" "hyperdoctrines")

% \documentclass[oneside]{book}
\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")

\input 2009-nd-in-hyps.dnt

% (eedn4-51-bounded)

%Index of the slides:
% To update the list of slides uncomment this line:
% 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")

% (find-LATEX "2009unilog-dnc.tex" "hyperdoctrines")


A {\sl hyperdoctrine} is a cloven fibration $p: \bbE \to \bbB$
with some extra structure:

(1) the base category $\bbB$ is a CCC,

(2) each fiber $\bbE_B$ is a CCC,

(3) for each ``first projection'' map $\pi \equiv (a,b \mto a)$ in
$bbB$ the associated ``weakening'' functor $\pi^*: \bbE_A \to \bbE_{A×B}$
has a left and a right adjoints,

(4) for each ``duplication'' map $\delta \equiv (b \mto b,b')$ in
$bbB$ the associated ``contraction'' functor $\delta^*: \bbE_{B×B} \to
\bbE_B$ has a left and a right adjoints, $Æ_\delta \dashv f* \dashv

 $Æ_\pi \dashv f* \dashv å_\pi$,

(3) a left adjoint, $Æ_f \dashv f*$,

(4) a right adjoint, $f^* \dashv å_f$,

and each change-of base functor $f^*$ preserves, modulo iso,

(5) the terminal,

(6) binary products,

(7) exponentials,

and furthermore the following three ``technical conditions'' hold:

(8) Beck-Chevalley for ``exists'',

(9) Beck-Chevalley for ``forall'',

(10) Frobenius.



% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End: