% (find-angg "LATEX/2009dnc-in-coq.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009dnc-in-coq.tex && latex    2009dnc-in-coq.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009dnc-in-coq.tex && pdflatex 2009dnc-in-coq.tex"))
% (eev "cd ~/LATEX/ && Scp 2009dnc-in-coq.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2009dnc-in-coq.dvi"))
% (find-dvipage "~/LATEX/2009dnc-in-coq.dvi")
% (find-pspage  "~/LATEX/2009dnc-in-coq.pdf")
% (find-pspage  "~/LATEX/2009dnc-in-coq.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2009dnc-in-coq.ps 2009dnc-in-coq.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2009dnc-in-coq.ps 2009dnc-in-coq.dvi && ps2pdf 2009dnc-in-coq.ps 2009dnc-in-coq.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2009dnc-in-coq.pdf" (ee-twupfile "LATEX/2009dnc-in-coq.pdf") 'over)
% (ee-cp "~/LATEX/2009dnc-in-coq.pdf" (ee-twusfile "LATEX/2009dnc-in-coq.pdf") 'over)
% (eev "Scp ~/LATEX/2009dnc-in-coq.pdf edrx@angg.twu.net:slow_html/LATEX/")

% «.convention»	(to "convention")
% «.yoneda»	(to "yoneda")


% \documentclass[oneside]{book}
% \documentclass[a4paper,12pt]{article}
\documentclass[a4paper]{article}
\usepackage{indentfirst}

\usepackage[latin1]{inputenc}
\usepackage{edrx08}       % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty"  -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex   % (find-dn4ex "edrxheadfoot.tex")
\begin{document}

\input 2009dnc-in-coq.dnt

%
% (eedn4-51-bounded)

%Index of the slides:
%\msk
% To update the list of slides uncomment this line:
%\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")

\def\Cod{¦{Cod}}
\def\Dom{¦{Dom}}
\def\Cod{\operatorname{Cod}}
\def\Dom{\operatorname{Dom}}
\def\wit{Ðw}
\def\Wits{ÐW}
\def\welld{Ð{wd}}
\def\Proofs{Ð{Proofs}}
\def\squigto{\rightsquigarrow}
\def\squigbij{\leftrightsquigarrow}
\def\Sets{{Ð{Sets}}}
\def\Q{\mathbb{Q}}
\def\pded#1{\begin{pmatrix}\ded{#1}\end{pmatrix}}
\def\sm#1{\begin{smallmatrix}#1\end{smallmatrix}}

% (find-es "tex" "llangle-and-rrangle")
% (find-dn4ex "edrx08.sty" "ttchars")
% (find-symbolspage 54 "\\llangle")
% (find-symbolstext    "\\llangle")
% http://ubuntuforums.org/archive/index.php/t-722871.html
\def\llangle{\langle\!\langle}
\def\rrangle{\rangle\!\rangle}
\def\angg#1{\llangle#1\rrangle}
\def\myotherttchars{
  \def«{\ttchar{$\llangle$}}
  \def»{\ttchar{$\rrangle$}}
  }
\def\myttchars{\basicttchars\myotherttchars}

\widemtos


\section{Introduction}
\label{introduction}



How do we formalize a proof in Category Theory? What is the correct
level of detail? Which entities should we introduce first?

Well, this depends on our target audience; if we are speaking to a
Category Theorist then we may start by saying just, for example, ``let
$f$ be a morphism'', and it will be understood that we have two
objects, $\Dom f$ and $\Cod f$, belonging to the same category --- at
this point unnamed --- and that $f$ goes from $\Dom f$ to $\Cod f$; if
later we say $f: A \to B$ or $A \ton{f} B$ then we will be giving
better (and shorter) names for $\Dom f$ and $\Cod f$, but the category
where $A$ and $B$ live may remain unnamed for a while more...

% rather than to a human
% (find-es "coq" "email-about-7-uples")

If we are talking to a proof assistant --- Coq, say --- instead of to
a human then we are forced to declare our entities in a certain order,
and to name all of them. For example:
%
{% \myttchars
% \footnotesize
\begin{verbatim}
  Variable CatC : Categories.
  let (C_0, Hom_C, id_C, o_C, idL_C, idR_C, assoc_C) := CatC in
    Variable A B : C_0, f : Hom_C A B.
    ...
  end.
\end{verbatim}
}

In this note we will show how to formalize some constructions and
proofs in a proof assistant in a way that:

\msk

1) lets us choose just a very few names,

2) lets us use names that are very close to a certain graphical
notation,

3) lets us split our constructions and proofs in two layers, or parts:
a ``syntactical'' part, that must necessarily come first, and a
``logical'' part,

4) lets us build easily dictionaries between several standard
notations.

\msk

We will say that a construction (or proof) that has both its
syntactical part and its logical part is happening in the ``real
world''; by dropping its logical part and keeping just its syntactical
part we obtain a corresponding construction in the ``syntactical
world''. We will call this passage from the real world to the
syntactical world a ``projection'' --- as projections discard some
information (intuitively coordinates, or components) and forget some
distinctions. The opposite operation is a ``lifting'': we may start
with a syntactical construction or proof, and then try to lift that to
the real world. The ``projection'' direction is easy, and we can
always be done (section \ref{abcats}; explain abelian categories, and
which ``always'' is that); the ``lifting'' direction is hard, and I
don't even know how to characterize when a given lifting can be done;
see the list of problems in section \ref{future}.

The plan of this paper is as follows. In section \ref{cats-in-coq} we
define ``category'', ``protocategory'', ``isomorphism'',
``proto-isomorphism'', etc, in the right way (for our purposes!). In
section \ref{dnc-in-coq} we explain a trick to make Coq accept our
notation; in section \ref{yoneda} we present an example: a syntactical
proof of the Yoneda Lemma. In section \ref{nd-for-cats}. we present a
system of Natural Deduction for (proto-)categories, and in section
\ref{nd-for-dt} we sketch how it can be extended to a system of
Natural Deduction for dependent types. Section \ref{future} discusses
open problems and directions for future work.



\section{Downcasing Functors}
\label{downcasing-functors}

\begin{quote}
  {\sl Fix an object $A$ of $\Set$. Let $(A×)$ be the functor that takes
    each object $B$ to $A×B$.}
\end{quote}

Why do we say ``{\sl the}'' functor in the sentence above? A functor,
$F$, is composed of an action on objects, $F_0$, and an action on
morphisms, $F_1$ --- plus some ``assertions'', that we will discuss
soon (section \ref{downcasing-assertions}) ---; the description above
says only that $F_0$ is $B \mto A×B$, i.e., $ðB¨\Sets.A×B$. In a first
moment we only know that $F_1$ is ``obvious''. How do we deduce it?

Let's draw a diagram. For a morphism $f:B \to C$ in $\Set$ we have
%
%D diagram dncf1
%D 2Dx     100       +30     +25       +30    +25     +30
%D 2D          F_0 
%D 2D  100 B |-----> F_0B    {B} |---> A×B    b ====> a,b
%D 2D      |          -       |         |     -        -
%D 2D      |   |-->   |       |   |-->  |     |  |->   |
%D 2D      v          v       v         v     v        v
%D 2D  +30 C |-----> F_0C    {C} |---> A×C    c ====> a,c
%D 2D
%D (( B F_0B  C F_0C
%D    @ 0 @ 1 |-> .plabel= a F_0
%D    @ 0 @ 2  -> .plabel= l f
%D    @ 1 @ 3  -> .plabel= r F_0f
%D    @ 2 @ 3 |-> .plabel= b F_0
%D    @ 0 @ 3 harrownodes nil 20 nil |->
%D ))
%D (( {B} A×B  {C} A×C
%D    @ 0 @ 1 |-> .plabel= a (A×)_0
%D    @ 0 @ 2  -> .plabel= l f
%D    @ 1 @ 3  -> .plabel= r A×f
%D    @ 2 @ 3 |-> .plabel= b (A×)_0
%D    @ 0 @ 3 harrownodes nil 20 nil |->
%D ))
%D (( b a,b  c a,c
%D    @ 0 @ 1  =>
%D    @ 0 @ 2 |->
%D    @ 1 @ 3 |->
%D    @ 2 @ 3  =>
%D    @ 0 @ 3 harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$\diag{dncf1}$$

The square at the right is the downcased version of the middle square.
The morphism $f$, a function, takes each point of $B$, $b$, to a point
of $C$, $c := f(b)$.

The notation $b \mto c$ --- instead of $b \mto f(b)$ --- is an
extrapolation of the the convention used by physicists. Given a
trajectory, $q(t) = (x(t), y(t), z(t))$, and two instants, $t_0$ and
$t_1$, physicists define by default that $x_0 = x(t_0)$, $q_0 = (x_0,
y_0, z_0)$, and so on, and sometimes $x=x(t)$, $y=y(t)$, $z=z(t)$,
$q=(x,y,z)$. Instead of defining lots of rules for default meanings we
will do domething else.

Our input to Coq will be filtered through a simple preprocessor that
allows ``long names'' --- downcasings, plus much more (maybe {\sl too
  much} more). Let's see an example:

% (find-es "tex" "verbatimbox")
% (find-dn4ex "edrx08.sty" "ttchars")
% (find-gregsymbolspage 1)
% (find-texbookpage 1)
% (find-texbookpage (+ 11 469) "\\langle")
% (find-texbookpage (+ 11 146) "\\langle")

\bsk

{\myttchars
\begin{verbbox}
a := proj1 «a,b»
b := proj2 «a,b»
c := «b|->c» b
«a,c» := (a, c)
...
\end{verbbox}
%
$\begin{array}{ccc}
  \theverbbox[c] & \squigto & \mathtt{foo.v} \\
       \dnto \\
   \mathtt{foo.dnc} \\
   \text{in ascii} \\
  \end{array}
$
}

\bsk

The preprocessor first builds a listing of all the long names (the
$\angg{\ldots}$ things) that appear in a set of \texttt{.dnc} files,
then associates a Coq-friendly identifier of the form \texttt{dnc}{\sl
  nnn} to each of them, then translates all the \texttt{.dnc} files to
\texttt{.v} files.

A modification of that idea allows one to use Coq interactively from
Emacs with a similar kind of long name translation; but this is not
relevant here (see dnc-0.el for details).

For typesetting \texttt{.dnc} files, like in the lower rectangle
above, we use a different kind of translation. We borrow the idea of
``abbreviations'' from Dednat4. In the default abbrev table for
Dednat4, ``\texttt{|->}'' becomes ``\verb|\tnto |'', and
``\verb|\tnto |'' is \verb|\def|'d in the default \LaTeX\ preamble for
Dednat4 as

\begin{center}
\verb.\def\tnto{\overset{\bullet}{\to}}.
\end{center}

The expansion process considers the longest matching abbrev at any
point. So, as ``\verb.|-.'' expands to ``\verb|\vdash |'',
``\verb.P,Q,R|-S.'' expands to ``\verb.P,Q,R\vdash S.'', which
typesets as $P,Q,R\vdash S$; ``\verb.b|->c.'' typesets as $b \mto c$.


% (find-books "__cats/__cats.el" "lawvere")
% (find-lawverecmpage (+ 15  13) "internal diagram of a set")

A remark: downcasings correspond, {\sl very} loosely, to the
``internal view'' of a function (see LawCM, p.14). For example,


%D diagram internal-view
%D 2Dx      100      +50
%D 2D  100 \N -----> \R
%D 2D
%D 2D  +15
%D 2D  +8   0 |----> 0{}
%D 2D  +8   1 |----> 1{}
%D 2D  +8   2 |----> \sqrt{2}
%D 2D  +10  \vdots   \vdots{}
%D 2D  +10  49 |---> 7
%D 2D  +12  n |---> \sqrt{n}
%D 2D
%D (( \N \R -> .plabel= a Ð{sqrt}
%D    0 0{} |->
%D    1 1{} |->
%D    2 \sqrt{2} |->
%D    \vdots place   \vdots{} place
%D    49 7 |->
%D    n \sqrt{n} |->
%D ))
%D enddiagram
%D
$$\diag{internal-view}$$


We are free to use long names as we please. Coherence is desirable but
not mandatory, and we may leave to define what is coherent naming
afterwards --- or never. This, for me, is a charming way to state that
$ýn¨\N.\sqrt{4n}=2\sqrt{n}$:


%D diagram sqrt-4
%D 2Dx      100     +30    +30      +30    +30       +30
%D 2D  100  25 |--> 5      \N ----> \R     n |---> \sqrt{n}
%D 2D       -       -      |         |     -          -
%D 2D       |       |      |         |     |          |
%D 2D       |       |      |         |     |          v
%D 2D  +21  v       v      v         v     v       2\sqrt{n}
%D 2D  +09 100 |--> 10   {}\N ----> \R{}  4n |---> \sqrt{4n}
%D 2D
%D (( 25 5 100 10
%D    @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D ))
%D (( \N \R {}\N \R{}  
%D    @ 0 @ 1 -> .plabel= a \sqrt{\;}
%D    @ 0 @ 2 -> .plabel= l 4·
%D    @ 1 @ 3 -> .plabel= r 2·
%D    @ 2 @ 3 -> .plabel= a \sqrt{\;}
%D ))
%D (( n \sqrt{n} 4n 2\sqrt{n} \sqrt{4n}
%D    @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 4 |->
%D ))
%D enddiagram
%D
$$\diag{sqrt-4}$$

In some contexts 25 is so big that $25 \mto 5$ ``can only be'' the
square root; similarly, $25 \to 100$ ``can only be'' multiplication by
4, and so on, and the commutativity of the square can be expressed as:

{\myttchars
\footnotesize
\begin{verbatim}
sqrt :=
  «25|->100» : N -> N = *4
  «100|->10» : N -> R = sqrt
  ...
  «\wd[25|->10]» : ...
\end{verbatim}
}

We will say that $\angg{25 \mto 5 \mto 10}$ and $\angg{25 \mto 100
  \mto 10}$ are two ``natural constructions'' for $\angg{25 \mto 10}$,
and we will use the last notation above, $\angg{welld{25 \mto 10}}$
--- that we pronounce as ``$25 \mto 10$ is well defined'' --- to mean
``all the most obvious natural constructions for $25 \mto 10$ yield
the same result''; these ``most obvious natural constructions'' will
usually be just two, only very rarely three, four, or more; in any
case, the Coq code will expand each $\angg{\welld[\ldots]}$ into an
explicit equality. Note that a $\angg{\welld[\aa]}$ is (usually) much
weaker than a coherence theorem (see \citation{Kromer}, p.\_\_) that
states that {\sl all} possible natural constructions for terms with
the same type as $\aa$ give the same result.

\section{Natural Deduction}
\label{natural-deduction}

\def\fourdicts{
  \begin{array}{rcl}
             a,b &:=& d \\
        b \mto c &:=& f \\
                        \\
               b &:=& '(a,b)       \\
               c &:=& (b \mto c)(b) \\
             a,c &:=& \ang{a,c}     \\
    a,b \mto a,c &:=& ð(a,b).(a,c)  \\
  \end{array}
  }

%:&\&
%:&´
%:×{×}
%:<\langle 
%:>\rangle 
%:
%:     f¨B->C                 Q->R      
%:  =============(?)      ============(?)
%:  f^\#¨A×B->A×C         (P&Q)->(P&R)   
%:                                
%:  ^4-functional?        ^4-logical?   
%:  
%:           [P&Q]^1                    [d¨A×B]^1          
%:           -------                    ---------          
%:  [P&Q]^1     Q     Q¶R   [d¨A×B]^1      'd¨B     f¨B->C 
%:  -------     ----------   ---------     ---------------- 
%:     P            R          d¨A           f('d)¨C      
%:     --------------          -----------------------      
%:         P&R                      <d,f('d)>¨A×C               
%:      ----------1          ------------------------------1
%:      (P&Q¶P&R)              ðd¨A×B.<d,f('d)>:A×B->A×C
%:                                                         
%:      ^4-logical              ^4-functional                  
%:
$$\ded{4-logical} \qquad \ded{4-functional}$$

%:           [a,b]^1                  [A×B]^1              
%:           -------                  -------               a,b := d
%:   [a,b]^1    b     b|->c   [A×B]^1    B     B->C       b|->c := f
%:   -------    -----------   -------    ----------  
%:       a           c            A           C               a :=  (a,b)     
%:       -------------            -------------               b := '(a,b)     
%:           a,c                      A×C                     c := (b|->c)(b)  
%:         ---------                ---------               a,c := <a,c>       
%:         a,b|->a,c                A×B->A×C          a,b|->a,c := ð(a,b).(a,c)
%:
%:         ^4-dnc                   ^4-sets
%:
$$\cded{4-dnc} \qquad \cded{4-sets}$$

$$\fourdicts$$

The squiggly arrow going downwards is evidently a projection --- it
just drops the rules and the ``term:'' part of each ``term:Type''
declaration --- the upper dotted arrow is the Curry-Howard
isomorphism, and the lower dotted arrow is a downcasing (to the left)
and an uppercasing (to the right).

Amazingly, the ``term:Type'' tree at the upper right can be
reconstructed from the downcased tree at the lower left.

Each bar of the downcased tree can be read as: ``if we know the values
of the terms above the bar then we have a natural construction for the
term below the bar''. This induces a dictionary --- of a new kind, not
of abbrevs as in section \_\_ --- that defines all entries not in the
``leaves'' of the tree as terms:

{\myttchars
\footnotesize
\begin{verbatim}
«b» := proj2 «a,b» etc
\end{verbatim}
}

If we preceed this with declarations for the left names as variables
--- and if we handle the discharges correctly, and if we use
uppercasings to determine the types --- then the root of the tree
becomes a term, whose free variables are the names of the undischarged
leaves.

We will use the symbol `$\equiv$' to mean ``change of notation''. Now,
if we just give the right standard names --- coming from the
``term:Type'' tree in the upper left, in diagram \_\_, --- to the
[undischarged?] variables, we can reconstruct the ``term:Type'' tree,
{\sl exactly}, from the downcased tree.

Let's review what we have done. Natural deduction trees can be read as
terms:
%
$$\ded{4-dnc} \quad \squigto \angg{b} := \angg{b} ...$$
%
and if we add dictionary entries for the standard names for the
variables in a downcased tree,
%
$$\angg{a,b} \equiv p ...$$
%
then the downcased tree can be considered as a shorthand
representation for the full, standard ``term:Type'' tree.

We left a question pending in section \_\_ --- why the action of a
functor $(A×)$ on morphisms, $(A×)_1$, is ``obvious'', and how do we
obtain it?

In the diagram

%D diagram bleu
%D 2Dx     100    +30
%D 2D  100 b ===> a,b
%D 2D      -       -
%D 2D      |       |
%D 2D      v       v
%D 2D  +30 c ===> a,c
%D 2D
%D (( b a,b  c a,c
%D    @ 0 @ 1 => @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D    @ 0 @ 3 harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$\diag{bleu}$$

the problem was to obtain the middle arrow, $(b \mto c) \mto (a,b \mto
a,c)$. In (``logical'') Natural Deduction it is common to abbreviate a
series of steps with a double bar; we will do something similar with
our ``function'' derivations, and use the trees with double bars as
abbreviations for the expanded trees. So, ``take the obvious $(b \mto
c) \mto (a,b \mto a,c)$'' means ``find an expansion for {\tiny
  $\cded{4=dnc}$}'':
%
% (find-kopkadaly4text "\\scriptsize, which is smaller than")
%:
%:    b|->c
%:  =========
%:  a,b|->a,c
%:
%:   ^4=dnc
%:
$$\ded{4=dnc} \quad\squigto\quad \ded{4-dnc}$$
%
and so:
%
$$\begin{array}{rcl}
  (A×)_1 &\equiv& ðB¨\Sets.ðC¨\Sets. \\
               && ð\angg{b \mto c}:B×C. \\
               && ð\angg{a,b}: A×B.\ang{\angg{a,b},\angg{b \mto c}('\angg{a,b})} \\
 \end{array}
$$

Now that we have the downcased notation and the `wd' construct we
can/may express the other components of the functor $(A×)$ quite
easily. One of them, $\respids_{(A×)}$, asserts that the functor
$(A×)$ ``respects identities''. In our shorthand notation, this is
%
$$ýB¨\Sets.\welld[a,b \mto a,b]$$
%
that we can expand as
%:
%:      B                B    
%:    -----\id          ---(A×)_0  
%:    b|->b             A×B  
%:  ---------(A×)_1  ---------\id
%:  a,b|->a,b        a,b|->a,b
%:
%:  ^expa1            ^expa2
%:
$$ýB¨\Sets.(\pded{expa1} = \pded{expa2})$$
%
which becomes, in standard notation,
%
$$ýB¨\Sets.(\id(A×)_0B = (A×)_1(\id B).$$

The other component, $\respcomp_{(A×)}$, asserts that $(A×)$
``respects compositions''. This is
%
$$ýB,C,D¨\Sets.ý(b \mto c),(c \mto d). \welld[a,b \mto a,d]$$
%
where $\welld[a,b \mto a,d]$ is:
%:
%:    b|->c       c|->d       b|->c       c|->d     
%:  ---------   ---------     -----------------   
%:  a,b|->a,c   a,c|->a,d         b|->d   
%:  ---------------------       ---------   
%:        a,b|->a,d             a,b|->a,d      
%:                                                  
%:        ^expa3                 ^expa4               
%:
$$\ded{expa3} \quad = \quad \ded{expa4}$$

Note that we didn't need to say $(b \mto c):B \to C$, $(c \mto d):C
\to D$; the translation to Coq will need this, of course, but in the
shorthand notation the typings can be reconstructed by uppercasing.

[Categories, $(a \mto b) : \Hom_\catC\,A\,B$, pseudopoints]






\section{Downcasing Assertions}
\label{downcasing-assertions}




\section{Categories and protocategories in Coq}
\label{cats-in-coq}

We start with some definitions. In this paper, categories, functors,
etc will be dependent uples. In each of the definitions below one of
the separators is `;' instead of ','; this is a trick for defining at
the same time a ``category'' and a ``protocategory'', a ``functor''
and a ``proto-functor'', and so on, as we shall see soon. The typings
of the components of the uples will also be discussed soon.

Category $\catA$

Morphism $f$

Iso $f$

Functor $F$

Natural transformation $T$

Natural iso $T$

Preuniversal arrow

Universal arrow

Preuniversal element

Universal element

------------


A category $\catC$ is an 8-uple, $(\catC_0, \catC_1, \Hom_\catC,
\id_\catC, ¢_\catC; \idL_\catC, \idR_\catC, \assoc_\catC)$, where:

$\catC_0$ is where the objects live,

$\catC_1$ is where the hom-sets live,

if $A, B : \catC_0$ then $\Hom_C A B : \catC_1$,

if $A : \catC_0$ then $\id_C A : Hom_\catC A A$,

if $A, B, C : \catC_0$, $f: \Hom_\catC A B$, $g: \Hom_\catC B C$ then
$¢_\catC A B C g f : \Hom_\catC A C$,

if $A, B : \catC_0$ and $f: \Hom_\catC A B$ then

$\idL_\catC A B f$ asserts that $¢_\catC A A B f (\id_\catC A) = f$, and

$\idR_\catC A B f$ asserts that $¢_\catC A B B (\id_\catC B) f = f$,

if $A, B, C, D : \catC_0$, $f: \Hom_\catC A B$, $g: \Hom_\catC B C$,
$h: \Hom_\catC C D$ then $\assoc_\catC$...

The ';' separator...

The superscript `$·^-$'...

A protocategory $\catC^-$ is a 4-uple, $(\catC_0, \catC_1, \Hom_\catC,
\id_\catC, ¢_\catC)$,

\msk

A category $\catC$ is an 8-uple, $(\catC_0, \catC_1, \Hom_\catC,
\id_\catC, ¢_\catC; \idL_\catC, \idR_\catC, \assoc_\catC)$.

A morphism $f$ is a 4-uple $(\catC, A, B, f)$.

A functor $F$ is a 4-uple $(\catA, \catB, F_0, F_1; \respids_F, \respcomp_F)$.

A natural $T$ transformation is a 6-uple $(\catA, \catB, F, G, T; \sqcond_T)$.

An iso $f$ is a 6-uple $(\catA, A, B, f, f³; f_\supset, f_\subset)$.

A split monic $f$ is a 5-uple $(\catA, A, B, f, f³; f_\supset)$.

A split epi $f$ is a 5-uple $(\catA, A, B, f, f³; f_\subset)$.

A natural iso $T$ is a 6-uple $(\catA, \catB, F, G, T, T³; T_\supset, T_\subset)$.

An adjunction $L \dashv R$ is an 8-uple $(\catA, \catB, L, R, \flat, \sharp; \supset, \subset)$.

\msk

Given a morphism $f$, ``$f$ is an iso'' is a structure with the three
components that we need to add to $f$ to make it an iso; ``$f$ is an
iso'' is $(f³; f_\supset, f_\subset)$.








\section{Categories in DNC}
\label{cats-in-dnc}

\section{DNC in Coq}
\label{dnc-in-coq}

\section{Logic in DNC}
\label{logic}

If $P$ is a proposition, $\Proofs[P]$ is the set of all proofs of $P$,
and $\Wits[P]$ is the ``space of witnesses'' of $P$, that is a
singleton when $P$ is true and an empty set when $P$ is false;
intuitively, $\Wits[P]$ is $\Proofs[P]$ with all elements identified.

A witness for $P$, that we write as $\wit[P]$, is an element of
$\Wits[P]$. All the inference rules of logic can be regarded as
operations that produce witnesses from other witnesses. For example,
the inferences
%:
%:
%:  a=b  a'=b'    2=3  4-4=0
%:  ----------    -----------
%:   a·a'=b·b'    2·(4-4)=3·0
%:
%:   ^mul1        ^mul2
%:
$$\ded{mul1} \qquad \ded{mul2}$$
%
correspond to functions $\Wits[a=b]×\Wits[a=b'] \to \Wits[a·a'=b·b']$
and $\Wits[2=3]×\Wits[4-4=0] \to \Wits[2·(4-4)=3·0]$.

Rules with discharges are a bit harder; we will approach them in two
ways. The derivation at left below can be regarded as a function from
$\Wits[P´Q]×\Wits[Q¶R]$ to $\Wits[P´Q]$:
%:
%:            P´Q   
%:            ---   
%:   P´Q        Q     Q¶R    
%:   ---        ---------    
%:     P           R         P´Q  Q¶R
%:     -------------         ::::::::
%:         P´R                 P¶R   
%:                
%:         ^disch1             ^disch2
%:
$$\ded{disch1} \qquad \ded{disch2}$$

The $¶$-introduction curries that function and produces a function
from $\Wits[Q¶R]$ to $(\Wits[P´Q] \to \Wits[P´R]) = \Wits[P´Q¶P´R]$.
%:
%:
%:           [P´Q]^1
%:           -------
%:  [P´Q]^1     Q     Q¶R
%:  -------     ---------
%:     P           R          [P´Q]^1  Q¶R
%:     -------------          ::::::::::::
%:         P´R                    P¶R        Q¶R
%:       -------1               -------1     :::
%:       P´Q¶P´R                P´Q¶P´R     P´Q¶P´R
%:
%:       ^disch3                ^disch4     ^disch5
%:
$$\ded{disch3} \qquad \ded{disch4} \qquad \ded{disch5}$$


% «convention»  (to ".convention")
\section{Conventions on names}
\label{conventions}

I tend to use some conventions for names in DNC. For example, in an
adjunction $L \dashv R$ the functor $L$ is usually drawn going
leftwards, and $R$ is drawn going to the right:
%
%D diagram conventions-1
%D 2Dx      100     +30    +30     +30
%D 2D  100 LA <---| A     a^L <=== a
%D 2D       |       |      -       |
%D 2D       |  <->  |      |  <->  |
%D 2D       v       v      v       v
%D 2D  +30  B |---> RB     b ====> b^R
%D 2D
%D (( LA A B RB
%D    @ 0 @ 1 <-| @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 |->
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D (( a^L a b b^R
%D    @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\diag{conventions-1}$$

The two categories are named $\catA$ and $\catB$.

The natural iso
%
$$\begin{array}{rcl}
  (A^\op,B) & \mto  & (\Hom_\catB(LA,B) \bij \Hom_\catA(A,RB) \\
  (a^\op;b) & \tnto & ((a^L \mto b) \bij (a \mto b^R)) \\
  \end{array}
$$
%

has two directions: one, $(a^L \mto b) \mto (a \mto b^R)$, shifts to
the right the position where the functor hits the object, and I call
that one `$\sharp$'; the other one, $(a^L \mto b) \mot (a \mto b^R)$,
shifts to the left the position where the functor hits the object, and
I call it `$\flat$'. So:
%
%D diagram conventions-2
%D 2Dx      100     +30    +30     +30
%D 2D  100 LA <---| A     a^L <=== a
%D 2D       |       |      -       |
%D 2D       |  <->  |      |  <->  |
%D 2D       v       v      v       v
%D 2D  +30  B |---> RB     b ====> b^R
%D 2D
%D (( LA A B RB
%D    @ 0 @ 1 <-| @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 |->
%D    @ 0 @ 3 harrownodes nil 20 nil <-  sl^ .plabel= a \flat
%D    @ 0 @ 3 harrownodes nil 20 nil  -> sl_ .plabel= b \sharp
%D ))
%D (( a^L a b b^R
%D    @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D ))
%D enddiagram
%D
$$\diag{conventions-2}$$

Each book on Category Theory uses its own notation and naming
conventions. The best way I found to show how to translate between DNC
and some other more standard notation is to do the translation in two
steps. For example,


%D diagram transla-1
%D 2Dx      100 +15 +15    +45 +15 +15    +45 +15 +15
%D 2D  100      --| x          --| A           /= a{}
%D 2D          /    -         /    -          //  -    
%D 2D         /     |        /     |         //   |    
%D 2D        v      v       v      v        \/    v    
%D 2D  +30 Fx |--> GFx    LA |--> RLA    a^L ==> a^{LR}
%D 2D       |       |      |       |      -       |    
%D 2D       |  <->  |      |  <->  |      |  <->  |    
%D 2D       v       v      v       v      v       v    
%D 2D  +30  a |---> Ga     B |---> RB     b ====> b^R  
%D 2D
%D 2D  +15  {A}     {X}  \catB   \catA
%D 2D
%D 2D  +15     X-`A           A-`B
%D 2D
%D 2D  +15                                    -`
%D 2D
%D (( x Fx GFx a Ga
%D    @ 0 @ 1 |->
%D    @ 0 @ 2  -> .plabel= r \eta_x
%D    @ 1 @ 2 |->
%D    @ 1 @ 3  -> .plabel= l f
%D    @ 2 @ 4  -> .plabel= r Gf
%D    @ 3 @ 4 |->
%D    @ 0 @ 4  -> .slide= 17pt .plabel= r \sm{\phi"f\;=\\"Gf¢\eta_x}
%D    @ 1 @ 4 harrownodes nil 20 nil |->
%D    {A} place {X} place
%D    X-`A .tex= \ang{F,G,\phi}:X\rightharpoonup"A place
%D ))
%D (( A LA RLA B RB
%D    @ 0 @ 1 |->
%D    @ 0 @ 2  -> .plabel= r \eta_A
%D    @ 1 @ 2 |->
%D    @ 1 @ 3  -> .plabel= l f
%D    @ 2 @ 4  -> .plabel= r Rf
%D    @ 3 @ 4 |->
%D    @ 0 @ 4  -> .slide= 17pt .plabel= r \sm{\phi"f\;=\\"Rf¢\eta_A}
%D    @ 1 @ 4 harrownodes nil 20 nil |->
%D    \catB place \catA place
%D    A-`B .tex= \ang{L,R,\phi}:\catA\rightharpoonup"\catB place
%D ))
%D (( a{} a^L a^{LR} b b^R
%D    @ 0 @ 1  =>
%D    @ 0 @ 2 |->
%D    @ 1 @ 2  =>
%D    @ 1 @ 3 |->
%D    @ 2 @ 4 |->
%D    @ 3 @ 4  =>
%D    @ 1 @ 4 harrownodes nil 20 nil |->
%D    -` .tex= \ang{L,R,(a^\op;b)-.>((a^L|->b)|->(a|->b^R))} place
%D ))
%D enddiagram
%D
$$\diag{transla-1}$$

In the first step we keep the symbols --- $\ang{\_,\_,\_}$,
$\rightharpoonup$, $\eta$, $\phi$, `$¢$' vs.\ `;' --- but we change
the names of the objects, functors, categories, and we obtain an
uppercase diagram with our favourite choices of letters, fonts, and
placing of the names; in the second step we downcase that.

The notation $\ang{F,G,\phi}: X\rightharpoonup A$ above is from CWM
(sec.\ IV.1). Slightly later the book introduces another notation for
adjunctions, $\ang{F,G,\eta,}: X\rightharpoonup A$; we downcase that
to $\ang{a\funto a^L, b\funto b^R, a \tnto (a \mto a^{LR}), b \tnto
  (b^{RL} \mto b)}$, or simply $\ang{L, R, a \tnto (a \mto a^{LR}), b
  \tnto (b^{RL} \mto b)}$.







% «yoneda»  (to ".yoneda")
\section{The Yoneda Lemma in DNC}
\label{yoneda}

Let's define a {\sl preuniversal} as a tuple $(\catA, \catB, R: \catB
\to A, A \in \catA_0, B \in \catB_0, f:A \to RB)$.

A {\sl universal} will be the same plus an extra component, that
asserts the ``universality'' of $f$; but we are only going to need
that later (sec.\ \_).

We will represent a preuniversal in DNC like this:

%D diagram pdown
%D 2Dx     100
%D 2D  100 #1
%D 2D
%D 2D  +20 #2
%D 2D
%D (( #1 #2 |->
%D ))
%D enddefpdiagram 2
%D
% $$\pdown ab$$

%D diagram pmetauniv
%D 2Dx     100    +20
%D 2D  100        #1
%D 2D             -
%D 2D           #4|
%D 2D             v
%D 2D  +20 #2 ==> #3
%D 2D
%D (( #1 #3 |-> .plabel= l #4
%D    #2 #3  =>
%D ))
%D enddefpdiagram 4
%
% $$\pmetauniv abcd$$

\def\ppreuniv#1#2#3{\pmetauniv{#1}{#2}{#3}{}}
\def\puniv#1#2#3{\pmetauniv{#1}{#2}{#3}{\text{univ}}}
\def\pdowneltnt#1#2#3#4{\big(
  #1 \tnto (\pdown{#2}{#3} \mto #4)
  \big)
  }
\def\pdownnt#1#2#3#4#5{\big(
  #1 \tnto (\pdown{#2}{#3} \mto \pdown{#4}{#5})
  \big)
  }

$$\ppreuniv{a}{b}{b^R}$$

There is a natural construction for a bijection between preuniversals
and natural transformations $T: \Hom_\catB(B,-) \to \Hom_\catA(A,-)$:
%
$$\ppreuniv{a}{b}{b^R} \;\bij\; \pdownnt{c}{b}{c}{a}{c^R}$$

The direction `$\mto$' of the bijection is obvious from the diagram:

(...)

For the other direction, we do:

%:
%:    B        B   c-.>((b|->c)|->(a|->c^R))
%:  -----\id   -----------------------------Ð{app}
%:  b|->b      (b|->b)|->(a|->b^R)
%:  ------------------------------Ð{app}
%:        a|->b^R
%:
%:        ^otherdir
%:
$$\ded{otherdir}$$

The Yoneda Lemma:
%
$$\begin{array}{ccc}
           b^R          &\diagxyto/<.>/<175>&  \pdowneltnt{c}{b}{c}{\;c^R\;} \\ \\
         \vbij          &                   &          \vbij            \\ \\
  \ppreuniv{*}{b}{b^R}  &\diagxyto/<->/<175>&  \pdownnt{c}{b}{c}{*}{c^R} \\
  \end{array}
$$

The corollary:
%
$$\begin{array}{ccc}
      \pdown{a}{b}           &\diagxyto/<.>/<175>&  \pdownnt{c}{b}{c}{a}{c} \\ \\
           \vbij             &                   &          \vbij            \\ \\
  \ppreuniv{*}{b}{a \mto b}  &\diagxyto/<->/<175>&  \pdownnt{c}{b}{c}{*}{a \mto c} \\
  \end{array}
$$


% $$\ppreuniv{*}{b}{a \mto b} \;\bij\; \pdownnt{c}{b}{c}{*}{a \mto c}$$


\bsk

(old stuff):

A functor $F: \catA \to \catB$ takes each object $A \in \catA_0$ to an
object $FA \in \catB_0$; we can write its action on objects as $A \mto
FA$. Its action on morphisms takes each morphism $f: A \to A'$ to a
morphism $Ff: FA \to A'$...

We downcase that to $a \funto a^F$.

An adjunction $L \dashv R$ between two functors, $L: \catA \to \catB$
and $R: \catB \to \catA$, gives, for any two objects $A:\catA_0$ and
$B:\catB_0$, a bijection between the hom-sets $\Hom_\catB(LA,B)$ and
$\Hom_\catA(A,RB)$; we will downcase this as







\section{A system of Natural Deduction for (proto-)\discretionary{}{}{}categories}
\label{nd-for-cats}

% (find-kopkadaly4text "\\discretionary{before}{after}{without}")

\section{Natural Deduction for dependent types}
\label{nd-for-dt}

\section{Abelian categories}
\label{abcats}

\section{Fibrations in DNC}
\label{fibrations}

%:\s{\pover{
\def\pover#1#2{\begin{pmatrix} #2 \\ #1 \end{pmatrix}}
\def\cartmto{\mton{\Box}}
\def\pdiag#1{\!\left(\!\!\diag{#1}\right)\!}
\def\cartmto{\mton{\Box}}
\widemtos

A morphism $\pover{b}{Q} \mto \pover{c}{R}$ is {\sl cartesian}
(notation: $\pover{b}{Q} \cartmto \pover{c}{R}$) when the induced
natural transformation below (taking morphisms with the right codomain
to ``\,`V's over commutative triangles'') is a natural iso:

%D diagram cartmorph1
%D 2Dx         100     +20      +30
%D 2D  100 \s{a}{P}
%D 2D  +20          \s{b}{Q}  \s{c}{R}
%D 2D  +10     a
%D 2D  +20             b        c
%D (( \s{a}{P} \s{b}{Q} \s{c}{R}
%D       a       b       c
%D    @ 0 @ 2 |-> @ 1 @ 2 |->
%D    @ 3 @ 4 |-> @ 3 @ 5 |-> @ 4 @ 5 |->
%D ))
%D enddiagram

\msk
$\pover{a}{P}^\op \tnto \; ((\pover{a}{P} \mto \pover{b}{Q})
		            \two/|->`<-|/<200>^{\natural}_{(ñ)}
		            \pdiag{cartmorph1})
$


\section{Open problems and future work}
\label{future}




% http://en.wikipedia.org/wiki/BHK_interpretation




%

\end{document}

% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End:
