% (find-angg "LATEX/2008topos-str.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008topos-str.tex && latex    2008topos-str.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008topos-str.tex && pdflatex 2008topos-str.tex"))
% (eev "cd ~/LATEX/ && Scp 2008topos-str.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008topos-str.dvi")
% (find-pspage  "~/LATEX/2008topos-str.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2008topos-str.ps 2008topos-str.dvi")
% (find-pspage  "~/LATEX/2008topos-str.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")

% «.biccc-and classifier»	(to "biccc-and classifier")
% «.pre-hyperdoctrine»		(to "pre-hyperdoctrine")
% «.topos-ccompc»		(to "topos-ccompc")
% «.nnos-basic-constructions»	(to "nnos-basic-constructions")
% «.nnos-p-prime»		(to "nnos-p-prime")


\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 2008topos-str.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")
\tocline {The BiCCC structure and the classifier axiom} {2}
\tocline {The pre-hyperdoctrine structure} {3}
\tocline {Two CCompC structures in a topos} {4}
\tocline {Basic constructions with NNOs} {5}
\tocline {NNOs: the morphism $\kappa $} {6}

%:&\&

\newpage
% --------------------
% «biccc-and classifier»  (to ".biccc-and classifier")
% (s "The BiCCC structure and the classifier axiom" "biccc-and classifier")
\myslide {The BiCCC structure and the classifier axiom} {biccc-and classifier}

%D diagram CCC
%D 2Dx    100     +25     +25  +15  +20      +25
%D 2D 100     --| p0 |-	       t0   a0 <==== a1
%D 2D	     /    -    \       -     -        -
%D 2D	    /     |	\      |     |  <-->  |
%D 2D	   v      v	 v     v     v	      v
%D 2D +25 p1 <--| p2 |--> p3   t1   a2 ====> a3
%D 2D
%D 2D +15 c0 |--> c1 <--| c2   i0
%D 2D      /      -	 \     -
%D 2D       \     |	/      |
%D 2D        \    v    /       v
%D 2D +25     --> c3 <-	       i1
%D 2D
%D ((            p0 .tex=  a
%D    p1 .tex= b p2 .tex= b,c p3 .tex= c
%D    @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D    @ 1 @ 2 <-| @ 2 @ 3 |->
%D ))
%D (( c0 .tex= a c1 .tex= a÷b c2 .tex= b
%D               c3 .tex=  c
%D    @ 0 @ 1 |-> @ 1 @ 2 <-|
%D    @ 0 @ 3 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D ))
%D (( t0 .tex= a t1 .tex= *
%D    @ 0 @ 1 |->
%D ))
%D (( i0 .tex= ® i1 .tex= a
%D    @ 0 @ 1 |->
%D ))
%D (( a0 .tex= a,b a1 .tex= a
%D    a2 .tex=  c  a3 .tex= b|->c
%D    @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram

%D diagram HA
%D 2Dx    100     +25     +25  +15  +20      +25
%D 2D 100     --| p0 |-	       t0   a0 <==== a1
%D 2D	     /    -    \       -     -        -
%D 2D	    /     |	\      |     |  <-->  |
%D 2D	   v      v	 v     v     v	      v
%D 2D +25 p1 <--| p2 |--> p3   t1   a2 ====> a3
%D 2D
%D 2D +15 c0 |--> c1 <--| c2   i0
%D 2D      /      -	 \     -
%D 2D       \     |	/      |
%D 2D        \    v    /       v
%D 2D +25     --> c3 <-	       i1
%D 2D
%D ((            p0 .tex=  P
%D    p1 .tex= Q p2 .tex= Q&R p3 .tex= R
%D    @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D    @ 1 @ 2 <-| @ 2 @ 3 |->
%D ))
%D (( c0 .tex= P c1 .tex= PQ c2 .tex= Q
%D               c3 .tex=  R
%D    @ 0 @ 1 |-> @ 1 @ 2 <-|
%D    @ 0 @ 3 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D ))
%D (( t0 .tex= P t1 .tex= {§}
%D    @ 0 @ 1 |->
%D ))
%D (( i0 .tex= ® i1 .tex= P
%D    @ 0 @ 1 |->
%D ))
%D (( a0 .tex= P&Q a1 .tex= P
%D    a2 .tex=  R  a3 .tex= Q¶R
%D    @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram

%D diagram Topos
%D 2Dx     100       +25    +20       +25
%D 2D 100  pb0 |---> pb1    cl0 |---> cl1
%D 2D      -  __|     -     v  __|     v 
%D 2D      |          |     | --\      | 
%D 2D      v          v     v    v     v 
%D 2D +25  pb2 |---> pb3    cl2 |---> cl3
%D 2D
%D (( pb0 .tex= (a,b)|_c pb1 .tex= b
%D    pb2 .tex= a        pb3 .tex= c
%D    @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D    # @ 0 _|
%D      @ 0 relplace 8 8 \pbsymbol{7}
%D ))
%D (( cl0 .tex= a|_P cl1 .tex= *
%D    cl2 .tex= a    cl3 .tex= Ï
%D    @ 0 @ 1 |-> @ 0 @ 2 >-> @ 1 @ 3 >-> .plabel= r § @ 2 @ 3 |-> .plabel= a P
%D    # @ 0 _|
%D      @ 0 relplace 8 8 \pbsymbol{7}
%D ))
%D enddiagram

CCC:

$\diag{CCC}$

\medskip

HA:

$\diag{HA}$

\medskip

Topos:

\smallskip

$\diag{Topos}$

\newpage
% --------------------
% «pre-hyperdoctrine»  (to ".pre-hyperdoctrine")
% (s "The pre-hyperdoctrine structure" "pre-hyperdoctrine")
\myslide {The pre-hyperdoctrine structure} {pre-hyperdoctrine}

%D diagram Hyperdoctrine
%D 2Dx     100      +30  +30        +45   +35        +40
%D 2D 100                eq0 =====> eq1   aw0 =====> aw1
%D 2D                     -          -     -          -    
%D 2D                     |   <-->   |     |   <-->   |    
%D 2D         |--->       v          v     v          v    
%D 2D +30  s0 <==== s1   eq2 <===== eq3   aw2 <===== aw3
%D 2D                                      -          - 
%D 2D                                      |   <-->   | 
%D 2D                                      v          v 
%D 2D +30                                 aw4 =====> aw5
%D 2D                                                      
%D 2D +20  s2 |---> s3   eq4 |----> eq5   aw6 |----> aw7   
%D
%D (( s0 .tex= \s[a|P]   s1 .tex= \s[b|P]
%D    @ 0 @ 1 <=  sl_  @ 0 @ 1 |-> sl^ .plabel= a {ñ}
%D ))
%D (( s2 .tex= a    s3 .tex= b
%D    @ 0 @ 1 |->
%D ))
%D (( eq0 .tex= \s[a,b|P]          eq1 .tex= \s[a,b,b'|b{=}b'&P]
%D    eq2 .tex= \s[a,b|{Q[b,b]}]   eq3 .tex= \s[a,b,b'|{Q[b,b']}]
%D    @ 0 @ 1 => sl_  @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D    @ 2 @ 3 <= sl_  @ 2 @ 3 |-> sl^ .plabel= a {ñ}
%D    @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D (( eq4 .tex= a,b      eq5 .tex= a,b,b'
%D    @ 0 @ 1 |->
%D ))
%D (( aw0 .tex= \s[a,b|P]   aw1 .tex= \s[a|Îb.P]
%D    aw2 .tex= \s[a,b|Q]   aw3 .tex= \s[a|Q]
%D    aw4 .tex= \s[a,b|R]   aw5 .tex= \s[a|ýb.R]
%D    @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D    @ 2 @ 3 <= sl_ @ 2 @ 3 |-> sl^ .plabel= a {ñ}
%D    @ 4 @ 5 => 
%D    @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <->
%D    @ 2 @ 4 |-> @ 3 @ 5 |-> @ 2 @ 5 harrownodes nil 20 nil <->
%D ))
%D (( aw6 .tex= a,b              aw7 .tex= a
%D    @ 0 @ 1 |->
%D ))
%D enddiagram

%D diagram LCCC
%D 2Dx     100      +30  +30        +45   +35        +40
%D 2D 100                eq0 =====> eq1   aw0 =====> aw1   
%D 2D                     -          -     -          -    
%D 2D                     |   <-->   |     |   <-->   |    
%D 2D         |--->       v          v     v          v    
%D 2D +30  s0 <==== s1   eq2 <===== eq3   aw2 <===== aw3   
%D 2D                                      -          - 
%D 2D                                      |   <-->   | 
%D 2D                                      v          v 
%D 2D +30                                 aw4 =====> aw5
%D 2D                                                      
%D 2D +20  s2 |---> s3   eq4 |----> eq5   aw6 |----> aw7   
%D
%D (( s0 .tex= \s[a|c]   s1 .tex= \s[b|c]
%D    @ 0 @ 1 <=  sl_  @ 0 @ 1 |-> sl^ .plabel= a {ñ}
%D ))
%D (( s2 .tex= a    s3 .tex= b
%D    @ 0 @ 1 |->
%D ))
%D (( eq0 .tex= \s[a,b|c]          eq1 .tex= \s[a,b,b'|(b{=}b'),c]
%D    eq2 .tex= \s[a,b|d]   eq3 .tex= \s[a,b,b'|d]
%D    @ 0 @ 1 => sl_  @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D    @ 2 @ 3 <= sl_  @ 2 @ 3 |-> sl^ .plabel= a {ñ}
%D    @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D (( eq4 .tex= a,b      eq5 .tex= a,b,b'
%D    @ 0 @ 1 |->
%D ))
%D (( aw0 .tex= \s[a,b|c]   aw1 .tex= \s[a|b,c]
%D    aw2 .tex= \s[a,b|d]   aw3 .tex= \s[a|d]
%D    aw4 .tex= \s[a,b|e]   aw5 .tex= \s[a|{b|->e}]
%D    @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D    @ 2 @ 3 <= sl_ @ 2 @ 3 |-> sl^ .plabel= a {ñ}
%D    @ 4 @ 5 => 
%D    @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <->
%D    @ 2 @ 4 |-> @ 3 @ 5 |-> @ 2 @ 5 harrownodes nil 20 nil <->
%D ))
%D (( aw6 .tex= a,b              aw7 .tex= a
%D    @ 0 @ 1 |->
%D ))
%D enddiagram

Hyperdoctrine:

\smallskip

$\diag{Hyperdoctrine}$

\medskip

LCCC:

\smallskip

$\diag{LCCC}$

\newpage
% --------------------
% «topos-ccompc»  (to ".topos-ccompc")
% (s "Two CCompC structures in a topos" "topos-ccompc")
\myslide {Two CCompC structures in a topos} {topos-ccompc}

The two CCompC structures in a topos:

%D diagram CCompHyp
%D 2Dx     100      +30      +30
%D 2D  100 a0 |---> a1 |---> a2
%D 2D      ||   ^   /\   ^   ||
%D 2D      ||   |   ||   |   ||
%D 2D      \/   v   ||   v   \/
%D 2D  +30 a3 |---> a4 |---> a5
%D 2D
%D ((  a0 .tex= \s[a|P]  a1 .tex= \s[b|§]  a2 .tex= \s[c|Q]
%D     a3 .tex= a        a4 .tex= b        a5 .tex= c|_Q
%D     @ 0 @ 1 |-> @ 1 @ 2 |->
%D     @ 0 @ 3 =>  @ 1 @ 4 <=  @ 2 @ 5 => 
%D     @ 0 @ 4 varrownodes nil 20 nil <->
%D     @ 1 @ 5 varrownodes nil 20 nil <->
%D     @ 3 @ 4 |-> @ 4 @ 5 |->
%D ))
%D enddiagram

%D diagram CCompLCCC
%D 2Dx     100      +30      +30
%D 2D  100 a0 |---> a1 |---> a2
%D 2D      ||   ^   /\   ^   ||
%D 2D      ||   |   ||   |   ||
%D 2D      \/   v   ||   v   \/
%D 2D  +30 a3 |---> a4 |---> a5
%D 2D
%D ((  a0 .tex= \s[a|b]  a1 .tex= \s[c|*]  a2 .tex= \s[d|e]
%D     a3 .tex= a        a4 .tex= c        a5 .tex= d,e
%D     @ 0 @ 1 |-> @ 1 @ 2 |->
%D     @ 0 @ 3 =>  @ 1 @ 4 <=  @ 2 @ 5 => 
%D     @ 0 @ 4 varrownodes nil 20 nil <->
%D     @ 1 @ 5 varrownodes nil 20 nil <->
%D     @ 3 @ 4 |-> @ 4 @ 5 |->
%D ))
%D enddiagram
%D
$$\diag{CCompHyp} \qquad \diag{CCompLCCC}$$

\medskip

Cartesian morphisms project into pullbacks:

%D diagram display1
%D 2Dx     100     +30     +30    +30     +30     +30    +30     +45     +45
%D 2D  100         a0   /                 q0   /                 e0   /     
%D 2D           // || /\ \             // || \\ \             // || \\ \    
%D 2D          //  ||  \\ v           //  ||  \\ v           //  ||  \\ v   
%D 2D         \/   \/   \\           \/   \/   \/           \/   \/   \/    
%D 2D  +30 a2 |--> a3      a1     q2 |--> q3      q1     e2 |--> e3      e1 
%D 2D          /      / // ||        /       / // ||        /       / // ||
%D 2D           \      //  ||         \       //  ||         \       //  ||
%D 2D            v    \/ v \/          v     \/ v \/          v     \/ v \/
%D 2D  +30         a4 |--> a5             q4 |--> q5             e4 |--> e5
%D 2D
%D (( a0 .tex= \s[a|P] a1 .tex= \s[b|P]
%D    a2 .tex= a|_P    a3 .tex= a
%D    a4 .tex= b|_P    a5 .tex= b
%D    @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a {ñ}
%D    @ 0 @ 2 => @ 0 @ 3 => @ 1 @ 4 => @ 1 @ 5 =>
%D    @ 2 @ 3 |-> @ 2 @ 4 |-> @ 3 @ 5 |-> @ 4 @ 5 |->
%D    @ 2 relplace 16 6 \pbsymbol{7}
%D ))
%D enddiagram

%D diagram displayLCCC1
%D 2Dx     100     +30     +30    +30     +30     +30    +30     +45     +45
%D 2D  100         a0   /                 q0   /                 e0   /     
%D 2D           // || /\ \             // || \\ \             // || \\ \    
%D 2D          //  ||  \\ v           //  ||  \\ v           //  ||  \\ v   
%D 2D         \/   \/   \\           \/   \/   \/           \/   \/   \/    
%D 2D  +30 a2 |--> a3      a1     q2 |--> q3      q1     e2 |--> e3      e1 
%D 2D          /      / // ||        /       / // ||        /       / // ||
%D 2D           \      //  ||         \       //  ||         \       //  ||
%D 2D            v    \/ v \/          v     \/ v \/          v     \/ v \/
%D 2D  +30         a4 |--> a5             q4 |--> q5             e4 |--> e5
%D 2D
%D (( a0 .tex= \s[a|c] a1 .tex= \s[b|c]
%D    a2 .tex= a,c    a3 .tex= a
%D    a4 .tex= b,c    a5 .tex= b
%D    @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a {ñ}
%D    @ 0 @ 2 => @ 0 @ 3 => @ 1 @ 4 => @ 1 @ 5 =>
%D    @ 2 @ 3 |-> @ 2 @ 4 |-> @ 3 @ 5 |-> @ 4 @ 5 |->
%D    @ 2 relplace 16 6 \pbsymbol{7}
%D ))
%D enddiagram

$$\diag{display1} \qquad \diag{displayLCCC1}$$

\medskip

%D diagram display2
%D 2Dx     100     +30     +30    +30     +30     +30    +30     +45     +45
%D 2D  100         a0   /                 q0   /                 e0   /     
%D 2D           // || /\ \             // || \\ \             // || \\ \    
%D 2D          //  ||  \\ v           //  ||  \\ v           //  ||  \\ v   
%D 2D         \/   \/   \\           \/   \/   \/           \/   \/   \/    
%D 2D  +30 a2 |--> a3      a1     q2 |--> q3      q1     e2 |--> e3      e1 
%D 2D          /      / // ||        /       / // ||        /       / // ||
%D 2D           \      //  ||         \       //  ||         \       //  ||
%D 2D            v    \/ v \/          v     \/ v \/          v     \/ v \/
%D 2D  +30         a4 |--> a5             q4 |--> q5             e4 |--> e5
%D 2D
%D (( q0 .tex= \s[a,b|P]   q1 .tex= \s[a|Îb.P]
%D    q2 .tex= a,b|_P      q3 .tex= a,b
%D    q4 .tex= a|_{Îb.P}   q5 .tex= a
%D    @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D    @ 0 @ 2 => @ 0 @ 3 => @ 1 @ 4 => @ 1 @ 5 =>
%D    @ 2 @ 3 |-> @ 2 @ 4 |->> @ 3 @ 5 |-> @ 4 @ 5 |->
%D ))
%D (( e0 .tex= \s[a,b|P]           e1 .tex= \s[a|b{=}b'&P]
%D    e2 .tex= a,b|_P              e3 .tex= a,b
%D    e4 .tex= a,b,b'|_{b{=}b'&P}  e5 .tex= a,b,b'
%D    @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D    @ 0 @ 2 => @ 0 @ 3 => @ 1 @ 4 => @ 1 @ 5 =>
%D    @ 2 @ 3 |-> @ 2 @ 4 <-> @ 3 @ 5 `-> @ 4 @ 5 |->
%D ))
%D enddiagram

%D diagram displayLCCC2
%D 2Dx     100     +30     +30    +30     +30     +30    +30     +45     +45
%D 2D  100         a0   /                 q0   /                 e0   /     
%D 2D           // || /\ \             // || \\ \             // || \\ \    
%D 2D          //  ||  \\ v           //  ||  \\ v           //  ||  \\ v   
%D 2D         \/   \/   \\           \/   \/   \/           \/   \/   \/    
%D 2D  +30 a2 |--> a3      a1     q2 |--> q3      q1     e2 |--> e3      e1 
%D 2D          /      / // ||        /       / // ||        /       / // ||
%D 2D           \      //  ||         \       //  ||         \       //  ||
%D 2D            v    \/ v \/          v     \/ v \/          v     \/ v \/
%D 2D  +30         a4 |--> a5             q4 |--> q5             e4 |--> e5
%D 2D
%D (( q0 .tex= \s[a,b|c]   q1 .tex= \s[a|b,c]
%D    q2 .tex= (a,b),c     q3 .tex= a,b
%D    q4 .tex= a,(b,c)     q5 .tex= a
%D    @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D    @ 0 @ 2 =>  @ 0 @ 3 =>  @ 1 @ 4 =>  @ 1 @ 5 =>
%D    @ 2 @ 3 |-> @ 2 @ 4 <-> @ 3 @ 5 |-> @ 4 @ 5 |->
%D ))
%D (( e0 .tex= \s[a,b|c]             e1 .tex= \s[a|(b{=}b'),c]
%D    e2 .tex= a,b,c                 e3 .tex= a,b
%D    e4 .tex= a,b,b',(b{=}b'),c     e5 .tex= a,b,b'
%D    @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D    @ 0 @ 2 => @ 0 @ 3 => @ 1 @ 4 => @ 1 @ 5 =>
%D    @ 2 @ 3 |-> @ 2 @ 4 <-> @ 3 @ 5 `-> @ 4 @ 5 |->
%D ))
%D enddiagram
%D

Cocartesian morphisms induce isos and epis:
$$\diag{display2}$$
$$\diag{displayLCCC2}$$

\newpage
% --------------------
% «nnos-basic-constructions»  (to ".nnos-basic-constructions")
% (s "Basic constructions with NNOs" "nnos-basic-constructions")
\myslide {Basic constructions with NNOs} {nnos-basic-constructions}

% (find-eoutput '(insert 8760))
%:-.{\overset{.}{-}}

\widemtos

%D diagram NNO+
%D 2Dx     100    +40    +45    +45   +45
%D 2D  100 * |--> 0 |--> 1 |--> 2     m
%D 2D        /    -      -      -     -
%D 2D         \   |      |      |     |
%D 2D          v  v      v      v     v
%D 2D  +30       a0 |-> a1 |-> a2    am
%D 2D
%D (( a0 .tex= (n|->n)  a1 .tex= (n|->n{+}1) a2 .tex= (n|->n{+}2)
%D    am .tex= n|->n{+}m
%D    *  0 |->  0  1 |->  1  2 |->
%D    * a0 |-> a0 a1 |-> a1 a2 |->
%D              0 a0 |->  1 a1 |-> 2 a2 |-> m am |->
%D ))
%D enddiagram
%D
$$\diag{NNO+}$$

%D diagram NNO*
%D 2Dx     100    +40    +45    +45   +45
%D 2D  100 * |--> 0 |--> 1 |--> 2     m
%D 2D        /    -      -      -     -
%D 2D         \   |      |      |     |
%D 2D          v  v      v      v     v
%D 2D  +30       a0 |-> a1 |-> a2    am
%D 2D
%D (( a0 .tex= (n|->0)  a1 .tex= (n|->n) a2 .tex= (n|->2n)
%D    am .tex= n|->mn
%D    *  0 |->  0  1 |->  1  2 |->
%D    * a0 |-> a0 a1 |-> a1 a2 |->
%D              0 a0 |->  1 a1 |-> 2 a2 |-> m am |->
%D ))
%D enddiagram
%D
$$\diag{NNO*}$$

%D diagram NNOexp
%D 2Dx     100    +40    +45    +45   +45
%D 2D  100 * |--> 0 |--> 1 |--> 2     m
%D 2D        /    -      -      -     -
%D 2D         \   |      |      |     |
%D 2D          v  v      v      v     v
%D 2D  +30       a0 |-> a1 |-> a2    am
%D 2D
%D (( a0 .tex= (n|->1)  a1 .tex= (n|->n) a2 .tex= (n|->n^2)
%D    am .tex= n|->n^m
%D    *  0 |->  0  1 |->  1  2 |->
%D    * a0 |-> a0 a1 |-> a1 a2 |->
%D              0 a0 |->  1 a1 |-> 2 a2 |-> m am |->
%D ))
%D enddiagram
%D
$$\diag{NNOexp}$$

%D diagram NNO-
%D 2Dx     100    +40    +45    +45   +45
%D 2D  100 * |--> 0 |--> 1 |--> 2     m
%D 2D        /    -      -      -     -
%D 2D         \   |      |      |     |
%D 2D          v  v      v      v     v
%D 2D  +30       a0 |-> a1 |-> a2    am
%D 2D
%D (( a0 .tex= (n|->n)  a1 .tex= (n|->n-.1) a2 .tex= (n|->n-.2)
%D    am .tex= n|->n-.m
%D    *  0 |->  0  1 |->  1  2 |->
%D    * a0 |-> a0 a1 |-> a1 a2 |->
%D              0 a0 |->  1 a1 |-> 2 a2 |-> m am |->
%D ))
%D enddiagram
%D
$$\diag{NNO-}$$


\newpage
% --------------------
% «nnos-p-prime»  (to ".nnos-p-prime")
% (s "NNOs: the morphism $p'$" "nnos-p-prime")
\myslide {NNOs: the morphism $p'$} {nnos-p-prime}

\def\kk{\kappa}

%:+{+}

Fact: in a topos with NNO the map $[0,s]: 1{+}N \to N$ is an iso.

\msk

First we need to define the arrow $s': 1{+}N \to 1{+}N$,

using a factorization through a coproduct.

Note that $s'$ takes the `$*$' in `$*÷n$' to 0, not to $*'$.

$s' := [0;\kk',s;\kk']$.

%D diagram NNO-sprime
%D 2Dx     100 +20 +20 +20 +20
%D 2D  100 a0 ---> a2 <--- a4
%D 2D        \     |      /
%D 2D         v    |     v
%D 2D  +20     b1  |   b3
%D 2D            \ |  /
%D 2D             vv v
%D 2D  +20         c2
%D 2D
%D (( a0 .tex= 1  a2 .tex= 1+N a4 .tex= N
%D    b1 .tex= N               b3 .tex= N
%D                c2 .tex= 1+N
%D    a0 a2 -> .plabel= a \kk a2 a4 <- .plabel= a \kk'
%D    a0 b1 -> .plabel= l 0   b1 c2 -> .plabel= l \kk'
%D    a2 c2 -> .plabel= m s'
%D    a4 b3 -> .plabel= r s
%D    b3 c2 -> .plabel= r \kk'
%D ))
%D enddiagram
%D
%D diagram NNO-sprime-dnc
%D 2Dx     100 +20 +20 +20 +20
%D 2D  100 a0 ---> a2 <--- a4
%D 2D        \     |      /
%D 2D         v    |     v
%D 2D  +20     b1  |   b3
%D 2D            \ |  /
%D 2D             vv v
%D 2D  +20         c2
%D 2D
%D (( a0 .tex= *  a2 .tex= *÷n a4 .tex= n
%D    b1 .tex= 0               b3 .tex= n+1
%D                c2 .tex= *'÷n+1
%D    a0 a2 -> a2 a4 <-
%D    a0 b1 -> b1 c2 -> a2 c2 -> a4 b3 -> b3 c2 ->
%D ))
%D enddiagram

\msk

$\diag{NNO-sprime} \qquad \diag{NNO-sprime-dnc}$

\bsk

Now we can define $p': N \to 1+N$ by factoring $(\kk, s')$ through the NNO.

It is possible to show that $p'$ and $[0,s]$ are inverses.

%D diagram NNO+1
%D 2Dx     100     +30      +30     +30   +30
%D 2D  100 a0 ---> a1 ----> a2 ---> a3    a4
%D 2D      | \     |        |       |     |
%D 2D      |  \    |        |       |     |
%D 2D      |   \   v        v       v     v
%D 2D  +20  \   -> b1 ----> b2 ---> b3    b4
%D 2D        \     |        |       |     |
%D 2D         \    |        |       |     |
%D 2D          \   v        v       v     v
%D 2D  +20      -> c1 ----> c2 ---> c3    c4
%D 2D
%D (( a0 .tex= 1 a1 .tex= N   a2 .tex=   N a3 .tex=   N a4 .tex= N
%D               b1 .tex= 1+N b2 .tex= 1+N b3 .tex= 1+N b4 .tex= 1+N
%D               c1 .tex= N   c2 .tex=   N c3 .tex=   N c4 .tex= N
%D    a0 a1 -> .plabel= a 0
%D             a1 a2 -> .plabel= a s  a2 a3 -> .plabel= a s
%D             b1 b2 -> .plabel= a s' b2 b3 -> .plabel= a s'
%D             c1 c2 -> .plabel= a s  c2 c3 -> .plabel= a s
%D    a0 b1 -> .plabel= m \kk
%D             a1 b1 -> .plabel= r p'
%D             a2 b2 -> .plabel= r p'
%D             a3 b3 -> .plabel= r p'
%D             a4 b4 -> .plabel= r p'
%D    a0 c1 -> .plabel= l 0
%D             b1 c1 -> .plabel= r [0,s]
%D             b2 c2 -> .plabel= r [0,s]
%D             b3 c3 -> .plabel= r [0,s]
%D             b4 c4 -> .plabel= r [0,s]
%D ))
%D enddiagram
%D
$$\diag{NNO+1}$$

%D diagram NNO+1-dnc
%D 2Dx     100     +30      +30     +30   +30
%D 2D  100 a0 ---> a1 ----> a2 ---> a3    a4
%D 2D      | \     |        |       |     |
%D 2D      |  \    |        |       |     |
%D 2D      |   \   v        v       v     v
%D 2D  +20  \   -> b1 ----> b2 ---> b3    b4
%D 2D        \     |        |       |     |
%D 2D         \    |        |       |     |
%D 2D          \   v        v       v     v
%D 2D  +20      -> c1 ----> c2 ---> c3    c4
%D 2D
%D (( a0 .tex= * a1 .tex=  0   a2 .tex=    1   a3 .tex=     2    a4 .tex= n
%D               b1 .tex= *÷0' b2 .tex= *'÷1'  b3 .tex= *''÷2'   b4 .tex= *÷n{-}1
%D               c1 .tex=  0   c2 .tex=    1   c3 .tex=     2    c4 .tex= n
%D    a0 a1 -> a1 a2 -> a2 a3 ->
%D             b1 b2 -> b2 b3 ->
%D             c1 c2 -> c2 c3 ->
%D    a0 b1 -> a1 b1 -> a2 b2 -> a3 b3 -> a4 b4 ->
%D    a0 c1 -> b1 c1 -> b2 c2 -> b3 c3 -> b4 c4 ->
%D ))
%D enddiagram
%D
$$\diag{NNO+1-dnc}$$

\msk

\def\dotminus{\overset{.}{-}}
%:-.{\dotminus}

Define $n \mto n {\dotminus} 1$ as $p';[0,\id]$,

The arrow $m \mto (n \dotminus m)$ of the previous page 



% (find-dn4ex "edrx08.sty")
% (find-dn4   "experimental.lua")

%

\end{document}

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