Warning: this is an htmlized version!
The original is across this link, and the conversion rules are here. |

% (find-angg "LATEX/2010diags.tex") % (find-angg ".emacs" "idct") % (find-dn4ex "edrx08.sty") % (find-angg ".emacs.templates" "s2008a") % (find-angg ".zshrc" "makebbl") % (defun b () (interactive) (find-zsh "makebbl 2010diags.bbl catsem,filters")) % (defun b () (interactive) (find-zsh "bibtex 2010diags")) % (defun b () (interactive) (find-zsh "bibtex 2010diags; makeindex 2010diags")) % (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010diags.tex && latex 2010diags.tex")) % (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010diags.tex && latex 2010diags.tex" 1 '(eek "M->"))) % (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010diags.tex && pdflatex 2010diags.tex")) % (eev "cd ~/LATEX/ && Scp 2010diags.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/") % (defun d () (interactive) (find-xdvipage "~/LATEX/2010diags.dvi")) % (find-dvipage "~/LATEX/2010diags.dvi") % % (setq b-cmd "bibtex 2010diags") % (setq c-cmd "~/dednat4/dednat41 2010diags.tex && latex 2010diags.tex") % (setq cbcbc-cmd (concat c-cmd " && " b-cmd " && " c-cmd " && " b-cmd " && " c-cmd)) % (defun bc () (interactive) (find-zsh cbcbc-cmd 1 '(eek "M->"))) % % (find-pspage "~/LATEX/2010diags.ps") % (find-pspage "~/LATEX/2010diags.pdf") % (find-xpdfpage "~/LATEX/2010diags.pdf") % (find-man "dvipdf") % (find-zsh0 "cd ~/LATEX/ && dvipdf 2010diags.dvi 2010diags.pdf") % (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2010diags.ps 2010diags.dvi") % (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2010diags.ps 2010diags.dvi && ps2pdf 2010diags.ps 2010diags.pdf") % (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi") % (find-pspage "~/LATEX/tmp.ps") % (ee-cp "~/LATEX/2010diags.pdf" (ee-twupfile "LATEX/2010diags.pdf") 'over) % (ee-cp "~/LATEX/2010diags.pdf" (ee-twusfile "LATEX/2010diags.pdf") 'over) % (find-twusfile "LATEX/" "2010diags") % http://angg.twu.net/LATEX/2010diags.pdf %«.mental-space»(to "mental-space") %«.projs-and-lifts»(to "projs-and-lifts") %«.dn-types»(to "dn-types") %«.dictionary»(to "dictionary") %«.internal»(to "internal") %«.parallel-notations»(to "parallel-notations") %«.functors»(to "functors") %«.nts»(to "nts") %«.adjunctions»(to "adjunctions") %«.fnta»(to "fnta") %«.transmission»(to "transmission") %«.intuition»(to "intuition") %«.skeletons»(to "skeletons") %«.hyps»(to "hyps") %«.pres-frob-bcc»(to "pres-frob-bcc") %«.eq-elim»(to "eq-elim") %«.archetypal»(to "archetypal") %«.CCCs»(to "CCCs") %«.olts»(to "olts") %«.database»(to "database") %«.synt-world»(to "synt-world") %«.formalizing-diags»(to "formalizing-diags") %«.prob-with-toposes»(to "prob-with-toposes") %«.epilogue»(to "epilogue") \def\Setito{\Set^{\ito}} \def\Setmto{\Set^{\monicto}} \def\Pred{¦{Pred}} \def\Pred{Ð{Pred}} \def\cob{¯{c.o.b.}} \def\EqE{{=}E} \def\TB{§\!_{B}} \def\TAB{§\!_{A×B}} \def\SDTB{Æ_\DD\!\TB} \def\pip { \pi'} \def\opip {\ov\pi'} \def\pipstar { \pi^{\prime*}} \def\opipstar{\ov\pi^{\prime*}} \def\pistar { \pi^{*}} \def\opistar {\ov\pi^{*}} \def\opi {\ov\pi} \def\EqEdomain{\opipstarÆ_\DD\TB \land \opistar\dd^*Q} \def\EqEL {\opipstarÆ_\DD\TB} \def\EqER {\opistar\dd^*Q} \def\EqEdomthin{\EqEL{∧}\EqER} \def\EqEdomwide{\EqEL\land\EqER} \def\fdiag#1{\fbox{\!\!\!$\diag{#1}$}} \def\fdiag#1{\fbox{$\diag{#1}$}} \def\ffdiag#1#2{\begin{tabular}{l}#2\\\fbox{$\diag{#1}$}\end{tabular}} \def\fdiag#1{\ffdiag{#1}{foo}} \def\ctabular#1{\begin{tabular}{c}#1\end{tabular}} \def\ltabular#1{\begin{tabular}{l}#1\end{tabular}} % \def\fdiagwithboxest#1#2{\ltabular{#2 \\ \fdiagwithboxes{#1}}} \def\fdiagest#1#2{\ltabular{#2 \\ \fdiag{#1}}} \def\fdiag#1{\fbox{$\diag{#1}$}} \def\sqrtdot{\sqrt{\,·\,}} \def\tondot{\ton{.\;}} \def\corn#1{\ulcorner#1\urcorner} %:*×*{×}*%:*=*{=}*%:*&*{∧}*%:*∧*{∧}*%:*⊃*{⊃}*% :*g^*f^**g^*\!f^**% -------------------- %«mental-space»(to ".mental-space") % (sec "Mental Space and Diagrams" "mental-space") \mysection {Mental Space and Diagrams} {mental-space} {\sl My memory is limited, and not very dependable: I often have to rededuce results to be sure of them, and I have to make them fit in as little ``mental space'' as possible...} Different people have different measures for ``mental space''; someone with a good algebraic memory may feel that an expression like % $\Frobnat: Æ_f(P∧f^*Q) \xton{\cong} Æ_fP∧Q$ % % % $$Æ_f(P∧f^*Q) \xton{\cong} Æ_fP∧Q$$ % is easy to remember, while I % % --- let's construct a semi-fictional ``I'' on the course of this % --- paper, and analyze how this ``I'' thinks --- again: while I % always think diagramatically, and so what I do is that I remember this diagram, $$\includegraphics[scale=0.5]{frob-sketch.eps}$$ % {\myttchars % \footnotesize % \begin{verbatim} % =========> % | / | % /====> - O % || \ | % \========= % % ---------> % \end{verbatim} % } \noindent and I reconstruct the formula from it. \msk I cannot yet define precisely what it is to ``think diagramatically'', but for the purposes of this paper a loose definition --- or rather, a set of concepts and techniques for diagrammatical thinking, plus non-trivial consequences of ``thinking'' in that way --- shall do. I will resort to a narrative device: {\sl I will speak as from a semi-fictional ``I'' who thinks as diagramatically as possible, and who always uses diagrams as a help for his bad algebraic thinking.} % -------------------- %«projs-and-lifts»(to ".projs-and-lifts") % (sec "Projections and Liftings" "projs-and-lifts") \mysection {Projections and Liftings} {projs-and-lifts} Take the concept of ``projection'', from the realm of covering spaces or from Linear Algebra. A projection map discards information --- coordinates, maybe --- and may collapse objects that were originally distinct. % When I represent projections diagrammatically I try to organize my diagrams to make the projection arrows --- most of them, at least --- go down. Figure \ref{2^100-2^99} is an example. {\sl Specialization} acts like a projection. Look at the top arrow in Figure \ref{2^100-2^99}: except for the choice of a particular value for $n$, we have only lost information. {\sl Discarding intermediate steps}, as in the bottom arrow, is a kind of {\sl erasing}, and erasings are evidently projections. % (find-854 "" "generalization") % (find-854page 14 "generalization") \def\twoninenyninelemma#1#2{ \fbox{ $\begin{array}{rcl} 2^{#2}-2^{#1} &=& 2^{1+#1}-2^{#1} \\ % &=& 2^{1}·2^{#1}-2^{#1} \\ &=& 2·2^{#1}-1·2^{#1} \\ &=& (2-1)·2^{#1} \\ % &=& 1·2^{#1} \\ &=& 2^{#1} \\ \end{array} $} } %:*&*&*%D diagram 2^100-2^99 %D 2Dx 100 %D 2D 100 proof-n %D 2D %D 2D +50 proof-99 %D 2D %D 2D +40 statement-99 %D 2D %D (( %D proof-n .tex= \twoninenyninelemma{n}{n+1} %D proof-99 .tex= \twoninenyninelemma{99}{100} %D statement-99 .tex= \fbox{$\begin{array}{rcl}2^{100}-2^{99}&=&2^{99}\end{array}$} %D @ 0 @ 1 -> %D @ 1 @ 2 -> %D )) %D enddiagram %D % $$\diag{2^100-2^99}$$ % $$\text{Figure [2-100-99]}$$ % \begin{figure}[H] $$\diag{2^100-2^99}$$ \caption{A specialization and an erasing.} \label{2^100-2^99} \end{figure} %:*&*{∧}*The opposite of {\sl to project} is {\sl to lift}; projecting is easy, lifting is hard. A projection map, $p: E \to B$, may have any number of preimages for a point $b$ in the base space --- one, many, none ---, and, to make things worse, we will often be interested in very specific cases where we are somehow able to recognize whether a given lifting is ``good'' or not --- for example, we may be looking for the ``right'' generalization for $2^{100}-2^{99} = 2^{99}$ ---, but where we are unable to define exactly what a ``good lifting'' is. % -------------------- %«dn-types»(to ".dn-types") % (sec "Downcased Types" "dn-types") \mysection {Downcased Types} {dn-types} Suppose that we have a point $pÝA×B$ and a function $f:B \to C$. There is a single ``obvious'' way to build a point of $C$ starting from this data. It is ``obvious'' because we have a search method that finds it; it is related to proof search ({\sl via} the Curry-Howard isomorphism). Here's how it works, briefly and informally. \widemtos A point $pÝA×B$ is a pair made of an `$a$' and a `$b$'. If we allow ``long names'' for variables we can replace the `$p$' by another name, that reflects its type more closely; so let's rename `$p$' to `$a,b$'. Similarly, an $f:B \to C$ is an operation that takes each `$b$' to a `$c$', so let's rename `$f$' to `$b \mto c$'. Now, with this new notation, we are looking for an operation that takes an `$a,b$' and a `$b \mto c$' and produces a term that ``deserves the name'' `$c$'. We start at the tree in the lower right rectangle in Figure \ref{arch-derivs}, and we want to arrive at the tree in the lower left; both trees have the same shape, and by relating them we will see that the term corresponding to $c$ is $f('p)$. Note that in this new language --- ``Downcased Types'' --- we have no syntactical distinction between variables and non-atomic terms. % (find-854 "" "standard-erasings") % (find-854page 13 "standard-erasings") % (find-854 "" "generalization") % (find-854page 14 "generalization") %L forths["<.>"] = function () pusharrow("<.>") end %L forths["<-->"] = function () pusharrow("<-->") end %L forths["|-->"] = function () pusharrow("|-->") end % This gives us a way to draw all the "standard % erasings" of a tree from a single tree definition. % Low-level words: % \def\archfull#1#2#3{#1\equiv #2:#3} \def\ARCHFULL {\let\arch=\archfull} \def\archdnc#1#2#3{#1} \def\ARCHDNC {\let\arch=\archdnc} \def\archtermtype#1#2#3{#2:#3} \def\ARCHTERMTYPE{\let\arch=\archtermtype} \def\archterm#1#2#3{#2} \def\ARCHTERM {\let\arch=\archterm} \def\archtype#1#2#3{#3} \def\ARCHTYPE {\let\arch=\archtype} \def\rY#1{#1} \def\RY {\let\r=\rY} \def\rN#1{} \def\RN {\let\r=\rN} \def\ptypeY#1{#1} \def\PTYPEY {\let\ptype=\ptypeY} \def\pytpeN#1{} \def\PTYPEN {\let\ptype=\pytpeN} % % High-level words: % \def\FULLRP{\ARCHFULL\RY\PTYPEY} \def\FULLR {\ARCHFULL\RY\PTYPEN} \def\FULLP {\ARCHFULL\RN\PTYPEY} \def\FULL {\ARCHFULL\RN\PTYPEN} \def\TERMTYPERP{\ARCHTERMTYPE\RY\PTYPEY} \def\TERMTYPER {\ARCHTERMTYPE\RY\PTYPEN} \def\TERMTYPEP {\ARCHTERMTYPE\RN\PTYPEY} \def\TERMTYPE {\ARCHTERMTYPE\RN\PTYPEN} \def\TERMRP{\ARCHTERM\RY\PTYPEY} \def\TERMR {\ARCHTERM\RY\PTYPEN} \def\TERMP {\ARCHTERM\RN\PTYPEY} \def\TERM {\ARCHTERM\RN\PTYPEN} \def\TYPER {\ARCHTYPE\RY\PTYPEN} \def\TYPE {\ARCHTYPE\RN\PTYPEN} \def\DNCR {\ARCHDNC\RY\PTYPEN} \def\DNC {\ARCHDNC\RN\PTYPEN} %: %: \arch{a,b}{p}{A×B} %: ------------------\r{'} %: \arch{b}{'p}{B} \arch{b|->c}{f}{B->C} %: -------------------------------------\r{\app} %: \arch{c}{f('p)}{C} %: %: ^archetypal-deriv %: %: %: \arch{a,b}{p}{A×B} \arch{b|->c}{f}{B->C} %: ========================================== %: \arch{c}{f('p)}{C} %: %: ^archetypal=deriv %: %D diagram archderivs2 %D 2Dx 100 +70 +05 +45 +35 %D 2D 100 \foo{\FULLRP} %D 2D %D 2D +50 \foo{\DNCR} \foo{\TERMTYPERP} %D 2D %D 2D +50 \foo{\DNC} \foo{\TERMR} \foo{\TYPE} %D 2D %D 2D +45 \fooo{\DNC} \fooo{\TERMR} \fooo{\TYPE} %D 2D %D (( \foo{\DNCR} x+= 15 %D # \foo{\TERMR} y+= -10 %D # \fooo{\TERMR} y+= -10 %D %D \foo{\FULLRP} \foo{\TERMTYPERP} -> %D \foo{\FULLRP} \foo{\DNCR} -> %D \foo{\TERMTYPERP} \foo{\TERMR} -> %D \foo{\TERMTYPERP} \foo{\TYPE} -> %D \foo{\DNCR} \foo{\DNC} -> %D \foo{\TYPE} \foo{\DNC} <--> .slide= 30pt %D %D \foo{\TERMR} \fooo{\TERMR} -> %D \foo{\TYPE} \fooo{\TYPE} -> %D \foo{\DNC} \fooo{\DNC} -> %D \fooo{\TYPE} \fooo{\DNC} <--> .slide= 25pt %D )) %D enddiagram %D % $$\def\foo#1{#1\fcded{archetypal-deriv}} % \def\fooo#1{#1\fcded{archetypal=deriv}} % \diag{archderivs2} % $$ % $$\text{Figure [Two]}$$ % \begin{figure} $$\def\foo#1{#1\fcded{archetypal-deriv}} \def\fooo#1{#1\fcded{archetypal=deriv}} \diag{archderivs2} $$ \caption{Downcased types.} \label {arch-derivs} % \caption{arch-derivs} \end{figure} All the solid arrows in Figure \ref{arch-derivs} are erasings. The dashed arrows are ``uppercasings'' when we go rightwards, ``downcasings'' when we go to the left; note that `$×$' is downcased to `$,$', and `$\to$' is downcased to `$\mto$'. If we start at the lower left and we move right through the dashed arrow, we get the types of the (three) objects involved; what we still need to do from there is a kind of ``term inference''... ``Type inference'' is very well-known, and polymorphic languages like Haskell and ML implement algorithms for it; ``term inference'', on the other hand, is rarely mentioned in the literature, but techniques like parametricity (\cite{WadlerTfF}, \cite{Bernardy10}) provide useful meta-theorems about properties that all possible inferrable terms must obey. It would be lovely if these techniques could do term inference for us, algorithmically --- but they can't, so when we need to infer terms we usually do the work by hand. As term inference is hard, let's turn our attention to something easier, and looser. ``Inference'' carries the connotation of something that can be done algorithmically, without any previous knowledge of the result. We will focus on the process of ``reconstructing'' the desired term, $c \equiv f('p)$, from the downcased tree in the lower left of Figure \ref{arch-derivs}. A ``reconstruction'' may need hints to be completed, and may depend on making the right choices at some points, motivated by unformalizable bits of common sense, or by intuition, hindsight, or by vague rememberances, by a sense of good style, or whatever else. A ``reconstruction'' is the result of an {\sl incomplete} algorithm (or a ``method'', rather than an ``algorithm''); when we perfect a method for reconstruction, and finish filling up all its gaps, it becomes an ``inference algorithm''. For our purposes, ``reconstruction'' will be enough --- and real ``inference'' will be close to impossible. % Amazingly, for our purposes, ``reconstruction'' will be enough --- % and real ``inference'' seems to be impossible. % -------------------- %«dictionary»(to ".dictionary") % (sec "The Dictionary" "dictionary") \mysection {The Dictionary} {dictionary} The downcased notation has to be used with care, as it doesn't come with any built-in devices to protect us from ambiguities. For example, we could have tried to find a term ``deserving the name'' `$a,a \mto a,a$' --- and there are four different ones!... One way to avoid this problem is to consider that the downcased ``names'' are just that, {\sl names}, and that we have a {\sl dictionary} that associates to each name its {\sl meaning}. In the case of $ð$-calculus, a dictionary relating each downcased name to its meaning can be extracted from a derivation tree (if all the rule names are present), and the derivation tree can be reconstructed from its associated dictionary. For example, %: %: a,b p %: ---' ---' %: b b|->c 'p f %: ----------\app -------\app %: c f('p) %: %: ^dict-1-dnc ^dict-1-std %: %D diagram dict-1 %D 2Dx 100 +90 %D 2D 100 dnc <----> dict %D 2D %D 2D +20 %D 2D %D (( dnc .tex= \fcded{dict-1-dnc} BOX %D dict .tex= \dict BOX %D @ 0 @ 1 -> sl^ %D @ 0 @ 1 <- sl_ %D )) %D enddiagram %D $$\def\dict{\fbox{$\begin{array}{rcl} \angg{b} &:=& '\angg{a,b} \\ \angg{c} &:=& \angg{b \mto c}\angg{b} \\ \end{array}$}} \diag{dict-1} $$ % and if we add to that dictionary the entries % $$\begin{array}{rcl} \angg{a,b} &:=& p \\ \angg{b \mto c} &:=& f \\ \end{array} $$ % then we can reconstruct the tree % $$\ded{dict-1-std}$$ % from that. Note that we use double angle brackets, $\angg{·}$, to separate names from one another and to distinguish them from standard notation, and that we use `$\equiv$' to indicate change of notation --- usually between downcased and standard. % -------------------- %«internal»(to ".internal") % (sec "Internal Diagrams" "internal") \mysection {Internal Diagrams} {internal} Several of the initial ideas for the system of downcased types came from attempts to formalize something that I will call ``physicist's notation'', and that should be familiar to most readers; I have never seen any detailed formalizations of it, though. Suppose that we have a function $f:\R \to \R$, and we draw the graph of $y=f(x)$. Then, given points $x_0$, $x_1$, $x_2$, $x'$ on the ``$x$-axis'' we have default meanings for the names $y_0$, $y_1$, $y_2$, $y'$: namely, $y_0 := f(x_0)$, $y' := f(x')$, and so on. It makes sense to write $X$ for the domain of $f$ and $Y$ for its codomain, and if we draw the ``internal diagram'' (as in \cite{LawvereSchanuel}, p.14) of the map $f$, we get this: % (find-LATEX "2010unilog-current.tex" "internal-diagram") % (find-854file "") % (find-854 "" "phys-notation") % (find-854page 9) % (find-854text 11) \def\ooo(#1,#2){\begin{picture}(0,0)\put(0,0){\oval(#1,#2)}\end{picture}} \def\oooo(#1,#2){{\setlength{\unitlength}{1ex}\ooo(#1,#2)}} \def\ctabular#1{\begin{tabular}{c}#1\end{tabular}} \def\ltabular#1{\begin{tabular}{l}#1\end{tabular}} \def\rtabular#1{\begin{tabular}{r}#1\end{tabular}} %D diagram x-to-y %D 2Dx 100 +35 +20 +20 +30 +15 +15 %D 2D 100 External \N ---> \R %D 2D +08 n |--> sn %D 2D %D 2D +20 internal n0 |--> r0 a0 |--> b0 %D 2D +08 internal n1 |--> r1 a1 |--> b1 %D 2D +08 Internal n2 |--> r2 a2 |--> b2 %D 2D +10 n. |--> r. a. |--> b. %D 2D +14 nn |--> rn an |--> bn %D 2D +08 ns |--> rs as |--> bs %D 2D %D 2D +20 stan down %D 2D %D (( External .tex= \rtabular{external\\view} y+= 4 place %D Internal .tex= \rtabular{internal\\view} place %D stan .tex= \ctabular{standard\\notation} place %D down .tex= \ctabular{downcased\\notation} place %D \N .tex= X \R .tex= Y -> .plabel= a f %D # \N .tex= \R \R -> .plabel= a f %D n .tex= x sn .tex= f(x) |-> %D n0 .tex= x_0 r0 .tex= y_0 |-> %D n1 .tex= x_1 r1 .tex= y_1 |-> %D # n2 .tex= x_2 r2 .tex= y_2 |-> %D n2 .tex= x' r2 .tex= y' |-> %D n. .tex= \vdots place r. .tex= \vdots place %D nn .tex= x_n rn .tex= y_n |-> %D n0 nn midpoint .TeX= \oooo(7,21) place %D r0 rn midpoint .TeX= \oooo(8,21) place %D %D a2 .tex= x_2 b2 .tex= y_2 |-> %D an .tex= x_n bn .tex= y_n |-> %D as .tex= x bs .tex= y |-> %D %D )) %D enddiagram %D $$\diag{x-to-y}$$ Note that for each name like $x_2$ of a point in the $x$-axis (the ``space of `$x$'s'', $X$) we have chosen a similar name for a point in the $y$-axis (the ``space of `$y$'s'', $Y$). We will call the implicit operation on names the {\sl syntactical action} of the function $f \equiv x \mto y$; in the case above, the syntactical action replaced the `$x$' of each original name into a `$y$', and kept all the ``decorations'' unchanged. The syntactical action does not need to be defined for all possible names of points in $X$ --- in fact, we restrict ourself to ``good'' names of points in $X$ exactly to make the syntactical action easier to describe. Now let's take a function less abstract: $\sqrtdot: \N \to \R$. Its action is implicit in its name (``$\sqrtdot$''), and if we examine its internal diagram, % %D diagram N-to-R %D 2Dx 100 +35 +20 +20 +30 +15 +15 %D 2D 100 External \N ---> \R %D 2D +08 n |--> sn %D 2D %D 2D +20 internal n0 |--> r0 a0 |--> b0 %D 2D +08 internal n1 |--> r1 a1 |--> b1 %D 2D +08 Internal n2 |--> r2 a2 |--> b2 %D 2D +10 n. |--> r. a. |--> b. %D 2D +14 nn |--> rn an |--> bn %D 2D +08 ns |--> rs as |--> bs %D 2D %D 2D +20 stan down %D 2D %D (( External .tex= \rtabular{external\\view} y+= 4 place %D Internal .tex= \rtabular{internal\\view} place %D stan .tex= \ctabular{standard\\notation} place %D down .tex= \ctabular{downcased\\notation} place %D \N \R -> .plabel= a \sqrt{\,·\,} %D n sn .tex= \sqrt{n} |-> %D # n0 .tex= 0 r0 .tex= \sqrt{0} |-> %D n0 .tex= 0 r0 .tex= 0 |-> %D # n1 .tex= 1 r1 .tex= \sqrt{1} |-> %D n1 .tex= 1 r1 .tex= 1 |-> %D n2 .tex= 2 r2 .tex= \sqrt{2} |-> %D n. .tex= \vdots place r. .tex= \vdots place %D nn .tex= n rn .tex= \sqrt{n} |-> %D n0 nn midpoint .TeX= \oooo(7,21) place %D r0 rn midpoint .TeX= \oooo(8,21) place %D %D a2 .tex= 2 b2 .tex= \sqrt{2} |-> %D an .tex= n bn .tex= \sqrt{n} |-> %D as .tex= n bs .tex= r |-> %D %D )) %D enddiagram %D $$\diag{N-to-R}$$ % we may conclude that it should be possible to use `$n \mto \sqrt{n}$' as its name; or even `$2 \mto \sqrt{2}$' --- ``the function that takes 2 to $\sqrt{2}$, for every value of `2'\,''... \bsk As the reader may have guessed, there is no clear separation between what are ``good names'' and ``bad names'' for an object; instead we have a murky line. We have just seen in the first example that `$x_0$', `$x'$', etc, can all be downcasings for `$X$', and maybe the `$1$' in second example, if taken as a name, should be uppercaseable both as $\N$ and as $\R$... The trick is all in our use of the dictionary: we {\sl can} define the meaning of `$n \mto \sqrt{n}$' to be $\sqrtdot:\N \to \R$, and, if we feel that $\#_\$^!$ is a good name for the square root, we can define it to stand for the square root too... % -------------------- %«parallel-notations»(to ".parallel-notations") % (sec "Parallel Notations" "parallel-notations") \mysection {Parallel Notations} {parallel-notations} We are using two notations --- downcased and standard --- in parallel; it is possible to use more. One way to visualize what is going on is to think in terms of computer interfaces. Imagine a user inspecting huge data structures by displaying them on a computer screen in several forms --- he can toggle switches that control what gets shown and what is omitted. The downcased notation of the previous sections is {\sl my} compromise between {\sl my} intuition and a formalization. Suppose that someone has created a third notation, that he claims that is much closer to {\sl his} intuitions. He can set the controls to display only his favorite notation, as in the left side of the diagram below; or he can display all together at the same time --- as at the top. % than his that is closer % % If that user has another notation, besides standard and downcased, % that is closer to his intuition than downcased types (that, after % all, are {\sl my} compromise between {\sl my} intuition and a % formalization), then he can set the controls to display only his % favorite notation, as in the left side of the diagram below; or he % can display all together at the same time --- as at the top. %D diagram int-down-std %D 2Dx 100 +40 +20 +50 +30 %D 2D 100 all %D 2D %D 2D +35 int dstd %D 2D %D 2D +45 _nt down std %D 2D %D (( all .tex= \ctabular{all"that\\together} %D int .tex= \ctabular{ineffable\\purely\\intuitive\\thought} y+= 5 x+= 10 %D dstd .tex= \foo{\FULLRP} %D down .tex= \foo{\DNC} %D std .tex= \foo{\TERMTYPERP} %D all int -> all dstd -> %D dstd down -> dstd std -> %D )) %D enddiagram %D \begin{figure} $$\def\foo#1{#1\fcded{archetypal-deriv}} \def\fooo#1{#1\fcded{archetypal=deriv}} \diag{int-down-std} $$ \caption{Parallel notations.} \label {screens} \end{figure} Working with three parallel notations is similar to working with two. \msk At this point our two notations, downcased and standard, generate {\sl trees} with exactly the same shapes; in the next section we will begin to compare {\sl diagrams} done in different notations, but having the same shapes; and starting on section \ref{hyps} the parallelism will be looser --- there will be correspondences between trees and dictionaries, on one side, and ``strictly 2-dimensional'' categorical diagrams, on another. In all cases it is convenient to work in a ``projected view'', yet pretend that we are in the situation with total information --- that the rest of the information ``is there'', but hidden. % -------------------- %«functors»(to ".functors") % (sec "Functors" "functors") \mysection {Functors} {functors} Fix a set $A$. It induces a functor $(A×)$, that takes each set $B$ to $A×B$ and each function $f:B \to C$ to a function $(A×)f:A×B \to A×C$. Let's use the subscripts `0' and `1' to distinguish the two actions of a functor: $(A×)_0$ is its action on objects (sets, in this case), $(A×)_1$ is its action on morphisms (i.e., on functions). It is quite common in the literature of Category Theory to see things like: ``let $(A×):\Set \to \Set$ the functor that takes each set $B$ to $A×B$''. The action on morphisms is not described --- it is ``obvious'', and it is left to the reader to discover. The reader should apply a kind of search algorithm to find it. Which algorithm is this? Let's downcase this problem. The action on objects takes each ``space of `$b$'s'' to a ``space of `$a,b$'s''; its syntactical action is to prepend an `$a,$'. The action on morphisms takes each $b \mto c$ to an $a,b \mto a,c$ --- i.e., the syntactical action on morphisms consists of applying the syntactical action on objects to both the domain and the codomain. {\sl This is a general pattern:} in all functors the two syntactical actions will be related in this way. % (find-854 "" "dn-functors") % (find-854page 27 "dn-functors") %D diagram functor-int-ext %D 2Dx 100 +30 +30 +30 +30 %D 2D 100 ext E0 ----> E1 %D 2D +08 E2 ----> E3 %D 2D %D 2D %D 2D +22 int I0 ----> I1 D0 ===> D1 %D 2D | | - - %D 2D | |-> | | |-> | %D 2D v v v v %D 2D +30 I2 ----> I3 D2 ===> D3 %D 2D %D 2D +20 std dnc %D 2D %D (( E0 .tex= \Set E1 .tex= \Set -> .plabel= a (A×) %D E2 .tex= B E3 .tex= A×B |-> %D ext .tex= \rtabular{external\\view} y+= 4 place %D )) %D (( I0 .tex= B I1 .tex= A×B %D I2 .tex= C I3 .tex= A×C %D int .tex= \rtabular{internal\\view} y+= 15 place %D I0 I1 |-> .plabel= a (A×)_0 %D I2 I3 |-> %D I0 I2 -> .plabel= l f %D I0 I3 harrownodes nil 20 nil |-> .plabel= a (A×)_1 %D I1 I3 -> .plabel= r (A×)f %D )) %D (( D0 .tex= b D1 .tex= a,b => %D D2 .tex= c D3 .tex= a,c => %D D0 D2 |-> D1 D3 |-> %D D0 D3 harrownodes nil 20 nil |-> %D )) %D (( std .tex= \ctabular{standard\\notation} x+= 15 place %D dnc .tex= \ctabular{downcased\\notation} x+= 15 place %D )) %D enddiagram %D % $$\diag{functor-int-ext}$$ % %\begin{figure} % $$\diag{functor-int-ext}$$ % \caption{Downcasing $(A×)$} % \label {functor-int-ext} %\end{figure} \begin{boxedfigure} \centering \subfloat[Downcasing the functor $(A×)$.]{ $\diag{functor-int-ext}$ \label{functor-int-ext} }\\ \subfloat[A way to reconstruct the ``obvious'' part.]{ $\diag{lifting-functor-1}$ \label{lifting-functor-1} } \caption{Functors.} %\label {} \end{boxedfigure} The diagram in Figure \ref{functor-int-ext} is very similar to the ones in the previous section, but there the blobs were sets and they had points; now the blobs --- which we are no longer drawing --- are categories, that have objects, and between these objects we may have {\sl morphisms}. Also, the downcasing is changing the notation more than before, and we are downcasing the `$\mto$'s that were functor actions as `$\funto$'... the `$\funto$' is to remind us that: 1) something non-obvious is going on --- points of $B$ are not being taken to points of $A×B$, instead the whole set $B$ was fed into $(A×)_0$, and we got back $A×B$ ---, and 2) that `$b \funto a,b$' is {\sl two} actions. \msk So, we know just the ``name'' of the action on morphisms of this functor. How do we reconstruct its ``meaning''? The answer is obtained by liftings, as in Figure \ref{lifting-functor-1}; we find that $(A×)f := ðp¨A×B.\ang{p,f('p)}$. %: %: b|->c %: =========(A×)_1 %: a,b|->a,c %: %: ^smashed-Axf %: %: [\arch{a,b}{p}{A×B}]^1 %: ------------------\r{'} %: [\arch{a,b}{p}{A×B}]^1 \arch{b}{'p}{B} \arch{b|->c}{f}{B->C} %: ------------------\r{} -------------------------------------\r{\app} %: \arch{a}{p}{A} \arch{c}{f('p)}{C} %: ------------------------------------------------\r{\ang,} %: \arch{a,c}{\ang{p,f('p)}}{A×C} %: --------------------------------------------------\r{ð;}1 %: \arch{a,b|->a,c}{ðp\ptype{¨(A×B)}.\ang{p,f('p)}}{A×B->A×C} %: %: ^archetypal-deriv-big %: %D diagram lifting-functor-1 %D 2Dx 100 +100 %D 2D 100 fulldnc fullterms %D 2D %D 2D +55 projected %D 2D %D (( fulldnc .tex= \DNC\fcded{archetypal-deriv-big} %D fullterms .tex= \TERMP\fcded{archetypal-deriv-big} %D projected .tex= \fcded{smashed-Axf} %D projected fulldnc --> %D fulldnc fullterms --> %D )) %D enddiagram %D % $$\diag{lifting-functor-1}$$ % %\begin{figure} % $$\diag{lifting-functor-1}$$ % \caption{Reconstructing $(A×)_1$} % \label {lifting-functor-1} %\end{figure} % -------------------- %«nts»(to ".nts") % (sec "Natural Transformations" "nts") \mysection {Natural Transformations} {nts} Now fix two sets, $A$ and $A'$, and a map $\aa: A \to A'$. We have natural constructions for functors $(A×)$ and $(A'×)$, and, besides that, a natural transformation (``NT'', from now on), $(\aa×)$, going from $(A×)$ to $(A'×)$. An NT has a {\sl single} action, that takes {\sl objects} to {\sl morphisms}. We will need a convention. If $X$ and $Y$ are objects of a category $\catC$, then both $f:X \to Y$ and $X \ton{f} Y$ will denote a morphism, but $X \to Y$ will denote the full hom-set $\Hom_\catC(X, Y)$. With that convention, if $F,G: \catA \to \catB$ are functors and $T:F \tondot G$ is a NT, we can represent the internal view of $T$ as: % $$A \mapsto (FA \ton{TA} GA).$$ Let's take the convention up one level: $A \tondot (FA \ton{TA} GA)$ will denote a specific NT, but $A \tondot (FA \to GA)$ will mean the class of all NTs from $F$ to $G$; and we downcase `$\tondot$' as `$\tnto$'; see Figures \ref{NT-alphax-int-ext} and \ref{NT-T-int-ext}. % %D diagram NT-alphax-int-ext %D 2Dx 100 +30 +30 +30 +30 %D 2D 100 E0 ----> E1 %D 2D +08 ext E2 E3 %D 2D +08 E4 ----> E5 %D 2D +08 E6 ----> E7 %D 2D %D 2D %D 2D +22 I1 D1 %D 2D |---> | ===> - %D 2D +20 int IL |-> I2 DL |-> D2 %D 2D |---> v ===> v %D 2D +20 I3 D3 %D 2D %D 2D +20 std dnc %D 2D %D (( E0 .tex= \phantom{\Set} E1 .tex= \phantom{\Set} %D E2 .tex= \Set E3 .tex= \Set %D E4 .tex= \phantom{\Set} E5 .tex= \phantom{\Set} %D E0 E1 -> sl_ .plabel= a A× %D E2 place E3 place %D E4 E5 -> sl^^ .plabel= b A'× %D E0 E1 midpoint E4 E5 midpoint -> sl_ .plabel= r \aa× %D E6 .tex= B E7 .tex= \aa×B |-> %D )) %D (( I1 .tex= A×B %D IL .tex= B I2 .tex= \phantom{O} %D I3 .tex= A'×B %D IL I1 |-> .plabel= a A× %D IL I3 |-> .plabel= b A'× %D IL I2 -> .PLABEL= ^(0.55) . %D IL I2 -> .PLABEL= _(0.55) \aa× %D I1 I3 -> .plabel= r \aa×B %D )) %D (( D1 .tex= a,b %D DL .tex= b D2 .tex= \phantom{O} %D D3 .tex= a',b %D DL D1 => %D DL D3 => %D DL D2 -> .PLABEL= ^(0.55)*%D D1 D3 |-> %D )) %D (( ext .tex= \rtabular{external\\view} y+= 5 place %D int .tex= \rtabular{internal\\view} y+= 0 place %D std .tex= \ctabular{standard\\notation} x+= 15 place %D dnc .tex= \ctabular{downcased\\notation} x+= 15 place %D )) %D enddiagram %D % \diag{NT-alphax-int-ext} %\begin{figure} % $$\diag{NT-alphax-int-ext}$$ % \caption{A natural transformation} % \label {NT-alphax-int-ext} %\end{figure} \begin{boxedfigure} \centering \subfloat[The NT $(\aa×): (A×) \tondot (A'×)$.]{ $\diag{NT-alphax-int-ext}$ \label{NT-alphax-int-ext} }\\ \subfloat[The generic case: $T: F \tondot G$.]{ $\diag{NT-T-int-ext}$ \label{NT-T-int-ext} } \caption{Natural transformations} %\label {NTs} \end{boxedfigure} We know the ``syntactical action'' of $(\aa×)$: it is $B \mto (A{×}B \ton{\aa{×}B} A'{×}B)$ in standard notation, $b \tnto (a,b \mto a',b)$ after downcasing. To obtain a ``meaning'' for that we can apply the same procedure as in the previous section; we discover that $\aa{×}B \; := \; ðp:A{×}B.\ang{f(p),'p}$. Now let's look at the notations for the general case. Let $F,G: \catA \to \catB$ be functors, and $T: F \tondot G$ be an NT between them. Everything is similar, but we need a way to downcase the objects $FA$ and $GA$... a good choice is as `$a^F$' and `$a^G$' --- because the idea of ``an $a^F$'' {\sl suggests nothing at all}, and so it reminds us that the functors $F$ and $G$ may be abstract. %D diagram NT-T-int-ext %D 2Dx 100 +30 +30 +30 +30 %D 2D 100 E0 ----> E1 %D 2D +08 ext E2 E3 %D 2D +08 E4 ----> E5 %D 2D +08 E6 ----> E7 %D 2D %D 2D %D 2D +22 I1 D1 %D 2D |---> | ===> - %D 2D +20 int IL |-> I2 DL |-> D2 %D 2D |---> v ===> v %D 2D +20 I3 D3 %D 2D %D 2D +20 std dnc %D 2D %D (( E0 .tex= \phantom{\catA} E1 .tex= \phantom{\catB} %D E2 .tex= \catA E3 .tex= \catB %D E4 .tex= \phantom{\catA} E5 .tex= \phantom{\catB} %D E0 E1 -> sl_ .plabel= a F %D E2 place E3 place %D E4 E5 -> sl^^ .plabel= b G %D E0 E1 midpoint E4 E5 midpoint -> sl_ .plabel= r T %D E6 .tex= A E7 .tex= TA |-> %D )) %D (( I1 .tex= FA %D IL .tex= A I2 .tex= \phantom{O} %D I3 .tex= GA %D IL I1 |-> .plabel= a F %D IL I3 |-> .plabel= b G %D IL I2 -> .PLABEL= ^(0.55) . %D IL I2 -> .PLABEL= _(0.55) T %D I1 I3 -> .plabel= r TA %D )) %D (( D1 .tex= a^F %D DL .tex= a D2 .tex= \phantom{O} %D D3 .tex= a^G %D DL D1 => %D DL D3 => %D DL D2 -> .PLABEL= ^(0.55)*%D D1 D3 |-> %D )) %D (( ext .tex= \rtabular{external\\view} y+= 5 place %D int .tex= \rtabular{internal\\view} y+= 0 place %D std .tex= \ctabular{standard\\notation} x+= 15 place %D dnc .tex= \ctabular{downcased\\notation} x+= 15 place %D )) %D enddiagram %D %\begin{figure} % $$\diag{NT-T-int-ext}$$ % \caption{A natural transformation (generic)} % \label {NT-T-int-ext} %\end{figure} We often have to deal with categories whose objects don't have any reasonable notion of ``elements''. If our $\catB$ is a category like that, then $a^F \mto a^G$ will be a name for a morphism, but the names `$a^F$' and `$a^G$' ``will not have semantics'' --- our dictionary will not attribute any meanings to them. See \cite{Kromer}, especially its sections 3.3.4.4 and 5.3.2.1, for a discussion; our downcased notation is, in a sense, ``a language for diagram chasing''. % -------------------- %«adjunctions»(to ".adjunctions") % (sec "Adjunctions" "adjunctions") \mysection {Adjunctions} {adjunctions} Fix an object $B$ of $\Set$, and let's write $B{\to}C$ for $C^B$. Then we have a functor $(B{\to}): \Set \to \Set$, whose syntactical action is $C \mapsto (B{\to}C)$, in standard notation, and $c \funto b \mto c$ after downcasing. This functor is right adjoint to $(×B): \Set \to \Set$, and we will represent that diagrammatically as a square: Figure \ref{adj-int-ext}. \def\cur {¯{cur}} \def\uncur{¯{uncur}} %D diagram adj-int-ext %D 2Dx 100 +35 +30 +30 +30 %D 2D 100 ext E0 ----> E1 %D # +08 E2 ----> E3 %D 2D %D 2D %D 2D +22 int I0 <---| I1 D0 <=== D1 %D 2D | | - - %D 2D | <-> | | <-> | %D 2D v v v v %D 2D +30 I2 |---> I3 D2 ===> D3 %D 2D %D 2D +20 std dnc %D 2D %D (( E0 .tex= \Set E1 .tex= \Set %D E0 E1 <- sl^ .plabel= a (×B) %D E0 E1 -> sl_ .plabel= b (B{\to}) %D )) %D (( I0 .tex= A×B I1 .tex= A %D I2 .tex= C I3 .tex= B{->}C %D I0 I1 <-| .plabel= a (×B) %D I2 I3 |-> .plabel= b (B{->}) %D I0 I2 -> .PLABEL= _(0.43) \uncur\;g %D I0 I2 -> .PLABEL= _(0.57) f %D I0 I3 harrownodes nil 20 nil <-| sl^ .plabel= a \uncur %D I0 I3 harrownodes nil 20 nil |-> sl_ .plabel= b \cur %D I1 I3 -> .PLABEL= ^(0.43) g %D I1 I3 -> .PLABEL= ^(0.57) \cur\;f %D )) %D (( D0 .tex= a,b D1 .tex= a <= %D D2 .tex= c D3 .tex= b|->c => %D D0 D2 |-> D1 D3 |-> %D D0 D3 harrownodes nil 20 nil <-> %D )) %D (( ext .tex= \rtabular{external\\view} y+= 4 place %D int .tex= \rtabular{internal\\view} y+= 15 place %D std .tex= \ctabular{standard\\notation} x+= 15 place %D dnc .tex= \ctabular{downcased\\notation} x+= 15 place %D )) %D enddiagram %D %$$\diag{adj-int-ext}$$ The two transpositions, $\cur$ and $\uncur$, are natural transformations with actions: % $$\begin{array}{lcl} (A^\op,C) \mapsto ((A{×}B \ton{f} C) \mapsto (A \ton{\cur\;f} (B{\to}C))) \\ (A^\op,C) \mapsto ((A \ton{g} (B{\to}C)) \mapsto (A{×}B \ton{\uncur\;g} C)) \\ \end{array} $$ % where $A^\op$ is an object of $\Set^\op$, and $(A^\op,C)$ is an object of $\Set^\op×\Set$. \msk The notation in the general case is similar. An adjunction $L \dashv R$ is represented diagrammatically as the square in Figure \ref{adj-gen-int-ext}. % %D diagram adj-gen-int-ext %D 2Dx 100 +35 +30 +30 +30 %D 2D 100 ext E0 ----> E1 %D # +08 E2 ----> E3 %D 2D %D 2D %D 2D +22 int I0 <---| I1 D0 <=== D1 %D 2D | | - - %D 2D | <-> | | <-> | %D 2D v v v v %D 2D +30 I2 |---> I3 D2 ===> D3 %D 2D %D 2D +20 std dnc %D 2D %D (( E0 .tex= \catB E1 .tex= \catA %D E0 E1 <- sl^ .plabel= a L %D E0 E1 -> sl_ .plabel= b R %D )) %D (( I0 .tex= LA I1 .tex= A %D I2 .tex= B I3 .tex= RB %D I0 I1 <-| .plabel= a L %D I2 I3 |-> .plabel= b R %D I0 I2 -> .PLABEL= _(0.43) g^\flat %D I0 I2 -> .PLABEL= _(0.57) f %D I0 I3 harrownodes nil 20 nil <-| sl^ .plabel= a \flat %D I0 I3 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp %D I1 I3 -> .PLABEL= ^(0.43) g %D I1 I3 -> .PLABEL= ^(0.57) f^\sharp %D )) %D (( D0 .tex= a^L D1 .tex= a <= %D D2 .tex= b D3 .tex= b^R => %D D0 D2 |-> D1 D3 |-> %D D0 D3 harrownodes nil 20 nil <-> %D )) %D (( ext .tex= \rtabular{external\\view} y+= 4 place %D int .tex= \rtabular{internal\\view} y+= 15 place %D std .tex= \ctabular{standard\\notation} x+= 15 place %D dnc .tex= \ctabular{downcased\\notation} x+= 15 place %D )) %D enddiagram %D %$$\diag{adj-gen-int-ext}$$ \begin{boxedfigure} \centering \subfloat[The adjunction $(×B) \dashv (B{\to})$.]{ $\diag{adj-int-ext}$ \label{adj-int-ext} }\\ \subfloat[Notation for a general case: $L \dashv R$.]{ $\diag{adj-gen-int-ext}$ \label{adj-gen-int-ext} } \caption{Adjunctions.} %\label {} \end{boxedfigure} \msk We will usually draw $L$ as going left, $R$ as going right, and call the transpositions `$\flat$' and `$\sharp$'. Note that in a square drawn in this way the adjunction $L \dashv R$ itself, viewed ``externally'', would be something vertical: $\begin{smallmatrix}L \\ \bot \\ R\end{smallmatrix}$ --- but its maps between hom-sets are horizontal arrows. % (which are horizontal!) % --- which are {\sl horizontal} actions, even though $L \dashv R$ % would be downwards --- \msk Just as a functor is two actions plus two properties --- namely, that the action on morphisms respects identities and composition ---, a natural isomorphism can be thought as two NTs going in opposite directions, plus the assurance that their composites are identities; the downcased squares for the $(×B) \dashv (B{\to})$ and $L \dashv R$ adjunctions in the Figures \ref{adj-int-ext} and \ref{adj-gen-int-ext} can be considered as being (two-dimensional) downcased names themselves (for natural isomorphisms), having the same meaning as their ``linearized'' versions, % $$\begin{array}{lcl} (a^\op;c) \tnto ((a,b \mto c) \bij (a \mto (b \mto c))) \\ (a^\op;b) \tnto ((a^L \mto c) \bij (a \mto b^R)) \\ \end{array} $$ % and those meanings can either be the 6-uples % $$\begin{array}{lcl} (\Set, \Set, (×B), (B{\to}), \uncur, \cur) \\ (\catA, \catB, L, R, \flat, \sharp) \\ \end{array} $$ % or longer tuples including, say, the properties and the unit and the counit of the adjunction. The possibility of changing some definitions while keeping the notations the same will be very important in sections \ref{synt-world} and \ref{formalizing-diags}, where that will be used to ``project out'' from the definitions all components which involve equalities of morphisms, keeping only the constructions. % -------------------- %«transmission»(to ".transmission") % (sec "Transmission" "transmission") \mysection {Transmission} {transmission} A good way to understand how {\sl reconstruction} works is to think on a simpler, more extreme case. When I reconstruct something that I have half-forgotten, I do have vague memories about it... how do they act? On the other hand, if I am reconstructing something that I have received from someone else in an {\sl incomplete}, but {\sl reconstructible}, form, then the vague memories are out of the picture. \msk Consider the following diagram, which describes, in a simplistic way, how a theorem $T$, discovered by an author $A$ and published in a paper $P$, is read and understood by a reader $R$. In the diagram the time flows to the left, and knowledge flows (roughly) downwards. %D diagram reconstruction %D 2Dx 100 +20 +20 +30 %D 2D 100 A_0 --------> A_2 %D 2D +08 T_1 --> T_2 %D 2D +08 T_3 %D 2D +08 P %D 2D +08 T'_0 --> T'_1 %D 2D +08 R_0 ---> R_1 %D 2D +08 %D 2D %D (( A_0 A_2 -> %D T_1 T_2 -> %D T_3 place %D P place %D T'_0 T'_1 -> %D R_0 R_1 -> %D )) %D enddiagram %D $$\diag{reconstruction}$$ The theorem was discovered in the form $T_1$, but in order to make it transmissible the author changed it a bit, and it became $T_2$, then $T_3$ in written form, which was what got published. The author was also slightly transformed in the process, and at the time of the publication he had become $A_2$. That particular theorem was difficult to state, so the reader $R$ started (as $R_0$) by understanding just parts of its statement; let's call that preliminary object understood by our reader a ``statement with holes''. Then, through weeks of study, more and more of the theorem's statement, and of the proof of the theorem (let's use the term ``theorem'' to refer to both the statement and the proof), became clear to $R$, up to the point where the object in $R$'s mind has become $T'_1$, which no longer has any holes; all gaps have been filled, the statement is now clearly a consequence of its proof, and our reader $R$, who at this point has become a slightly different person, $R_1$, now has even some {\it intuition} about the theorem (whatever that means)... Our reader $R$ has {\sl reconstructed}, in his mind, the author $A$'s theorem, from what was published in the paper $P$. $R$'s task was harder than the task I face when I try to reconstruct a theorem that at some point I knew --- if I review all that I have studied before, I {\sl should} be able to fill up all my gaps, but $R$ has no guarantee that just by looking in the literature he will be able to find all the missing knowledge he needs... even though we {\sl expect} published papers to be clear enough, and complete enough. The process of reconstruction performed by $R$ {\sl ought} to be considered an algorithm --- even though we know that what $R$ did to understand the paper $P$ was, at best, a ``method''. % Let's see why, by examining an ideal case. % Let's treat an ideal case. Suppose that the $A$ wanted to be clear, that he was lucid in his choice of exposition, and that the paper $P$ was submitted to a journal with no space constraints. So $A$, and also his editors and referees, {\sl want} the paper $P$ to be as readable as possible. The reader $R_0$ receives the paper $P$ being aware that the theorem $T_3$ in it should be readable, and starts to devote his time to understand $T_3$. After a few weeks $R$ succeeds. {\sl What did the reader $R$ do?} And what did $A$ and the journal's editors do to be sure that $A$ would succeed in his task? When $R$ checks the paper's details and fills up the gaps his process is akin to {\sl proof search}, and thus a kind of {\sl lifting}... What $R$ does is too complex to be formalizable as an ``algorithm''; yet the author and the editors are aware of what their intended readers are expected to be able to do, and they added to the paper enough ``hints'' to let the readers succeed --- so the reader performs a ``proof search with hints''. There are algorithms that do proof searches with hints, so let's commit an abuse of language here and take the analogy with algorithms seriously: the reader $R$ is performing a proof search with hints, and $A$ provided enough hints in the paper $P$ to be sure that, given $P$ as input, the reader $R$ will check its theorems completing all the missing details, then stop. % There's more, though. Let's now suppose that both $A$ and $R$ are people whose thinking is mostly diagrammatical, like the semi-fictional ``me''. How does does $R$ (re)con\-struct in his mind some ``intuition'' about the theorems? The theorem $T_3$ was published in algebraic form, so part of $R$'s task --- and he needs to do this to be able to fill the logical gaps --- is to find the diagrams to let him reason about the paper; another part of his task is to work out the details in the paper's examples; for that he needs to take his ``general'' diagrams and apply them to particular cases; this is {\sl specialization}, as in Section \ref{projs-and-lifts}. What we call ``intuition'' should comprise the ability to specialize, plus a lot more. % (find-kopkadaly4page (+ 12 607) "Index") % (find-kopkadaly4page (+ 12 637) "\\ref") % (find-kopkadaly4page (+ 12 615) "cross-reference") % (find-kopkadaly4page (+ 12 56) "cross-reference") % (find-kopkadaly4page (+ 12 213) "cross-reference") % (find-kopkadaly4text) % synthetic form % -------------------- %«intuition»(to ".intuition") % (sec "Intuition" "intuition") \mysection {Intuition} {intuition} When $R$ finally understands the paper $P$ he would have developed some ``intuitions'' about the theorem $T$. His intuitions may or may not be the same as $A$'s, so let's name them differently: $I_A$ for the author's intuitions, $I_R$ for the reader's. Instead of taking the easy way and saying that ``it is impossible to talk about what mathematical intuition is'', we will improvise a simple model that will let us talk about {\sl some aspects} of having intuition about a theorem. Let's suppose that that theorem $T$ says that when the hypotheses $H_1$ and $H_2$ hold, then the conclusion $C_2$ also does; and the proof of $T$ is made of two lemmas, $L_1$ and $L_2$, and structured like this: % $$\ded{int-full}$$ % so the stronger theorem $H_1 \land H_2 \vdash C_1 \land C_2$ is also true. Note that the tree above represents $T'_1$, not $T_3$; $T_3$ was written in a ``linear'', ``algebraic'' way, to comply with the usual mathematical practice, even though both $A$ and $R$ tend to think diagrammatically. The reader $R_1$ is able to do several things with $T'_1$; most of them can be understood diagrammatically, as movements through parts of the diagram below. Let's use the following convention (that will hold for this diagram only): a double bar with the name of a lemma at its right will stand for {\sl all the steps in the lemma} --- they are known, but are not visible ---, while a double bar without a label will mean a situation where the intermediate steps are not known at that moment, and will have to be reconstructed. %: %: %: H_1 H_1 H_1\subs %: ===L_1 === ========L_1 %: H_1 C_1 H_2 C_1 H_2 C_1\subs H_2\subs %: ===L_1 ===========L_2 =========== =====================L_2 %: C_1 C_2 C_2 C_2\subs %: %: ^int-1p ^int-full ^int-struct ^int-subs %: %D diagram intuition %D 2Dx 100 +45 +90 %D 2D 100 full %D 2D %D 2D +50 firstpart struct subs %D 2D %D 2D +40 H1|-C1 H1H2|-C2 H1H2|-C2[Set] %D 2D %D (( full .tex= \fcded{int-full} BOX %D firstpart .tex= \fcded{int-1p} BOX %D struct .tex= \fcded{int-struct} BOX %D subs .tex= \fcded{int-subs} BOX %D H1|-C1 .tex= \fbox{$H_1|-C_1$} BOX %D H1H2|-C2 .tex= \fbox{$H_1,H_2|-C_2$} BOX %D H1H2|-C2[Set] .tex= \fbox{$H_1[\catC{:}{=}\Set],H_2[\catC{:}{=}\Set]|-C_2[\catC{:}{=}\Set]$} BOX %D full firstpart -> .plabel= l (1) %D full struct -> .plabel= r (2) %D full subs -> .plabel= r (3) %D firstpart H1|-C1 -> .plabel= r (4) %D struct H1H2|-C2 -> .plabel= r (5) %D subs H1H2|-C2[Set] -> .plabel= r (6) %D )) %D enddiagram %D $$\def\subs{[\catC:=\Set]} \diag{intuition} $$ The center box is a sketch of the full proof, and the small box below it is the statement of the full theorem. If the reader $R_1$ remembers any of those, he can reconstruct the other one by projecting or lifting through (5). The box at the top is the full proof, and $R_1$ can reconstruct it by completing the sketch of the proof, lifting through (2). One day $R_1$ decides to present the theorem to some colleagues. He assigns a temporal order to the lemmas: ``Lemma $L_1$ has to be presented first''. Its statement and its proof are obtained by projecting through (1) and (4). Note that (1) is a case of {\sl zooming in} into a part of the proof. $R_1$ is also able to {\sl use} the theorem. He can apply it to a particular case, projecting through (3) and (6) or just through (3) (compare that with the arrow (3) in Figure \ref{Fib}). He can also reuse the {\sl structure} of parts of the proof, but changing the theorem in deeper ways (e.g., in the Curry-Howard isomorphism); this is not shown above. We will pretend that ``having intuition about a theorem'' means having the abilities discussed above: remembering parts, reconstructing, zooming out, zooming it, temporal order, transmission, specializing, reusing the structure. % -------------------- %«skeletons»(to ".skeletons") % (sec "Skeletons of proofs" "skeletons") \mysection {Skeletons of proofs} {skeletons} Let's call the ``projected'' version of a mathematical object its ``skeleton''. The underlying idea in this paper is that for the {\sl right kinds} of projections, and for {\sl some kinds} of mathetical objects, it should be possible to reconstruct enough of the original object from its skeleton and few extra clues --- just like paleontologists can reconstruct from a fossil skeleton the look of an animal when it was alive. Now the irresistible questions are: which kinds of objects do have skeletons? What do these skeletons look like? How does the reconstruction process work, and how much of it can be performed by computers? When is it that the liftings become ambiguous, what kinds of hints are needed, and how should we specify them? And in what situations is this idea doomed to fail, because for each non-trivial way of separating the object's data into ``skeleton'' and ``non-skeleton'' something doesn't work? Answering all this in a general setting is obviously a daunting task. A first natural step, though, is to start from a handful of natural examples --- and then say: these are our archetypal examples of skeletons, projections, and liftings. How do we formalize and generalize what we got here? In Section \ref{synt-world} we will sketch an approach that {\sl may} yield a reasonbably rich family of examples: namely, that on a sizeable fragment of Category Theory all definitions can be split into a {\sl structure} part plus {\sl properties}, and each theorem into a {\sl construction} plus an {\sl equational part}. A big part of Mathematics is definitions plus theorems --- and in that fragment of Category Theory these can be clearly split into a ``syntactical'' skeleton, with just the ``structures'' and ``constructions'', plus, on top of that, a reconstructible, ``equational'' flesh. We will call the system with just this skeleton the ``syntactical world''. It would be very hard to explain precisely the general ideas here before first showing a language on which they can make sense, so we will now look at some examples. We will have to use hyperdoctrines, even though they are weaker, less familiar, and harder to define than toposes; that's because of technical difficulties that we will discuss in section \ref{prob-with-toposes}. % -------------------- %«hyps»(to ".hyps") % (sec "Hyperdoctrines" "hyps") \mysection {Hyperdoctrines} {hyps} Let's take the {\sl beginning} of the definition of a hyperdoctrine (\cite{LawvereAdjFo}, \cite{LawvereEqHyp}, \cite{SeelyBeck}, \cite{TaylorPhDThesis}, \cite{Jacobs}). A hyperdoctrine is a cloven fibration $p:\bbE \to \bbB$, where the ``base category'' $\bbB$ has finite products and each fiber $\bbE_B$ is cartesian closed, plus for each morphism $f:A \to B$ in $\bbB$ adjoints $Æ_f \dashv f^* \dashv å_f$ for the change-of-base functor $f^*$, {\sl plus more structure}; but let's skip the ``plus more structure'' part for the moment --- we will describe that extra structure briefly at Section \ref{pres-frob-bcc}, and the full details can be found at \cite{OchsUniLog}. It turns out that this definition {\sl generalizes} a familiar object: the ``co\-domain fibration'', $\Cod: \Setmto \to \Set$ --- that we will abbreviate as $\Pred$ --- is a hyperdoctrine. Actually $\Pred$ can be considered to be the {\sl archetypical} hyperdoctrine, in a sense that can be made precise; we will return to ``generalizations'' and ``archetypes'' in Section \ref{archetypal}. An object $P$ of $\Setmto$ is a monic: $P \equiv (A' \monicto A)$. A morphism $P \to Q$ in $\Setmto$, where $Q \equiv (B' \monicto B)$, is a pair of arrows $(f':A' \to B', f:A \to B)$ making the obvious square commute. The projection functor $\Cod$ takes $P \equiv (A' \monicto A)$ to $A$ and $(f',f):P \to Q$ to $f$. A monic with codomain $A$, $(A' \monicto A)$, is said to be a {\sl subobject} of $A$. In $\Set$ we have {\sl canonical subobjects} --- the ones whose maps are inclusions --- and we can think of them as being {\sl predicates} over sets. We will have a special shorthand for predicates: instead of writing, for example, % $$\sst{(x,y)ÝX×Y}{P(x,y)} \ito X×Y$$ % we will write just: % $$\ssst{x,y}{Pxy}$$ % The double bar in `$\ssst{x,y}{Pxy}$' is to remind us that this is two objects, plus a map; and we write the `$\monicto$' as `$\ito$' when we want to stress that the map is an inclusion. \msk We will draw objects of $\bbE$ above their projections, and we'll usually omit the projection arrows. We will downcase a predicate like `$\ssst{x,y}{Pxy}$' in diagrams as just `$P(x,y)$' --- the `$x,y$' part can be recovered by looking down. Let's focus on what happens in $\Pred$. For a map $f: A \to B$ in $\bbB$, the change-of-base functor $f^*$ takes each predicate $\ssst{b}{P(b)}$ over $B$ to a predicate $\ssst{a}{P(f(a))}$ over $A$. When $f$ is a projection map, like $:X×Y \to X$, the adjoints $Æ_$ and $å_$ ``are'' $Îy$ and $ýy$ (Figure \ref{3-pi}); when $f$ is the ``diagonal'' map $\DD:B \to B×B$ or the ``dependent diagonal'' $\dd:A×B \to A×B×B$, the adjoints ``are'' the operations `$b{=}b'∧$' and `$b{=}b'⊃$' (Figure \ref{3-dd}). This is not hard to believe if we start with the right examples, and we check first the particular cases and then generalize. Take $X=\{0,1,2,3,4\}$, $Y=\{3,4\}$, $A=\{0\}$, $B=\{0,1,2,3\}$, and let's use a positional notation for predicates: we will write $\ssst{x,y}{x \ge y}$ as $\sm{00001\\00011}$, i.e.: $$\def\pr#1{#1} \def\ph#1{\phantom{#1}} \def\dmat#1#2{ \sm{ \pr{\{}#1\pr{,}\ph{\}}\\ \ph{\{}#2\pr{\}}\ph{,}\\ }} % \dmat{\ph{(0,4),(1,4),(2,4),(3,4),}\pr{(4,4)}} {\ph{(0,3),(1,3),(2,3),}\pr{(3,3),(4,3)}} % \;\ito\;\, % \dmat{\pr{(0,4),(1,4),(2,4),(3,4),}\pr{(4,4)}} {\pr{(0,3),(1,3),(2,3),}\pr{(3,3),(4,3)}} $$ % (find-angg ".emacs.papers" "jacobs") % (find-jacobspage (+ 19 43) "fibration of monos") % (find-books "__cats/__cats.el" "lambek-scott") % (find-lambekscottpage (+ 8 200) "Toposes with canonical subobjects") % (find-angg ".emacs.papers" "taylor") % (find-paultaylorthesispage (+ 11 84) "hyperdoctrine") %D diagram 3-pi %D 2Dx 100 +30 +30 +30 +30 +30 %D 2D 100 A0 A1 B0 B1 C0 C1 %D 2D %D 2D +20 A2 A3 B2 B3 C2 C3 %D 2D %D 2D +20 A4 A5 B4 B5 C4 C5 %D 2D %D 2D +20 A6 A7 B6 B7 C6 C7 %D 2D %D (( A0 .tex= P A1 .tex= Æ_P %D A2 .tex= ^*Q A3 .tex= Q %D A4 .tex= R A5 .tex= å_R %D A6 .tex= X×Y A7 .tex= X %D )) %D (( B0 .tex= Pxy B1 .tex= Îy.Pxy %D B2 .tex= Qx B3 .tex= Qx %D B4 .tex= Rxy B5 .tex= ýy.Rxy %D B6 .tex= x,y B7 .tex= x %D )) %D (( C0 .tex= \sm{00001\\00011} C1 .tex= \sm{00011} %D C2 .tex= \sm{00111\\00111} C3 .tex= \sm{00111} %D C4 .tex= \sm{01111\\11111} C5 .tex= \sm{01111} %D C6 .tex= X×Y C7 .tex= X %D )) %D (( A0 A1 A2 A3 A4 A5 A6 A7 %D @ 0 @ 1 |-> @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <-> %D @ 2 @ 3 <-| @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <-> %D @ 4 @ 5 |-> @ 6 @ 7 -> .plabel= a \pi %D )) %D (( B0 B1 B2 B3 B4 B5 B6 B7 %D @ 0 @ 1 => @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <-> %D @ 2 @ 3 <= @ 2 @ 4 |-> @ 3 @ 5 |-> @ 2 @ 5 harrownodes nil 20 nil <-> %D @ 4 @ 5 => @ 6 @ 7 |-> .plabel= a \pi %D )) %D (( C0 C1 C2 C3 C4 C5 C6 C7 %D @ 0 @ 1 |-> @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <-> %D @ 2 @ 3 <-| @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <-> %D @ 4 @ 5 |-> @ 6 @ 7 -> .plabel= a \pi %D )) %D enddiagram %D %$$\diag{3-pi}$$ %D diagram 3-dd %D 2Dx 100 +30 +30 +30 +30 +30 %D 2D 100 A0 A1 B0 B1 C0 C1 %D 2D %D 2D +30 A2 A3 B2 B3 C2 C3 %D 2D %D 2D +30 A4 A5 B4 B5 C4 C5 %D 2D %D 2D +20 A6 A7 B6 B7 C6 C7 %D 2D %D (( A0 .tex= P A1 .tex= Æ_P %D A2 .tex= ^*Q A3 .tex= Q %D A4 .tex= R A5 .tex= å_R %D A6 .tex= A×B A7 .tex= A×B×B -> .plabel= a \dd %D )) %D (( B0 .tex= Pab B1 .tex= b=b'∧Pab %D B2 .tex= Qabb B3 .tex= Qabb' %D B4 .tex= Rab B5 .tex= b=b'⊃Rab %D B6 .tex= a,b B7 .tex= a,b,b' |-> .plabel= a b':=b %D )) %D (( C0 .tex= \dsm1000 C1 .tex= \sm{0001\\0000\\0000\\0000} %D C2 .tex= \dsm1100 C3 .tex= \sm{0011\\0011\\0011\\0000} %D C4 .tex= \dsm1110 C5 .tex= \sm{1111\\1111\\1111\\0111} %D C6 .tex= A×B C7 .tex= A×B×B -> .plabel= a \dd %D )) %D (( A0 A1 A2 A3 A4 A5 A6 A7 %D @ 0 @ 1 |-> @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <-> %D @ 2 @ 3 <-| @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <-> %D @ 4 @ 5 |-> %D )) %D (( B0 B1 B2 B3 B4 B5 B6 B7 %D @ 0 @ 1 => @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <-> %D @ 2 @ 3 <= @ 2 @ 4 |-> @ 3 @ 5 |-> @ 2 @ 5 harrownodes nil 20 nil <-> %D @ 4 @ 5 => %D )) %D (( C0 C1 C2 C3 C4 C5 C6 C7 %D @ 0 @ 1 |-> @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <-> %D @ 2 @ 3 <-| @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <-> %D @ 4 @ 5 |-> %D )) %D enddiagram %D %$$\def¨{\phantom{0}} % \def\dsm#1#2#3#4{\sm{¨¨¨#1\\¨¨#2¨\\¨#3¨¨\\#4¨¨¨}} % \diag{3-dd} %$$ \msk \begin{boxedfigure} \centering \subfloat[Adjoints to $\pi^*$ (quantifiers).]{ $\diag{3-pi}$ \label{3-pi} }\\ \subfloat[Adjoints to $\dd^*$ (equality).]{ $\def¨{\phantom{0}} \def\dsm#1#2#3#4{\sm{¨¨¨#1\\¨¨#2¨\\¨#3¨¨\\#4¨¨¨}} \diag{3-dd}$ \label{3-dd} }\\ \subfloat[Adjoints to an arbitrary change-of-base functor.]{ $\phantom{make it wider} \diag{adjs-to-DD*-sst} \phantom{make it wider} $ \label{adjs-to-DD*-sst} } \caption{Adjoints to change-of-base in a hyperdoctrine.} \label {adjoints-to-cob} \end{boxedfigure} \begin{figure} $$\def\fibrationbox{\fbox{\ltabular{ A fibration $p:\bbE \to \bbB$ \\ plus for each $f:A \to B$ in $\bbB$ \\ adjoints $Æ_f \dashv f^* \dashv å_f$ \\ }}} \diag{adjoints-to-cob} $$ \caption{How the hyperdoctrine diagrams in Figure \ref{adjoints-to-cob} were obtained.} \label {Fib} \end{figure} In Figures \ref{3-pi} and \ref{3-dd} the left side shows the abstract view, the right side shows a very particular case, and in the middle, in downcased notation, we see how these change-of-base functors and their adjoints act on arbitrary predicates. % Also, each arrow `$\bij$' in an adjunction square stands for two transpositions, one in each direction. Let's establish another convention: $P \to f^*Q$ is an hom-set, but $P \vdash f^*Q$ is (the name of) a morphism --- we have $P \vdash f^*Q : P \to f^*Q$. With that convention we can write the transpositions rules (cf.\ the ``mate rules'' in \cite{Jacobs}) as: %: %: Q|-å_R x;Qx|-ýy.Rxy %: -------ý^\flat ------------ý^\flat %: ^*Q|-R x,y;Qx|-Rxy %: %: ^Fa-flat-std ^Fa-flat-dnc %: %: ^*Q|-R x,y;Qx|-Rxy %: -------ý^\sharp ------------ý^\sharp %: Q|-å_R x;Qx|-ýy.Rxy %: %: ^Fa-sharp-std ^Fa-sharp-dnc %: $$\ded{Fa-flat-std} \qquad \ded{Fa-flat-dnc}$$ $$\ded{Fa-sharp-std} \qquad \ded{Fa-sharp-dnc}$$ Note that `$\vdash$' has different meanings in standard and in downcased notations. We will only use `$\vdash$' to refer to vertical morphisms. \msk It turns out that it is possible to {\sl define} the adjoints $Æ_f \dashv f^* \dashv å_f$ in $\Pred$, for an arbitrary $f: A \to B$, from just $f^*$, $Æ_$, $å_$, $Æ_$, $å_$. % % :*=*=*%:*∧*∧*%:*⊃*⊃*% %D diagram adjs-to-DD*-sst %D 2Dx 100 +65 %D 2D 100 P ====> ÆP %D 2D - - %D 2D | <-> | %D 2D v v %D 2D +25 Q* <=== Q %D 2D - - %D 2D | <-> | %D 2D v v %D 2D +25 R ====> åR %D 2D %D 2D +20 A |---> B %D 2D %D (( P .tex= \ssst{a,b}{Pab} ÆP .tex= \ssst{a,b,b'}{b=b'∧Pab} %D Q* .tex= \ssst{a,b}{Qabb} Q .tex= \ssst{a,b,b'}{Qabb'} %D R .tex= \ssst{a,b}{Qab} åR .tex= \ssst{a,b,b'}{b=b'⊃Pab} %D A .tex= A×B B .tex= A×B×B %D )) %D (( P .tex= \ssst{a}{P(a)} ÆP .tex= \ssst{b}{Îa.f(a)=b∧P(a)} %D Q* .tex= \ssst{a}{Q(f(a))} Q .tex= \ssst{b}{Q(b)} %D R .tex= \ssst{a}{R(a)} åR .tex= \ssst{b}{ýa.f(a)=b⊃R(a)} %D A .tex= A B .tex= B %D )) %D (( P ÆP |-> %D P Q* -> ÆP Q -> P Q harrownodes nil 20 nil <-> %D Q* Q <-| %D Q* R -> Q åR -> Q* åR harrownodes nil 20 nil <-> %D R åR |-> %D A B -> .plabel= a f %D )) %D enddiagram %D %$$\diag{adjs-to-DD*-sst} %$$ % %:*=*{=}*%:*∧*{∧}*%:*⊃*{⊃}*% The transpositions and the functor actions implicit in the adjunction diagram in Figure \ref{adjs-to-DD*-sst} above can be expressed as derived rules. The proof is hard (see \cite{SeelyBeck}); we will see how to understand it diagrammatically in \cite{OchsUniLog}. \bsk What really matters here is: how were the diagrams above obtained? Look at Figure \ref{Fib}; it shows some of the projections involved. We start with the definition in English, at the top. By representing it diagrammatically (projection (1)) we lose the subtleties of the English language --- see \cite{Freyd76} and \cite{FreydScedrov} for a diagrammatic notation in which at least the quantifiers are preserved --- but we add positional notation. The projections (3) and (4) are specializations: we take $\bbE := \Setito$, $p := \Cod$, $A:=X×Y$, and so on. The arrows (2) and (5) produce internal diagrams, as in the section \ref{adjunctions}. The downcased diagrams are not shown; Figure \ref{Fib} is a map of interesting projections, and it could have been far larger than it is. %D diagram 5-algebraic-internal %D 2Dx 100 +35 %D 2D 100 P ====> ÆP %D 2D - - %D 2D | <-> | %D 2D v v %D 2D +20 Q* <=== Q %D 2D - - %D 2D | <-> | %D 2D v v %D 2D +20 R ====> åR %D 2D %D 2D +15 A |---> B %D 2D %D (( P .tex= P ÆP .tex= Æ_fP %D Q* .tex= f^*Q Q .tex= Q %D R .tex= R åR .tex= å_fR %D A .tex= A B .tex= B %D )) %D (( P ÆP |-> %D P Q* -> ÆP Q -> P Q harrownodes nil 20 nil <-> %D Q* Q <-| %D Q* R -> Q åR -> Q* åR harrownodes nil 20 nil <-> %D R åR |-> %D A B -> .plabel= a f %D )) %D enddiagram %D % $$\diag{5-algebraic-internal}$$ % %D diagram 5-set-binary %D 2Dx 100 +35 %D 2D 100 P ====> ÆP %D 2D - - %D 2D | <-> | %D 2D v v %D 2D +20 Q* <=== Q %D 2D - - %D 2D | <-> | %D 2D v v %D 2D +20 R ====> åR %D 2D %D 2D +15 A |---> B %D 2D %D (( P .tex= \sm{00001\\00011} ÆP .tex= \sm{00011} %D Q* .tex= \sm{00111\\00111} Q .tex= \sm{00111} %D R .tex= \sm{01111\\11111} åR .tex= \sm{01111} %D A .tex= X×Y B .tex= X %D )) %D (( P ÆP |-> %D P Q* -> ÆP Q -> P Q harrownodes nil 20 nil <-> %D Q* Q <-| %D Q* R -> Q åR -> Q* åR harrownodes nil 20 nil <-> %D R åR |-> %D A B -> .plabel= a \pi %D )) %D enddiagram %D % $$\diag{5-set-binary}$$ % %D diagram 5-algebraic-external %D 2Dx 100 +25 +40 %D 2D 100 \bbE \bbE_A \bbE_B %D 2D %D 2D +35 \bbB A B %D 2D %D (( \bbE_A \bbE_B %D @ 0 @ 1 -> .slide= 13pt .plabel= a Æ_f %D @ 0 @ 1 <- .plabel= m f^* %D @ 0 @ 1 -> .slide= -13pt .plabel= b å_f %D @ 0 @ 1 midpoint y+= -5 .TeX= \text{\tiny$®$} place %D @ 0 @ 1 midpoint y+= 5 .TeX= \text{\tiny$®$} place %D )) %D (( \bbE \bbB -> .plabel= l p %D A B -> .plabel= a f %D )) %D enddiagram %D % $$\diag{5-algebraic-external}$$ % %D diagram 5-set-external %D 2Dx 100 +25 +40 %D 2D 100 \bbE \bbE_A \bbE_B %D 2D %D 2D +35 \bbB A B %D 2D %D (( \bbE_A .tex= \Setito_{X×Y} \bbE_B .tex= \Setito_X %D @ 0 @ 1 -> .slide= 13pt .plabel= a Æ_\pi %D @ 0 @ 1 <- .plabel= m \pi^* %D @ 0 @ 1 -> .slide= -13pt .plabel= b å_\pi %D @ 0 @ 1 midpoint y+= -5 .TeX= \text{\tiny$®$} place %D @ 0 @ 1 midpoint y+= 5 .TeX= \text{\tiny$®$} place %D )) %D (( \bbE .tex= \Setito \bbB .tex= \Set -> .plabel= l \Cod %D A .tex= X×Y B .tex= X -> .plabel= a \pi %D )) %D enddiagram %D % $$\diag{5-set-external}$$ % %D diagram adjoints-to-cob %D 2Dx 100 +95 %D 2D 100 text %D 2D %D 2D +60 EAEB PQR %D 2D %D 2D +85 EXYEX binary %D 2D %D (( %D text .tex= \fibrationbox BOX place %D EAEB .tex= \fdiag{5-algebraic-external} BOX place %D EXYEX .tex= \fdiag{5-set-external} BOX place %D PQR .tex= \fdiag{5-algebraic-internal} BOX place %D binary .tex= \fdiag{5-set-binary} BOX place %D text EAEB -> .plabel= l (1) %D EAEB PQR -> .plabel= a (2) %D EAEB EXYEX -> .plabel= l (3) %D PQR binary -> .plabel= r (4) %D EXYEX binary -> .plabel= a (5) %D )) %D enddiagram %D % $$\diag{adjoints-to-cob}$$ % -------------------- %«pres-frob-bcc»(to ".pres-frob-bcc") % (sec "Preservations, Frobenius, Beck-Chevalley" "pres-frob-bcc") \mysection {Preservations, Frobenius, Beck-Chevalley} {pres-frob-bcc} The complete definition of a hyperdoctrine is what we have seen in the last section, plus these {\sl properties}:*each $f^*$ preserves, modulo iso, the $§$, the $∧$, and the $⊃$ of each fiber;*the Frobenius Property holds,*the Beck-Chevalley Condition holds. We can regard these properties as {\sl structure}. They can all be stated in the same way: for $f:A \to B$ in $\bbB$ and for predicates $P$ and $Q$ over $B$, we have natural constructions $\Ptruenat$, $\Pandnat$, $\Pimpnat$, $\Frobnat$, that produce arrows that we want to be isos; so we establish rules $\Ptrue$, $\Pand$, $\Pimp$, $\Frob$, that produce arrows going in the opposite directions of the previous ones. %: %: f:A->B f:A->B %: ===========\Ptruenat -----------\Ptrue %: f^*§_B|-§_A §_A|-f^*§_B %: %: ^Ptruenat-short-std ^Ptrue-std %: %: f P Q f P Q %: ===================\Pandnat -------------------\Pand %: f^*(P∧Q)|-f^*P∧f^*Q f^*P∧f^*Q|-f^*(P∧Q) %: %: ^Pandnat-short-std ^Pand-std %: %: f Q R f Q R %: ===================\Pimpnat -------------------\Pimp %: f^*P∧f^*Q|-f^*(Q⊃R) f^*(Q⊃R)|-f^*P⊃f^*Q %: %: ^Pimpnat-short-std ^Pimp-std %: %: %: f P Q f P Q %: =====================\Frobnat ---------------------\Frob %: Æ_f(P∧f^*Q)|-(Æ_fP)∧Q Æ_f(P∧f^*Q)|-(Æ_fP)∧Q %: %: ^Frobnat-short-std ^Frob-std %: $$\ded{Ptruenat-short-std} \qquad \ded{Ptrue-std}$$ $$\ded{Pandnat-short-std} \qquad \ded{Pand-std}$$ $$\ded{Pimpnat-short-std} \qquad \ded{Pimp-std}$$ $$\ded{Frobnat-short-std} \qquad \ded{Frob-std}$$ \msk The natural construction for the $\Frobnat$ arrow is given by the diagram below. Note that it shows both $\Frobnat$ (going rightwards, shortened to just `$\nat$') and $\Frob$: % % (find-854 "" "frobenius") % (find-854 "" "frobenius" "diagram Frob-std") % (find-854page 80 "Frobenius") % %D diagram Frob-std %D 2Dx 100 +45 +35 +10 +30 %D 2D 100 B0 ================> B1 %D 2D ^ ^ ^ %D 2D | / | %D 2D - \ - %D 2D +20 B2 ========> B3 <--> B3' %D 2D - / - %D 2D | \ | %D 2D v v v %D 2D +20 B4 <================ B5 %D 2D %D 2D +15 b0 |---------------> b1 %D 2D %D (( B0 .tex= P B1 .tex= Æ_fP %D B2 .tex= P&f^*Q B3 .tex= Æ_f(P&f^*Q) B3' .tex= (Æ_fP)&Q %D B4 .tex= f^*Q B5 .tex= Q %D b0 .tex= A b1 .tex= B %D )) %D (( %D B0 B1 |-> B2 B0 -> B3 B1 -> B3' B1 -> %D B4 B5 <-| B2 B4 -> B3 B5 -> B3' B5 -> %D B2 B3 |-> B3 B3' -> sl^ .plabel= a \nat B3 B3' <- sl_ .plabel= b \Frob %D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |-> %D B2 B4 midpoint B3 B5 midpoint harrownodes nil 20 nil |-> %D )) %D (( b0 b1 -> .plabel= a f %D )) %D enddiagram % $$\diag{Frob-std}$$ Similarly to what we have done in the section \ref{dictionary}, we can extract from the diagram above a dictionary defining some names in terms of the others; note that due to our conventions $P{∧}f^*Q \to P$ is a hom-set, but $P{∧}f^*Q \vdash P$ is a particular morphism, and we can treat it as a name. By expanding the definitions in $Æ_f(P{\land}f^*Q) \vdash (Æ_fP){\land}Q$, we obtain a definition for the $\Frobnat$ rule: %: %: f Q f Q %: ---\cob -----\cob %: P f^*Q P f^*Q %: --------- ------------' %: P∧f^*Q|-P f P∧f^*Q|-f^*Q %: -----------------Æ_f --------------{Æ_f}^\flat %: Æ_f(P∧f^*Q)|-Æ_fP Æ_f(P∧f^*Q)|-Q %: -------------------------------------\ang{,} %: Æ_f(P∧f^*Q)|-(Æ_fP)∧Q %: %: ^Frobnat-std %: $$\begin{array}{l} \ded{Frobnat-short-std} \quad := \\ \\ \phantom{OO} \ded{Frobnat-std} \\ \end{array} $$ The diagram also says that the arrow generated by the $\Frob$ rule is inverse to the arrow generated by the (derived) rule $\Frobnat$. This is by a convention: in a `$\leftrightarrows$' the two arrows are the two directions of an iso. % (find-854 "" "frobenius") % (find-854 "" "frobenius" "diagram Frob-std") % (find-854page 80 "Frobenius") \msk The statement of the Beck-Chevalley Condition (``BCC'' from now on) is slightly more complex: it requires four arrows in $\bbB$. For any commutative square in $\bbB$ as below, % %D diagram BCCL-std %D 2Dx 100 +45 +55 +45 %D 2D 100 B0 <====================== B1 %D 2D -\\ -\\ %D 2D | \\ | \\ %D 2D v \\ v \\ %D 2D +20 B2 <\\> B2' ============== B3 \\ %D 2D /\ \/ /\ \/ %D 2D +15 \\ B4 \\ B5 %D 2D \\ - \\ - %D 2D \\ | \\| %D 2D \\v \v %D 2D +20 B6 <===================== B7 %D 2D %D 2D +10 b0 |---------------------> b1 %D 2D |-> |-> %D 2D +35 b2 |--------------------> b3 %D 2D %D (( %D B0 .tex= f^{\prime*}P B1 .tex= P %D B2 .tex= z^{\prime*}f^*Æ_zP B2' .tex= f^{\prime*}z^*Æ_zP B3 .tex= z^*Æ_zP %D B4 .tex= Æ_{z'}f^{\prime*}P B5 .tex= Æ_zP %D B6 .tex= f^*Æ_zP B7 .tex= Æ_zP %D B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-| %D B0 B4 |-> B1 B5 |-> %D B2 B6 <-| B3 B7 <-| %D B6 B7 <-| B5 B7 -> .plabel= r \id %D B4 B6 -> sl_ .plabel= l î B4 B6 <- sl^ .plabel= r \BCCL %D B0 B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-| %D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |-> %D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-| %D )) %D (( b0 .tex= X×_{Y}Z b1 .tex= Z b2 .tex= X b3 .tex= Y %D b0 b1 -> .plabel= b f' %D b0 b2 -> .plabel= l z' %D b1 b3 -> .plabel= r z %D b2 b3 -> .plabel= a f %D b0 relplace 20 7 \pbsymbol{7} %D )) %D enddiagram % $$\diag{BCCL-std}$$ % and any object $P$ over $Z$, we have a natural construction for an arrow: % $$\BCCLnat: Æ_{z'} f^{\prime*} P \to f^* Æ_z P$$ The rule $\BCCL$ says that when $f$, $f'$, $z$, $z'$ form a pullback the arrow $\BCCLnat$ has an inverse, $\BCCL$: %: %: f z f' z' P %: ---------------\BCCL %: f^*Æ_zP|-Æ_{z'}f^{\prime*}P %: %: ^BCCL-rule %: $$\ded{BCCL-rule}$$ We will sometimes write $\BCCLnat$ and $\BCCL$ together as an iso, and call that iso $\BCCL$ (by a slight abuse of language); and we simplify the diagram for Beck-Chevalley by drawing only its square in $\bbB$ and on top of it the two faces of the cube in $\bbE$ that border on the missing edge. We will sometimes draw the arrows generated by $\Ptrue$, $\Pand$, $\Pimp$ and $\Frob$ as isos, too. % Beck-Chevalley (for the left adjoint to $f^*$): % -------------------- %«eq-elim»(to ".eq-elim") % (sec "The Eq-Elim rule" "eq-elim") \mysection {The Eq-Elim rule} {eq-elim} % (find-angg ".emacs.papers" "jacobs") % (find-jacobspage (+ 19 179) "replacement") The main interest of hyperdoctrines is that they are exactly the categories in which we can interpret (a certain system of typed, intuitionistic) first-order logic. The proof of this includes a way to interpret each deduction rule of first-order logic categorically, and another ``translation'' going in the opposite direction. Let's look at a tiny part --- possibly the hardest one --- of these translations. \msk The rule for equality-elimination in Natural Deduction can be formulated as this (\cite{SeelyBeck}, p.507): %: %: b=b' Qabb %: ---=I -----------=E %: b=b Qabb' %: %: ^=I ^=E %: $$\ded{=E}$$ Categorically, it will become this morphism (we will call it $\EqE$): % $$\ssst{a,b,b'}{b{=}b'{∧}Qabb} \vdash \ssst{a,b,b'}{Qabb'}$$ There are three different natural constructions in a hyperdoctrine for objects deserving the name $\ssst{a,b,b'}{b{=}b'{∧}Qabb}$. We will use this one in $\EqE$: %: %: \DD \ssst{b}{§} \dd \ssst{a,b,b'}{Qabb'} %: ----------------Æ_0 -------------------------\cob %: \opip \ssst{b,b'}{b=b'} \opi \ssst{a,b}{Qabb} %: ------------------------\cob -----------------------\cob %: \ssst{a,b,b'}{b=b'} \ssst{a,b,b'}{Qabb} %: ---------------------------------------------------{∧} %: \ssst{a,b,b'}{b=b'∧Qabb} %: %: ^=E-domain-pred %: %: %: b|->b,b' \ssst{b}{§} a,b|->a,b,b' \ssst{a,b,b'}{Qabb'} %: ----------------Æ_0 -------------------------\cob %: a,b,b'|->b,b' \ssst{b,b'}{b=b'} a,b,b'|->a,b \ssst{a,b}{Qabb} %: --------------------------\cob -----------------------\cob %: \ssst{a,b,b'}{b=b'} \ssst{a,b,b'}{Qabb'} %: ---------------------------------------------------{∧} %: \ssst{a,b,b'}{b=b'∧Qabb'} %: %: ^=E-domain-pred %: %: %: \DD \TB \dd Q %: --------Æ_0 ------\cob %: \opip Æ_\DD\TB \opi \dd^*Q %: ---------------\cob --------------\cob %: \opipstar"Æ_\DD\TB \opistar\dd^*Q %: -------------------------------------{∧} %: \opipstar"Æ_\DD\TB∧\opistar\dd^*Q %: %: ^=E-domain-std %: $$\thinmtos \footnotesize \ded{=E-domain-pred}$$ $$\ded{=E-domain-std}$$ Note that $\opi:A{×}B{×}B \to A{×}B$ is the projection on the first two coordinates, and $\opip:A{×}B{×}B \to B{×}B$ the projection on the last two coordinates. To show that the rule $\EqE$ can be interpreted in a hyperdoctrine we need a way to construct, for arbitrary objects $A$, $B$ in the base category and an arbitrary predicate $Q$ over $A{×}B{×}B$, a morphism $\EqEdomwide \vdash Q$. We will construct it as a composite of three maps. % Let $f := \opip:A×B×B \to B×B$ be the projection on the two last % coordinates, and Take $P := \TB = \ssst{b}{§}$, $f:=\opistar$, $z:=\DD$, $z':=$, $f':=\pi'$ in the diagram for Beck-Chevalley. Then the $\BCCL$ iso says that {\sl two} different categorical constructions for $\ssst{a,b,b'}{b=b'}$ are isomorphic, and by drawing also the $\Ptrue$ iso and its image by $Æ_\dd$ we get isos between the {\sl three} different categorical constructions for $\ssst{a,b,b'}{b=b'}$: %D diagram eq-simpl-std %D 2Dx 100 +40 +50 %D 2D PT %D 2D 100 E0 <-> E1 <--| E2 %D 2D - - - - %D 2D | | | | %D 2D v v v | %D 2D +30 E3 <-> E4 | %D 2D ^ ^ | %D 2D \ |BCC | %D 2D v v v %D 2D +20 E5 <--| E6 %D 2D %D 2D +15 B0 ---> B1 %D 2D | _| | %D 2D | | %D 2D v v %D 2D +30 B2 ---> B3 %D 2D %D (( E0 .tex= \TAB E1 .tex= \pipstar\TB E2 .tex= \TB %D E3 .tex= Æ_\TAB E4 .tex= Æ_\pipstar\TB %D E5 .tex= \opipstarÆ_\DD\TB E6 .tex= Æ_\DD\TB %D E0 E1 <-> .plabel= a \Ptrue E1 E2 <-| %D E0 E3 |-> E1 E4 |-> E2 E6 |-> E0 E4 varrownodes nil 17 nil |-> %D E3 E4 <-> %D E3 E5 <-> .plabel= l i E4 E5 <-> .plabel= r \BCCL %D E5 E6 <-| %D )) %D (( B0 .tex= A×B B1 .tex= B %D B2 .tex= A×B×B B3 .tex= B×B %D @ 0 @ 1 -> .plabel= b \pip %D @ 0 @ 2 -> .plabel= l \dd @ 1 @ 3 -> .plabel= r \DD %D @ 2 @ 3 -> .plabel= b \opip %D @ 0 relplace 7 7 \pbsymbol{7} %D )) %D enddiagram %D %D diagram eq-simpl-dnc %D 2Dx 100 +30 +45 %D 2D PT %D 2D 100 E0 <-> E1 <--| E2 %D 2D - - - - %D 2D | | | | %D 2D v v v | %D 2D +30 E3 <-> E4 | %D 2D ^ ^ | %D 2D \ |BCCL | %D 2D v v v %D 2D +20 E5 <--| E6 %D 2D %D 2D +15 B0 ---> B1 %D 2D | _| | %D 2D | | %D 2D v v %D 2D +30 B2 ---> B3 %D 2D %D (( E0 .tex= § E1 .tex= § E2 .tex= § %D E3 .tex= b=b' E4 .tex= b=b' %D E5 .tex= b=b' E6 .tex= b=b' %D E0 E1 <-> .plabel= a \Ptrue E1 E2 <= %D E0 E3 => E1 E4 => E2 E6 => E0 E4 varrownodes nil 17 nil |-> %D E3 E4 <-> %D E3 E5 <-> .plabel= l i E4 E5 <-> .plabel= r \BCCL %D E5 E6 <= %D )) %D (( B0 .tex= a,b B1 .tex= b %D B2 .tex= a,b,b' B3 .tex= b,b' %D @ 0 @ 1 |-> .plabel= b \pip %D @ 0 @ 2 |-> .plabel= l \dd @ 1 @ 3 |-> .plabel= r \DD %D @ 2 @ 3 |-> .plabel= b \opip %D @ 0 relplace 7 7 \pbsymbol{7} %D )) %D enddiagram %D %$$\diag{eq-simpl-std} % \qquad % \diag{eq-simpl-dnc} %$$ \begin{boxedfigure} \centering \subfloat[The components `$\Frob'$' and $\ee_Q$ of the $({=}E)$ map (standard)]{ $\def\TAB{§\!_{A×B}} \def\f{} \def\g{{\ov}} \diag{Frob-5} $ \label{Frob=E-std} }\\ \subfloat[The components `$\Frob'$' and $\ee_Q$ of the $({=}E)$ map (downcased)]{ $\def\TAB{§\!_{A×B}} \def\f{} \def\g{{\ov}} \diag{Frob-5-dnc} $ \label{Frob=E-dnc} } \caption{$({=}E)$ via Frobenius} \label {=E-via-frobenius} \end{boxedfigure} \begin{boxedfigure} \centering \subfloat[The iso `$i$' used to build $({=}E)$ (standard)]{ $\diag{eq-simpl-std}$ \label{eq-simpl-std} } \!\!\!\!\!\!\!\!\!\!%\!\!\!\!\!\!\!\! \subfloat[The iso `$i$' used to build $({=}E)$ (downcased)]{ $\diag{eq-simpl-dnc}$ \label{eq-simpl-dnc} }\\ \subfloat[The map $({=}E)$ as a composite]{ $\diag{EqE-as-composite}$ \label{EqE-as-composite} } \caption{$({=}E)$ as a composite} %\label {} \end{boxedfigure} Now look at the diagram in Figure \ref{Frob=E-std}. The arrow $\Frob^{\prime\nat}$ (going rightwards, shortened to $\nat$) is built in the same way as $\Frobnat$, but using the maps $!$ and $\cong$ in place of $$ and $'$. In any fibration we have natural isos $f^*g^*P \bij (f;g)^*P$ and $\id^*P \bij P$ (for {\sl diagrammatic} proofs for that, see \cite{OchsUniLog}), and as $;\opi=\id$, this gives us the map $\cong$. The arrow $\Frob'$ is the inverse of $\Frob^{\prime\nat}$; its construction (not shown) is an easy consequence of Frobenius. The map $_Q$ is a counit for the adjunction $Æ_ \dashv ^*$. %D diagram Frob-5 %D 2Dx 100 +30 +50 +40 %D 2D 100 E0 ================> E1 %D 2D ^ ^ ^ %D 2D | / | %D 2D - \ - %D 2D +25 E2 ========> E3 <--> E3' %D 2D - / - %D 2D | \ | %D 2D v v v %D 2D +25 E4 <================ E5 <=== E6 %D 2D %D 2D +15 S2 ========> S3 <--> S3' %D 2D - / - %D 2D | \ | %D 2D v v v %D 2D +25 S4 <================ S5 %D 2D %D 2D +15 B0 |---------------> B1 <--- B2 %D 2D %D (( E0 .tex= \TAB E1 .tex= Æ_\f\TAB %D E2 .tex= \f^*Q E3 .tex= Æ_\f\f^*Q E3' .tex= (Æ_\f\TAB)&\g^*\f^*Q %D E4 .tex= \f^*\g^*(\f^*Q) E5 .tex= \g^*\f^*Q E6 .tex= \f^*Q %D %D S2 .tex= \f^*Q S3 .tex= Æ_\f\f^*Q S3' .tex= (Æ_\f\TAB)&\g^*\f^*Q %D S4 .tex= \f^*Q S5 .tex= Q %D %D B0 .tex= A×B B1 .tex= A×B×B B2 .tex= A×B %D )) %D (( E0 E1 |-> %D E2 E0 -> E3 E1 -> E3' E1 -> %D # E2 E3 |-> E3 E3' <-> %D E2 E3 |-> E3 E3' -> sl^ .PLABEL= ^(0.40) \nat %D E3 E3' <- sl_ .PLABEL= _(0.43) \Frob' %D E2 E4 -> .plabel= l \cong E3 E5 -> E3' E5 -> %D E4 E5 <-| E5 E6 <-| %D E0 E2 midpoint E1 E3 midpoint harrownodes nil 20 nil |-> %D E2 E4 midpoint E3 E5 midpoint harrownodes nil 20 nil |-> %D )) %D (( # S0 S1 |-> %D # S2 S0 -> S3 S1 -> S3' S1 -> %D # S2 S3 |-> S3 S3' <-> %D S2 S3 |-> # S3 S3' -> sl^ .PLABEL= ^(0.40) \nat %D # S3 S3' <- sl_ .PLABEL= _(0.43) \Frob_5 %D S2 S4 -> .plabel= l \id S3 S5 -> .plabel= a \ee_Q # S3' S5 -> %D S4 S5 <-| # S5 S6 <-| %D # S0 S2 midpoint S1 S3 midpoint harrownodes nil 20 nil |-> %D S2 S4 midpoint S3 S5 midpoint harrownodes nil 20 nil |-> %D %D # S3 S3' <- .plabel= a \Frob' S3' S5 --> .plabel= r =E'_Q %D )) %D (( B0 B1 -> .plabel= a \f %D B1 B2 -> .plabel= a \g %D B0 B2 -> sl__ .plabel= b \id %D )) %D enddiagram % %\begin{figure} % $$\def\TAB{§\!_{A×B}} % \def\f{} % \def\g{{\ov}} % \diag{Frob-5} % $$ % \caption{$({=}E)$ via Frobenius (standard)} % % \caption{$b{=}b',Qabb \vdash Qabb'$ via Frobenius (standard)} % \label {Frob=E-std} %\end{figure} If $Q \equiv \ssst{a,b,b'}{Qabb'}$ then we can downcase the diagram above into the one in Figure \ref{Frob=E-dnc}; the arrow $\EqE$ is the composite in Figure \ref{EqE-as-composite}. %D diagram Frob-5-dnc %D 2Dx 100 +40 +45 +40 %D 2D 100 E0 ================> E1 %D 2D ^ ^ ^ %D 2D | / | %D 2D - \ - %D 2D +25 E2 ========> E3 <--> E3' %D 2D - / - %D 2D | \ | %D 2D v v v %D 2D +25 E4 <================ E5 <=== E6 %D 2D %D 2D +15 S2 ========> S3 <--> S3' %D 2D - / - %D 2D | \ | %D 2D v v v %D 2D +25 S4 <================ S5 %D 2D %D 2D +15 B0 |---------------> B1 <--- B2 %D 2D %D (( E0 .tex= § E1 .tex= b=b' %D E2 .tex= Qabb E3 .tex= b=b'∧Qabb E3' .tex= b=b'∧Qabb %D E4 .tex= Qabb E5 .tex= Qabb E6 .tex= Qabb %D %D S2 .tex= Qabb S3 .tex= b=b'∧Qabb S3' .tex= b=b'∧Qabb %D S4 .tex= Qabb S5 .tex= Qabb' %D %D B0 .tex= a,b B1 .tex= a,b,b' B2 .tex= a,b %D )) %D (( E0 E1 => %D E2 E0 |-> E3 E1 |-> E3' E1 |-> %D # E2 E3 => E3 E3' <-> %D E2 E3 => E3 E3' |-> sl^ .PLABEL= ^(0.50) \nat %D E3 E3' <-| sl_ .PLABEL= _(0.50) \Frob' %D E2 E4 <-> .plabel= l \cong E3 E5 |-> E3' E5 |-> %D E4 E5 <= E5 E6 <= %D E0 E2 midpoint E1 E3 midpoint harrownodes nil 20 nil |-> %D E2 E4 midpoint E3 E5 midpoint harrownodes nil 20 nil |-> %D )) %D (( S2 S3 => # S3 S3' |-> sl^ .PLABEL= ^(0.40) \nat %D # S3 S3' <-| sl_ .PLABEL= _(0.43) \Frob_5 %D S2 S4 |-> .plabel= l \id S3 S5 |-> .plabel= a \ee_Q # S3' S5 |-> %D S4 S5 <= # S5 S6 <= %D S2 S4 midpoint S3 S5 midpoint harrownodes nil 20 nil |-> %D %D # S3 S3' <-| .plabel= a \Frob' S3' S5 |--> .plabel= r =E'_Q %D )) %D (( B0 B1 |-> .plabel= a b':=b %D B1 B2 |-> # .plabel= a \g %D B0 B2 |-> sl__ .plabel= b \id %D )) %D enddiagram % %\begin{figure} % $$\def\TAB{§\!_{A×B}} % \def\f{} % \def\g{{\ov}} % \diag{Frob-5-dnc} % $$ % \caption{$=E$ via Frobenius (downcased)} % \label {Frob=E-dnc} %\end{figure} % %D diagram EqE-as-composite %D 2Dx 100 +55 +55 +50 %D 2D 100 A0 A1 B0 B1 %D 2D %D 2D +30 A2 A3 B2 B3 %D 2D %D (( A2 x+= 30 %D A3 x+= 30 %D B2 x+= 30 %D B3 x+= 30 %D )) %D (( A0 .tex= Æ_^*Q A1 .tex= (Æ_\TAB)∧\opistar^*Q %D A2 .tex= Q A3 .tex= \EqEdomthin %D A0 A1 <-> .plabel= a \Frob' %D A0 A2 -> .PLABEL= _(0.43) _Q A1 A3 <-> .PLABEL= ^(0.60) i×\opistar^*Q %D A2 A3 <-- .plabel= b \EqE %D )) %D (( B0 .tex= b=b'∧Qabb %D B1 .tex= b=b'∧Qabb %D B2 .tex= Qabb' %D B3 .tex= b=b'∧Qabb %D B0 B1 <-> %D B0 B2 |-> B1 B3 <-> %D B2 B3 <--| .plabel= b \EqE %D )) %D enddiagram %D %\begin{figure} % $$\diag{EqE-as-composite}$$ % \caption{$({=}E)$ as a composite} % \label {EqE-as-composite} %\end{figure} % -------------------- %«archetypal»(to ".archetypal") % (sec "Archetypal Models" "archetypal") \mysection {Archetypal Models} {archetypal} Imagine that we have placed side to side the downcased and the standard diagrams of the last section. When we go from downcased to standard --- e.g, from $\ssst{a,b}{b{=}b'∧Qabb}$ to $Æ_^*Q$ --- we are attributing a precise meaning to a (potentially ambiguous) ``name''; however, when we go in the opposite direction, from standard to downcased, we are ``attributing meaning'' in another sense: we are giving an ``intuitive meaning'' (or better: ``intuitive content'') to something that, if we had received it in an article, as in the section \ref{transmission}, could have felt initially as something purely abstract... I had to make some ``informal definitions'' in the course of this paper, using terms that I could not define precisely, like {\sl diagrammatical reasoning}, {\sl reconstruction}, and {\sl intuition}... I will have to make a few more. \begin{quote} % (Informal) definition. The {\sl archetypal model} for a structure --- for example, the archetypal model for a hyperdoctrine, which is going to be $\Pred$ --- is {\sl a particular case of that structure that ``suggests'' a certain ``language'' for working on that structure} --- i.e., for doing constructions and proofs on it. \end{quote} That ``archetypical language'' does not need to be unambiguous --- think in $\ssst{a,b}{b{=}b'∧Qabb}$ and its several different precise meanings ---, does not need to have a downcased version --- in section \ref{hyps} the internal diagrams were what mattered, the downcasings were mentioned just in passing ---, and does not need to be convenient for expressing {\sl all} possible constructions. What is relevant is that the archetypical language, {\sl when used side-to-side with the ``algebraic'' language}, should give us a way to reason, both {\sl intuitively} and {\sl precisely}, about the structure we're working on; in particular, it should let us formulate reasonable conjectures quickly, and check them with reasonable ease... but what are ``reasonable conjectures'', and where do they come from? If we want to be able to reconstruct a theory from minimal information we need to have ways to: 1) generate ``reasonable conjectures'', 2) filter out those which are either impossible or too hard to prove, 3) prove the others. {\sl Bounded} proof search takes care of points (1) and (2); to give a partial answer to (1) we will concentrate our attention on Category Theory --- more specifically, on situations where we are trying to generalize a ``base case''. There we have two (non-disjoint) sources of ``reasonable conjectures'': 1a) constructions and proofs that make sense and hold in the base case, that we may expect to generalize; 1b) {\sl language}. Our choice of names for objects in a hyperdoctrine gave us several different formal meanings for $\ssst{a,b}{b{=}b'∧Qabb}$ --- we expect them to be at least equivalent modulo isomorphism. This is similar to writing $a+b+c$ instead of $a+(b+c)$ or $(a+b)+c$: our choice of language ``suggests'' that $a+(b+c) = (a+b)+c$. An ``archetypal example'', in which all the main ideas appear, is: \begin{quote} $\Set$ is the archetypical CCC. \end{quote} % -------------------- %«CCCs»(to ".CCCs") % (sec "Cartesian Closed Categories" "CCCs") \mysection {Cartesian Closed Categories} {CCCs} % (find-854 "" "CCCs") % (find-854 "" "CCCs") % (find-854page 43 "CCCs") % (find-854 "" "lambda-calc-in-a-hyp") % (find-854page 87 "lambda-calc-in-a-hyp") % Here is a well-know example --- maybe even the ``archetypical % example'' for our method. A {\sl Cartesian Closed Category} $(\catC, ×, 1, \to)$ is a category $\catC$ plus a ``cartesian closed structure'' $(×, 1, \to)$ on it. The following diagram fixes the (categorical) notation that we will use for the operations induced by $(×, 1, \to)$: %D diagram CCC-1 %D 2Dx 100 +30 +30 +25 +30 +30 %D 2D 100 P0 T0 E0 E1 %D 2D %D 2D +30 P1 P2 P3 T1 E2 E3 %D 2D %D (( P0 .tex= A P1 .tex= B P2 .tex= B×C P3 .tex= C %D P0 P1 -> .plabel= a f %D P0 P2 -> .plabel= m \ang{f,g} %D P0 P3 -> .plabel= a g %D P1 P2 <- .plabel= b \pi %D P2 P3 -> .plabel= b \pi' %D )) %D (( T0 .tex= A T1 .tex= 1 -> .plabel= r ! %D )) %D (( E0 .tex= A×B E1 .tex= A %D E2 .tex= C E3 .tex= B{->}C %D E0 E1 <-| %D E0 E2 -> .PLABEL= _(0.43) \uncur"g %D E0 E2 -> .PLABEL= _(0.57) f %D E1 E3 -> .PLABEL= ^(0.43) g %D E1 E3 -> .PLABEL= ^(0.57) \cur"f %D E0 E3 harrownodes nil 20 nil <-| sl^ %D E0 E3 harrownodes nil 20 nil |-> sl_ %D E2 E3 |-> %D )) %D enddiagram %D $$\diag{CCC-1}$$ Each of its three parts can be attributed a precise meaning, as we did with the adjunction square in section \ref{adjunctions}; and if we regard each of them as a different adjunction (see \cite{Awodey}, pages 182 and 188, for the three adjunctions), then we get the equations that these operations have to obey. \msk The Big Theorem is: {\sl CCCs are exactly the categorical models for the simply-typed $ð$-calculus with pairs and unit}. \msk The precise, ``standard'' statement for that theorem, including definitions, statements, and proofs, is quite long. Amazingly, it can be reconstructed from just this downcased diagram, % (find-854 "" "lambda-calc-in-a-hyp") %D diagram CCC-1-dnc %D 2Dx 100 +30 +30 +25 +30 +30 %D 2D 100 P0 T0 E0 E1 %D 2D %D 2D +30 P1 P2 P3 T1 E2 E3 %D 2D %D (( P0 .tex= a P1 .tex= b P2 .tex= b,c P3 .tex= c %D P0 P1 |-> %D P0 P2 |-> %D P0 P3 |-> %D P1 P2 <-| %D P2 P3 |-> %D )) %D (( T0 .tex= a T1 .tex= * |-> %D )) %D (( E0 .tex= a,b E1 .tex= a %D E2 .tex= c E3 .tex= b|->c %D E0 E1 <= %D E0 E2 |-> %D E1 E3 |-> %D E0 E3 harrownodes nil 20 nil <-> %D E2 E3 => %D )) %D enddiagram %D $$\diag{CCC-1-dnc}$$ % plus this downcasing of the Natural Deduction rules for $∧$, $§$, and $⊃$: %: %: a a %: : : %: b c b,c b,c %: ----\ang{,} --- ---' %: b,c b c %: %: ^HLD-1 ^HLD-2 ^HLD-3 %: %: a %: -! %: * %: %: ^HLD-4 %: %: a a a [b]^1 %: : : :::: %: b b|->c c %: ---------\app -----ð;1 %: c b|->c %: %: ^HLD-5 ^HLD-6 %: $$\begin{array}{cccc} \ded{HLD-1} & \ded{HLD-2} \quad \ded{HLD-3} \\ \\ \ded{HLD-4} \\ \\ \ded{HLD-5} & \ded{HLD-6} \\ \end{array} $$ Starting from that, we uppercase the downcased diagram in the following way, that makes clear how an intermediate, ``sequent-like'' form (as in \cite{LambekScott}, pp.47--49), should behave: % % (find-books "__cats/__cats.el" "lambek-scott") % (find-lambekscottpage (+ 8 47) "1. Propositional calculus as a deductive system") % %D diagram CCC-HL2 %D 2Dx 100 +30 +30 +25 +30 +30 +35 %D 2D 100 P0 T0 E0 E1 E0' %D 2D %D 2D +30 P1 P2 P3 T1 E2 E3 E2' %D 2D %D (( P0 .tex= A P1 .tex= B P2 .tex= B{×}C P3 .tex= C %D P0 P1 -> .plabel= a a|-b %D P0 P2 -> .plabel= m a|-\ang{b,c} %D P0 P3 -> .plabel= a a|-c %D P1 P2 <- .plabel= b p|-p %D P2 P3 -> .plabel= b p|-p' %D )) %D (( T0 .tex= A T1 .tex= 1 -> .plabel= l a|-* %D )) % %D (( E0' .tex= (B{->}C){×}B E2' .tex= C % %D E0' E2' -> .plabel= c \ev_{BC} % %D )) %D (( E0 .tex= A×B E1 .tex= A %D E2 .tex= C E3 .tex= B{->}C %D E0 E1 <-| %D E0 E2 -> .PLABEL= _(0.43) a,b|-fb %D E0 E2 -> .PLABEL= _(0.57) a,b|-c %D E1 E3 -> .PLABEL= ^(0.43) a|-f %D E1 E3 -> .PLABEL= ^(0.57) a|-ðb¨B.c %D E0 E3 harrownodes nil 20 nil <-| sl^ %D E0 E3 harrownodes nil 20 nil |-> sl_ %D E2 E3 |-> %D )) %D enddiagram %D $$\diag{CCC-HL2}$$ % Then the next steps are to state precisely:*the syntax and the rules of the type system,*the operations of a CCC,*the translation of each of the rules of the type system,*the translation of each of the operations of the CCC,*the reductions and conversions of the type system,*the equations obeyed by the operations of a CCC, \noindent and then we have to prove that the CCC equations are respected by the translation to $ð$-calculus, and that the $ð$-calculus equations are respected by the translation to categories. We also need to allow ``impurities'' in both the $ð$-calculus and in the CCCs. Take a look at the CCC of the next section: it has extra {\sl constants} --- an object $A$ and morphisms $\corn0$, $\corn1$, $+$, $·$ --- that do not exist in all CCCs, and these constants obey certain {\sl equations}. In a {\sl Pure Type System} (\cite{GeuversPhD}) extra constants and equations are not allowed, but in theorems like the Big Theorem above (\cite{Jacobs} has many more like it) we allow in the type system exactly the kinds of constants and equations that are easy to interpret in the categorical models. The kinds of allowed ``impurities'' are usually defined in the beginning, in the definition of the type system and of the categorical structure, but this can be delayed until after the translations are presented. % (find-books "__cats/__cats.el" "awodey") % -------------------- %«olts»(to ".olts") % (sec "Objects of Line Type" "olts") \mysection {Objects of Line Type} {olts} Our approach also works in cases where we do have an archetypical language with clear intuitive content, but where we have no concrete archetypical model besides a term model built purely syntactically. Through this section let's pretend that we do not know Synthetic Differential Geometry (\cite{Kock81}, \cite{BellSIA}, \cite{MoeRey}). \msk Let $(A, \corn0, \corn1, +, ·)$ be a commutative ring in a CCC. That means: we have a diagram % %D diagram ring-object %D 2Dx 100 +35 +35 %D 2D 100 A0 ====> A1 <============== A2 %D 2D %D 2D +20 a0 |---> b0 %D 2D +6 a1 |---> b1 %D 2D +6 b2 <-------------| c2 %D 2D +6 b3 <-------------| c3 %D 2D %D (( A0 .tex= 1 A1 .tex= A A2 .tex= A×A %D a0 .tex= * b0 .tex= 0 %D a1 .tex= * b1 .tex= 1 %D b2 .tex= a+b c2 .tex= a,b %D b3 .tex= ab c3 .tex= a,b %D )) %D (( A0 A1 -> sl^ .plabel= a \corn0 %D A0 A1 -> sl_ .plabel= b \corn1 %D A1 A2 <- sl^ .plabel= a + %D A1 A2 <- sl_ .plabel= b · %D a0 b0 |-> %D a1 b1 |-> %D b2 c2 <-| %D b3 c3 <-| %D )) %D enddiagram %D $$\diag{ring-object}$$ % and the morphisms $\corn0$, $\corn1$, $+$, $·$ behave as expected. Let $D$ be the set of zero-square infinitesimals of $A$, i.e., $\sst{ÝA}{^2=0}$; $D$ can be defined categorically as an equalizer. If we take $A:=\R$, then $D=\{0\}$; but if we let $A$ be a ring with nilpotent infinitesimals, then $\{0\} \subsetneq A$. % Our notation will suggest that we are in $\R$, though. \msk The main theorem of \cite{Kock77} says that if the map % $$\begin{array}{rrcl} \aa: & A×A & \to & (D{\to}A) \\ & (a,b) & \mto & ð¨D.(a+b) \\ \end{array} $$ % is invertible, then we can use $\aa$ and $\aa³$ to {\sl define} the derivative of maps from $A$ to $A$ --- {\sl every} morphism $f: A \to A$ in the category $\catC$ will be ``differentiable'' ---, and the resulting differentiation operation $f \mapsto f'$ behaves as expected: we have, for example, $(fg)'=f'g+fg'$ and $(f¢g)' = (f'¢g)g'$. Commutative rings with the property that their map $\aa$ is invertible are called {\sl ring objects of line type}. ROLTs are hard to construct, so most of the proofs about them have to be done in a very abstract setting. However, if we can use the following downcasings for $\aa$ and $\aa³$ --- note that $\bb=(\aa³;)$, that $\cc=(\aa³;')$, and that these notations do not make immediately obvious that $\aa$ and $\aa³$ are inverses ---, % %D diagram aa-and-aa-inverse %D 2Dx 100 +30 +30 +15 +40 +40 %D 2D 100 A0 <-- A1 --> A2 b0 <-- b1 --> b2 %D 2D ^ |^ ^ ^ |^ ^ %D 2D \ || / \ || / %D 2D \ v| / \ v| / %D 2D +30 A3 b3 %D 2D %D 2D +15 B0 <-- B1 --> B2 C0 <-- C1 --> C2 %D 2D ^ |^ ^ ^ |^ ^ %D 2D \ || / \ || / %D 2D \ v| / \ v| / %D 2D +30 B3 C3 %D 2D %D (( A0 .tex= A A1 .tex= A×A A2 .tex= A %D A3 .tex= (D{->}A) %D @ 0 @ 1 <- .plabel= a %D @ 1 @ 2 -> .plabel= a ' %D @ 0 @ 3 <- .plabel= l \bb # \sm{\bb\;:=\\\aa³;} %D @ 1 @ 3 -> sl_ .PLABEL= _(0.42) \aa %D @ 1 @ 3 <- sl^ .PLABEL= ^(0.38) \aa³ %D @ 2 @ 3 <- .plabel= r \cc %D )) %D (( B0 .tex= a B1 .tex= a,b B2 .tex= b %D B3 .tex= (\mapsto"a+b) %D @ 0 @ 1 <-| .plabel= a %D @ 1 @ 2 |-> .plabel= a ' %D @ 0 @ 3 <-| .plabel= l \bb %D @ 1 @ 3 |-> .PLABEL= _(0.43) \aa %D @ 2 @ 3 <-| .plabel= r \cc %D )) %D (( C0 .tex= f(0) C1 .tex= (f(0),f'(0)) C2 .tex= f'(0) %D C3 .tex= (\mapsto"f()) %D @ 0 @ 1 <-| .plabel= a %D @ 1 @ 2 |-> .plabel= a ' %D @ 0 @ 3 <-| .plabel= l \bb %D @ 1 @ 3 <-| .PLABEL= ^(0.43) \aa³ %D @ 2 @ 3 <-| .plabel= r \cc %D )) %D enddiagram %D $$\diag{aa-and-aa-inverse}$$ % then all the proofs in the first two sections of \cite{Kock77} can be reconstructed from half-diagrammatic, half-$ð$-calculus-style proofs, done in the archetypal language, where the intuitive content is clear. This will be shown in a sequel to \cite{OchsUniLog}. % -------------------- %«synt-world»(to ".synt-world") % (sec "The syntactical world" "synt-world") \mysection {The syntactical world} {synt-world} We can now explain our archetypal projection: the one from the ``real world'' to the ``syntactical world'' for a fragment of Category Theory, that we mentioned in section \ref{skeletons}. We have been avoiding all mentions to equations between morphisms --- for example, in the section \ref{adjunctions} we glossed over the usual standard requirement that $f^{\sharp\flat} = f$. That was deliberate. % (find-854 "" "abstract") \msk A category $\catC$ is a 7-uple, % $$\catC = (\catC_0, \Hom_\catC, \id_\catC, ¢_\catC; \assoc_\catC, \idL_\catC, \idR_\catC)$$ % where the three last components are assurances that the composition $¢_\catC$ is associative and that the identities behave as expected with respect to composition at the left and the right. These three last components are exactly the ones whose typings --- all this can be formalized in an adequate type system --- involve equalities of morphisms. By dropping them we get what we will call the {\sl proto-category} associated to $\catC$: % $$\catC^- = (\catC_0, \Hom_\catC, \id_\catC, ¢_\catC)$$ % The same idea can be applied to lots of categorical structures. We can define, in a similar way, proto-functors, proto-natural transformations, proto-isos, proto-adjunctions, proto-products, proto-terminals, proto-exponentials, proto-cartesian-closed categories, a proto-Yoneda lemma, proto-fibrations, and so on. Also, it turns out that many categorical proofs can be projected onto their corresponding ``proto-proofs'', by dropping all parts that involve equalities of morphisms --- and the resulting proto-proofs keep the {\it constructions} of the original proofs, but leave out the diagram chasings. This is explained in great detail, with many diagrams, at \cite{OchsUniLog}. % [\url{http://angg.twu.net/math-b.html\#unilog-2010}]. % -------------------- %«prob-with-toposes»(to ".prob-with-toposes") % (sec "The problem with toposes" "prob-with-toposes") \mysection {The problem with toposes} {prob-with-toposes} {\sl Elementary toposes} are very simple to define --- an elementary topos is just a CCC with pullbacks and a classifier object --- and it is well-known that they are exactly the categorical models for a certain (intuitionistic) fragment of Set Theory (called ``IST'' in \cite{BellLST}). {\sl Why did we have to resort to clumsy hyperdoctrines?} % What are our reasons for using hyperdoctrines instead? The problem is that we can't define {\sl classifier object} without defining {\sl monic arrow} first; all my attempts to find a usable definition of ``proto-monic'' have failed rather miserably\footnote{The reader who doesn't believe that this can be hard is urged to try to find the syntactical skeleton of the proof that in a topos every singleton map $\setof{·}_A : A \to \Omega^A$ is monic.}, so I can't rely on either ``proto-classifiers'' or ``proto-toposes''. This means that if I had to stick with toposes I wouldn't be able to apply the idea of ``projection into the syntactical world'' to the metatheory, i.e., to the categorical models for the polymorphic type theory needed to formalize the projection from the real world into the syntactical world. \msk The usual approach to interpreting IST in a topos is to use the classifier object to define the logical connectives and the quantifiers, and then check that these definitions have all the expected properties. An alternative approach is to split this into two parts: 1) a classifier on a CCC with pullbacks induces a hyperdoctrine structure on it, and 2) the hyperdoctrine structure is {\sl exactly} what is needed to interpret first-order logic with equality. This is how things are done in \cite{Jacobs}, which then proceeds to show which extra structure is needed for interpreting polymorphism and dependent types... These are beautiful but hard theorems, whose details are not as widely-known as they should; what I felt was missing the most when I learned them was a way to make their intuitive content clearer. The tools in this paper {\sl can} be a way to fill that gap --- the next section sketches what that could mean. % [***Todo: explain that the classifier object in a topos induces a % hyperdoctrine structure on the underlying CCC, and it is that % structure which is needed for interpreting first-order logic with % equality there; the details are not as well-known as they should, % and to add polymorphism we need to add extra structure which is % even less familiar. I believe that these and other results in % categorical semantics can become much more accessible with the use % of diagrams in a downcased language, as in the sections \ref{hyps} % and \ref{olts}; the diagrams for these semantics, translations, % and their computer implementations are high-priority future work.] % -------------------- %«formalizing-diags»(to ".formalizing-diags") % (sec "Formalizing diagrams (in Type Theory)" "formalizing-diags") \mysection {Formalizing diagrams (in Type Theory)} {formalizing-diags} We saw at sections \ref{dn-types} and \ref{functors} how to make each downcased ``name'' stand for both a ``name'' and its ``meaning''. In our downcased categorical diagrams, each node and each arrow has a definite meaning as a categorical entity; so, let's consider each node and arrow in a downcased diagram a {\sl diagrammatical name}. { \def\f{} \def\g{{\ov}} Note that diagrammatic names are {\sl positional} --- in the sense that entities with the same apparent names but at different positions of a diagram are allowed to have different meanings. That happened, for example, in Figure~\ref{=E-via-frobenius}, where both $\dd^*Q$ and $\dd^*\opistar(\dd^*Q)$ became $\ssst{a,b}{Qabb}$ --- abbreviated to a `$Qabb$' above an `$a,b$' --- in the downcasing. \msk Now take any downcased diagram $D$, and draw two {\sl copies} of it, one above another, like this: % $$\begin{matrix} D \\ \dnto \\ D^- \end{matrix}$$ Let's take the positionality of names a step further. At the top diagram, $D$, all meanings are in the ``real world'', and are non-proto categorical entities. At the lower diagram, $D^-$, in the ``syntactical world'', each meaning is the proto-categorical entity corresponding to the non-proto entity above. For example, the meanings for an iso arrow `$a,b \bij b,a$' will be just a pair $(\ang{'_{AB},_{AB}}, \ang{'_{BA},_{BA}})$ in the syntactical world, but in the real world it will be this plus the assurances that both composites are identities. } Suppose that we tag with a different number --- in light gray, say --- each node and each arrow in the diagram $D \to D^-$; for example, our two copies of `$a,b \bij b,a$' may get tagged as `$\bij_{2099}$' in the real-world diagram, and as `$\bij_{99}$' in the syntactical world. With this we get numerical suffixes that we can use for the corresponding terms, and in the formalization of that diagram in a proof assistant the terms {\tt flip\_AB\_99} and {\tt flip\_AB\_2099} will, by convention, stand for the proto-iso and for the iso respectively. Now imagine a diagram editor working in tandem with a text editor that not only edits a formalization of the diagram, but also controls a proof assistant. It shouldn't be hard to make the occurrences of the term {\tt flip\_AB\_99} be highlighted when the arrow `$\bij_{99}$' is selected, and vice-versa. Allowing 2D diagrammatic ``names'' in the editor, as, e.g., the squares of Section \ref{adjunctions}, as synonyms for some ascii terms, can be added later as a separate feature. % \msk % An important point to notice is that each node and arrow in each of % our diagrams stands for a definite categorical entity --- objects, % morphisms, categories, functors, etc, are ``entities'' ---, and the % downcased language has been designed to let each diagram be a % blueprint for a formalization --- in a type system, and thus on % proof assistants --- of a construction. % At the lower % diagram, $D^-$, we will be at the syntactical world, and all meanings % will be proto-categorial entities; the corres % then in the lower copy, that we are calling $D^-$, each node or arrow % will stand for a proto-entity, and the corresponding node or arrow in % $D$ will stand for the corresponding non-proto-entity. This notation % is obviously positional: two different arrows with similar names, say, % `$a \mto b'$, at different positions in the full diagram will usually % stand for different objects in the formalization of the diagram in % Type Theory. A primitive way to implement this on proof assistants is % easy to describe: [example - $a \bij b \bij c$?] % -------------------- %«database»(to ".database") % (sec "A Database of Categorical Theorems" "database") \mysection {A Database of Categorical Theorems} {database} {\sl We, the people who think mostly diagrammatically, would like to have a database of theorems from Category Theory, all presented in a diagrammatical form.} This database would include the theorems I know, the theorems I have half-forgotten, and lots of theorems that I never knew, that were added to the database by other people. \msk That database already exists, but in a non-ideal, not-very-diagrammatical form: it is the published literature on Category Theory. Each paper has its own notion of ``obviousness'': when an author skips over details and claims that something is obvious, he supposes --- in the spirit of section \ref{transmission} --- that the reader will be able to fill up the gaps. I started to work on this subject because my notion of ``obvious'' seemed to be too different from the ones that I could find in the literature. The ``archetypal models'' being generalized are almost always mentioned in the papers, but only in passing, and after all the axioms having been laid down; all the formal arguments are made in the abstract notation only; and informal notations can only be presented when they are used to prove new nontrivial results, and when their formalization has been completed --- but then they are not ``informal'' anymore, and they have been promoted to ``internal languages'', ``term calculi'', ``proof nets'', ``circuit diagrams'', etc (\cite{JoyalStreet} is an early example of an informal notation made formal, with a nice discussion). As each notion of ``obvious'' is backed by a method for proof search, it ought to be possible to formalize --- even if roughly --- how each such proof-search method would work; and each different notion of what is ``obvious'' leads to a different way to present, and store, theorems. The same theorem $T$ is remembered by a reader $R_1$ as $T_1$ and by a reader $R_2$ as $T_2$; as the two readers reconstruct the missing details the theorems grow to $T_1'$, $T_2'$, $T_1''$, $T_2''$. If we could put these objects side to side we could clarify how these different kinds of reasonings work. {\sl It is possible to reason coherently with infinitesimals.} This became clear when Non-Standard Analysis was invented, and then even clearer when Synthetical Differential Geometry came up. One way to prove that a way of reasoning is coherent is to model it mathematically --- and to show that the model has good properties. NSA and SDG ``validate'' reasonings with infinitesimals. Similarly, one way to validate reasonings based on internal diagrams, archetypal languages and informal notations is to formalize how these reasonings work --- and to build bridges between them and the standard ways. \msk Diagrams like the ones in sections \ref{pres-frob-bcc} and \ref{eq-elim} can be interpreted formally: a diagram induces a dictionary, which induces trees, which then let us interpret each object and arrow from the diagram as a $ð$-term. A full set of rules for interpreting diagrams can be developed --- including ways to deal with lists of exceptions and hints --- and so it would be conceivable to have a database of categorical definitions and theorems in which the entries would appear as diagrams (plus their associated hints), but at the same time they would have precise meanings, understood by a proof assistant... Note that diagrams are becoming more and more meaningful mathematically in the last decades. Compare these ideas with the discussion in \cite{Kromer}, p.83, where he quotes this from \cite{EilenbergSteenrod}, p.xi: \begin{quote} The diagrams incorporate a large amount of information. Their use provides extensive savings in space and in mental effort. In the case of many theorems, the setting up of the correct diagram is the major part of the proof. We therefore urge that the reader stop at the end of each theorem and attempt to construct for himself the relevant diagram before examining the one which is given in the text. Once this is done, the subsequent demonstration can be followed more readily; in fact, the reader can usually supply it himself. \end{quote} % (find-kromerpage (+ 34 83) "The diagrams incorporate a large amount of information.") % (find-kromertext "The diagrams incorporate a large amount of information") % -------------------- %«epilogue»(to ".epilogue") % (sec "Epilogue" "epilogue") \mysection {Epilogue} {epilogue} This is an atypical paper. It has no theorems, and it doesn't prove any new mathematical truths --- instead, we have shown several ways to represent constructions, and to structure proofs in several layers. ``Theorems'' usually involve {\sl equalities} between {\sl constructions}, and hence they do not belong do the lowest layers; there are even ways --- see Section \ref{synt-world} --- to ``project out'' the parts of a theorem that involve equalities, and keep only the constructions... The result is a sort of a ``syntactical skeleton'' of the theorem. Our ``structuring'' puts a situation with total information at the top, and below that, in different, parallel ``legs'', we put different partial views. Theorems do not belong to the {\sl structuring}, either. At some point we will have ``meta-theorems'' about properties of this structuring. But finding these meta-theorems should not be top priority right now: these meta-theorems will use known theorems, and at this point it is more important to put more known theorems in this format. \msk The above may look too vague, too philosophical (in contraposition to ``mathematical''), too abstract. Category Theory used to be called ``abstract nonsense''; the ideas of this paper, then, could look like ``meta-abstract nonsense''... However, we are not pointing only towards the more abstract: we are showing ways --- and reasons --- to do the {\sl general} in parallel with the {\sl particular}, and to arrange the results of doing mathematics like that in forms that are better for {\sl reconstruction} and {\sl transmission}. Our structuring allows the controlled use of {\sl informal notations}. Several different informal notations can be used in parallel at the same time. This can be useful for comparing different people's notations, and for changing details on a notation and letting it evolve over time. The database of categorical knowledge proposed in the last section does not need a unified notation, and one of its functions could be to serve as a dictionary between notations --- and as a way to make parts of the existing literature more accessible. % (find-books "__phil/__phil.el" "corfield") % (find-books "__analysis/__analysis.el" "needham") % (find-books "__analysis/__analysis.el" "nelsen") % (find-eface-links 'default) % (find-eface-links 'tex-verbatim) % (find-efacedescr 'tex-verbatim) % (find-efunction 'set-face-attribute) % (face-attribute 'tex-verbatim :family) % (set-face-attribute 'tex-verbatim nil :family "courier") % (set-face-attribute 'tex-verbatim nil :family nil) % (find-854 "" "trees-to-dictionaries") % (find-854page 21 "trees-to-dictionaries") % Local Variables: % coding: raw-text-unix % ee-anchor-format: "«%s»" % End: