
Sheaves for children
1. Sheaves for Children
Category Theory <> lambda calculus
Topos Theory
Sheaves

2. Why?
Category theory fascinates many people, but is usually done in a level
that is too abstract...
At the same time, that level of abstraction is exactly what is needed
to make lots of proofs be _almost_ automatic: _proving_ something in
CT means _constructing_ something, and all ``natural'' constructions
are equivalent. More or less like this:
Let A and B be (arbitrary) sets. Then there is an ``obvious''
function flip:A×B>B×A.
This idea can be formalized in (typed, polymorphic) lambdacalculus 
because lambdacalculus is made for expressing computations. Roughly,
we have this parallel:
lambdacalculus:
computations
lambdaterms
categories:
constructions
diagrams

3. Why? (2)
The new Girl from Ipanema
2012: 4month long strike involving almost all federal universities in
Brazil
2013: many protests in Brazil, with many demands
Public education being dismantled.
Clear split between ``research universities'' and ``teaching
colleges''
Most texts about CT are for specialists in research universities...
Category theory should be more accessible.
To whom?...
Nonspecialists (in research universities)
Grad students (in research universities)
Undergrads (in research universities)
Nonspecialists (in conferences  where we have to be quick)
Undergrads (e.g., in CompSci  in teaching colleges)
(``Children'')

4. ZSets
Take a finite, nonempty subset of Nē;
translate it lowerleftwards as most as possible in Nē,
until you get something some touches both axes.
Subsets of Nē obtained in this way are said to be
"wellpositioned", and we call them _ZSets_.
We can use a positional notation with bullets
to denote our favourite ZSets (unambiguously!)...
V
Lambda
Kite
House

5. ZDAGs
An arrow between points of Nē that goes one unit down
and 0/1/1 units horizontally is called a _black pawn's move_.
Take a ZSet, D, and draw all possible black pawns moves
between its points; that gives us a set of arrows BPM(D),
that turns D, a ZSet, into a directed, acyclical, graph
in a canonical way.
Notation (note the change of font):
D is a ZSet,
bbD = (D, BPM(D)) is a _ZDAG_.
Example: K and bbK.

6. Closure and essentiality
We usually prefer transitive and reflexive relations.
If (A,R) is a graph,
then (A,R*) is its transitivereflexive closure.
The operation R > R^* is wellknown.
Now look for the smallest set of arrows, R^,
such that (R^)^* = R^*.
Example: bbK <==> bbK*
Fact: this generalizes to _any_ ZSet 
on ZSets/ZDAGs the dual operation to "*" is well defined!
For any ZSet D, (D, BPM(D)) is canonical in another sense 
the set BPM(D) has only the arrows that are "essential" to
generate bbD = (D, BPM(D)^*).
Duals of closure operations are usually _partial_ functions...
Magic fact: in the world of ZSets and ZDAGs _many_ closure
operations  many more that expected  have duals!
_Some people hate this_  they seem to believe that a family
of particular cases in which some bonus properties hold
is useless for understanding the general case...
_They are wrong._

7. Truthvalues
A function from a ZSet D to {0,1} is a _modal truthvalue_.
The positional notation gives us a way to write modal truthvalues
very compactly, and the points on a ZSet have a natural order 
the "reading order", in which we read them line by line,
left to right in each line.
This gives us a way to _read aloud_ modal truthvalues.
Example:
1 0
2 3 0 1
4 1
5 0
reading P:K>{0,1}
order on K "0,0,1,1,0"
Now consider that each 1 is covered with black paint.
Then Kite 00110 is not _stable_, because the paint on position 4
may flow into the 0 of position 5.
_Stable_ modal truthvalues are called
_intuitionistic truthvalues_.

8. Priming
For any ZDAG D, write Omega(D) (supset Pts(D)) for the set of all
intuitionistic truthvalues on D.
Example: Omega(V) = {...}
Diagram:
1 1 (1,3)
1 / \
/ \ / \
v v v v
1 0 0 1 (0,2) (2,2)
1 1 \ /
\ / \ /
v v v v
0 0 (1,1)
1 
 
v v
0 0 (1,0)
0
(Omega(V), supseteq) iso (K, BPM(K)) = V'
Some Omega(D)s are (isomorphic to) ZDAGs!
Which ones?

9. Priming: theorems
For each ZDAG bbD, let catD be bbD^* seen as a category.
We say that bbC subset bbD when there is a
proper inclusion catC `> catD.
We say that bbD is 3thin when 3 notsubseq bbD.
We say that bbD is squarethin when square notsubseq bbD.
We say that bbD is thin when it is both 3thin and squarethin.
Fact: is bbD is 3thin then Omega(D) is (iso to) a ZDAG.
Fact: is bbD is thin then Omega(D) is (iso to) a ZDAG.
Fact: every D' = (Omega(D), supseteq)  whether planar or not 
is a Heyting algebra  i.e., we can interpret T, F, and, or, imp,
not on it.
So: priming gives us LOTS of Heyting algebras.

10. Modal logic
On any ZDAG D the directed graph bbD^* = (D, BPM(D)^*)
is a Kripke frame, and Pts(D) is a model of S4;
also, Omega(D) is a Heyting algebra, and a model of
IPL (intuitionistic propositional logic); the Tarski
translation holds, with these definitions (where "M"
means the "modal" operation, and "I" the "intuitionistic"
operation): if P,Q in Omega(D), then
T_I = T_M
F_I = F_M
P and_I Q = P and_M Q
P or_I Q = P or_M Q
P imp_I Q = nec (P imp_M Q)
not_I P = nec (not_M P)
Amazing fact: for any wff E in IPL that is not
a theorem, the method of tableaux can find a finite
countermodel for it, using a treelike frame; By making
a ZDAG with that shape  with possibly more points 
we can make a ZDAGcountermodel for E.
Example: let E be ... .
Let P = ..., Q = ... .
Then: ... = ... = ... != T
Thus E = ... is not a tautology in IPL,
and can't be a theorem of IPL 
but E' = ... is a theorem...
So ZDAGs can give people a concrete feeling of how
intuitionistic propositional logic works  which WFFs
can be theorems, which ones can't be, and why.

11. Categories
Remember: each catD  i.e., (D, BPM(D)^*) can be seen as a category 
the identity maps and the composition of morphisms is trivial
to define.
Each D' is a Heyting Algebra  a cartesian closed category , and we
have nice names for its objects  for example, V' is (the
transitivereflexive closure of) this:
We can explain the operations and, or, imp, not, plus T and F, and
their properties, by their categorical definitions (via diagrams!):

