|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2007dnc-sets.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2007dnc-sets.tex && latex 2007dnc-sets.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2007dnc-sets.tex && pdflatex 2007dnc-sets.tex"))
% (eev "cd ~/LATEX/ && Scp 2007dnc-sets.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2007dnc-sets.dvi")
% (find-pspage "~/LATEX/2007dnc-sets.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2007dnc-sets.ps 2007dnc-sets.dvi")
% (find-pspage "~/LATEX/2007dnc-sets.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvired -o tmp.ps 2007dnc-sets.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2007dnc-sets.dvi" (ee-twupfile "LATEX/2007dnc-sets.dvi") 'over)
% (ee-cp "~/LATEX/2007dnc-sets.dvi" (ee-twusfile "LATEX/2007dnc-sets.dvi") 'over)
% (ee-cp "~/LATEX/2007dnc-sets.pdf" (ee-twupfile "LATEX/2007dnc-sets.pdf") 'over)
% (ee-cp "~/LATEX/2007dnc-sets.pdf" (ee-twusfile "LATEX/2007dnc-sets.pdf") 'over)
% (find-twupfile "LATEX/")
% (find-twusfile "LATEX/")
% http://angg.twu.net/LATEX/
% http://angg.twu.net/LATEX/2007dnc-sets.pdf
% «.lifting-archetypal-proofs» (to "lifting-archetypal-proofs")
% «.lifting-set-like-notation» (to "lifting-set-like-notation")
% «.curry-howard» (to "curry-howard")
% «.dnc-main-ideas» (to "dnc-main-ideas")
% «.reconstructing-the-dic» (to "reconstructing-the-dic")
% «.contexts-and-discharges» (to "contexts-and-discharges")
% «.contexts-and-discharges-2» (to "contexts-and-discharges-2")
% «.expanding-trees» (to "expanding-trees")
% «.theorems-for-free» (to "theorems-for-free")
% «.ambiguities» (to "ambiguities")
% «.informal-coherence» (to "informal-coherence")
% «.informal-coherence-ex» (to "informal-coherence-ex")
% «.informal-coherence-ex-2» (to "informal-coherence-ex-2")
% «.downcasing-functors» (to "downcasing-functors")
% «.products-via-NTs» (to "products-via-NTs")
% «.downcasing-NTs» (to "downcasing-NTs")
% «.translating-trees» (to "translating-trees")
% «.downcasing-cat-diagrams» (to "downcasing-cat-diagrams")
% «.why-pseudopoints» (to "why-pseudopoints")
% «.subobject-maps» (to "subobject-maps")
% «.quantifiers-categorically» (to "quantifiers-categorically")
% «.archetypes-more-1» (to "archetypes-more-1")
% «.archetypes-more-2» (to "archetypes-more-2")
% «.archetypes-more-3» (to "archetypes-more-3")
\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 2007dnc-sets.dnt
%*
% (eedn4-51-bounded)
% (find-TH "2007dnc-sets")
% (find-TH "2007dnc-cats")
% (fooi-re "\\[tsec [^ \n]+ (to \".\\([^ \"]+\\)\")\n...N.. \\([^\n]+\\)\n" "% (s \"\\2\" \"\\1\")\n")
%*
% (eedn4-51-bounded)
{\bf Downcasing types}
(Introductory notes)
\msk
Eduardo Ochs
% (find-zsh "dmissing tetex | grep url")
% (find-lsrcfile "misc/url.sty")
\url{eduardoochs@gmail.com}
\url{http://angg.twu.net/}
\url{http://angg.twu.net/math-b.html}
\url{http://angg.twu.net/LATEX/2007dnc-sets.{tex,dvi,pdf}}
\bsk
Written: 2007.
\LaTeX ing and minor additions and revisions: may 2008.
Current version: 2008may20 (see the footer)
\bsk
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 {Main idea: lifting archetypal proofs} {2}
\tocline {Lifting set-like notation} {3}
\tocline {Starting point: the Curry-Howard Isomorphism} {4}
\tocline {Main ideas} {5}
\tocline {Reconstructing the types and the dictionary from trees} {6}
\tocline {Contexts and discharges} {7}
\tocline {Contexts and discharges (2)} {8}
\tocline {Expanding trees} {9}
\tocline {Theorems for Free} {10}
\tocline {Ambiguity plays on our side (usually)} {11}
\tocline {Informal coherence} {12}
\tocline {Informal coherence: examples} {13}
\tocline {Informal coherence: examples (2)} {14}
\tocline {Downcasing functors} {15}
\tocline {Products via natural transformations} {16}
\tocline {Downcasing Natural Transformations} {17}
\tocline {Translating bigger trees} {18}
\tocline {Downcasing categorical diagrams (in general)} {19}
\tocline {Why we want to allow pseudopoints} {20}
\tocline {Maps between subobjects: the general case} {21}
\tocline {Quantifiers, categorically} {22}
\tocline {More notes about archetypes (1)} {23}
\tocline {More notes about archetypes (2)} {24}
\tocline {More notes about archetypes (3)} {25}
\def\myttchars{\ttchars}
\setlength{\parindent}{0em}
\newpage
% --------------------
% «lifting-archetypal-proofs» (to ".lifting-archetypal-proofs")
% (s "Main idea: lifting archetypal proofs" "lifting-archetypal-proofs")
\myslide {Main idea: lifting archetypal proofs} {lifting-archetypal-proofs}
{\myttchars
\footnotesize
\begin{verbatim}
Take a proof of some general statement.
Now specialize it to a particular case.
``Specializing'' is somehow like doing a
projection - some distinctions collapse,
some details are lost -
Here we are concerned with the opposite
of specializing proofs.
We start with an ``archetypal proof'' -
a proof of a certain very particular case,
done in a certain language - and then we
/change our dictionary a bit/ - and some
terms change meaning; and the same proof
becomes a proof of the general case -
We call this ``lifting''. Archetypal proofs
/lift/ to more general proofs, and when this
happens we get general proofs done in a
language inherited from the archetypal cases.
My favorite examples of such liftings of
proofs are for proofs in Categorical
Semantics.
The fist significant example will be this
one (we call it ``CCC<->ð1''):
The Cartesian-Closed Categories (CCCs)
are exactly the categories where we can
interpret the simply-typed ð-calculus
(``System ð1'').
After ``CCC<->ð1'' we will see ``Hyp<->LPCE'':
The hyperdoctrines are exactly the
categories in which we can interpret
(a certain system of intuitionistic, typed)
first-order logic (``LPCE'').
\end{verbatim}
}
\newpage
% --------------------
% «lifting-set-like-notation» (to ".lifting-set-like-notation")
% (s "Lifting set-like notation" "lifting-set-like-notation")
\myslide {Lifting set-like notation} {lifting-set-like-notation}
{\myttchars
\footnotesize
\begin{verbatim}
Our approach:
`Set' is our archetypal CCC.
Sets are also our archetypal model for ð1.
Most of the proof - even most of the details
of the statement of the theorem! - will appear
more or less naturally from taking the
diagrams below, done in the language of
``downcased types'' (DNC) and translating
them in several ways.
--| a |-- a a,b <==== a
/ - \ - - -
/ | \ | | <--> |
v v v v v v
b <---| b,c |---> c * c ===> b|->c
--| P |-- P P&Q <==== P
/ - \ - - -
/ | \ | | <--> |
v v v v v v
Q <---| Q&R |---> R § R ====> Q⊃R
Later, Set (or, more precisely, the fibration Set^>->),
we will also be our archetypal hyperdoctrine.
\end{verbatim}
}
\newpage
% --------------------
% «curry-howard» (to ".curry-howard")
% (s "Starting point: the Curry-Howard Isomorphism" "curry-howard")
\myslide {Starting point: the Curry-Howard Isomorphism} {curry-howard}
{\myttchars
\footnotesize
\begin{verbatim}
There is a correspondence between
Natural Deduction trees and
terms of the simply-typed ð-calculus (ð1).
Example:
P&Q d:A×B
--- -----
P&Q Q Q⊃R d:A×B 'd:B f:B->C
--- ---------- ----- ---------------
P R d:A f('d):C
----------- ------------------
P&R <d,f('d)>:A×C
Sometimes the usual notation for type theory/
ð-calculus feels too verbose.
The DNC notation started as an informal reasoning tool -
I used it in my private notes as a system of abbreviations
for ð-calculus.
DNC grew with time and started to look more formal...
It got special arrow symbols (a.k.a. ``connectives'' - `=>' and
`-.>') to represent functors and natural transformations.
In 2001 I found that `=>' and `-.>' had introduction rules
besides the obvious elimination rules (think in introd and
elim of `&', `⊃', `\or', etc in Natural Deduction) -
so DNC could be the basis for a system of natural deduction
for categories.
DNC never became formal enough to be a ``system'', and nowadays it
lives a more unpretentious existence as an auxiliary language for
type theory and category theory (esp. categorical semantics).
I changed the meaning for ``DNC'' -
from a sytem for ``Natural Deduction for Categories'' to
a notation of ``DowNCased types''.
\end{verbatim}
}
\newpage
% --------------------
% «dnc-main-ideas» (to ".dnc-main-ideas")
% (s "Main ideas" "dnc-main-ideas")
\myslide {Main ideas} {dnc-main-ideas}
{\myttchars
\footnotesize
\begin{verbatim}
Long names for variables
------------------------
In {(n,r)ÝN×R | r^2=n}
the (n,r) is the name of a variable -
N×R is the space of pairs made of a
natural number and a real.
A dictionary
------------
Define n := (n,r)
r := '(n,r)
(r,n) := <r,n>
The syntactical distinction between variables and terms
-------------------------------------------------------
We've sacrificed it.
Also, without the dictionary there is no way to tell from
(n,r), n, r, (r,n) which of them are more primitive than
the others.
Downcasing
----------
The default name for a variable ranging over A is `a'.
The default (long!) name for a variable ranging over A×B is `(a,b)'.
Well-formed formulas, expressions, etc
--------------------------------------
We don't have these notions in DNC.
Anything can be a DNC ``name''. 8-(
Spaces of functions
-------------------
In f:A->B we will read ``A->B'' as B^A
and the ``:'' as the `:' of Type Theory.
(For mathematicians: `:' is roughly like `Ý', but ``f:A->B''
means also ```f' is of type `A->B''', and each term has
a single type. We are not interesting in `\subset', `\subseteq', etc).
Notation for functions
----------------------
An `a|->b' is an element of A->B.
An `a|->b' is a function that takes each `a' to a `b'.
\end{verbatim}
}
\newpage
% --------------------
% «reconstructing-the-dic» (to ".reconstructing-the-dic")
% (s "Reconstructing the types and the dictionary from trees" "reconstructing-the-dic")
\myslide {Reconstructing the types and the dictionary from trees} {reconstructing-the-dic}
{\myttchars
\footnotesize
\begin{verbatim}
d:A×B
-----
d:A×B 'd:B f:B->C
----- ---------------
d:A f('d):C
------------------
<d,f('d)>:A×C
a,b
---
a,b b b|->c a := (a,b)
--- ---------- b := '(a,b)
a c c := (b|->c)(b)
----------- a,c := <a,c>
a,c
Now add ``a,b := d'' and ``b|->c := f'' and we get
the ð-calculus terms back from the DNC tree.
Note that we obtain the types back by uppercasing
the DNC ``terms'' -
`|->' is uppercased to `->',
`,' to `×', etc.
\end{verbatim}
}
\newpage
% --------------------
% «contexts-and-discharges» (to ".contexts-and-discharges")
% (s "Contexts and discharges" "contexts-and-discharges")
\myslide {Contexts and discharges} {contexts-and-discharges}
{\myttchars
\footnotesize
\begin{verbatim}
Each subtree of a Natural Deduction tree/derivation/proof
corresponds to a smaller proof contained in a bigger one.
For each node of a tree let's look at the tree above the
node, and make its hypotheses explicit.
P&Q P&Q|-P&Q
--- --------
P&Q Q Q⊃R P&Q|-P&Q P&Q|-Q Q⊃R|-Q⊃R
--- ---------- -------- --------------------
P R P&Q|-P Q⊃R,P&Q|-R
----------- -------------------------
P&R Q⊃R,P&Q|-P&R
Now we can understand the ``⊃-introduction'' rule;
it involves a discharge.
[P&Q]^1 P&Q|-P&Q
------- --------
[P&Q]^1 Q Q⊃R P&Q|-P&Q P&Q|-Q Q⊃R|-Q⊃R
------- --------- -------- --------------------
P R P&Q|-P Q⊃R,P&Q|-R
------------- -------------------------
P&R Q⊃R,P&Q|-P&R
-------1 ------------
P&Q⊃P&R Q⊃R|-P&Q⊃P&R
Below the bar marked with ``1'' the hypotheses marked with
``[·]^1'' should no longer be in the list of hypotheses -
they've been ``discharged'' (into the conclusion).
\end{verbatim}
}
\newpage
% --------------------
% «contexts-and-discharges-2» (to ".contexts-and-discharges-2")
% (s "Contexts and discharges (2)" "contexts-and-discharges-2")
\myslide {Contexts and discharges (2)} {contexts-and-discharges-2}
{\myttchars
\footnotesize
\begin{verbatim}
Let's look at the functional side of this (Curry-Howard):
[a,b]^1 (a,b)|-(a,b)
------- ------------
[a,b]^1 b b|->c (a,b)|-(a,b) (a,b)|-b (b|->c)|-(b|->c)
------- ----------- ------------ ---------------------------
a c (a,b)|-a (b|->c),(a,b)|-c
--------------- ---------------------------------------
a,c (b|->c),(a,b)|-(a,c)
---------1 --------------------
a,b|->a,c (b|->c)|-(a,b|->a,c)
[p]^1 p|-p
----- ------
[p]^1 'p f p|-p p|-'p f|-f
----- --------- ----- ---------------
p f('p) p|-p f,p|-f('p)
----------------- ----------------------
<p,f('p)> f,p|-<p,f('p)>
--------------1 -----------------1
ðp.<p,f('p)> f|-ðp.<p,f('p)>
The ``⊃-introduction'' rule (last bar) corresponds to introducing a `ð';
one variable ceases to be free, and is removed from the list of hypotheses.
One way of reading ``f,p|-<p,f('p)>'' -
or ``f:B->C,p:A×B|-<p,f('p)>:A×C'' - is:
if we know the value of f and p (points of B->C and A×B)
we know the value of <p,f('p)> (a point of A×C).
\end{verbatim}
}
\newpage
% --------------------
% «expanding-trees» (to ".expanding-trees")
% (s "Expanding trees" "expanding-trees")
\myslide {Expanding trees} {expanding-trees}
{\myttchars
\footnotesize
\begin{verbatim}
a,b a,b:A×B
--- |--------------> -------
a a:A
- - - -
| \ | \
| v | v
| a,b|-a,b | a,b:A×B|-a,b:A×B
| -------- |---------> ----------------
| a,b|-a | a,b:A×B|-a:A
| - | - -
| | | | \
| | | | v
| | | | (a,b|-a,b):A×B->A×B
| | | | -------------------
p | p:A×B | (a,b|-a):A×B->A
-- |- - - | - - - -> ----- | -
p | p:A | |
- | - | |
\ | \ | |
v v v v |
p|-p p:A×B|-p:A×B |
----- |- - - - - - -> ------------ |
p|-p p:A×B|-p:A |
- - |
\ \ |
v v v
id id_{A×B}:A×B->A×B
--- |- - - - - - - -> -----------------
_0 _{0\,A,B}:A×B->A
\end{verbatim}
}
\newpage
% --------------------
% «theorems-for-free» (to ".theorems-for-free")
% (s "Theorems for Free" "theorems-for-free")
\myslide {Theorems for Free} {theorems-for-free}
{\myttchars
\footnotesize
\begin{verbatim}
From the ``Theorems for Free'' paper (Wadler 1989):
* All closed terms of type ýA.ýB.(A×B->B×A)
obey a certain theorem
* Corollary: all terms of type ýA.ýB.(A×B->B×A)
are the flip function.
Something similar (but much looser) happens in DNC:
`a,b|->b,a' has a ``natural definition'' -
apply Curry-Howard, prove P&Q⊃Q&P, translate the
proof to ð-calculus in DNC notation -
[P&Q]^1 [P&Q]^1 [a,b]^1 [a,b]^1 [p]^1 [p]^1
------- ------- ------- ------- ----- -----
Q P b a 'p p
----------- ----------- ----------
Q&P b,a <'p,p>
-------1 ---------1 -----------1
P&Q⊃Q&P a,b|->b,a ðp.<'p,p>
and an argument using normalization of ND proofs
can be used to show that all other ND proofs (= ð-terms)
are equivalent to that one.
In DNC we won't be interested in the ``uniqueness'' part
very often, though.
\end{verbatim}
}
\newpage
% --------------------
% «ambiguities» (to ".ambiguities")
% (s "Ambiguity plays on our side (usually)" "ambiguities")
\myslide {Ambiguity plays on our side (usually)} {ambiguities}
{\myttchars
\footnotesize
\begin{verbatim}
a,b a,b p p
--- --- -- --- a := (a,b)
a b p 'p b := '(a,b)
------- -------- a,b := <a,b>
a,b <p,'p>
Apparently the DNC tree on the left, above
introduces a ``secondary definition'' for a,b
and a circularity in the dictionary, and such
things have to be avoided at all costs -
But we can be careful and interpret each tree
as a term, and in
a,b a,b p p
--- --- -- ---
a b p 'p
------- --------
a,b = a,b <p,'p> = p
what happens is that we have two different
``natural constructions'' for a,b from a,b,
and we're saying that the two ``must give the
same result'', i.e., <p,'p> = p...
In many contexts we will have two different
natural constructions for a DNC ``term'' with
a certain name, and we will want to say that
the two constructions give the same result
(sometimes this will be an axiom, sometimes
a theorem, sometimes a hypothesis) -
We will sometimes use the expression ``is well
defined'' (notation: ``wd[·]'') in a funny sense:
``wd[a,b]'' will mean ``the two obvious natural
constructions for a,b give the same result''.
\end{verbatim}
}
\newpage
% --------------------
% «informal-coherence» (to ".informal-coherence")
% (s "Informal coherence" "informal-coherence")
\myslide {Informal coherence} {informal-coherence}
{\myttchars
\footnotesize
\begin{verbatim}
A /coherence theorem/ says that
there is exactly one entity
of a given type...
For example: that ``there is
exactly one map A×B->B×A'' -
the flip function.
Coherence would allow us to say
``_the_ map a,b|->a,b'' instead of
``_a_ map a,b|->a,b''.
We have something weaker in DNC:
a dictionary, and a vague notion
of assigning ``natural meanings''
to names.
Each ``natural meaning'' comes
from a ``natural construction''.
Instead of proving ``real'' coherence -
e.g., ``all natural constructions for
a,b|->b,a give the same result'' -
we will use something MUCH weaker:
``all the `obvious' natural
constructions for a,b|->b,a
(in a given context - given
some base objects,
operations, and diagrams)
yield the same result.''
\end{verbatim}
}
\newpage
% --------------------
% «informal-coherence-ex» (to ".informal-coherence-ex")
% (s "Informal coherence: examples" "informal-coherence-ex")
\myslide {Informal coherence: examples} {informal-coherence-ex}
{\myttchars
\footnotesize
\begin{verbatim}
If we have set meanings for the
four arrows in the diagram below,
f'
A ----> B a |---> b
| | - -
g' | | g | |
v v v v
C ----> D c |---> d
f
then we have two different ``natural
constructions'' for a|->d, each one
giving a (possibly different)
``natural meaning'' for a|->d...
``wd[\alpha]'' (pronounced:
``\alpha is well-defined'')
means:
``all the obvious natural
constructions for \alpha
yield the same result''
In the diagram above
``\wd[a|->d]'' means f';g=g';f
(i.e., a|->b|->d = a|->c|->d)
i.e.: ``the square commutes''.
Giving meaning to a ``wd'' expression
involves deciding which are the
``obvious natural constructions''.
\end{verbatim}
}
\newpage
% --------------------
% «informal-coherence-ex-2» (to ".informal-coherence-ex-2")
% (s "Informal coherence: examples (2)" "informal-coherence-ex-2")
\myslide {Informal coherence: examples (2)} {informal-coherence-ex-2}
{\myttchars
\footnotesize
\begin{verbatim}
Each sentence ``wd[\alpha]'' is a
proposition whose precise meaning
is given as an entry in the dictionary.
Another example: in
a |---> b |---> c
- - -
| | |
v v v
d |---> e |---> f
- - -
| | |
v v v
g |---> h |---> i
we have:
wd[a|->e] & wd[b|->f] &
wd[d|->h] & wd[e|->i] => wd[a|->i].
Note that:
wd[a|->i] := (a|->b|->c|->f|->i =
a|->b|->e|->f|->i =
a|->b|->e|->h|->i =
a|->d|->e|->f|->i =
a|->d|->e|->h|->i =
a|->d|->g|->h|->i).
Each of the other `wd[·]'s is an equality
between only two composites (not six).
\end{verbatim}
}
\newpage
% --------------------
% «downcasing-functors» (to ".downcasing-functors")
% (s "Downcasing functors" "downcasing-functors")
\myslide {Downcasing functors} {downcasing-functors}
{\myttchars
\footnotesize
\begin{verbatim}
A functor F:\catC->\catD is composed of two operations:
F_0 - its action on objects, and
F_1 - its action of morphisms.
Fix a set B, and look at these diagrams, for the functors
(×B):Set->Set and (B->):Set->Set:
A×B <---| A a,b <==== a
- - - -
f×B| <-| |f | <-| |
v v v v
A'×B <---| A' a',b <==== a'
C |----> B->C c ====> b|->c
- - - -
g| |-> |B->g | |-> |
v v v v
C' |---> B->C' c' ===> b|->c'
Functors act on two levels, so we will use a double arrow -
`=>' - to denote them. Their names in DNC will come from
their action on objects:
A|->A×B a=>a,b
C|->B->C c=>b|->c
Their ``syntactical actions'' on morphisms can be derived
from their names: a=>a,b adds a ``,b'' to the name of each
object, so it takes a|->a' to a,b|->a',b; same for c=>b|->c.
To find the ``real action'' of (×B)=(a=>a,b) on morphisms,
look for a natural construction of a,b|->a',b from a|->a;
f×B = a,b|->a',b = ðp.<f(p),'p>.
Note that a functor a=>a,b does not take `a's into `a,b's,
like an arrow a|->a,b would do; instead, it takes the
whole space of `a's, E[a]=A, into the space of `a,b's,
E[a,b]=A×B - (×B)_0 = ðA:Sets.A×B.
\end{verbatim}
}
\newpage
% --------------------
% «products-via-NTs» (to ".products-via-NTs")
% (s "Products via natural transformations" "products-via-NTs")
\myslide {Products via natural transformations} {products-via-NTs}
{\myttchars
\footnotesize
\begin{verbatim}
Any diagram b <--| p |--> c induces an operation that
takes any object A to a map of sets
(A->P) -> (A->B)×(A->C)
/ a \ / a \
| - | | - - |
| | | |--> | / \ |
| v | | v v |
\ p / \ b c /
\end{verbatim}
}
\newpage
% --------------------
% «downcasing-NTs» (to ".downcasing-NTs")
% (s "Downcasing Natural Transformations" "downcasing-NTs")
\myslide {Downcasing Natural Transformations} {downcasing-NTs}
{\myttchars
\footnotesize
\begin{verbatim}
Between two contravariant functors,
Hom(-,P): Set^op -> Set
A |-> A->P
a^op => a|->p
Hom(-,B)×Hom(-,C): Set^op -> Set
A |-> (A->B)×(A->C)
a^op => (a|->b),(a|->c)
The natural transformation
T: Hom(-,P) -> Hom(-,B)×Hom(-,C)
takes each object A of Set (or: an object of Set^op)
to a function:
TA: (A->P) -> ((A->B)×(A->C))
We will represent this natural transformation T in DNC
by just downcasing the triangle:
A
- - -
/ | \
v v v
(A->P) -> ((A->B)×(A->C))
\end{verbatim}
}
\newpage
% --------------------
% «translating-trees» (to ".translating-trees")
% (s "Translating bigger trees" "translating-trees")
\myslide {Translating bigger trees} {translating-trees}
{\myttchars
\footnotesize
\begin{verbatim}
a,b a,b|-a,b
--- --------
a,b a a|-b|->c a,b|-a,b a,b|-a a|-b|->c
--- -------------- |---> -------- -------------------
b b|->c a,b|-b a,b|-b|->c
-------------- ------------------------
c a,b|-c
- -
| |
v v
p a|-f(a) p|-p a|-f(a)
-- ---------ren ----- ---------ren
p p p|-f(p) p|-p p|-p p|-f(p)
--- --------------- |---> ------ ------------------
'p f(p) p|-'p p|-f(p)
---------------- ---------------------
f(p)('p) p|-f(p)('p)
id
--
id f
-- -------
' ;f
-----------
<;f,'>;ev = f^v
\end{verbatim}
}
% (fooi-re "\\[tsec [^ \n]+ (to \".\\([^ \"]+\\)\")\n...N.. \\([^\n]+\\)\n" "% (s \"\\2\" \"\\1\")\n")
% (s "DNC for Categories" "dnc-for-cats")
\newpage
% --------------------
% «downcasing-cat-diagrams» (to ".downcasing-cat-diagrams")
% (s "Downcasing categorical diagrams (in general)" "downcasing-cat-diagrams")
\myslide {Downcasing categorical diagrams (in general)} {downcasing-cat-diagrams}
{\myttchars
\footnotesize
\begin{verbatim}
One day I realized that the same notation that I was using for sets
did also work - with no changes in the syntax, only in the semantics -
for categories.
Here's a comparison; in the second situation, at the right, \catC is
an arbitrary category.
A is a set | A is an object of \catC, AÝ|\catC|
B is a set | B is an object of \catC, BÝ|\catC|
|
A ---> B (a function) | A ---> B (a morphism)
a |--> b (a function) | a |--> b (a morphism)
|
A is the space of `a's | Now:
B is the space of `b's | ``an `a''' is an abuse of language
A = E[a] | ``a `b''' is an abuse of language
B = E[b] | `a|->b' has semantics - it's a morphism -
| but `a' and `b' have no semantics
An `a' is a point of A, |
a `b' is a point of B, | `a's and `b's are not points in this case,
aÝA, bÝB. | just ``pseudopoints'', and pseudopoints
| don't need to exist - they may be just
| syntactical devices
|
| To enforce the distinction we say
| ``object of'' instead of ``space of''
| and we write O[·] instead of E[·]
|
| A is the objects of `a's
| B is the objects of `b's
| A = O[a]
| B = O[b]
Note: it's almost impossible to understand this is the general case
without examples...
\end{verbatim}
}
\newpage
% --------------------
% «why-pseudopoints» (to ".why-pseudopoints")
% (s "Why we want to allow pseudopoints" "why-pseudopoints")
\myslide {Why we want to allow pseudopoints} {why-pseudopoints}
{\myttchars
\footnotesize
\begin{verbatim}
For example, for subobjects.
Implications can be seen as inclusions.
ýaÝA.P(a)⊃Q(a)
{aÝA|P(a)} \subset {aÝA|Q(a)}
Categorically,
{a|P(a)} ------> {a|Q(a)} /{a|P(a)}\ /{a|Q(a)}\
v v | v | | v |
| | | | | ---> | | |
v v | v | | v |
A -------------> A \ A / \ A /
This is a morphism between two objects of Set^>->, where
Set^>-> is the category of monic arrows between objects of Set.
Set^>-> is also called Sub(Set) - the category of subojects of Set.
Notational trick:
/{a|P(a)}\ /{a|Q(a)}\
| v | | v |
{a||P(a)} ---> {a||Q(a)} := | | | ---> | | |
| v | | v |
\ A / \ A /
The `|' in {a|P(a)} is called the ``such that'' bar;
we're doubling it to represent subobjects.
We downcase that into:
a||P(a) |-> a||Q(a)
this morphism - in Set^>-> is not just a mapping of points...
in fact, it's two morphisms in Set - a|P(a) |-> a|Q(a) and a|->a -
plus the information that the square below commutes:
a|P(a) |---> a|Q(a)
/ /
| |
v v
a |--------> a
\end{verbatim}
}
\newpage
% --------------------
% «subobject-maps» (to ".subobject-maps")
% (s "Maps between subobjects: the general case" "subobject-maps")
\myslide {Maps between subobjects: the general case} {subobject-maps}
{\myttchars
\footnotesize
\begin{verbatim}
More generally,
{a||P(a)} -> {b||Q(b)} is:
b:=b(a)
/{a|P(a)}\ /{b|Q(b)}\ a|P(a) |-------> b|Q(b)
| v | | v | / /
| | | ---> | | | | |
| v | | v | v b:=b(a) v
\ A / \ B / a |------------> b
a||P(a) |-> b||Q(b) means ýa.P(a)⊃Q(b(a)).
Note the use of a bit of ``physicist's notation'' here -
in the presence of a function f = a|->b the value of b can
be seen as a function of a, and a physicist would write
b=f(a) or b=b(a)... we will prefer b=b(a) to avoid using
new letters, and the dictionary will translate such
expressions (atrocities!) into something mathematically
sound.
We will usually write pseudopoints like a||P(a)
as ``P(a) over a'' (in parentheses), and we will draw these
things over their ``codomain projections'':
{a||P(a)} ---> {b||Q(b)} /P(a)\ |---> /Q(b)\
- - \ a / \ b /
cod | | cod || ||
v f v \/ b:=b(a) \/
A -----------> B a |--------> b
In some rare occasions, when space is at premium, we will
write just P(a) instead of ``P(a) over a''.
The ``codomain projection'' functor arrows will usually
not be draw.
{a||P(a)} ---> {b||Q(b)} P(a) |-----> Q(b)
f b:=b(a)
A -----------> B a |--------> b
\end{verbatim}
}
% **** TODO: ****
% add ( P ) as a notation for pseudopoints (like a,b||P)
% (a,b)
% «.quantifiers-categorically» (to "quantifiers-categorically")
\newpage
% --------------------
% «quantifiers-categorically» (to ".quantifiers-categorically")
% (s "Quantifiers, categorically" "quantifiers-categorically")
\myslide {Quantifiers, categorically} {quantifiers-categorically}
{\myttchars
\footnotesize
\begin{verbatim}
In Set^>-> the functors that quantify over a variable
are adjoints to ``weakening functors'' that add a dummy
variable to the domain:
{a,b||P(a,b)} |---> {a||Îb.P(a,b)} P(a,b) ===> Îb.P(a,b)
| | - -
| <-> | | <-> |
v v v v
{a,b||Q(a)} <------| {a||Q(a)} Q(a) <====== Q(a)
| | - -
| <-> | | <-> |
v v v v
{a,b||R(a,b)} |---> {a||ýb.R(a,b)} R(a,b) ===> ýb.R(a,b)
A×B ----------------> A a,b |------> a
These functors do not operate on the whole of Set^>-> -
they go from one ``fiber'' of Set^>-> to another.
The best way to formalize this is via /fibrations/;
Set^>-> is a fibration over Set.
A fibration is composed of:
an ``entire category'' Set^>->
a ``base category'' Set
a ``projection functor'' Cod: Set^>-> -> Set
and enough ``cartesian liftings''. (?!?!?! - next slide)
In our diagrams we will not usually draw the projection functors.
Instead we will just draw the objects of the entire category
over their projections - and we will often omit the part
of their names that can be recovered from the projections.
In the diagram above we wrote just `Q(a)', not `a||Q(a)'.
\end{verbatim}
}
\newpage
% --------------------
% «archetypes-more-1» (to ".archetypes-more-1")
% (s "More notes about archetypes (1)" "archetypes-more-1")
\myslide {More notes about archetypes (1)} {archetypes-more-1}
{\myttchars
\footnotesize
\begin{verbatim}
There are different levels of mathematical truths -
some ideas are "obvious", and I can use them implicitly
or by just mentioning them briefly, and my interlocutor
will accept them; other ideas - for example, theorems
that have been published, but whose proofs are hard -
I can only use with extreme care, and a proof that makes
use of these hard theorems automatically gets marked
with a small red or black flag -
A statement like "the composite (a,b)|->(b,a)|->(a,b)
is the identity" takes very little "mental space", and
is intuitively true, even though in different settings
it may have different proofs, and some of these proofs -
in ð-calculus, for example - may look too technical at
first...
Where do these "intuitively true statements" live?
What languages can we develop to work with them?
Here is a diagram showing some kinds of mathematical
truths. The arrows go from "weaker truths" to "stronger
truths".
True in a particular model
v
True in some particular models
v
True in all models
v
- Provable --
/ | \
/ | \
v v v
Provable by Provable with Provable with
elementary means a proof that a proof that
generalizes I understand
well \ /
v v
Provable in an
insightful way
\end{verbatim}
}
\newpage
% --------------------
% «archetypes-more-2» (to ".archetypes-more-2")
% (s "More notes about archetypes (2)" "archetypes-more-2")
\myslide {More notes about archetypes (2)} {archetypes-more-2}
{\myttchars
\footnotesize
\begin{verbatim}
(Note: D stands for a DAG - usually finite,
and in most examples having at most five
vertices)
For me, this is the archetype behind the idea of "topos":
Every Set^D is a topos.
However, the resulting concept is much more general than that -
and the "archetypical language" for a topos comes from a very
particular case - Set^D = Set, D = the one-point DAG.
This is the archetype of a "sheaf":
Every Set^O(D)^op has a notion of ``\dbul-sheaf''.
The resulting notion of ``sheaf'' - based on Lawvere-Tierney
topologies and modalities - admits several other kinds of
sheaves: ``¬¬-sheaves'', ``(\aa⊃)-sheaves'', ``(\bb∨)-sheaves'',
and forcing.
The precise definition of what a topos is
can be expressed in the language of the archetype;
we can use the language of the archetype to express most
(i.e., "enough") of the most important constructions
and theorems; we can use it to help us build dictionaries
between the standard, more precise notations; and proofs done
in the archetype take relatively little mental space, and
generalize easily. Also, the archetypal language for a
topos may collapse (in the syntax!) some things that are
different in some toposes, but it is "non-trivial enough" -
it does not collapse too much.
\end{verbatim}
}
\newpage
% --------------------
% «archetypes-more-3» (to ".archetypes-more-3")
% (s "More notes about archetypes (3)" "archetypes-more-3")
\myslide {More notes about archetypes (3)} {archetypes-more-3}
{\myttchars
\footnotesize
\begin{verbatim}
What do I expect from an archetype and its language?
"It should be expressive enough"
Most of the basic theory - constructions and theorems -
can be done in the archetypal language, and then lifted
to the general case; the general definition can be
expressed using the archetypal language.
"It collapses enough"
The archetypal syntax identifies (in the "wd[·]" sense)
many constructions that are expected to give the same
results.
"It is non-trivial enough"
Even though the archetypal syntax may identify some
constructions that are distinct in some models
(see the example "x,ab,cd<-|x,a,b,c,d" in monads)
it does not collapse too much.
Also, it can't take up too much "mental space" -
\end{verbatim}
}
% [# **** TODO: ****
% add equality.
% #]
% Should I add these?
% (find-THfile "2007dnc-bcc.blogme")
% (find-THfile "2007dnc-halfdnc.blogme")
% (find-THfile "2007dnc-lst.blogme")
% (find-THfile "2007dnc-monads.blogme")
% (find-THfile "2007dnc-sdg.blogme")
% (find-THfile "2007hyperdoctrines.blogme")
% (find-THfile "2007lcccs.blogme")
% (find-THfile "2007semantics.blogme")
% (find-THfile "2007sheaves.blogme")
% (find-THfile "")
%*
\end{document}
% ----------
% Not typeset yet...
----
What are the proofs that I can re-deduce easily,
Mental space
But are actually more general than that
The "archetypical language" for topos is based on Set,
but with downcasings
that is it is a lifting
based on Set
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: