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

% «.2»	(to "2")

\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 2008kocknsext.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")

% (eev-math-glyph-names "Delta" 916 "eta" 951 "mu" 956 "nu" 957)
% (eev-math-glyph-names "gamma" 947 "phi" 966 "pf" 5862)
% Greek:      (find-einsert '((913 987)))
% Pitchforks: (find-einsert '(8916 5862))
% (find-amsguidepage 19 "\\ulcorner")
% (find-amsguidepage 22 "\\pitchfork")
% (eev-math-glyphs-set 'eev-glyph-face-math  "nabla   " "na"    "")
% (eev-math-glyphs-set 'eev-glyph-face-greek "theta nu" "te nu" " Û")
% (eev-math-glyphs-set 'eev-glyph-face-greek   "Delta"         "DD"    "")
% (eev-math-glyphs-set 'eev-glyph-face-greek   "phi gamma"     "ph gg" " ")
% (eev-math-glyphs-set 'eev-glyph-face-logical "ulcorn urcorn pf" "ul ur pf" "  ")

\def\myttchars{%
  \ttchars%
  \def{\ttchar{$\Delta$}}%
  \def{\ttchar{$\gamma$}}%
  \def{\ttchar{$\phi$}}%
  \def{\ttchar{$\ulcorner$}}%
  \def{\ttchar{$\urcorner$}}%
  \def{\ttchar{$\pitchfork$}}%
  \def{\ttchar{${}^{-1}$}}
  \def{\ttchar{${}^{\text{-\!1}}$}}
  }


{\myttchars
\footnotesize
\begin{verbatim}
Anders Kock and C. J. Mikkelsen,
Topos theoretic factorization of
non-standard extensions,
SLNM 369, pp.122--143; 1974.

Notation:

    A -----> 1       A×A <--| A               A ------> 1
    v _|     v        |       |               v _|      v     
   |        |    _A |  |->  | {}_A   {}_A |         |
    v   _A  v        v       v               v   s_A   v
   A×A ---->          |--> ^A             ^A ----->     


   A <---> 1×A <---| 1    
       \    |        |    
      f \   |  <-->  | f
         v  v        v    
            B |---> B^A   

    A -----> 1            A <---> 1×A <---| 1    
    v _|     v                \    |        |    
 id |        | true     true_A \   |  <-->  | true_A
    v        v                  v  v        v    
    A ----->                       |---> ^A   
      true_A

    Y |----> Y^X              B^A --> (^B)^A
    |         |                | _|      |
  g |   |->   | g^X, or 1X    |         | (s_B)^A
    v         v                v         v
    Z |----> Z^X               1 -----> ^A
                                true_A

          _f                   (f)      
   \P(A) ----> \P(B)       ^A ------> ^B

          f                     ^f      
   \P(A) <---- \P(B)       ^A <------ ^B

          _f                   (f)      
   \P(A) ----> \P(B)       ^A ------> ^B

           f                      f     
      A ------> B            A ------> B
\end{verbatim}
}

\newpage
% --------------------
% «2»  (to ".2")
% (s "page 2" "2")
\myslide {page 2} {2}

{\myttchars
\footnotesize
\begin{verbatim}
   _A ---->> (2) ----> 1     ^A×B <---| ^A
    v   \      v _|     v       |          |
    |    \     |        |   (3) |   <->    | (f)
    v     v    v        v       v          |
  ^A×A ---> ^A×B --->         |-----> ^B
                   (3)

            (1_\E) =
   1_\E |---> 1_\E_0 ---> 1_\E_0
    v           v _|        v
    | true_\E   |           |
    v           v          v
   _\E |--> (_\E) --> _\E_0

         
    \E -----> \E_0


(2.4) \hat_A,B: (A->B) -> ((A)->(B))
      is the "externalizer":

      (A->B)^\U -> (A^\U->B^\U)

      in particular:

      (A->)^\U >-> (A^\U->)
\end{verbatim}
}



%*

\end{document}

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