|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: