% (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 1‡X    |         | (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: