Downcasing Categories

Quick index:
```1. DNC for Categories
=====================

```
```2. Downcasing categorical diagrams (in general)
===============================================
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...

L

```
```3. Why we want to allow pseudopoints
====================================
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

More generally:

b:=b(a)
a|P(a) |-------> b|Q(b)
/                /
|                |
v     b:=b(a)    v
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.

```
```4. Quantifiers, categorically
=============================
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)'.

```