Downcasing Sets

Quick index:
```1. Main idea: lifting archetypal proofs
=======================================
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.
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'').

```
```2. Lifting set-like notation
============================
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.

```
```3. Starting point: the Curry-Howard Isomorphism
===============================================
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''.

```
```4. Main ideas
=============
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)'.

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'.

Reconstructing the types and the dictionary from trees
------------------------------------------------------
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.

```
```5. Contexts and discharges
--------------------------
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).

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 if 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).

```
```6. Expanding trees
==================

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

L

```
```7. Theorems for Free
====================
* 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.

L

```
```8. Ambiguity plays on our side (usually)
========================================

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''.

L

```

```9. Downcasing functors
======================
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.

```
```10. Products via natural transformations
========================================
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 /

```
```11. Downcasing Natural Transformations
======================================
(...)
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))

```
```12. Translating bigger trees
============================

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

```