|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2002fmcs.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2002fmcs.tex && latex 2002fmcs.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2002fmcs.tex && pdflatex 2002fmcs.tex"))
% (eev "cd ~/LATEX/ && Scp 2002fmcs.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2002fmcs.dvi")
% (find-pspage "~/LATEX/2002fmcs.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2002fmcs.ps 2002fmcs.dvi")
% (find-pspage "~/LATEX/2002fmcs.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% «.toc» (to "toc")
% «.abstract» (to "abstract")
% «.motivation-1» (to "motivation-1")
% «.sketch-of-solution» (to "sketch-of-solution")
% «.GP» (to "GP")
% «.functor-NT-in-GP» (to "functor-NT-in-GP")
% «.Yoneda-proof» (to "Yoneda-proof")
% «.Yoneda-proof-2» (to "Yoneda-proof-2")
% «.adjs-as-DNC-diags» (to "adjs-as-DNC-diags")
% «.intro-CC-1» (to "intro-CC-1")
% «.preterms-and-prejudgs» (to "preterms-and-prejudgs")
% «.naive-semantics» (to "naive-semantics")
% «.intro-CC-2» (to "intro-CC-2")
% «.rules-CC» (to "rules-CC")
% «.some-facts-about-CC» (to "some-facts-about-CC")
% «.more-facts-about-CC» (to "more-facts-about-CC")
% «.CC-to-CCMC-and-back» (to "CC-to-CCMC-and-back")
% «.CC-to-CCMC-and-back-2» (to "CC-to-CCMC-and-back-2")
% «.props-and-proofs-in-CC» (to "props-and-proofs-in-CC")
% «.terms-for-equality» (to "terms-for-equality")
% «.protocategories» (to "protocategories")
% «.protocategories-sets» (to "protocategories-sets")
% «.protocategories-generic» (to "protocategories-generic")
% «.DNC-rules» (to "DNC-rules")
% «.DNC-rules-funtoI» (to "DNC-rules-funtoI")
% «.DNC-rules-tntoI» (to "DNC-rules-tntoI")
% «.future-work» (to "future-work")
% «.before-SN-for-DNC» (to "before-SN-for-DNC")
% «.notes-about-slides» (to "notes-about-slides")
\documentclass[oneside]{book}
\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 2002fmcs.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")
\tocline {Abstract} {2}
\tocline {Motivation} {3}
\tocline {Sketch of the solution} {4}
\tocline {The ``generic point'' notation} {5}
\tocline {Functors and NTs in this notation} {6}
\tocline {The proof of the Yoneda Lemma in DNC} {7}
\tocline {The proof of the Yoneda Lemma in DNC (2)} {8}
\tocline {Adjunctions as DNC diagrams} {9}
\tocline {Introduction to the Calculus of Constructions (1)} {10}
\tocline {Pre-terms and pre-judgements} {11}
\tocline {Naive semantics: $\lambda $ and $\Pi $} {12}
\tocline {Introduction to CC (2) - example of a valid derivation} {13}
\tocline {The rules of the Calculus of Constructions} {14}
\tocline {Some facts (i.e., theorems) about CC} {15}
\tocline {More facts about CC: ``classes'' of terms, variations of the rules} {16}
\tocline {From CC with minimal contexts to ND and back} {17}
\tocline {From CC with minimal contexts to ND and back (2)} {18}
\tocline {Representing propositions and proofs in CC} {19}
\tocline {Terms for equality} {20}
\tocline {Protocategories} {21}
\tocline {A very special example: $\Set $ as a $ñÞ$-protocategory} {22}
\tocline {A typical $\Box Þ$-protocategory} {23}
\tocline {System DNC: rules} {24}
\tocline {System DNC: $(\Rightarrow I)$, example} {25}
\tocline {System DNC: $(\tnto I)$, example} {26}
\tocline {Future work} {27}
\tocline {What comes before studying SN for DNC} {28}
\tocline {Notes for people downloading these slides} {29}
% (eedn4a-bounded)
\def\lambdaC{ð¦{C}}
\defå{\Pi}
\def\CCMC{\text{CC}_\text{MC}}
\widemtos
%%%%%
%
% «toc» (to ".toc")
%
%%%%%
{\bf Table of Contents}
\medskip
\smallskip
\bigskip
Don't believe any idea here that you can't figure out the details
yourself, or you've seen it stated in serious articles written by
grown-ups. These notes contain unintentional errors and omissions.
Feedback is not only welcome but also desperately needed. Etc, Etc.
\medskip
Eduardo Ochs
{\tt http://angg.twu.net/}
{\tt http://www.mat.puc-rio.br/\~{}edrx/}
{\tt edrx@inx.com.br}
\bigskip
Note: I'm currently at McGill university, as a visitor --- I'm doing a
``sandwich PhD'' (really!) thanks to a CAPES ({\tt
http://www.capes.gov.br/}) grant...
\newpage
\def\:{{:}}
\def¸{\mto}
\def\ssapp#1#2{(#1,#2)\text{-app}}
\def\ssabs#1#2{(#1,#2)\text{-abs}}
\def\tstart{Þ\text{-start}}
\def\kstart{ñ\text{-start}}
\def\cat{{{cat}}}
\def\deg{{¦{deg}}}
\def\prop{{¦{prop}}}
\def\e{{e}}
\def\ang#1{\langle #1 \rangle}
\def\sqto{\rightsquigarrow}
\def\sqbij{\leftrightsquigarrow}
% \def\dicto{\rightsquigarrow}
\def\dicto{\dashrightarrow}
\def\smallpb#1#2#3{
\begin{smallmatrix}
& & #1 \mathstrut \\
& & \downarrow \\
#2 & \to & #3 \mathstrut \\
\end{smallmatrix}
}
\def\Orders{\text{Orders}}
\def\Types{\text{Types}}
\def\Lam{\Lambda}
\def\Vee{¦V}
\def\Prod{\Pi}
\def\Sum{\Sigma}
\def\Theory{\mathcal{T}}
\def\Obj{{\operatorname{Obj}}}
\def\Objs{{\operatorname{Objs}}}
\def\Homsets{{\operatorname{Homsets}}}
\def\Props{{\operatorname{Props}}}
\def\prop{{\operatorname{prop}}}
\def\prf{{\operatorname{prf}}}
\widemtos
\catcode`Ð=13 \defÐ{\vec} % pe
\def\slice#1#2{\begin{pmatrix} #1 \\ \dnto \\ #2 \end{pmatrix}}
\def\eslice#1#2{\begin{pmatrix} #1 \\ \dnto \\ #2 \end{pmatrix}} % should be ÷>
\def\clm#1#2{{#1{\text-}#2}}
\def\GG{\Gamma}
%:*->^*\ton * %
%:*ˆ->*\ito * %
%:*-.>*\tnto * %
%:*=>*\funto * %
%:*<->*\bij * %
%:*->*\to * %
%:*[s]*{[s]}* %
%:*|-*\vdash * %
%:*÷>*\mto * %
%:*"* * %
\newpage
% --------------------
% «abstract» (to ".abstract")
% (s "Abstract" "abstract")
\myslide {Abstract} {abstract}
(For the FMCS talk)
We will present a logic (system DNC) whose terms represent categories,
objects, morphisms, functors, natural transformations, sets, points,
and functions, and whose rules of deduction represent certain
constructive operations involving those entities. Derivation trees in
this system only represent the ``T-part'' (for ``terms'' and
``types'') of the constructions, not the ``P-part'' (``proofs'' and
``propositions''): the rules that generate functors and natural
transformations do not check that they obey the necessary equations.
So, we can see derivations in this system either as constructions
happening in a ``syntactical world'', that should be related to the
``real world'' in some way (maybe through meta-theorems that are yet to
be found), or as being just ``skeletons'' of the real constructions,
with the P-parts having been omitted for briefness.
Even though derivations in DNC tell only half of the story, they still
have a certain charm: DNC terms represent ``types'', but a tree
represents a construction of a lambda-calculus term; there's a
Curry-Howard isomorphism going on, and a tree can be a visual help for
understanding how the lambda-calculus term works --- how the data flows
inside a given categorical construction. Also, if we are looking for a
categorical entity of a certain ``type'' we can try to express it as a
DNC term, and then look for a DNC ``deduction'' having it as its
``conclusion''; the deduction will give us a T-part, and we will still
have to go back to the standard language to supply a P-part, but at
least the search has been broken in two parts...
The way to formalize DNC, and to provide a translation between terms
in its ``logic'' and the usual notations for Category Theory, is based
on the following idea. Take a derivation tree $D$ in the Calculus of
Constructions, and erase all the contexts and all the typings that
appear in it; also erase all the deduction steps that now look
redundant. Call the new tree $D'$. If the original derivation, $D$,
obeys some mild conditions, then it is possible to reconstruct it ---
modulo exchanges and unessential weakenings in the contexts --- from
$D'$, that is much shorter. The algorithm that does the reconstruction
generates as a by-product a ``dictionary'' that tells the type and the
``minimal context'' for each term that appears in $D'$; by extending
the language that the dictionary can deal with we get a way to
translate DNC terms and trees --- and also, curiously, with a few
tricks more, and with some minimal information to ``bootstrap'' the
dictionary, categorical diagrams written in a DNC-like language.
\newpage
\setlength{\parindent}{5pt}
% --------------------
% «motivation-1» (to ".motivation-1")
% (s "Motivation" "motivation-1")
\myslide {Motivation} {motivation-1}
% (find-angg "LATEX/2002d.tex" "first-functor")
A language for ``skeletons of proofs'' that would...
$\bullet$ let me write down just the essential --- an (imaginary)
computer would fill out the missing details;
$\bullet$ allow me say things like ``the natural entity of type/name
$a,(a \mto b) \mto b$'' (ev);
$\bullet$ have a diagrammatic version,
$\bullet$ and a linear version (for derivation trees and Curry-Howard);
$\bullet$ easy to translate to the usual languages;
$\bullet$ be able to represent categorical concepts;
$\bullet$ allow for the ``right amount'' of ambiguity;
$\bullet$ read aloud as something that's happening in the simplest
models --- e.g., in $\Set$ instead of in an arbitrary topos;
$\bullet$ be concise and clear enough --- because I have a very bad
memory and I tended to change my notations madly, so I needed short
diagrams that would ``say everything'', without the need for pages of
definitions...
\newpage
% --------------------
% «sketch-of-solution» (to ".sketch-of-solution")
% (s "Sketch of the solution" "sketch-of-solution")
\myslide {Sketch of the solution} {sketch-of-solution}
A notation that looks like an ambiguous $ð$-calculus (I call it the
``generic point'' notation);
add some symbols to GP to let it represent functors, natural
transformations, objects, categories, etc;
a {dictionary} will translate GP terms into something precise (in the
Calculus of Constructions)
(diagrams and derivation trees are recyclable! Just change the
dictionary...)
modify the Calculus of Constructions to get something that looks more
like natural deduction --- i.e., that has discharges instead of
``$\ldots \vdash \ldots$''s --- to get rid of some redundancy
The system of natural deduction for categories (``system DNC'') is
essentially this modified CC, with the GP notation with categorical
extensions, and a dictionary.
DNC derivations can either represent just the ``T-part'' (terms and
types) of categorical constructions, and omit the ``P-part''
(propositions and proofs), or they can be complete.
\newpage
% --------------------
% «GP» (to ".GP")
% (s "The ``generic point'' notation" "GP")
\myslide {The ``generic point'' notation} {GP}
What would be the natural name for a variable in...
$\begin{array}{lllll}
A & \dicto & a && A = \E[a] \\
B & \dicto & b && B = \E[b] \\
A×B & \dicto & a,b && A×B = \E[a,b] = \E[a]×\E[b] \\
B^A & \dicto & a \mto b && B^A = \E[a \mto b] = \E[b]^{\E[a]}
\end{array}
$
We will allow strange {{names}} for variables and terms
and we will have a {dictionary} to translate these names
into something precise (in the Calculus of Constructions).
\medskip
`$\E$' is pronounced as ``the space of''.
\newpage
% --------------------
% «functor-NT-in-GP» (to ".functor-NT-in-GP")
% (s "Functors and NTs in this notation" "functor-NT-in-GP")
\myslide {Functors and NTs in this notation} {functor-NT-in-GP}
Choose sets $A$ and $B$, and a function $B \ton{g} A$.
In GP/DNC notation we write $\Hom(A,-)$ as $x \funto (a \mto x)$.
Note that from the name ``$x \funto (a \mto x)$'' we can extract both
the action on objects, $\E[x] \mto \E[a \mto x]$, and the action on
morphisms, $(x \mto y) \mto ((a \mto x) \mto (a \mto y))$.
%D diagram functors
%D 2Dx 100 +30 +35 +30
%D 2D 100 x ====> (a|->x) X |---> \Hom(A,X)
%D 2D - - | |
%D 2D | |--> | f | |--> | \Hom(A,f)
%D 2D v v v v
%D 2D +30 y ====> (a|->y) Y |---> \Hom(A,Y)
%D 2D
%D (( x (a|->x)
%D y (a|->y)
%D @ 0 @ 1 => @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D ))
%D (( X \Hom(A,X)
%D Y \Hom(A,Y)
%D @ 0 @ 1 |-> @ 0 @ 2 -> .plabel= l f @ 1 @ 3 -> .plabel= r \Hom(A,f) @ 2 @ 3 |->
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$\diag{functors}$
% $\bfig
% \square(-250,-250)/=>`|->`|->`=>/<500,500>[x`(a \mto x)`y`(a \mto y);```]
% \morphism(-250,0)/|->/<500,0>[\phantom{*}`\phantom{*};]
% \efig
% \qquad
% \bfig
% \square(-250,-250)/|->`->`->`|->/<500,500>[
% X `
% \Hom(A,X) `
% Y `
% \Hom(A,Y) ; ` f ` \Hom(A,f) ` ]
% \morphism(-250,0)/|->/<500,0>[\phantom{*}`\phantom{*};]
% \efig
% $
\medskip
$x \tnto ((b \mto x) \mto (a \mto x))$ is a natural transformation
going from $x \funto (b \mto x)$ to $x \funto (a \mto x)$.
It works as $\E[x] \mto ((b \mto x) \mto (a \mto x))$, but it also
obeys a naturality condition...
%D diagram NTs
%D 2Dx 100 +25 +25 +45 +25 +25
%D 2D 100 x X
%D 2D // | \\ - - -
%D 2D // |* \\ \Hom(B,-) / |* \ \Hom(A,-)
%D 2D \/ v \/ v v v
%D 2D +30 (b|->x) |---> (a|->x) \Hom(B,X) ---> \Hom(A,X)
%D 2D
%D (( x (b|->x) (a|->x)
%D @ 0 @ 1 => @ 0 @ 2 =>
%D @ 0 @ 1 @ 2 midpoint -> .PLABEL= ^(0.575) \bullet
%D @ 1 @ 2 |->
%D ))
%D (( X \Hom(B,X) \Hom(A,X)
%D @ 0 @ 1 |-> .plabel= l \Hom(B,-)
%D @ 0 @ 2 |-> .plabel= r \Hom(A,-)
%D @ 0 @ 1 @ 2 midpoint |-> .PLABEL= ^(0.55) .
%D @ 1 @ 2 ->
%D ))
%D enddiagram
%D
$\diag{NTs}$
% $\bfig
% \Atriangle(-500,-250)/=>`=>`|->/<500,500>[
% x `
% (b \mto x) ` (a \mto x) ;``]
% \morphism(0,250)|r|/->/<0,-500>[x`\phantom{\cdot};\bullet]
% \efig
% \qquad
% \bfig
% \Atriangle(-500,-250)/|->`|->`->/<500,500>[
% X `
% \Hom(B,X) ` \Hom(A,X) ; \Hom(B,-) ` \Hom(A,-) ` ]
% \morphism(0,250)|r|/|->/<0,-500>[X`\phantom{\cdot};]
% \efig
% $
\newpage
% --------------------
% «Yoneda-proof» (to ".Yoneda-proof")
% (s "The proof of the Yoneda Lemma in DNC" "Yoneda-proof")
\myslide {The proof of the Yoneda Lemma in DNC} {Yoneda-proof}
%:
%: [a÷>x']^1 [x'÷>x'']^2
%: ----------------------
%: \O[a] [\O[x]]^1 a÷>x''
%: -----------------\Hom_\catC -----------------1
%: \E[a÷>x] (a÷>x')÷>(a÷>x'')
%: ---------------1 -----------------(=>I);2
%: \O[x]÷>\E[a÷>x] x=>(a÷>x)
%:
%: ^yoneda-0a ^yoneda-0b
%:
$$\ded{yoneda-0a} \qquad \ded{yoneda-0b}$$
%: \O[a]
%: =========
%: x=>(a÷>x)
%: -------------¦{ren}
%: \O[x=>(a÷>x)] \O[x=>x^F]
%: -------------------------------\Hom_{\Set^\catC}
%: \E[x-.>((a÷>x)÷>x^F)]
%: ---------------------[s]^1
%: \O[a] \O[a] x-.>((a÷>x)÷>x^F) A A T:\Hom_\catC(A,-)-.>F
%: ----- -------------------------- ---------- ------------------------
%: a÷>a (a÷>a)÷>a^F \id_A:A->A T_A:\Hom_\catC(A,A)->F(A)
%: ----------------------- -------------------------------------
%: a^F T_A(\id_A)ÎF(A)
%: ------------------------1
%: (x-.>((a÷>x)÷>x^F))÷>a^F ^prfyoneda1-balloon
%:
%: ^prfyoneda1
%:
$$\ded{prfyoneda1}$$
% $$\ded{prfyoneda1-balloon}$$
%:
%:
%: \O[x=>x^F] \O_a [\O_x]^2
%: ----------¦{ren} -----------
%: \O_a x=>x^F \E[a÷>x] \O[x=>x^F]
%: ------------- --------[s]^1 ----------¦{ren}
%: \E[a^F] a÷>x x=>x^F
%: -------[s]^3 ---------------------
%: a^F a^F÷>x^F
%: --------------------------------
%: x^F
%: -----------1
%: (a÷>x)÷>x^F
%: -----------------2
%: x-.>((a÷>x)÷>x^F)
%: ------------------------3
%: a^F÷>(x-.>((a÷>x)÷>x^F))
%:
%: ^prfyoneda2
%:
$$\ded{prfyoneda2}$$
%: [\O_a]^1 [\O[x=>x^F]]^1 [\O_a]^1 [\O[x=>x^F]]^1
%: ======================== ========================
%: a^F÷>(x-.>((a÷>x)÷>x^F)) (x-.>((a÷>x)÷>x^F))÷>a^F
%: ---------------------------------------------------
%: a^F<->(x-.>((a÷>x)÷>x^F))
%: ----------------------------------------1
%: (a;x=>x^F)-.>(a^F<->(x-.>((a÷>x)÷>x^F)))
%:
%: ^prfyoneda3
%:
$$\ded{prfyoneda3}$$
\newpage
% --------------------
% «Yoneda-proof-2» (to ".Yoneda-proof-2")
% (s "The proof of the Yoneda Lemma in DNC (2)" "Yoneda-proof-2")
\myslide {The proof of the Yoneda Lemma in DNC (2)} {Yoneda-proof-2}
...and if we want to prove that the functors implicit in the outer
`$\tnto$' of $(a;x \funto x^F) \tnto (a^F \bij (x \tnto ((a
\to x) \to x^F)))$ are really (proto!) functors, we need this:
%:
%: [(x=>x^{F'})÷>(x=>x^{F''})]^1
%: -----------------------------¦{ren}
%: [a'÷>a'']^1 x-.>(x^{F'}÷>x^{F''})
%: ====================================
%: {a'}^{F'}÷>{a''}^{F''}
%: ----------------------1
%: (a;x=>x^F)=>a^F
%:
%: ^prfyonedaftr1
%:
%: [\O_a]^1
%: =========
%: x=>(a÷>x)
%: -------------¦{ren}
%: \O[x=>(a÷>x)] [\O[x=>x^F]]^1
%: -----------------------------------\Hom_{\Set^\catC}
%: \E[x-.>((a÷>x)÷>x^F)]
%: -----------------------------------1
%: \O[a;x=>x^F]÷>\E[x-.>((a÷>x)÷>x^F)]
%:
%: ^prfyonedaftr2
%:
%: [a'÷>a'']^4 [a''÷>x]^1 [\O_x]^2 [x-.>((a'÷>x)÷>x^{F'})]^3
%: --------------------- -------------
%: a'÷>x (a'÷>x)÷>x^{F'} [\O_x]^2 [x-.>(x^{F'}÷>x^{F''})]^4
%: ----------------------------------- -----------------------------------
%: x^{F'} x^{F'}÷>x^{F''}
%: ---------------------------------------------------
%: x^{F''}
%: -----------------1
%: (a''÷>x)÷>x^{F''}
%: -----------------------(-.>I);2
%: x-.>((a''÷>x)÷>x^{F''})
%: --------------------------------------------------3
%: (x-.>((a'÷>x)÷>x^{F'}))÷>(x-.>((a''÷>x)÷>x^{F''}))
%: --------------------------------------------------(=>I);4
%: (a;x=>x^F)=>(x-.>((a÷>x)÷>x^F))
%:
%: ^prfyonedaftr3
%:
$$\ded{prfyonedaftr1}$$
$$\ded{prfyonedaftr2}$$
$$\ded{prfyonedaftr3}$$
\newpage
% --------------------
% «adjs-as-DNC-diags» (to ".adjs-as-DNC-diags")
% (s "Adjunctions as DNC diagrams" "adjs-as-DNC-diags")
\myslide {Adjunctions as DNC diagrams} {adjs-as-DNC-diags}
$L \dashv R$ is $(a;b) \tnto ((a^L \mto b) \bij (a \mto b^R))$
$(-)×B \dashv (-)^B$ is $(a;c) \tnto ((a,b \mto c) \bij (a \mto (b \mto c)))$
%D diagram adjunctions
%D 2Dx 100 +25 +25 +25
%D 2D 100 a^L <==== a a,b <=== {a}
%D 2D - - - -
%D 2D | <--> | | <--> |
%D 2D v v v v
%D 2D +25 b ====> b^R {c} ===> b|->c
%D 2D
%D (( a^L a b b^R
%D @ 0 @ 1 <= .plabel= a L @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 => .plabel= b R
%D @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D (( a,b {a} {c} b|->c
%D @ 0 @ 1 <= .plabel= a (-)×B @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 => .plabel= b (-)^B
%D @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
$$\diag{adjunctions}$$
% $$\bfig
% \square|alrb|/<=`|->`|->`=>/<400,400>[
% a^L
% ` a
% ` b
% ` b^R
% ; L ` ` ` R ]
% \efig
% \qquad
% \bfig
% \square|alrb|/<=`|->`|->`=>/<400,400>[
% a,b
% ` a
% ` c
% ` b \mto c
% ; (-)×B ` ` ` (-)^B ]
% \efig
% $$
\def\mydmapp#1#2#3{\left(\bfig\morphism(0,#1)|r|/|->/<0,-#2>[#3]\efig\right)}
\def\mydmap[#1]{\mydmapp{120}{240}{#1}}
\def\mydmap[#1`#2;#3]{\begin{pmatrix}#1\\ \dnto\\#2\end{pmatrix}}
\def\Sub{{¦{Sub}}}
The functor from $\Sub(A)$ to $\Sub(A×B)$ ($A, B$ sets, for example)
has a left adjoint $Î$ and a right adjoint $ý$.
The weakening functor induced by $\GG,a \mto \GG$ in a ``good''
codomain fibration has a left adjoint $\Sigma$ and a right adjoint
$\Pi$.
%D diagram quantifiers
%D 2Dx 100 +45 +45 +50
%D 2D 100 aw0 =====> aw1 bw0 =====> bw1
%D 2D - - - -
%D 2D | <--> | | <--> |
%D 2D v v v v
%D 2D +40 aw2 <===== aw3 bw2 <===== bw3
%D 2D - - - -
%D 2D | <--> | | <--> |
%D 2D v v v v
%D 2D +40 aw4 =====> aw5 bw4 =====> bw5
%D
%D (( aw0 .tex= (a,b)|_{P(a,b)} aw1 .tex= a|_{Îb.P(a,b)}
%D aw2 .tex= (a,b)|_{Q(a)} aw3 .tex= a|_{Q(a)}
%D aw4 .tex= (a,b)|_{R(a,b)} aw5 .tex= a|_{ýb.R(a,b)}
%D @ 0 @ 1 => .plabel= a {Î}
%D @ 2 @ 3 <=
%D @ 4 @ 5 => .plabel= b {ý}
%D @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 4 |-> @ 3 @ 5 |-> @ 2 @ 5 harrownodes nil 20 nil <->
%D ))
%D (( bw0 .tex= \ss[\GG,a|p] bw1 .tex= \ss[\GG|a,p]
%D bw2 .tex= \ss[\GG,a|q] bw3 .tex= \ss[\GG|q]
%D bw4 .tex= \ss[\GG,a|r] bw5 .tex= \ss[\GG|(a|->r)]
%D @ 0 @ 1 => .plabel= a Æ
%D @ 2 @ 3 <=
%D @ 4 @ 5 => .plabel= b å
%D @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 4 |-> @ 3 @ 5 |-> @ 2 @ 5 harrownodes nil 20 nil <->
%D ))
%D enddiagram
$$\def\ss[#1|#2]{\begin{pmatrix} #1,#2 \\ \dnto \\ #1 \end{pmatrix}}
\diag{quantifiers}
$$
% $$\bfig
% \square(0,600)|alrm|/<=`|->`|->`=>/<700,600>[
% a|_{Ýb.P(a,b)}
% ` (a,b)|_{P(a,b)}
% ` a|_{Q(a)}
% ` (a,b)|_{Q(a)}
% ; Ý ` ` ` ]
% \square/`|->`|->`<=/<700,600>[
% a|_{Q(a)}
% ` (a,b)|_{Q(a)}
% ` a|_{ýb.R(a,b)}
% ` (a,b)|_{R(a,b)}
% ; ` ` ` ý ]
% \efig
% \qquad
% \bfig
% \square(0,600)|alrm|/<=`|->`|->`=>/<700,600>[
% {\mydmap[\GG,a,p`\GG ;]}
% ` {\mydmap[\GG,a,p`\GG,a;]}
% ` {\mydmap[\GG, q`\GG ;]}
% ` {\mydmap[\GG,a,q`\GG,a;]}
% ; \Sigma ` ` ` ]
% \square/`|->`|->`<=/<700,600>[
% {\mydmap[\GG, q`\GG ;]}
% ` {\mydmap[\GG,a,q`\GG,a;]}
% ` {\mydmap[\GG,(a \mto r)`\GG;]}
% ` {\mydmap[\GG,a,r`\GG,a;]}
% ; ` ` ` \Pi ]
% \efig
% $$
\newpage
% --------------------
% «intro-CC-1» (to ".intro-CC-1")
% (s "Introduction to the Calculus of Constructions (1)" "intro-CC-1")
\myslide {Introduction to the Calculus of Constructions (1)} {intro-CC-1}
CC is a particular case of a {\sl pure type system}.
A PTS has a set of {\sl sorts} (for CC, $\{Þ,ñ\}$),
a set of {\sl axioms} involving sorts (for CC, $\{\vdash Þ\:ñ\}$),
and a set of pairs of sorts (for CC, $\{(Þ,Þ), (Þ,ñ), (ñ,Þ), (ñ,ñ)\}$)
that specify which variations of the derivation rules are valid.
We also need a countable set of {\sl variables} ---
e.g.\ $\{a,b,c,\ldots, A,B,C,\ldots\}$.
From that we define {\sl pre-terms}, {\sl pre-judgements} and (valid)
derivations.
Terms and judgements are pre-terms and pre-judgements that
can appear in valid derivations.
\newpage
% --------------------
% «preterms-and-prejudgs» (to ".preterms-and-prejudgs")
% (s "Pre-terms and pre-judgements" "preterms-and-prejudgs")
\myslide {Pre-terms and pre-judgements} {preterms-and-prejudgs}
The set of pre-terms is the least set closed under the following
rules:
$\bullet$ sorts are pre-terms
$\bullet$ variables are pre-terms
If $v$ is a variable, $f, t, t'$ pre-terms,
$\bullet$ $f t$ is a pre-term (application)
$\bullet$ $ðv\:t.t'$ is a pre-term (abstraction, function)
$\bullet$ $åv\:t.t'$ is a pre-term (function space)
Examples of (pre-)terms:
$ðA\:Þ.ða\:A.a$ \qquad (polymorphic identity)
$ðI\:Þ.ðA\:(åi\:I.Þ).(åi\:I.Ai)$
\smallskip
A pre-judgement is something like
$x_1\:A_1, \ldots, x_n\:A_n \vdash t\:t'$
where $x_1, \ldots, x_n$ {are all distinct}
and $A_1, \ldots, A_n, t, t'$ are pre-terms.
$n$ can be 0 (``empty context'').
\newpage
% --------------------
% «naive-semantics» (to ".naive-semantics")
% (s "Naive semantics: $ð$ and $å$" "naive-semantics")
\myslide {Naive semantics: $ð$ and $å$} {naive-semantics}
The $ð$ of CC is like the usual $ð$ of $ð$-calculus, but
with a restriction on the type of the input.
$(ða\:A.b) a'$ will only be a (valid) term if $a'\:A$.
\smallskip
The $å$ forms function spaces:
If $b:B$ then $(ða\:A.b)\:(åa\:A.B)$.
\smallskip
Dependent types: in $ða\:A.b$ and $åa\:A.B$, with $b\:B$,
$B$ can be a term involving $a$!
\smallskip
$f a'$ will only be a (valid) term if $f$ and $a'$ can be typed as
$f\:(åa\:A.B)$ and $a'\:A$.
\medskip
{\bf Naive semantics for `$å$':} example: if $I=\{1,2,3\}$,
then $åi\:I.A_i = \prod_{i \in I} A_i =$
$= \{\{(1,a_1), (2,a_2), (3,a_3)\} \;|\; a_1ÎA_1, a_2ÎA_2, a_3ÎA_3\}$
$\cong A_1 × A_2 × A_3$
\newpage
% --------------------
% «intro-CC-2» (to ".intro-CC-2")
% (s "Introduction to CC (2) - example of a valid derivation" "intro-CC-2")
\myslide {Introduction to CC (2) - example of a valid derivation} {intro-CC-2}
%: |-Þ\:ñ |-Þ\:ñ |-Þ\:ñ .
%: ---------------¦{weak}_ñ ----------¦s_ñ .
%: |-Þ\:ñ X\:Þ|-Þ\:ñ X\:Þ|-X\:Þ .
%: ----------¦s_ñ ---------------------------------¦{weak}_Þ .
%: X\:Þ|-X\:Þ X\:Þ,x\:X|-Þ\:ñ .
%: --------------------------------å_{Þñ} .
%: X\:Þ|-(åx\:X.Þ)\:ñ .
%: -------------------------------¦s_ñ .
%: X\:Þ,F\:(åx\:X.Þ)|-F\:(åx\:X.Þ) .
%: .
%: ^exvalidderCC .
%:
$$\ded{exvalidderCC}$$
A tree of (pre-)judgements
The leaves are axioms
The root is the conclusion
The bars are applications of the rules (coming soon!)
Most of the tree is ``bureaucracy'' (weakings, for example)
$\underbrace{
x_1\overbrace{\:A_1}^{\text{typing}}, \ldots,
x_n\overbrace{\:A_n}^{\text{typing}} \vdash
}_{\text{context}}
t \overbrace{\:T }^{\text{typing}}
$
The {\sl terms} are the pre-terms that can appear as `$x_i$'s,
`$A_i$'s, $t$ or $T$.
\newpage
% --------------------
% «rules-CC» (to ".rules-CC")
% (s "The rules of the Calculus of Constructions" "rules-CC")
\myslide {The rules of the Calculus of Constructions} {rules-CC}
Rules of the system: ax, s, $å$, $ð$, app, weak, conv
(conv is not shown; if $a\:A$ and $A =_\bb A'$ then $a\:A'$)
%
% (find-defded nil "30apr-ax1")
%:
%: ------¦{ax}
%: |-Þ\:ñ{}
%:
%: ^30apr-ax2
%:
%: \GG|-A\:R
%: --------------¦s_R
%: \GG,a\:A|-a\:A
%:
%: ^30apr-s2
%:
%: \GG|-A\:R \GG,a\:A|-B\:S
%: -------------------------å_{RS}
%: \GG|-(åa\:A.B)\:S
%:
%: ^30apr-Prod2
%:
%: \GG,a\:A|-b\:B \GG|-(åa\:A.B)\:S
%: ---------------------------------ð_{RS}
%: \GG|-(ða\:A.b)\:(åa\:A.B)
%:
%: ^30apr-lambda2
%:
%: \GG|-f\:(åa\:A.B) \GG|-a'\:A
%: -----------------------------¦{app}_{RS}
%: \GG|-fa'\:B[a:=a']
%:
%: ^30apr-app2
%:
%: \GG,\Delta|-c\:C \GG|-A\:R
%: ---------------------------¦{weak}_R
%: \GG,a\:A,\Delta|-c\:C
%:
%: ^30apr-weak2
%:
%:
$$\begin{array}{cc}
\ded{30apr-Prod2} & \ded{30apr-ax2} \\
\ded{30apr-lambda2} & \ded{30apr-s2} \\
\ded{30apr-app2} & \ded{30apr-weak2}
\end{array}
$$
$R$, $S$ sorts; $a$ variable; $\GG$, $\Delta$ contexts
All other letters ($a'$, $A$, $b$, $B$, $c$, $C$, $f$) represent terms
(Remember: even in a pre-judgement we can't have repeated
declarations for the same variable)
\newpage
% --------------------
% «some-facts-about-CC» (to ".some-facts-about-CC")
% (s "Some facts (i.e., theorems) about CC}" "some-facts-about-CC")
\myslide {Some facts (i.e., theorems) about CC} {some-facts-about-CC}
Each term of CC is either a sort, or a member of a sort, or
a member of a member or a sort.
\smallskip
Each variable is a member of a member of a sort.
\smallskip
If $x_1\:A_1, \ldots, x_n\:A_n \vdash t\:T$ then
the list $x_1, \ldots, x_n$ contains all the free variables of $t$ and
$T$;
there exist sorts $S_1, \ldots, S_n$ such that
$\vdash A_1\:S_1$,
$x_1\:A_1 \vdash A_2\:S_2$,
$x_1\:A_1, x_2\:A_2 \vdash A_3\:S_3$,
$\ldots$,
and if $T$ is not a sort then there exists a sort $S$ s.t.:
$x_1\:A_1, \ldots, x_n\:A_n \vdash T\:S$.
\smallskip
{\bf Reading a pre-judgement aloud}
Examples:
$\vdash (ðA\:Þ.ða\:A.a) \: (åA\:Þ.åa\:A.A)$
$I\:Þ, A\:(åi\:I.Þ) \vdash (åi\:I.Ai)\:Þ$
\newpage
% --------------------
% «more-facts-about-CC» (to ".more-facts-about-CC")
% (s "More facts about CC: ``classes'' of terms, variations of the rules" "more-facts-about-CC")
\myslide {More facts about CC: ``classes'' of terms, variations of the rules} {more-facts-about-CC}
If we know the ``class'' of each variable we know the class
of every term:
$(ða^\clm R2 \: A^\clm R1 . b^\clm S2)^\clm S2$
\qquad
$(f^\clm S2 a^\clm R2)^\clm S2$
$(åa^\clm R2 \: A^\clm R1 . B^\clm S1)^\clm S1$
\smallskip
$\begin{array}{cccccccc}
& & ¦{operator} &:& ¦{kind} &:& ñ \\
¦{element} &:& ¦{set} &:& Þ & &
\end{array}
$
\medskip
\def\hone#1#2{&&&å_{#1#2},}
\def\htwo#1#2{&&&ð_{#1#2},}
\def\hthr#1#2{&&&¦{app}_{#1#2}}
$\begin{array}{cccccccc|cl}
a,a' &:& A &:& Þ & & \honeÞÞ \\
b,fa' &:& B &:& Þ & & \htwoÞÞ \\
f,(ða\:A.b) &:& (åa\:A.B) &:& Þ & & \hthrÞÞ \\ \hline
%
& & a,a' &:& A &:& ñ \honeñÞ \\
b,fa' &:& B &:& Þ & & \htwoñÞ \\
f,(ða\:A.b) &:& (åa\:A.B) &:& Þ & & \hthrñÞ \\ \hline
%
a,a' &:& A &:& Þ & & \honeÞñ \\
& & b,fa' &:& B &:& ñ \htwoÞñ \\
& & f,(ða\:A.b) &:& (åa\:A.B) &:& ñ \hthrÞñ \\ \hline
%
& & a,a' &:& A &:& ñ \honeññ \\
& & b,fa' &:& B &:& ñ \htwoññ \\
& & f,(ða\:A.b) &:& (åa\:A.B) &:& ñ \hthrññ %
\end{array}
$
\newpage
% --------------------
% «CC-to-CCMC-and-back» (to ".CC-to-CCMC-and-back")
% (s "From CC with minimal contexts to ND and back" "CC-to-CCMC-and-back")
\myslide {From CC with minimal contexts to ND and back} {CC-to-CCMC-and-back}
Definition: a ``good'' derivation tree is one in which:
$\bullet$ each variable appears always with the same type
$\bullet$ whenever there are two subtrees ``deriving the same term'',
they are equal
\medskip
Take a good tree with minimal contexts, for example,
%:
%: ------
%: |-Þ\:ñ %
%: ----------[¦s_ñ]^{C2} ------ ------
%: I\:Þ|-I\:Þ |-Þ\:ñ |-Þ\:ñ %
%: ----------------------------å_{Þñ} ----------[¦s_ñ]^{C1}
%: I\:Þ|-(åi\:I.Þ)\:ñ I\:Þ|-I\:Þ
%: ------ ------------------------------¦s_ñ ---------------[¦s_Þ]^2
%: |-Þ\:ñ I\:Þ,A\:(åi\:I.Þ)|-A\:(åi\:I.Þ) I\:Þ,i\:I|-i\:I
%: ----------s_ñ ----------------------------------------------¦{app}_{Þñ};1
%: I\:Þ|-I\:Þ I\:Þ,A\:(åi\:I.Þ),i\:I|-Ai\:Þ
%: --------------------------------------------å_{ÞÞ};2
%: I\:Þ,A\:(åi\:I.Þ)|-(åi\:I.Ai)\:Þ
%: ----------------------------------------------s_Þ
%: I\:Þ,A\:(åi\:I.Þ),f\:(åi\:I.Ai)|-f\:(åi\:I.Ai)
%:
%: ^apr30a
%:
$$\ded{apr30a}$$
erase its contexts, and put in the dictionary all the remaining typings:
%:
%: ----
%: Þ\:ñ %
%: ----[¦s_ñ]^{C2} ---- ----
%: I\:Þ Þ\:ñ Þ\:ñ %
%: ---------------------å_{Þñ} ----[¦s_ñ]^{C1}
%: (åi\:I.Þ)\:ñ I\:Þ
%: ---- ------------¦s_ñ ----[¦s_Þ]^2
%: Þ\:ñ A\:(åi\:I.Þ) i\:I
%: ----s_ñ ------------------------------¦{app}_{Þñ};1
%: I\:Þ Ai\:Þ
%: --------------------------å_{ÞÞ};2
%: (åi\:I.Ai)\:Þ
%: -------------s_Þ
%: f\:(åi\:I.Ai)
%:
%: ^apr30b
%:
$$\ded{apr30b}
\qquad
\begin{array}[b]{l}
\text{Dictionary:} \\
i : I : Þ \\
A : (åi\:I.Þ) : ñ \\
Ai : Þ \\
f : (åi\:I.Ai) : Þ
\end{array}
$$
\newpage
% --------------------
% «CC-to-CCMC-and-back-2» (to ".CC-to-CCMC-and-back-2")
% (s "From CC with minimal contexts to ND and back (2)" "CC-to-CCMC-and-back-2")
\myslide {From CC with minimal contexts to ND and back (2)} {CC-to-CCMC-and-back-2}
...now erase the typings too:
%:
%: -
%: Þ
%: -[¦s_ñ]^{C2} - -
%: I Þ Þ
%: ---------------å_{Þñ} -[¦s_ñ]^{C1}
%: åi\:I.Þ I
%: - -------¦s_ñ -[¦s_Þ]^2
%: Þ A i
%: -s_ñ ---------------------¦{app}_{Þñ};1
%: I Ai
%: --------------------------å_{ÞÞ};2
%: åi\:I.Ai
%: --------s_Þ
%: f
%:
%: ^apr30c
%:
$$\ded{apr30c}
\qquad
\begin{array}[b]{l}
\text{Dictionary:} \\
i : I : Þ \\
A : (åi\:I.Þ) : ñ \\
Ai : Þ \\
f : (åi\:I.Ai) : Þ
\end{array}
$$
Fact: it is possible to reconstruct the original tree from this one.
New variables are introduced only at the ``s'' rules.
To help keep track of what's happening, we mark discharges with `$[·]^n$'s
and ``contractions'' with `$[·]^{Cn}$'s.
\medskip
{\sl It is also possible to discard the dictionary and reconstruct it
just from}
{\sl that last tree.}
\medskip
Next step (not shown): replace the terms in a tree with names for them
in the GP notation; let the dictionary translate some terms as
applications --- example, $b \dicto (a \mto b)(a)$.
\newpage
% --------------------
% «props-and-proofs-in-CC» (to ".props-and-proofs-in-CC")
% (s "Representing propositions and proofs in CC" "props-and-proofs-in-CC")
\myslide {Representing propositions and proofs in CC} {props-and-proofs-in-CC}
Props is a sort; in CC, $\Props = Þ$
(in other PTSs we may have $\Props \neq Þ$ and we
may be able to formalize {\sl irrelevance of proofs})
\medskip
$\prop[P]$ is $P$ seen as a proposition.
Naively, $\prop[P]$ is the set of proofs of $P$.
$\prf[P] : \prop[P] : \Props \quad (= Þ)$
\medskip
Dictionary:
$\begin{array}{rcl}
\prop[P⊃Q] & \dicto & (å\prf[P]\:\prop[P].\prop[Q]) \\
\prf[P⊃Q] & \dicto & (\prf[P] \mto \prf[Q]) \\
\prop[ýx.P(x)] & \dicto & (åx\:\E[x].\prop[P(x)]) \\
\prf[ýx.P(x)] & \dicto & (x \mto \prf[P(x)])
\end{array}
$
\newpage
% --------------------
% «terms-for-equality» (to ".terms-for-equality")
% (s "Terms for equality" "terms-for-equality")
\myslide {Terms for equality} {terms-for-equality}
To speak ``internally'' about equality between members of the same set
we need a package of terms, that will be added to contexts...
\medskip
$¦{equality}_Þ$ is a package consisting of:
$\begin{array}{ll}
¦{eq}_Þ & (¦{eq}_Þ A a a') : \Props \\
& \prop[a=a'] \dicto ¦{eq}_Þ A a a' \\
¦{refl}_Þ & (¦{refl}_Þ A a) : \prop[a=a] \\
& \prf[a=a] \dicto ¦{refl}_Þ A a \\
¦{sim}_Þ & (¦{sim}_Þ A a a') : \prop[a=a'⊃a'=a] \\
& \prf[a=a'⊃a'=a] \dicto (¦{sim}_Þ A a a') \\
¦{trans}_Þ & (¦{trans}_Þ A a a' a'') : \prop[a=a'⊃(a'=a''⊃a=a'')] \\
& \prf[a=a'⊃(a'=a''⊃a=a'')] \dicto (¦{trans}_Þ A a a' a'')
\end{array}
$
\medskip
$¦{f's.r.equality}_{ÞÞ}$ is a package of terms saying that
all functions $f\:(åa\:A.B)$ ``respect equality''.
This is a bit trickier, as it involves the ``conv'' rule.
\medskip
Note: $a,a',a''\:A\:Þ$, $B\:Þ$
\newpage
% --------------------
% «protocategories» (to ".protocategories")
% (s "Protocategories" "protocategories")
\myslide {Protocategories} {protocategories}
The prefix ``{\sl proto}'' will always mean ``{\sl without the terms
for equalities}''.
\smallskip
A protocategory $\catC : ¦{Protocats}_{SR}$
(where $S$, $R$ are sorts --- typically $S=ñ$, $R=Þ$)
is a package containing
$$\begin{array}{lll}
\Objs_\catC : S & & \\
\Hom_\catC & & \Hom_\catC A B : R \\
\id_\catC & & \id_\catC A : \Hom_\catC A A \\
¢_\catC & & ¢_\catC ABC (a \mto b) (b \mto c) : \Hom_\catC AC
\end{array}
$$
($A, B, C : \Objs_\catC$)
\medskip
Notational trick: $a \mto b : \E[a \mto b]$,
and the dictionary translates $\E[a \mto b] \dicto \Hom_\catC A B$.
% Actually we'll use $\O[a], \O[b], \O[c]$ instead of $A, B, C$.
\medskip
A protocategory comes without the `prf' terms that say the $¢_\catC$
behaves well.
A category is a protocategory plus such terms.
\newpage
% --------------------
% «protocategories-sets» (to ".protocategories-sets")
% (s "A very special example: $\\Set$ as a $ñÞ$-protocategory" "protocategories-sets")
\myslide {A very special example: $\protect\Set$ as a $\protectñÞ$-protocategory} {protocategories-sets}
$\Set : ¦{Protocats}_{ñÞ}$
$\Objs_\Set = Þ : ñ$
$\Hom_\Set \E[x] \E[y] = \E[x \mto y] : Þ$
$\Hom_\Set := ðX\:Þ.ðY\:Þ.(åx\:X.Y)$
$\id_\Set \E[x] = x \mto x$
$\id_\Set := ðX\:Þ.ðx\:X.x$
$¢_\Set \E[x] \E[y] \E[z] (x \mto y) (y \mto z) = (y \mto z)¢(x \mto y)$
$¢_\Set := ðX\:Þ.ðY\:Þ.ðZ\:Þ.$
{\qquad \qquad} $ðf\:(\Hom_\Set XY).ðg\:(\Hom_\Set YZ).$
{\qquad \qquad \quad} $ðx\:X.g(fx)$
\bigskip
\newpage
% --------------------
% «protocategories-generic» (to ".protocategories-generic")
% (s "A typical $ñÞ$-protocategory" "protocategories-generic")
\myslide {A typical $ñÞ$-protocategory} {protocategories-generic}
$\Objs_\catC : ñ$
$\Hom_\catC : å\O[a]\:\Objs_\catC.å\O[b]\:\Objs_\catC.Þ$
$\O[a], \O[b], \O[c] : \Objs_\catC$
like $\E[x], \E[y], \E[z] : \Objs_\Set = Þ$
but {we don't have a semantics} for ``$a$'', ``$b$'', ``$c$''!!!
Just for $\O[a]$, $\O[b]$, $\O[c]$, $(a \mto b)$, $(b \mto c)$, $(a \mto c)$.
\medskip
%D diagram triangles
%D 2Dx 100 +20 +20 +20
%D 2D 100 x |-> y a |-> b
%D 2D / - / -
%D 2D \ | \ |
%D 2D v v v v
%D 2D +20 z c
%D 2D
%D (( x y |-> x z |-> y z |->
%D a b |-> a c |-> b c |->
%D ))
%D enddiagram
%D
$\diag{triangles}$
% $\bfig
% \qtriangle/|->`|->`|->/<250,250>[x`y`z;``]
% \efig
% \qquad
% \bfig
% \qtriangle/|->`|->`|->/<250,250>[a`b`c;``]
% \efig
% $
% {\qquad}
in $\Set$ \qquad \qquad in $\catC$
\medskip
New ``operator'' in the dictionary: $\Cat$ ---
$\Cat[x] \dicto \Set$, $\Cat[a] \dicto \catC$ ($\O[a]\:\Objs_\catC$)
\medskip
$x \mto y : \E[x \mto y] = \E[x] \to \E[y]$
$a \mto b : \E[a \mto b] = \Hom_\catC \O[a] \O[b]$
\newpage
% --------------------
% «DNC-rules» (to ".DNC-rules")
% (s "System DNC: rules" "DNC-rules")
\myslide {System DNC: rules} {DNC-rules}
%:
%: \O[a] a=>a^F a'÷>a'' a=>a^F
%: -------------(=>E_O) ---------------(=>E_M)
%: \O[a^F] {a'}^F÷>{a''}^F
%:
%: ^funtoEO ^funtoEM
%:
%: \O[a] a-.>(a^F÷>a^G)
%: ---------------------(-.>E)
%: a^F÷>a^G
%:
%: ^tnE
%:
$\ded{funtoEO} \qquad \ded{funtoEM}$
$\ded{tnE}$
\medskip
Several ``ren'' rules, e.g.,
%:
%: a=>a^F a-.>(a^F÷>a^G)
%: ----------¦{ren} ------------------¦{ren}
%: \O[a=>a^F] (a=>a^F)÷>(a=>a^G)
%:
%: ^renftr1 ^renftr2
%:
$\ded{renftr1} \qquad \ded{renftr2}$
\medskip
Discharges are written in usual ND style:
%:
%: \Objs_\catC
%: -----------[¦s]^1
%: \O[a] \ldots [\O[a]]^1 \ldots
%: ======================== ==================
%: \O[a^F] \O[a^F]
%: --------------1 --------------1
%: \O[a]÷>\O[a^F] \O[a]÷>\O[a^F]
%:
%: ^disch-nonND ^disch-ND
%:
$\ded{disch-nonND} \quad \sqto \quad \ded{disch-ND}$
but then we need to know that $\O[a]\:\Objs_\catC$ (dictionary!)
and the trees may split into several...
\newpage
% --------------------
% «DNC-rules-funtoI» (to ".DNC-rules-funtoI")
% (s "System DNC: $(\\funto I)$, example" "DNC-rules-funtoI")
\myslide {System DNC: $(\funto I)$, example} {DNC-rules-funtoI}
If we know the action of $x \funto (a \mto x)$ on objects, i.e.,
\medskip
%:
%: [\O[x]]^1
%: ---------¦{ren}
%: \E[a] \E[x]
%: -------------
%: \E[a÷>x]
%: --------¦{ren}
%: \O[a÷>x]
%: ---------------1
%: \O[x]÷>\O[a÷>x]
%:
%: ^funtoi-ex1
%:
$\ded{funtoi-ex1}$
\medskip
then:
%:
%: [a÷>x']^1 [x'÷>x'']^2
%: ----------------------
%: a÷>x''
%: -----------------1
%: (a÷>x')÷>(a÷>x'')
%: ------------------------------2
%: (x'÷>x'')÷>((a÷>x')÷>(a÷>x''))
%: ------------------------------\text{``$(\funto"I)$''}
%: x=>(a÷>x)
%:
%: ^funtoi-ex2
%:
$\ded{funtoi-ex2}$
Note that we are constructing a {proto}-functor ---
we are leaving out the ``prf'' terms!
\newpage
% --------------------
% «DNC-rules-tntoI» (to ".DNC-rules-tntoI")
% (s "System DNC: $(\\tnto I)$, example" "DNC-rules-tntoI")
\myslide {System DNC: $(\protect\tnto I)$, example} {DNC-rules-tntoI}
If we know $x \funto (b \mto x)$ and $x \funto (a \mto x)$, then
the rule for creating
$x \tnto ((b \mto x) \mto (a \mto x))$
is essentially the same as the rule for creating
$\O[x] \mto ((b \mto x) \mto (a \mto x))$
--- again, we leave out the ``prf'' terms, and we only
build a {proto}-natural transformation.
Example:
%:
%: \O[b] [\O[x]]^2
%: ----------------
%: \E[b÷>x]
%: --------[s]^1
%: a÷>b [b÷>x]^1 a÷>b b÷>x
%: --------------- ------------
%: a÷>x a÷>x
%: --------------1 --------------1
%: (b÷>x)÷>(a÷>x) (b÷>x)÷>(a÷>x)
%: --------------------2 --------------------2
%: x-.>((b÷>x)÷>(a÷>x)) x-.>((b÷>x)÷>(a÷>x))
%:
%: ^extntoI-a ^extntoI-b
%:
$\ded{extntoI-a} \qquad \ded{extntoI-b}$
\newpage
% --------------------
% «future-work» (to ".future-work")
% (s "Future work" "future-work")
\myslide {Future work} {future-work}
{\bf Is DNC strongly normalizing?}
Problems with this question:
\begin{itemize}
\item Right now DNC is just a layer of syntax on top of CC
\item We need to formalize better how the dictionary works
\item Some rules (e.g. $(\funto E)$) involve a certain amount of
pattern-matching
\item Reductions (cut-elimination) may require non-trivial renamings
\item Which names are valid? DNC terms are inherently ambiguous...
\end{itemize}
DNC is not well-defined enough yet!!
\newpage
% --------------------
% «before-SN-for-DNC» (to ".before-SN-for-DNC")
% (s "What comes before studying SN for DNC" "before-SN-for-DNC")
\myslide {What comes before studying SN for DNC} {before-SN-for-DNC}
% (find-lsrcfile "base/ltlists.dtx" "\\cs{topsep}")
% (find-lsrcfile "base/ltlists.dtx" "\\begin{environment}{itemize}")
% (find-lsrcfile "base/ltlists.dtx" "\\def\\@item[#1]")
\smallskip
{\bf We need to learn more about DNC's ambiguities:}
If a DNC term $\aa$ has a natural construction,
\begin{itemize}
\setlength{\itemsep}{0pt}
\setlength{\parsep}{0pt}
\item is it essentially unique?
\item does it lift from the ``syntactical world'' to the ``real world''?
\item coherence/parametricity
\end{itemize}
\smallskip
Missing: rules for defining new categories
\smallskip
{\bf DNC and GP are tools for expressing the (intuitive) skeletons of
some proofs (more precisely, the T-parts of proofs).} So, morally, we
should be able to represent nicely in GP/DNC:
\begin{itemize}
\item SN proofs for CC
\item Categorical models for CC and other type theories
\item ``Basic category theory'' (everything that a categorist would say
is trivial)
\item A lot about fibrations
\item And also:
\begin{itemize}
\item Topos logic (and a ND for it!)
\item Terms involving infinitesimals and derivatives (my original
motivation, years ago)
\end{itemize}
\end{itemize}
\newpage
% --------------------
% «notes-about-slides» (to ".notes-about-slides")
% (s "Notes for people downloading these slides" "notes-about-slides")
\myslide {Notes for people downloading these slides} {notes-about-slides}
In a very near future (before the end of June, I hope) I'm going to
add notes about how I handwaved over these slides in the presentation,
and, even more important, how to ``pronounce'' the DNC terms and
diagrams... and also pointers to the literature, thanks to the people
that discussed these ideas with me and helped me shape the
presentation (Robert Seely, Jeff Egger, Robin Cockett), and a few
other things.
Now I have to hurry up and prepare the slides for my presentation at
the CMS 2002, in Quebec city... it's going to be only 15 mins long
(this one was 45 mins) so I'll have to use a different approach, with
more motivation and less details...
So: please check {\tt http://angg.twu.net/} again in a few weeks for a
new version of this. Sorry for the mess! Edrx, 2002jun13
% other way to see: a judgement is a program, that given any seq $x_1,
% \ldots x_n$ produces a $t:T$.
%
% judgements - example (polyid) - cases when we can't select members (in
% the naive semantics)
%
% the rules of CC (with annotations to help, and coloured bubbles to
% indicate what we'll discard, and which parts are ``morally
% unnecessary'' --- we could get rid of them if the class annotations
% were more formal)
%
% a system with rules that ``mix'' contexts (instead of having to weaken
% eeeeverything)
%
% We say that a judgement has {minimal context} if we can't delete one
% of its premises and still have a (valid) judgement...
%
% $A:Þ \vdash (ða\:A.a)\:(åa\:A.A)$ has minimal context
%
% $A:Þ, a:Þ \vdash (ða\:A.a)\:(åa\:A.A)$ doesn't
%
% What happens if we try to create a system like CC, but where each
% judgement has minimal context? Ex:
%
% %:
% %: I\:Þ,A\:(åi\:I.Þ)|-A\:(åi\:I.Þ) I\:Þ,i\:I|-i\:I
% %: -------------------------------------------------¦{app}_{Þñ}
% %: I\:Þ,i\:I,A\:(åi\:I.Þ)|-Ai\:Þ
% %:
% %: ^ex-minctxts
% %:
% $$\ded{ex-minctxts}$$
%
% Hidden weakenings
%
% Hidden ``conv''s
%
% % (find-diagxyfile "diaxydoc.tex" "\\Atriangle(x,y)|ppp|")
%
% for good trees the typings and contexts can be recovered from
% the dictionary! And we can also get rid of the right hypothesis in
% $å_{RS}$ and $ð_{RS}$.
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: