λ, etc)
(Chapa 1)


Sheaves for children

1. Sheaves for Children

Category Theory     <->  lambda calculus
  Topos Theory
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) lambda-calculus -
because lambda-calculus is made for expressing computations. Roughly,
we have this parallel:


3. Why? (2)

The new Girl from Ipanema

2012: 4-month long strike involving almost all federal universities in

2013: many protests in Brazil, with many demands

Public education being dismantled.

Clear split between ``research universities'' and ``teaching

Most texts about CT are for specialists in research universities...

Category theory should be more accessible.

To whom?...

Non-specialists (in research universities)
Grad students (in research universities)
Undergrads (in research universities)
Non-specialists (in conferences - where we have to be quick)
Undergrads (e.g., in CompSci - in teaching colleges)
4. ZSets

Take a finite, non-empty 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
"well-positioned", and we call them _ZSets_.

We can use a positional notation with bullets
to denote our favourite ZSets (unambiguously!)...

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 transitive-reflexive closure.

The operation R |-> R^* is well-known.
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. Truth-values

A function from a ZSet D to {0,1} is a _modal truth-value_.

The positional notation gives us a way to write modal truth-values
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 truth-values.

    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 truth-values are called
_intuitionistic truth-values_.
8. Priming

For any ZDAG D, write Omega(D) (supset Pts(D)) for the set of all
intuitionistic truth-values on D.

Example: Omega(V) = {...}

             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)

   (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 3-thin when 3 notsubseq bbD.
We say that bbD is square-thin when square notsubseq bbD.
We say that bbD is thin when it is both 3-thin and square-thin.
Fact: is bbD is 3-thin 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 tree-like frame; By making
a ZDAG with that shape - with possibly more points -
we can make a ZDAG-countermodel 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
transitive-reflexive 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!):