Downcasing types (Introductory notes)

Eduardo Ochs

eduardoochs@gmail.com
http://angg.twu.net/
http://angg.twu.net/math-b.html
http://angg.twu.net/LATEX/2007dnc-sets.{tex,dvi,pdf}

Written: 2007. L^{A}TEXing and minor revisions: may 2008. Current version: 2008may20 (see the footer)

Index of the slides:

Main idea: lifting archetypal proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 Lifting set-like notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Starting point: the Curry-Howard Isomorphism . . . . . . . . . . . . . . . . . . . . . . . . . 4 Main ideas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Reconstructing the types and the dictionary from trees . . . . . . . . . . . . . . . . . . 6 Contexts and discharges . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7 Contexts and discharges (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Expanding trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Theorems for Free . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 Ambiguity plays on our side (usually) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Downcasing functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Products via natural transformations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Downcasing Natural Transformations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Translating bigger trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 Downcasing categorical diagrams (in general) . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Why we want to allow pseudopoints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .17 Maps between subobjects: the general case . . . . . . . . . . . . . . . . . . . . . . . . . . . . .18 Quantifiers, categorically . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .19 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.
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'').

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 [figure] R
Later, Set (or, more precisely, the fibration Set^>->),
we will also be our archetypal hyperdoctrine.

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 [figure] 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 `&', ` [figure] ', `\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''.

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

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.

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 [figure] R    P&Q|-P&Q    P&Q|-Q      Q [figure] R|-Q [figure] R
   ---    ----------    --------    --------------------
    P         R          P&Q|-P         Q [figure] R,P&Q|-R
    -----------          -------------------------
       P&R                     Q [figure] R,P&Q|-P&R
Now we can understand the `` [figure] -introduction'' rule;
it involves a discharge.
           [P&Q]^1                    P&Q|-P&Q
           -------                    --------
  [P&Q]^1     Q     Q [figure] R    P&Q|-P&Q    P&Q|-Q      Q [figure] R|-Q [figure] R
  -------     ---------    --------    --------------------
     P           R          P&Q|-P         Q [figure] R,P&Q|-R
     -------------          -------------------------
         P&R                     Q [figure] R,P&Q|-P&R
       -------1                  ------------
       P&Q [figure] P&R                   Q [figure] R|-P&Q [figure] 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).

Contexts and discharges (2)

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 `` [figure] -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).

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

Theorems for Free

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 [figure] 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 [figure] 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.

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

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.

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 /

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

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

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

Why we want to allow pseudopoints

For example, for subobjects.
Implications can be seen as inclusions.
  ∀a∈A.P(a) [figure] 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

Maps between subobjects: the general case

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) [figure] 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

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