|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: