% (find-angg "LATEX/2009unilog-obso.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009unilog-obso.tex && latex    2009unilog-obso.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009unilog-obso.tex && pdflatex 2009unilog-obso.tex"))
% (eev "cd ~/LATEX/ && Scp 2009unilog-obso.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2009unilog-obso.dvi"))
% (find-dvipage "~/LATEX/2009unilog-obso.dvi")
% (find-pspage  "~/LATEX/2009unilog-obso.pdf")
% (find-pspage  "~/LATEX/2009unilog-obso.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2009unilog-obso.ps 2009unilog-obso.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2009unilog-obso.ps 2009unilog-obso.dvi && ps2pdf 2009unilog-obso.ps 2009unilog-obso.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2009unilog-obso.pdf" (ee-twupfile "LATEX/2009unilog-obso.pdf") 'over)
% (ee-cp "~/LATEX/2009unilog-obso.pdf" (ee-twusfile "LATEX/2009unilog-obso.pdf") 'over)

%   «.dn-currying-functors»	(to "dn-currying-functors")



\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 2009unilog-obso.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")



(Transcribed from the blue notebook).

$$

\def\PTS{Ð{PTS}}
\def\DJ{¯{DJ}}

Over the next few sections we are going to understand several {\sl
  pure type systems}, then follow the formal definition of PTSs in
[GeuvThesis]. The reader is encouraged to think that the PTSs that we
will (begin to) define in sections \_, \_, \_, \_, namely, $\PTS_{Þ}$,
$\PTS_{Þñ}$, $\PTS_{}$, $\PTS_{}$, $\PTS_{}$, are ``fragments'' of a
bigger type system, $\PTS_{ØÞñ}$, that will be formally defined in
section $\_$; they are ``fragments'' in the sense that they allow only
a few of the rules of the bigger type system in their derivations (see
section \_), and so their sets of derivable judgments,
$\DJ(\PTS_{Þ})$, ..., $\DJ(\PTS_{Þñ})$, are subsets of
$\DJ(\PTS_{ØÞñ})$.

In a {\sl pure} type system there are no constants besides the {\sl
  sorts}, and the only ``axioms'' --- i.e., the judgments that can
appear in the leaves of the derivations --- are only `$\vdash Þ¨ñ$'
and `$\vdash Ø¨Þ$'. Buth both the rules and the models become much
easier to understand if we allow a few ``impurities'' of certain
kinds; for example, if $\N$ is a set, $0¨\N$ its element zero, and
$s:\N \to \N$ is the successor function, then $s(s(0))$ is an element
of $\N$, and we can derive $\vdash s(s(0)):\N$ from these hypotheses
using only the rules of $\PTS_{Þ}$. We express this as:
%:
%:  |-\N:Þ  |-0:\N  |-s:\N->\N
%:  ==========================\PTS_{Þ}
%:       |-s(s(0)):\N
%:
%:       ^pts-N-ex-short
%:
$$\ded{pts-N-ex-short}$$
%
where the double bar represents several derivation rules in
$\PTS_{Þ}$; the expansion of that derivation tree is:
%:
%:  |-0:\N  |-s:\N->\N
%:  ------------------\app_{ÞÞ}
%:     |-s(0):\N                 |-s:\N->\N
%:     ------------------------------------\app_{ÞÞ}
%:                 |-s(s(0)):\N
%:
%:                 ^pts-N-ex-long
%:
$$\ded{pts-N-ex-long}$$

$$

The intuitive way to recognize that a judgment like
%
$$A:Þ,\, B:A \to Þ,\, f:åa¨A.Ba,\, a:A \vdash fa:Ba$$
%
makes sense is to ``read it aloud'' --- i.e., translate it to English
--- and check that its translated version ``makes sense'' --- i.e.,
that all the variables that it mentions have been declared and that
all the typings are correct. Let's see.

\begin{longtable}{p{2cm}cp{6cm}}
$A:Þ,$         &&
  If we know the value of $A$, and it is an element of $Þ$ (i.e., $A$
  is a set),
  \\ \\
$B:A \to Þ,$   &&
  and if we know the value of $B$, and it is an operation that maps
  each element of $A$ to a set (i.e., $B$ is a family of sets, indexed
  by $A$),
  \\ \\
$f:åa¨A.Ba,$   &&
  and if we know the value of $f$, and it is a function that takes
  each element $a$ of $A$ to an element of the set $Ba$,
  \\ \\
$a:A$          &&
  and if we know the value of $a$, and it is an element of the set $A$,
  \\ \\
$\vdash fa:Ba$ &&
  then we know the value of $fa$, and it is an element of the set $Ba$.
  \\
\end{longtable}

The $Þ$ is one of our few constants; it is a ``sort'' (more on
``sorts'' later), and it will play the role, {\sl very} roughly, of
the class of all sets. Mnemonic: ``$Þ$'' is for ``{\sl Th}ets''.

$$

$$\def\judgpts#1#2{#1 && #2 \\}
  \begin{array}{ccl}
  \judgpts {A:Þ,\, B:Þ,\, f:A \to B,\, a:A \vdash fa:B} {\PTS_{Þ}}
  \judgpts {A:Þ,\, B:A \to Þ,\, f:åa¨A.Ba,\, a:A \vdash fa:Ba} {\PTS_{Þñ}}
  \judgpts {A:Þ \vdash ða¨A.a : A \to A} {\PTS_{Þ}}
  \judgpts {P:Þ \vdash ðp¨P.p : P \to P} {\PTS_{Ø}}
  \judgpts {A:Þ \vdash (ðA¨Þ.ða¨A.a)A : A \to A} {\PTS_{ñÞ}}
  \judgpts {P:Ø \vdash (ðP¨Ø.ðp¨P.p)P : P \to P} {\PTS_{ÞØ}}
  \end{array}
$$ 

$$\def\judgpts#1#2{#1 && #2 \\}
  \begin{array}{ccl}
  \judgpts {A:Þ \vdash ða¨A.a : A \to A} {\PTS_{Þ}}
  \judgpts {P:Þ \vdash ðp¨P.p : P \to P} {\PTS_{Ø}}
  \judgpts {A:Þ \vdash (ðA¨Þ.ða¨A.a)A : A \to A} {\PTS_{ñÞ}}
  \judgpts {P:Ø \vdash (ðP¨Ø.ðp¨P.p)P : P \to P} {\PTS_{ÞØ}}
  \end{array}
$$

[How to interpret a judgment like $a¨A, b¨B_a, c¨C_{abc} \vdash
  d_{abc}¨D_{abc}$, where $d_{abc}$ is a term, as a series of
  morphisms; actually to interpret these judgments categorically we
  will need LCCCs, that can only be explained after hyperdoctrines...]


%D diagram typehier-ThBox
%D 2Dx     100
%D 2D  100
%D 2D
%D 2D  +20
%D 2D
%D ((
%D
%D ))
%D enddiagram
%D
$$\diag{typehier-ThBox}$$

% 
(Transcribed from the back of p.247 in ``On Property-Like Structures'').

($A \to B$ is a hom-set, $A \ton{f} B$ is a morphism)

(Conventions for downcasing arrows)



\bsk

$$

Here's the adjoint presentation:

$$A^\op \TNto ((A \to B×C) \bij ((A,A) \to (B,C)))$$
                       $$h \mto (h;,\,h;')$$
               $$\ang{f,g} \mot (f,g)$$
$$(A^\op,B,C) \TNto ((A \to B×C) \bij ((A,A) \to (B,C)))$$
$$(A^\op) \TNto ((A \to 1) \bij \{*\})$$
                       $$f \mto *$$
                     $$!_A \mot *$$
$$(A^\op) \TNto ((A×B \to C) \bij (A \to (B{\to}C)))$$
                       $$f \mto \cur f$$
   $$\uncur g := (g×\id_B);\ev_{BC} \mot g$$
$$(A^\op,B^\op,C) \TNto ((A×B \to C) \bij (A \to (B{\to}C)))$$

Some uppercasings (messy):

%:
%:
%:  B  C       B  C	       B  C           f:A->B  g:A->C
%:  ----×  -------------  -------------'    ----------------\ang{,}
%:   B×C   _{BC}:B×C->B   '_{BC}:B×C->C     \ang{f,g}:A->B×C
%:
%:   ^CCC-shortp1 ^CCC-shortp2  ^CCC-shortp3  ^CCC-shortp4
%:
%:                    A
%:  -1            --------!
%:  1             !_A:A->1
%:  
%:  ^CCC-short!1   ^CCC-short!2
%:
%:  B  C            B  C                  f:A×B->C
%:  ----"->   ------------------\ev   ----------------\cur
%:  B{->}C    \ev_{BC}:(B{->}C)×B->C  \cur"f:A->(B{->}C)
%:
%:  ^CCC-shorte1  ^CCC-shorte2          ^CCC-shorte3
%:
$$\ded{CCC-shortp1} \qquad \ded{CCC-shortp2} \qquad \ded{CCC-shortp3}$$
$$\ded{CCC-shortp4}$$
$$\ded{CCC-short!1} \qquad \ded{CCC-short!2}$$
$$\ded{CCC-shorte1} \qquad \ded{CCC-shorte2} \qquad \ded{CCC-shorte3}$$


\newpage

% --------------------
% «dn-currying-functors»  (to ".dn-currying-functors")
% (sec      "Currying Functors" "dn-currying-functors")
\mysection {Currying Functors} {dn-currying-functors}

% (find-angg ".emacs" "caderno")
% (find-caderno2page 58 "A lemma about bifunctors")
% (find-caderno2page 59 "A lemma about bifunctors")
% (find-caderno2page 60 "Product categories")
% (find-caderno2page 61 "A lemma on bifunctors")

% The following fact appears as an exercise in most basic books on
% Category Theory. For any fixed category $\bbB$, $(×\bbB):\Cat \to
% \Cat$ and $(\bbB \to):\Cat \to \Cat$ are functors, and we have an
% adjunction $(×\bbB) \dashv (\bbB\to)$. The construction of the
% functors $(\bbB×)$ and $(\bbB\to)$ are easy, but the rest of the
% proof --- the construction of the transpositions, etc --- is
% suprisingly hairy; let's see its syntactical skeleton.

If $\bbA$, $\bbB$, and $\bbC$ and categories, then we can form the
product category $\bbA×\bbB$ and the category of functors $\bbB \to
\bbC$. It turns out that for any fixed category $\bbB$,\linebreak[1]
$(×\bbB):\Cat \to \Cat$ and $(\bbB \to):\Cat \to \Cat$ are functors
--- this is easy to prove --- and we have $(×\bbB) \dashv (\bbB\to)$;
the adjunction part is left as an exercise in most basic Category
Theory books, and its proof is quite hairy. We will look at its
syntactical skeleton --- which is just the construction of the two
transpositions, $\flat$ and $\sharp$. The figure is:
%
%D diagram prodcat-1
%D 2Dx        100         +30
%D 2D  100 \bbA×\bbB <--- \bbA
%D 2D          |           |
%D 2D      G^b |   <---|   | G
%D 2D        F |   |--->   | F^#
%D 2D          v           v   
%D 2D  +30   \bbC ---> \bbB->\bbC
%D 2D
%D (( \bbA×\bbB \bbA
%D    \bbC \bbB->\bbC
%D    @ 0 @ 1 <-|
%D    @ 0 @ 2 -> .plabel= l \sm{G^\flat\\F}
%D    @ 1 @ 3 -> .plabel= r \sm{G\\F^\sharp}
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl^
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl_
%D    @ 2 @ 3 |->
%D ))
%D enddiagram
%D
$$\diag{prodcat-1}$$

In the syntactical world the `$\sharp$' takes each protofunctor $F
\equiv (F_0,F_1): \bbA×\bbB \to \bbC$ and produces a protofunctor
$F^\sharp \equiv ({{F^\sharp}_0,{F^\sharp}_1}): \bbA \to (\bbB \to
\bbC)$. The action of $F^\sharp$ on morphisms, ${F^\sharp}_0$, takes
each object $A$ of $\bbA$ to an object ${F^\sharp}_0A \equiv
{F^\sharp}A$ of $\bbB \to \bbC$; this ${F^\sharp}A:\bbB \to \bbC$ is
itself a (proto)functor, and so it is made of two components:
${F^\sharp}A \equiv (({F^\sharp}A)_0, ({F^\sharp}A)_1)$. The action of
$F^\sharp$ on morphisms, ${F^\sharp}_1$, takes each morphism $\aa:A
\to A'$ of $\bbA$ to a morphism ${F^\sharp}_1\aa \equiv F^\sharp\aa:
F^\sharp A \to F^\sharp A'$ between two functors $F^\sharp A, F^\sharp
A': \bbB \to \bbC$. This is a natural transformation, that we can
write as $B \TNto (F^\sharp AB \ton{F^\sharp \aa B} F^\sharp A'B)$).
The full construction is:
%:
%:                          [A]^3
%:                          -----\id
%:  [A]^3  [B]^1            \id_A     [\bb]^2                            [B]^4
%:  ---------\ang{,}        -----------------                            -----
%:     (A,B)           F        (\id_A,\bb)     F               [\aa]^5  \id_B
%:     ----------------=>E_0    -----------------=>E_1          -------------
%:     F^\sharp"AB==F(A,B)      F^\sharp"A\bb==F(\id_A,\bb)       (\aa,\id_B)    F
%:  ------------------------1    -------------------------2       ----------------=>E_1
%:  (F^\sharp"A)_0==ðB.F(A,B)  (F^\sharp"A)_1==ð\bb.F(\id_A,\bb)   F^\sharp\aa"B==F(\aa,\id_B)
%:  ------------------------------------------------------\ang{,}  --------------------4
%:       F^\sharp"A==(ðB.F(A,B),ð\bb.F(\id_A,\bb))                 F^\sharp\aa==ðB.F(\aa,\id_B)
%:  ---------------------------------------------3    -----------------------------------5
%:  {F^\sharp}_0==ðA.(ðB.F(A,B),ð\bb.F(\id_A,\bb))    {F^\sharp}_1==ð\aa.ðB.F(\aa,\id_B)
%:  --------------------------------------------------------------------------------\ang{,}
%:     F^\sharp:=(ðA.(ðB.F(A,B),ð\bb.F(\id_A,\bb)),ð\aa.ðB.F(\aa,\id_B))
%:
%:        ^prodcat-sharp-3-std
%:
$$\ded{prodcat-sharp-3-std}$$
%
but how could anyone have arrived at this?... and how could anyone
check whether this construction is right?

One possible answer is: ``start from the types''.



% If $\bbA$, $\bbB$ and categories, then we can form their product
% category $\bbA×\bbB$. An object of $\bbA×\bbB$ is a pair or objects,
% $(A,B)$, where $A:\bbA_0$ and $B:\bbB_0$; a morphism from $(A,B)$ to
% $(A',B')$ in $\bbA×\bbB$ is pair of morphisms, $(\aa,\bb)$, where
% $\aa:A \to A'$ in $\bbA$ and $\bb:B \to B'$ in $\bbB$.

% If $\bbB$ and $\bbC$ are categories, then we can form the category
% of functors $\bbB \to \bbC$. An object $H:\bbB \to \bbC$ is a
% functor from $\bbB$ to $\bbC$; a morphism $T:H \to K$ (or: $B \TNto
% (HB \ton{TB} KB)$) is a functor from $H$ to $K$.




% \newpage

$$\diag{prodcat-1}$$


%:
%:           (A,B)                            (A,B)              
%:           -----                           -----             
%:    (A,B)    A     a=>(b=>c)        (A,B)     A     G          
%:    -----'  ---------------=>E_0   -----'   -------=>E_0     
%:      B          b=>c                 B         GA             
%:      ---------------=>E_0            -----------------=>E_0   
%:            C                         G^\flat(A,B)==GAB        
%:                                                               
%:            ^prodcat-flat-0-dnc          ^prodcat-flat-0-std  
%:
%:           P                        
%:           --                      
%:     P     P   G                   
%:    ---'  --------=>E_0            
%:    'P     G_0(P)                 
%:     ----------------=>E_0          
%:    {G^\flat}_0(P)==(G_0(P))_0('P)
%:                                    
%:    ^prodcat-flat-0-std-long             
%:
$$\ded{prodcat-flat-0-dnc} \qquad \ded{prodcat-flat-0-std}$$
% $$\ded{prodcat-flat-0-std-long}$$

%:
%:                                                       (\aa,\bb)
%:                                                       ---------
%:              (\aa,\bb)                                  \aa              G
%:              ---------                                -----\ren   ---------------\ren
%:  (\aa,\bb)    \aa            G             (\aa,\bb)   a|->a'      a=>(b=>(a;b)^F)
%:  ---------'  ---\src  -------------\ren   ---------' ---------------------------=>E_1
%:     \bb        A       a=>(b=>(a;b)^F)      \bb        (b=>(a;b)^F)|->(b=>(a';b)^F)
%:    -----\ren   ---------------------=>E_0   ---\tgt   -----------------------------\ren
%:    b|->b'           b=>(a;b)^F              B'        b-.>((a;b)^F|->(a';b)^F)
%:    -------------------------=>E_1           ---------------------------------"-.>E
%:      (a;b)^F|->(a;b')^F                     (a;b')^F|->(a';b')^F
%:      -----------------------------------------------------------;
%:                      (a;b)^F|->(a';b')^F
%:               
%:                      ^prodcat-flat-1-dnc
%:
%:              (\aa,\bb)                                   
%:              ---------                                  
%:               \aa               (\aa,\bb)           (\aa,\bb) 
%:               ---\src           --------'          ---------
%:  (\aa,\bb)     A       G        \bb            \aa     G      
%:  ---------'  ----------=>E_0   ---\tgt        ---------=>E_1 
%:    \bb            GA             B'             G\aa          
%:    -----------------=>E_1        -------------------"-.>E
%:          GA\bb                      G\aa"B'
%:          ----------------------------------;
%:             G^\flat(\aa,\bb)==GA\bb;G\aa"B'
%:               
%:                      ^prodcat-flat-1-std
%:
$$\ded{prodcat-flat-1-dnc}$$
$$\ded{prodcat-flat-1-std}$$


%:
%:
%:                                         [(\aa,\bb)]^2                                         
%:                                         ---------                                            
%:                                            \aa             [(\aa,\bb)]^2        [(\aa,\bb)]^2 
%:                                            ---\src         ------------'       ------------ 
%:             [(A,B)]^1       [(\aa,\bb)]^2    A      G         \bb          \aa     G                 
%:             -----          ------------'   -------=>E_0     ---\tgt      ---------=>E_1        
%:  [(A,B)]^1     A     G          \bb             GA             B'            G\aa                 
%:  -----'       -------=>E_0     -----------------=>E_1         -------------------"-.>E           
%:     B               GA              GA\bb                        G\aa"B'                             
%:     -----------------=>E_0          ----------------------------------;                        
%:     G^\flat(A,B)==GAB                  G^\flat(\aa,\bb)==GA\bb;G\aa"B'                         
%:     -----------------------1        ----------------------------------2                                      
%:     {G^\flat}_0==ð(A,B).GAB         {G^\flat}_1==ð(\aa,\bb).GA\bb;G\aa"B'                                         
%:     ---------------------------------------------------------------------                     
%:     {G^\flat}==(ð(A,B).GAB,ð(\aa,\bb).GA\bb;G\aa"B')                                         
%:                          
%:      ^prodcat-flat-2-std  
%:
$$\ded{prodcat-flat-2-std}$$








%

\end{document}

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