|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2009unilog-dnc.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (find-angg ".zshrc" "makebbl")
% (defun b () (interactive) (find-zsh "makebbl 2009unilog-dnc.bbl catsem,filters"))
% (defun b () (interactive) (find-zsh "bibtex 2009unilog-dnc"))
% (defun b () (interactive) (find-zsh "bibtex 2009unilog-dnc; makeindex 2009unilog-dnc"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009unilog-dnc.tex && latex 2009unilog-dnc.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009unilog-dnc.tex && pdflatex 2009unilog-dnc.tex"))
% (eev "cd ~/LATEX/ && Scp 2009unilog-dnc.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2009unilog-dnc.dvi"))
% (defun i () (interactive) (find-LATEXsh "egrep '^% \\((chap|sec|subsec) ' 2009unilog-dnc.tex"))
% (defun i () (interactive) (find-LATEXsh "egrep '\\\\index' 2009unilog-dnc.tex"))
% (defun i () (interactive) (find-LATEXgrep "grep -nH -e '\\\\index' 2009unilog-dnc.tex"))
% (find-dvipage "~/LATEX/2009unilog-dnc.dvi")
% (find-pspage "~/LATEX/2009unilog-dnc.pdf")
% (find-pspage "~/LATEX/2009unilog-dnc.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2009unilog-dnc.ps 2009unilog-dnc.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2009unilog-dnc.ps 2009unilog-dnc.dvi && ps2pdf 2009unilog-dnc.ps 2009unilog-dnc.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2009unilog-dnc.ps 2009unilog-dnc.dvi && ps2pdf 2009unilog-dnc.ps 2009unilog-dnc.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2009unilog-dnc.pdf" (ee-twupfile "LATEX/2009unilog-dnc.pdf") 'over)
% (ee-cp "~/LATEX/2009unilog-dnc.pdf" (ee-twusfile "LATEX/2009unilog-dnc.pdf") 'over)
% http://angg.twu.net/LATEX/2009unilog-dnc.pdf
% (find-LATEXfile "2009unilog-dnc.bbl")
% (find-LATEXfile "2009unilog-dnc.ilg")
% (find-LATEXfile "2009unilog-dnc.ind")
% (find-angg "bin/gsub.lua")
% (find-LATEXfile "2009unilog-dnc.aux" "\\newlabel{dn-lawvere-70-eq}{{3.24.3}{47}}")
% (find-LATEXsh0 "gsub.lua '^.newlabel{dn-(.*)' '(%1)' < 2009unilog-dnc.aux")
% (find-LATEXsh0 "gsub.lua '^.newlabel{(.*)}' '(%1)' < 2009unilog-dnc.aux")
% (find-LATEXsh0 "echo gsub.lua '^.newlabel{(.*)}' '(%1)'")
% (find-fline "/tmp/pen/")
% (find-sh0 "cp -v ~/LATEX/2009unilog-dnc.pdf /tmp/pen/")
% (fooi-re "\\\\mysection {\\([^{}]*\\)} {\\([^{}]*\\)}" "% (sec \"\\1\" \"\\2\")")
% (find-LATEX "2009unilog-abs1.tex")
\documentclass[oneside]{book}
% \documentclass[oneside]{article}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\usepackage[latin1]{inputenc}
\usepackage{longtable}
% (find-es "tex" "makeindex")
\usepackage{makeidx}
\usepackage{showidx}
\usepackage{showlabels}
\makeindex
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\begin{document}
\def\diagprep#1{}
\def\defprepareddiag#1#2#3{\expandafter\def\csname diag-#1\endcsname{#2\bfig#3\efig}}
\def\defdiag#1#2{\expandafter\def\csname diag-#1\endcsname{\bfig#2\efig}}
\def\ifdiagundefined#1{\expandafter\ifx\csname diag-#1\endcsname\relax}
\def\diag#1{\ifdiagundefined{#1}
\errmessage{UNDEFINED DIAGRAM: #1}
\else
\csname diag-#1\endcsname
\fi
}
%
\input 2009unilog-dnc.dnt
%*
% (eedn4-51-bounded)
%Index of the slides:
%\msk
% To update the list of slides uncomment this line:
%\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\widemtos
% (find-es "tex" "llangle-and-rrangle")
% (find-dn4ex "edrx08.sty" "ttchars")
% (find-symbolspage 54 "\\llangle")
% (find-symbolstext "\\llangle")
% http://ubuntuforums.org/archive/index.php/t-722871.html
\def\llangle{\langle\!\langle}
\def\rrangle{\rangle\!\rangle}
\def\angg#1{\llangle#1\rrangle}
\def\nat{\natural}
\def\myotherttchars{
\def«{\ttchar{$\llangle$}}
\def»{\ttchar{$\rrangle$}}
}
\def\myttchars{\basicttchars\myotherttchars}
% For "article":
\def\mychapter #1#2{\section{#1}\label{#2}}
\def\mysection #1#2{\subsection{#1}\label{#2}}
\def\mysubsection#1#2{\subsubsection{#1}\label{#2}}
% For "book":
\def\mychapter #1#2{\chapter{#1}\label{#2}}
\def\mysection #1#2{\section{#1}\label{#2}}
\def\mysubsection#1#2{\subsection{#1}\label{#2}}
\def\Sub{¯{Sub}}
\def\Sub{\text{Sub}}
\def\Cod{\operatorname{Cod}}
\def\Nat{\operatorname{Nat}}
\def\Monicto{\diagxyto/ >->/<150>}
\def\CanSub{\operatorname{CanSub}}
\def\Sub {\operatorname{Sub}}
%:*&*\land *
%:*==*\equiv *
%:*>->*\monicto *
%:*-.->*\TNto *
%% (find-dn4 "experimental.lua" "thereplusxy")
%L thereplusxy = function (dx, dy, tag)
%L ds[1] = storenode({x = ds[1].x + dx, y = ds[1].y + dy, tag = tag})
%L return ds[1]
%L end
%L forths["there+xy:"] = function ()
%L thereplusxy(getwordasluaexpr(), getwordasluaexpr(), getword())
%L end
\def\Eq{Ð{Eq}}
\def\sm#1{\begin{smallmatrix}#1\end{smallmatrix}}
\def\catAK{{\catA_T}}
\def\catAEM{{\catA^T}}
\def\KOBJ #1#2{[#1 \diagxyto/-->/<150> #2]}
\def\EMOBJ #1#2#3{[#1 \diagxyto/<-/<150>^{#3} #2]}
\def\EMOBJT#1#2{[#1 \diagxyto/<-/<150>^{#2} T#1]}
\def\projdiag#1#2#3#4#5#6{
#1 \diagxyto/<-/<#5>^{_{#2#3}} #2×#3 \diagxyto/->/<#6>^{'_{#2#3}} #4
}
\def\ren {¯{ren}}
\def\iso {¯{iso}}
\def\Cur {¯{Cur}^\sharp}
\def\Uncur {¯{Cur}^\flat}
\def\Cur {¯{Cur}}
\def\Uncur {¯{Uncur}}
\def\Ptrue {ÐP§}
\def\Ptruenat{ÐP§^\nat}
\def\Pand {ÐP∧}
\def\Pandnat {ÐP∧^\nat}
\def\Pimp {ÐP⊃}
\def\Pimpnat {ÐP⊃^\nat}
\def\Frob {Ð{Frob}}
\def\Frobnat {Ð{Frob}^\nat}
\def\BCCL {Ð{BCCL}}
\def\BCCLnat {Ð{BCCL}^\nat}
\def\BCCR {Ð{BCCR}}
\def\BCCRnat {Ð{BCCR}^\nat}
\def\BCCex {Ð{BCCÎ}}
\def\BCCexnat{Ð{BCCÎ}^\nat}
\def\BCCeq {Ð{BCC{=}}}
\def\BCCeqnat{Ð{BCC{=}}^\nat}
\def\BCCfa {Ð{BCCÎ}}
\def\BCCfanat{Ð{BCCÎ}^\nat}
\def\cur{\operatorname{cur}}
\def\uncur{\operatorname{uncur}}
\def\app{\operatorname{app}}
\def\lnameof#1{\ulcorner#1\urcorner}
\tableofcontents
% Set the marker "i" to the end of the list of anchors
% before running the <<myexpandsecs>>...
%
% (defun mymove () (interactive) (eek "C-a C-SPC <down> C-w C-x r SPC a C-x r j i C-y C-x r SPC i C-x r j a"))
% (defun myexpandsec () (interactive (eek "M-e 2*RET 7*<up> <<mymove>> RET 6*<down>")))
% (setq last-kbd-macro (kbd "<<myexpandsec>>"))
% (eek "C-e 2*RET C-x r SPC i")
% «.introduction» (to "introduction")
% «.abstract» (to "abstract")
% «.no-theorems» (to "no-theorems")
% «.syntactical-world» (to "syntactical-world")
% «.proto-cats» (to "proto-cats")
% «.proto-functors» (to "proto-functors")
% «.proto-NTs» (to "proto-NTs")
% «.proto-isos» (to "proto-isos")
% «.proto-epis-and-monics» (to "proto-epis-and-monics")
% «.proto-adjunctions» (to "proto-adjunctions")
% «.proto-monads» (to "proto-monads")
% «.proto-kleisli» (to "proto-kleisli")
% «.proto-EM» (to "proto-EM")
% «.proto-comparison» (to "proto-comparison")
% «.proto-monadicity» (to "proto-monadicity")
% «.proto-beck» (to "proto-beck")
% «.proto-universals» (to "proto-universals")
% «.proto-yoneda» (to "proto-yoneda")
% «.proto-products» (to "proto-products")
% «.to-deserve-a-name» (to "to-deserve-a-name")
% «.mad-names» (to "mad-names")
% «.proto-exponentials» (to "proto-exponentials")
% «.proto-terminals» (to "proto-terminals")
% «.proto-cart-cats» (to "proto-cart-cats")
% «.proto-CCCs» (to "proto-CCCs")
% «.proto-ind-fib-hyp» (to "proto-ind-fib-hyp")
% «.proto-subobjects» (to "proto-subobjects")
% «.proto-arch-fibration» (to "proto-arch-fibration")
% «.proto-indexed-cats» (to "proto-indexed-cats")
% «.proto-cart-morphs» (to "proto-cart-morphs")
% «.proto-cleavages» (to "proto-cleavages")
% «.proto-cleavages-2» (to "proto-cleavages-2")
% «.proto-change-of-base» (to "proto-change-of-base")
% «.proto-fibers» (to "proto-fibers")
% «.proto-preservations» (to "proto-preservations")
% «.proto-frobenius» (to "proto-frobenius")
% «.proto-BCC» (to "proto-BCC")
% «.proto-adjs-to-cobs» (to "proto-adjs-to-cobs")
% «.dn-intro» (to "dn-intro")
% «.dn-simple» (to "dn-simple")
% «.dn-functors» (to "dn-functors")
% «.dn-cats» (to "dn-cats")
% «.dn-pseudopoints» (to "dn-pseudopoints")
% «.dn-NTs» (to "dn-NTs")
% «.dn-adjunctions» (to "dn-adjunctions")
% «.dn-CCCs» (to "dn-CCCs")
% «.dn-contexts» (to "dn-contexts")
% «.dn-contexts-single» (to "dn-contexts-single")
% «.dn-context-morphs» (to "dn-context-morphs")
% «.dn-contexts-multi» (to "dn-contexts-multi")
% «.dn-discharges» (to "dn-discharges")
% «.dn-subsets» (to "dn-subsets")
% «.dn-subobjects» (to "dn-subobjects")
% «.dn-proj-functors» (to "dn-proj-functors")
% «.dn-uc-intro» (to "dn-uc-intro")
% «.dn-uc-semi-logical» (to "dn-uc-semi-logical")
% «.dn-uc-lawvere» (to "dn-uc-lawvere")
% «.dn-uc-seely» (to "dn-uc-seely")
% «.dn-uc-jacobs» (to "dn-uc-jacobs")
% «.dn-uc-maclane» (to "dn-uc-maclane")
% «.dn-uc-awodey» (to "dn-uc-awodey")
% «.dn-arch-hyperdoctrine» (to "dn-arch-hyperdoctrine")
% «.dn-change-of-base» (to "dn-change-of-base")
% «.dn-preservations» (to "dn-preservations")
% «.dn-display-maps» (to "dn-display-maps")
% «.dn-quantifiers» (to "dn-quantifiers")
% «.dn-equality» (to "dn-equality")
% «.dn-bcc-for-exists» (to "dn-bcc-for-exists")
% «.dn-bcc-for-forall» (to "dn-bcc-for-forall")
% «.dn-bcc-for-equality» (to "dn-bcc-for-equality")
% «.dn-frob-for-exists» (to "dn-frob-for-exists")
% «.dn-frob-for-equality» (to "dn-frob-for-equality")
% «.dn-hyperdoctrines» (to "dn-hyperdoctrines")
% «.dn-lawvere-70» (to "dn-lawvere-70")
% «.dn-frob-and-pimp» (to "dn-frob-and-pimp")
% «.dn-arbitrary-cobs» (to "dn-arbitrary-cobs")
% «.dn-lawvere-70-eq» (to "dn-lawvere-70-eq")
% «.notes-and-further» (to "notes-and-further")
% --------------------
% «introduction» (to ".introduction")
% (chap "Introduction" "introduction")
\mychapter {Introduction} {introduction}
\noindent{\bf Downcasing types (working draft, 2009nov16)}
{\myttchars
\footnotesize
\begin{verbatim}
Eduardo Ochs
LLaRC, PURO/UFF
eduardoochs@gmail.com
http://www.uff.br/llarc/
http://angg.twu.net/
\end{verbatim}
\noindent The latest version can be found at:
\noindent \url{http://angg.twu.net/LATEX/2009unilog-dnc.pdf}
}
\msk
Note: this is a {\sl first, very rough working draft} of a paper on
Downcasing Types... let me explain how it came into being. When I
started writing down my material about DNC (from ``DowNCasing'') a few
months ago I was with the impression that it would be too hard to
publish it as an article in a journal --- because of the reasons in
section \ref{no-theorems} --- but it occurred to me that I could take
an alternative route: to write first a technical report, mainly for a
very specific audience --- for the people in my research group in Rio
das Ostras and for few other groups in Rio de Janeiro (and there are
no categorists in the strict sense here!), with all details and all
dictionaries of notations, to help these people understand some papers
and books in CT...
% (find-w3m "~/TH/L/math-b.html#PhD")
Then another excuse to finish it appeared: I was trying to help
Valeria de Paiva --- whom I knew from several events in Logic in
Brazil, and who had even watched my very first international talk (see
\url{http://angg.twu.net/math-b.html#PhD}) --- to find out how she
could become a visiting researcher in Brazil for a few months, and at
one point she asked casually if I wasn't going to submit anything to
the session on Categorical Logic at UNILOG'10, where she was one of
the organizers... I wrote the first version of the abstract --- not
the one below ---, asked for comments (``what she thought the referees
could complain about'', etc, as we still had ten days before the
deadline), and she pointed out that I made liftings look too easy,
that the notion of downcasing --- and its non-triviality --- didn't
make enough sense from what I wrote, and a few other things that don't
matter now...
Then, in the space of little more than one week, I was able to write
all this down (with some bits of cut-and-paste from past seminar
notes, of course). It doesn't matter exactly what Valeria said; in
some situations what really matters is {\sl what we do} with what
other people say to us --- and we both wanted these ideas to be
written down, and now they are {\sl much} closer to being in a
readable form than they were before...
\msk
[Expect big changes in the text below over the next few weeks...]
% --------------------
% «abstract» (to ".abstract")
% (sec "Abstract" "abstract")
\mysection {Abstract} {abstract}
(Taken from: \url{http://angg.twu.net/LATEX/2009unilog-abs1.pdf})
\msk
When we represent a category $\catC$ in Type Theory it becomes a
7-uple: $(\catC_0, \Hom_\catC, \id_\catC, ¢_\catC; Ð{assoc}_\catC,
Ð{idL}_\catC, Ð{idR}_\catC)$, where the first four components are
``structure'' and the last three are ``properties''.
We call the ``structure'' components the ``syntactical part'', and the
``properties'' components the ``logical part''. A {\sl protocategory}
is a 4-uple $(\catC_0, \Hom_\catC, \linebreak[1] \id_\catC, ¢_\catC)$
--- just the ``syntactical skeleton'' of what a category is, without
the components that talk about equality of morphisms. By splitting at
the right places the uples that represent functors, natural
transformations, isos, adjunctions, limits, etc, we define
proto-functors, proto-NTs, and so on.
The operation that takes entities and returns the corresponding
proto-entities behaves as a projection, and we say that it goes from
the ``real world'' --- where everything has both a ``syntactical'' and
a ``logical'' part --- to the ``syntactical world'', where only the
syntactical parts have been kept.
The opposite of to {\sl project} is to {\sl lift}. We may start with a
proto-something, $s^-$, in the syntactical world, and try to lift it
to an $s$ in the real world that projects into $s^-$. Meta-theorems
about lifting are hard to obtain, but we know many interesting
liftings --- each object $r$ of the (projectable fragment of the) real
world projects to an proto-object $r^-$ that can be lifted back to $r$
--- and we can start by studying them to understand how liftings
behave.
% about lifting are hard to obtain, but each object of the
% (projectable fragment of the) real world may be lifted by first
% constructing its projection and then ``completing'' it using
% information from the original object.
Proto-objects --- even proto-proofs --- are especially amenable to
being represented diagrammatically, and there is a simple way to
attribute a precise meaning to each entity --- each node, arrow, etc
--- appearing in these diagrams. We will show how to formalize two
such diagrammatic proofs --- the Yoneda Lemma and one of the weakest
monadicity theorems --- as terms in Coq.
\def\BCCLobj{f^* \Pi_{\pi_{BC}} P}
\def\BCCRobj{\Pi_{\pi_{AC}} (f×C)^* P}
\def\BCCS{\ssst{aÝA}{ýcÝC.P(fa,c)}}
\def\psst#1#2{(#1\;||\;#2)}
\def\psst#1#2{#1||#2}
\def\bccp{\psst{a}{ýc.P(fa,c)}}
\def\bcc{\psst{a}{ýc.P(fa,c)}}
\def\bcca{\psst{a}{ýc.P}}
\def\bccbc{\psst{b,c}{P}}
For most applications in Categorical Semantics one further trick is
needed: ``downcasing types'', that lets us name entities by what they
represent in the ``archetypical case''. For example, in a
hyperdoctrine, if $P$ is an object over $B×C$ and $f:A \to B$ then
Beck-Chevalley Condition for $\forall$ says that the natural morphism
from $\BCCLobj$ to $\BCCRobj$ should be an iso. In the archetypical
hyperdoctrine, $\Sub(\Set)$, $P$ ``is'' a subset
$\sst{(b,c)ÝB×C}{P(b,c)}$ of $B×C$, and both $\BCCLobj$ and $\BCCRobj$
``deserve the name'' $\sst{aÝA}{ýcÝC.\,P(fa,c)}$. The downcasing of
$P$ is $\psst{b,c}{P}$, and the BCC map becomes a map $\bcca \mto
\bcca$ that is not the identity, whose construction can be read out
from a diagram.
% In the downcasing, this becomes $\psst{a}{ýc.P(fa,c)} \mto
% \psst{a}{ýc.P(fa,c)}$, which looks like an identity map; however, if
% we give a unique tag to each node and arrow and define the BCC
% morphism by a diagram showing its construction, then the BCC
% morphism becomes an iso between the two objects that ``are'' the
% same {\sl in the archetypal hyperdoctrine}, $\Sub(\Set)$.
Roughly, what is the happening is the following: the formal definition
of hyperdoctrine generalizes {\sl some} of the structure of
$\Sub(\Set)$; with our way of interpreting diagrams we can define all
this structure diagrammatically, in a notation that ``suggests'' that
we are in $\Sub(\Set)$, i.e., ``in the archetypical case'', and then
we can ``lift'' these definitions to diagrams with the same
two-dimensional structure, but in any of the standard notations.
Several categorical theorems become quite clear when we find
``archetypical diagrams'' for their (proto-)proofs, and then we lift
those to standard notations; we will show some examples from Lawvere's
``Adjointness in Foundations'' (1969) and ``Equality in
Hyperdoctrines'' (1970) papers.
% Hi Jean-Yves, Andrei, Valeria,
%
% > Ask the selected contributors to send before December 22 to
% > unilog2010@gmail.com a description of their talk within an e-mail
% > with no special formatation, no attachment and with the name of the
% > session as object of the e-mail. The description should be as
% > follows: Name, Institution, E-mail Title of the talk Abstract of 10
% > to 20 lines, with few mathematical symbols and few bibliographical
% > references.
%
% Here it goes: 22 non-blank lines, plus 3 blanks, plus name/
% institution/title. Is that acceptable? Feel free to remove the {\it}s,
% the {\bf}s and to simplify $P^-$ to "P^-" or "P-" (in ascii)...
%
% Sorry for the delay - my academic semester ended two hours ago - I
% just typed the last student grades into a web interface... I hope
% (again!) that it's not too late... 8-\
%
%
% Name: Eduardo Ochs
% Instituion: LLaRC / PURO-UFF
% Title of the talk and short abstract:
%
% Downcasing Types
% ================
%
% When we represent a category C in a type system it becomes a 7-uple,
% whose first four components - class of objects, Hom, id, composition -
% are ``structure''; the other three components are ``properties'', and
% only these last three involve equalities of morphisms.
%
% We can define a projection that keeps the ``structure'' and drops the
% ``properties'' part; it takes a category and returns a
% ``proto-category'', and it also acts on functors, isos, adjunctions,
% proofs, etc, producing proto-functors, proto-proofs, and so on.
%
% We say that this projection goes from the ``real world'' to the
% ``syntactical world''; and that it takes a ``real proof'', P, of some
% categorical fact, and returns its ``syntactical skeleton'', P^-. This
% P^- is especially amenable to diagrammatic representations, because it
% has only the {\it constructions} from the original P --- the diagram
% chasings have been dropped.
%
% We will show how to ``lift'' the proto-proofs of the Yoneda Lemma and
% of some facts about monads and about hyperdoctrines from the
% syntactical world to the real world. Also, we will show how each arrow
% in our diagrams is a term in a precise diagrammatic language, and how
% these diagrams can be read out as definitions. The ``downcased''
% diagrams for hyperdoctrines, in particular, look as diagrams about
% {\bf Set} (the archetypical hyperdoctrine), yet they state the
% definition of an arbitrary hyperdoctrine, plus (proto-)theorems.
%
% Cheers,
% Eduardo
% --------------------
% «no-theorems» (to ".no-theorems")
% (sec "There Are no Theorems in This Paper" "no-theorems")
\mysection {There Are no Theorems in This Paper} {no-theorems}
...because the things that we usually call ``theorems'' in Category
Theory belong to the real world --- they are a construction {\sl plus
something more}.
Take for example the Yoneda Lemma. It says that given a functor $R:
\catB \to \Set$ and an object $B$ of $\catB$ we have a bijection
between the set $RB$ and the set of natural transformations $C \TNto
((B \to C) \to RC)$. Here we are working in the syntactical world only
--- we {\sl mention} liftings, but we don't do any liftings
explicitly, and so what we get is just the projection of that
bijection, which is a proto-iso between $RB$ and the set of proto-NTs
$C \TNto ((B \to C) \to RC)$. Usually a ``theorem'' involving a such
construction would have to either show that it is always a bijection,
or to show a case where it is {\sl not} a bijection.
What we do have here is the definition of the two worlds (mostly via
examples, but whatever...), of the projections, of the liftings, some
ideas of how to work with this splitting of worlds, and examples.
% --------------------
% «syntactical-world» (to ".syntactical-world")
% (chap "The syntactical world" "syntactical-world")
\mychapter {The syntactical world} {syntactical-world}
% --------------------
% «proto-cats» (to ".proto-cats")
% (sec "Categories" "proto-cats")
\mysection {Categories} {proto-cats}
[Typeset this from my handwritten notes]
% --------------------
% «proto-functors» (to ".proto-functors")
% (sec "Functors" "proto-functors")
\mysection {Functors} {proto-functors}
% --------------------
% «proto-NTs» (to ".proto-NTs")
% (sec "Natural Transformations" "proto-NTs")
\mysection {Natural Transformations} {proto-NTs}
% --------------------
% «proto-isos» (to ".proto-isos")
% (sec "Isos" "proto-isos")
\mysection {Isos} {proto-isos}
% --------------------
% «proto-epis-and-monics» (to ".proto-epis-and-monics")
% (sec "Epis and Monics" "proto-epis-and-monics")
\mysection {Epis and Monics} {proto-epis-and-monics}
% --------------------
% «proto-adjunctions» (to ".proto-adjunctions")
% (sec "Adjunctions" "proto-adjunctions")
\mysection {Adjunctions} {proto-adjunctions}
If $L$ and $R$ are functors going in opposite directions between two
categories, say,
%
$$\catB \two/<-`->/<150>^L_R \catA$$
%
then a {\sl proto-adjunction}, $L \dashv R$, is an 8-uple,
%
$$(\catA, \catB, L, R, \flat, \sharp, \eta, \ee)$$
%
that we draw as:
%
%D diagram adj1
%D 2Dx 100 +30 +30 +30
%D 2D 100 S1B LA <---| A T0A
%D 2D | | | |
%D 2D | | <-> | |
%D 2D v v v v
%D 2D +30 S0B B |---> RB T1A
%D 2D
%D 2D +20 \catB <=> \catA
%D 2D
%D (( S1B .tex= LRB S0B .tex= B
%D S1B S0B -> .plabel= l _B
%D ))
%D (( T0A .tex= A T1A .tex= RLA
%D T0A T1A -> .plabel= r \eta_A
%D ))
%D (( LA A B RB
%D @ 0 @ 1 <-|
%D @ 0 @ 2 -> .PLABEL= _(0.43) g^\flat
%D @ 0 @ 2 -> .PLABEL= _(0.57) f
%D @ 1 @ 3 -> .PLABEL= ^(0.43) g
%D @ 1 @ 3 -> .PLABEL= ^(0.57) f^\sharp
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl^
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl_
%D @ 2 @ 3 |->
%D ))
%D (( \catB \catA <- sl^ .plabel= a L
%D \catB \catA -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\diag{adj1}$$
% [Transpositions, unit, counit]
There is some redundancy in this definition, as we may reconstruct
some of the entities $\flat$, $\sharp$, $\eta$, $\ee$ in terms of the
other ones:
%
%D diagram adj-reconstruction-LR
%D 2Dx 100 +30 +40 +30 +40 +30
%D 2D 100 L0 <--| L1
%D 2D | |
%D 2D | | |
%D 2D | | v
%D 2D +30 | <-| | L3
%D 2D | v |
%D 2D v v
%D 2D +18 L4 <--| L5
%D 2D
%D 2D +15 F0 <--| F1
%D 2D / | |
%D 2D | | <--| |
%D 2D | v v
%D 2D +30 C0 <--| C1 | F2 <--| F3 U0 <--| U1
%D 2D | | | | | |
%D 2D +12 | | \ | S0 | |
%D 2D | <--| | vv |\ | |--> |
%D 2D +6 | | F4 | | | |
%D 2D v v v | v v
%D 2D +12 C2 |--> C3 S1 |--> S2 | U2 |--> U3
%D 2D | | |
%D 2D | |--> | /
%D 2D v vv
%D 2D +30 S3 |--> S4
%D 2D
%D 2D +15 R0 |--> R1
%D 2D | |
%D 2D v | |
%D 2D +18 R2 | |-> |
%D 2D | | |
%D 2D | v |
%D 2D v v
%D 2D +30 R4 |--> R5
%D 2D
%D 2D
%D (( F0 .tex= LA F1 .tex= A
%D F2 .tex= LRB F3 .tex= RB
%D F4 .tex= B
%D F0 F1 <-|
%D F0 F4 -> .slide= -16pt .plabel= l \sm{g^\flat\;:=\\Lg;_B}
%D F0 F2 -> .plabel= l Lg
%D F1 F3 -> .plabel= r g
%D F0 F3 harrownodes nil 20 nil <-|
%D F2 F3 <-|
%D F2 F4 -> .plabel= l _B
%D ))
%D (( S0 .tex= A
%D S1 .tex= LA S2 .tex= RLA
%D S3 .tex= B S4 .tex= RB
%D S0 S2 -> .plabel= r \eta_A
%D S1 S2 |->
%D S1 S3 -> .plabel= l f
%D S2 S4 -> .plabel= r Rf
%D S0 S4 -> .slide= 16pt .plabel= r \sm{f^\sharp\;:=\\\eta_A;Rf}
%D S1 S4 harrownodes nil 20 nil |->
%D S3 S4 |->
%D S3 S4 -> .plabel= l _B
%D ))
%D (( C0 .tex= LRB C1 .tex= RB
%D C2 .tex= B C3 .tex= RB
%D C0 C1 <-|
%D C0 C2 -> .plabel= l \sm{_B\;:=\\{\id_{RB}}^\flat}
%D C1 C3 -> .plabel= r \id_{RB}
%D C2 C3 |->
%D C0 C3 harrownodes nil 20 nil <-|
%D ))
%D (( U0 .tex= LA U1 .tex= A
%D U2 .tex= LA U3 .tex= RLA
%D U0 U1 <-|
%D U0 U2 -> .plabel= l \id_{LA}
%D U1 U3 -> .plabel= r \sm{\eta_A\;:=\\{\id_{LA}}^\sharp}
%D U2 U3 |->
%D U0 U3 harrownodes nil 20 nil |->
%D ))
%D (( L0 .tex= LA' L1 .tex= A'
%D L3 .tex= A
%D L4 .tex= LA L5 .tex= RLA
%D L0 L1 <-|
%D L0 L4 -> .plabel= l \sm{L\aa\;:=\\(\aa;\eta_A)^\flat}
%D L1 L5 -> .slide= -10pt
%D L1 L3 -> .plabel= r \aa
%D L3 L5 -> .plabel= r \eta_A
%D L4 L5 <-|
%D L0 L5 harrownodes nil 20 5 <-|
%D ))
%D (( R0 .tex= LRB R1 .tex= RB
%D R2 .tex= B
%D R4 .tex= B' R5 .tex= RB'
%D R0 R1 |->
%D R0 R2 -> .plabel= l \ee_B
%D R2 R4 -> .plabel= l \bb
%D R0 R4 -> .slide= 10pt
%D R1 R5 -> .plabel= r \sm{R\bb\;:=\\(\ee_B;\bb)^\sharp}
%D R4 R5 |->
%D R0 R5 harrownodes 5 20 nil |->
%D ))
%D enddiagram
%D
$$\diag{adj-reconstruction-LR}$$
% --------------------
% «proto-monads» (to ".proto-monads")
% (sec "Monads" "proto-monads")
\mysection {Monads} {proto-monads}
A {\sl protomonad} for a proto-endofunctor $T: \catA \to \catA$ is a
4-uple:
%
$$(\catA, T, \eta, \mu)$$
%
that we draw as:
%
$$A \diagxyto/->/<150>^{\eta_A} TA \diagxyto/<-/<150>^{\mu_A} TTA$$
% [unit, multiplication]
A {\sl proto-comonad} for a proto-endofunctor $S: \catB \to \catB$ is a
4-uple:
%
$$(\catB, S, , )$$
%
that we draw as:
%
$$B \diagxyto/<-/<150>^{_B} SB \diagxyto/->/<150>^{_B} SSB$$
% [counit, comultiplication]
Each proto-adjunction induces both a proto-monad and a proto-comonad.
We draw all these together as:
%
%D diagram adj-with-monads-1
%D 2Dx 100 +30 +30 +30
%D 2D 100 S2B
%D 2D ^
%D 2D |
%D 2D |
%D 2D +30 S1B LA <---| A T0A
%D 2D | | | |
%D 2D | | <-> | |
%D 2D v v v v
%D 2D +30 S0B B |---> RB T1A
%D 2D ^
%D 2D +15 |
%D 2D |
%D 2D +15 \catB <=> \catA T2A
%D 2D
%D (( S2B .tex= LRLRB S1B .tex= LRB S0B .tex= B
%D S2B S1B <- .plabel= l \sm{_B\;:=\\L\eta_{RB}}
%D S1B S0B -> .plabel= l \sm{_B\;:=\\\id_{RB}{}^\flat}
%D ))
%D (( T0A .tex= A T1A .tex= RLA T2A .tex= RLRLA
%D T0A T1A -> .plabel= r \sm{\eta"A\;:=\\\id_{LA}{}^\sharp}
%D T1A T2A <- .plabel= r \sm{\mu"A\;:=\\R\ee_{LA}}
%D ))
%D (( LA A B RB
%D @ 0 @ 1 <-|
%D @ 0 @ 2 -> .PLABEL= _(0.43) g^\flat
%D @ 0 @ 2 -> .PLABEL= _(0.57) f
%D @ 1 @ 3 -> .PLABEL= ^(0.43) g
%D @ 1 @ 3 -> .PLABEL= ^(0.57) f^\sharp
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl^
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl_
%D @ 2 @ 3 |->
%D ))
%D (( \catB \catA <- sl^ .plabel= a L
%D \catB \catA -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\diag{adj-with-monads-1}$$
We define $\mu_A := R\ee_{LA}$ and $_B := L\eta_{RB}$:
%:
%: LA RB
%: -----------------\ee -----------------\sharp
%: \ee_{LA}:LRLA->LA \eta_{RB}:RB->RLRB
%: -----------------------------R -------------------------L
%: \mu_A:=R\ee_{LA}:RLRLA->RLA _B:=L\eta_{RB}:LRB->LRLRB
%:
%: ^def-muA ^def-deltaB
%:
$$\ded{def-muA} \qquad \ded{def-deltaB}$$
We have seen how a proto-adjunction induces a proto-monad; now we will
see how a proto-monad induces {\sl two} proto-adjunctions.
% --------------------
% «proto-kleisli» (to ".proto-kleisli")
% (subsec "The Kleisli Category of a Monad" "proto-kleisli")
\mysubsection {The Kleisli Category of a Monad} {proto-kleisli}
The {\sl Kleisli proto-category} of a proto-monad $(\catA, T, \eta,
\mu)$ is the proto-category:
%
$$\catAK := ((\catAK)_0, \Hom_\catAK, \id_\catAK, ¢_\catAK)$$
%
where $(\catAK)_0$ is equal to $\catA_0$, but we write the objects of
$(\catAK)_0$ in a funny way: an object $A Ý \catA$ becomes
%
$$\KOBJ{A}{TA}$$
%
when we regard it as an object of $(\catAK)_0$.
A morphism in $\Hom_\catAK(\KOBJ{A}{TA}, \KOBJ{C}{TC})$ is just a map
$f:A \to TC$ in $\Hom_\catA(A, TC)$. We write it as $[f]:
\Hom_\catAK(\KOBJ{A}{TA}, \KOBJ{C}{TC})$ to stress that its (formal)
type is different from $f$.
The identity operation, $\id_\catAK$, is the $\eta$ (the ``unit'') of
the monad in disguise:
%
%$$\id_\catAK(\KOBJ{A}{TA}) := [\eta_A]$$
%
%Note that:
%:
%: A
%: ------------\eta
%: \eta_A:A->TA
%: -----------------------------------\ren
%: [\eta_A]:\KOBJ{A}{TA}->\KOBJ{A}{TA}
%: -----------------------------------------------------\ren
%: \id_{[A-"->TA]}:\Hom_\catAK(\KOBJ{A}{TA},\KOBJ{A}{TA})
%:
%: ^typing-id-kleisli
%:
%: \id_\catAK(\KOBJ{A}{TA}):\Hom_\catAK(\KOBJ{A}{TA},\KOBJ{A}{TA})
%:
$$\ded{typing-id-kleisli}$$
The composition, $¢_\catAK$, needs a trick: if $f:A \to TC$ and $g: C
\to TE$ then $[f];[g] := [f;Tg;\mu_E]$. In diagrams:
%
%D diagram kleisli-id-and-comp
%D 2Dx 100 +60 +30 +30
%D 2D 100 A0 A{}
%D 2D | \
%D 2D | \
%D 2D v v
%D 2D +30 A1 TA
%D 2D
%D 2D +30 KA A
%D 2D | \
%D 2D | \
%D 2D v v
%D 2D +30 KC C ..> TC
%D 2D | \ \
%D 2D | \ \
%D 2D v v v
%D 2D +30 KE E ..> TE <-- TTE
%D 2D
%D (( A0 .tex= \KOBJ{A}{TA} BOX
%D A1 .tex= \KOBJ{A}{TA} BOX
%D A0 A1 -> .plabel= r \id_{[A-"->TA]:=[\eta_A]}
%D ))
%D (( A{} TA -> .plabel= r \eta_A
%D ))
%D (( KA .tex= \KOBJ{A}{TA} BOX
%D KC .tex= \KOBJ{C}{TC} BOX
%D KE .tex= \KOBJ{E}{TE} BOX
%D KA KC -> .plabel= r [f]
%D KC KE -> .plabel= r [g]
%D KA KE -> .slide= 27pt .plabel= r \sm{[f];[g]\;:=\\"[f;Tg;\mu_E]}
%D ))
%D (( A TC -> .plabel= r f
%D C TC -->
%D C TE -> .plabel= r g TC TTE -> .plabel= r Tg
%D E TE --> TE TTE <- .plabel= b \mu_E
%D ))
%D enddiagram
%D
$$\diag{kleisli-id-and-comp}
$$
The dashed arrow in, say, $\KOBJ{A}{TA}$, is to suggest three things:
that morphisms in $\catAK$ follow the direction of the
`$\diagxyto/-->/<150>$',
that a morphism $A \to TA$ is not part of the definition of an object
$\KOBJ{A}{TA}$,
that the `$\diagxyto/-->/<150>$' is the ghost of the unit of the monad
--- the unit would go from $A$ to $TA$, but it is not used in the
definitions; nevertheless, its memory remains.
\msk
Note that the functors $L_T$ and $R_T$ act on morphisms in non-trivial
ways. In a diagram:
%D diagram L_T1-and-R_T1
%D 2Dx 100 +40
%D 2D 100 LTA <---| A
%D 2D | |
%D 2D | <-| |
%D 2D v |
%D 2D +30 LTA' <--| A'
%D 2D
%D 2D +20 LTC |---> TC
%D 2D | |
%D 2D | |-> |
%D 2D v |
%D 2D +30 LTC' |--> TC'
%D 2D
%D (( LTA .tex= \KOBJ{A}{TA} BOX A
%D LTA' .tex= \KOBJ{A'}{TA'} BOX A'
%D @ 0 @ 1 <-|
%D @ 0 @ 2 -> .plabel= l \sm{L_T\aa\;:=\\{}[\aa;\eta_{A'}]}
%D @ 1 @ 3 -> .plabel= r \aa
%D @ 2 @ 3 <-|
%D @ 0 @ 3 harrownodes nil 20 nil <-|
%D ))
%D ((
%D LTC .tex= \KOBJ{C}{TC} BOX TC
%D LTC' .tex= \KOBJ{C'}{TC'} BOX TC'
%D @ 0 @ 1 |->
%D @ 0 @ 2 -> .plabel= l [\cc]
%D @ 1 @ 3 -> .plabel= r \sm{R_T([\cc])\;:=\\{}T\cc;\mu_{C'}}
%D @ 2 @ 3 |->
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$\diag{L_T1-and-R_T1}$$
\msk
We can draw the Kleisli (proto-)adjunction as:
%
%D diagram kleisli-adj
%D 2Dx 100 +50 +35 +25
%D 2D 100 S2B
%D 2D ^
%D 2D |
%D 2D |
%D 2D +35 S1B KA <---| A T0A
%D 2D | | | |
%D 2D | | <-> | |
%D 2D v v v v
%D 2D +30 S0B KC |---> TC T1A
%D 2D ^
%D 2D +15 |
%D 2D |
%D 2D +15 \catAK <=> \catA T2A
%D 2D
%D (( KA .tex= \KOBJ{A}{TA} BOX
%D KC .tex= \KOBJ{C}{TC} BOX
%D KA A <-|
%D KA KC -> .PLABEL= _(0.41) f^\flat:=[f]
%D KA KC -> .PLABEL= _(0.59) [g]
%D A TC -> .PLABEL= ^(0.41) f
%D A TC -> .PLABEL= ^(0.59) [g]^\sharp:=g
%D KA TC harrownodes nil 20 nil <-| sl^
%D KA TC harrownodes nil 20 nil |-> sl_
%D KC TC |->
%D ))
%D (( \catAK \catA
%D @ 0 @ 1 <- sl^ .plabel= a L_T
%D @ 0 @ 1 -> sl_ .plabel= b R_T
%D ))
%D (( S2B .tex= \KOBJ{TTC}{TTTC} BOX
%D S1B .tex= \KOBJ{TC}{TTC} BOX
%D S0B .tex= \KOBJ{C}{TC} BOX
%D S2B S1B <- .plabel= l \sm{\dd_{[C-"->TC]}\;:=\\L_T(\eta_{(R_T[C-"->TC])})\;=\\L_T(\eta_{TC})\;=\\{}[\eta_{TC};\eta_{TTC}]}
%D S1B S0B -> .plabel= l \sm{\ee_{[C-"->TC]}\;:=\\{}[\id_{TC}]}
%D ))
%D (( T0A .tex= A
%D T1A .tex= TA
%D T2A .tex= TTA
%D T0A T1A -> .plabel= r \eta_A
%D T1A T2A <- .plabel= r \mu_A
%D ))
%D enddiagram
%D
$$\diag{kleisli-adj}
$$
% --------------------
% «proto-EM» (to ".proto-EM")
% (subsec "The Eilenberg-Moore Category of a Monad" "proto-EM")
\mysubsection {The Eilenberg-Moore Category of a Monad} {proto-EM}
The {\sl Eilenberg-Moore proto-category} for a proto-monad $(\catA, T,
\eta, \mu)$ is:
%
$$\catAEM := ((\catAEM)_0, \Hom_\catAEM, \id_\catAEM, ¢_\catAEM)$$
%
where a (proto-)object of $\catAEM$ is a pair $(A,\aa)$ (a
``proto-algebra''), that we write as:
%
$$\EMOBJT{A}{\aa}$$
%
We use a non-dashed arrow, `$\diagxyto/<-/<150>$', to stress that
the map $\aa:\Hom_\catA(TA, A)$ is part of the definition of the
object.
A proto-morphism $f:\EMOBJT{A}{\aa} \to \EMOBJT{C}{\cc}$ is just a
morphism $f:\Hom_\catA(A,C)$.
% A morphism $f:\EMOBJT{A}{\aa} \to \EMOBJT{C}{\cc}$ is a morphism
% $f:\Hom_\catA(A,C)$ plus the assurance that $(\aa;f)=(Tf;\cc)$.
{\sl Important.} The Eilenberg-Moore {\sl category} for a monad $T$
has fewer objects, and fewer morphisms, than the Eilenberg-Moore {\sl
proto-}category for $T$. An {\sl algebra} is a pair $(A,\aa)$ plus
the assurance that $\mu_A;\aa=T\aa;\aa$. A {\sl morphism} $f:(A,\aa)
\to (C,\cc)$ of algebras is a map $f:A \to C$ plus the assurance that
$\aa;f=Tf;\cc$.
We will focus our attention on the Eilenberg-Moore {\sl
proto-}category.
The identity $\id_\catAEM$ and the
composition $¢_\catAEM$ are defined in the obvious way (inherited from
$\catA$).
The Eilenberg-Moore adjunction can be drawn as:
%
%D diagram em-adj
%D 2Dx 100 +50 +40 +30
%D 2D 100 S2B
%D 2D ^
%D 2D |
%D 2D |
%D 2D +30 S1B EMA <---| A T0A
%D 2D | | | |
%D 2D | | <-> | |
%D 2D v v v v
%D 2D +30 S0B EMC |---> TC T1A
%D 2D ^
%D 2D +15 \catAEM <=> \catA |
%D 2D |
%D 2D +15 T2A
%D 2D
%D (( EMA .tex= \EMOBJT{TA}{\mu_A} BOX
%D EMC .tex= \EMOBJT{C}{\cc} BOX
%D EMA A <-|
%D EMA EMC -> .PLABEL= _(0.41) f^\flat:=Tf;\cc
%D EMA EMC -> .PLABEL= _(0.59) g
%D A TC -> .PLABEL= ^(0.41) f
%D A TC -> .PLABEL= ^(0.59) g^\sharp:=\eta_A;g
%D EMA TC harrownodes nil 20 nil <-| sl^
%D EMA TC harrownodes nil 20 nil |-> sl_
%D EMC TC |->
%D ))
%D (( \catAEM \catA
%D @ 0 @ 1 <- sl^ .plabel= a L^T
%D @ 0 @ 1 -> sl_ .plabel= b R^T
%D ))
%D (( S2B .tex= \EMOBJT{TTC}{TT\cc} BOX
%D S1B .tex= \EMOBJT{TC}{T\cc} BOX
%D S0B .tex= \EMOBJT{C}{\cc} BOX
%D S2B S1B <- .plabel= l \dd_\cc:=T\eta_C?
%D S1B S0B -> .plabel= l \ee_\cc:=\cc
%D ))
%D (( T0A .tex= A
%D T1A .tex= TA
%D T2A .tex= TTA
%D T0A T1A -> .plabel= r \eta_A
%D T1A T2A <- .plabel= r \mu_A
%D ))
%D enddiagram
%D
$$% \savebox{\myboxa}{$\EMOBJT{TA}{\mu_A}$}
% \savebox{\myboxc}{$\EMOBJT{C}{\cc}$}
% \savebox{\myboxd}{$\EMOBJT{TC}{T\cc}$}
% \savebox{\myboxe}{$\EMOBJT{TTC}{TT\cc}$}
\diag{em-adj}
$$
%
where [two triangles showing the transpositions]:
%D diagram em-transpositions
%D 2Dx 100
%D 2D 100
%D 2D
%D 2D +20
%D 2D
%D ((
%D
%D ))
%D enddiagram
%D
$$\diag{em-transpositions}$$
% --------------------
% «proto-comparison» (to ".proto-comparison")
% (subsec "The Comparison Theorem" "proto-comparison")
\mysubsection {The Comparison Theorem} {proto-comparison}
If $\catB \two/<-`->/<150>^L_R \catA$ and $\catB'
\two/<-`->/<150>^{L'}_{R'} \catA$ are two proto-adjunctions --- the
full definition with `$\flat$'s, `$\sharp$'s, `$\eta$'s and `$$'s
will not be relevant now --- then a {\sl proto-comparison} from $L'
\dashv R'$ to $L \dashv R$ is just a proto-functor $F:\catB' \to
\catB$,
%
%D diagram comparison
%D 2Dx 100 +40
%D 2D 100 \catB'
%D 2D
%D 2D +20 \catA
%D 2D
%D 2D +20 \catB
%D 2D
%D (( \catB' \catA \catB
%D @ 0 @ 2 -> .plabel= l F
%D @ 0 @ 1 <- sl^ .plabel= a L'
%D @ 0 @ 1 -> sl_ .plabel= b R'
%D @ 2 @ 1 <- sl^ .plabel= a L
%D @ 2 @ 1 -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\diag{comparison}$$
%
such that $(L';F)_0 = L_0$ and $(F;R)_0 = R'_0$, i.e., two of the
triangles in the figure commute on objects (remember that in the
syntactical world equality of morphisms rarely matters). Note that we
only need to care for the objects of $\catB$ that are images of
objects in $\catB'$.
Now start with a proto-adjunction, $\catB \two/<-`->/<150>^L_R \catA$,
build its protomonad,
%
$$(\catA, T, \eta, \mu) = (A, (R;L), \eta,
(ðA¨\catA_0.R(\id_{RLA}{}^\flat))),$$
%
and build its Kleisli proto-adjunction $\catA_T
\two/<-`->/<150>^{L_T}_{R_T} \catA$, and its Eilenberg-Moore
proto-adjunction, $\catA^T \two/<-`->/<150>^{L^T}_{R^T} \catA$. It
turns out that we have proto-comparison functors $F_T:\catA_T \to
\catB$ and $F^T: \catB \to \catA^T$:
% (find-LATEX "2008monads.tex" "monads-resolutions-cat")
%
%D diagram comparisons
%D 2Dx 100 +35 +35
%D 2D 100 \catA_T
%D 2D
%D 2D +35 \catB \catA
%D 2D
%D 2D +35 \catA^T
%D 2D
%D (( \catA_T
%D \catB \catA
%D \catA^T
%D @ 0 @ 1 -> .plabel= l F_T
%D @ 1 @ 3 -> .plabel= l F^T
%D @ 0 @ 2 <- sl^ .plabel= a L_T
%D @ 0 @ 2 -> sl_ .plabel= b R_T
%D @ 1 @ 2 <- sl^ .PLABEL= ^(0.46) L
%D @ 1 @ 2 -> sl_ .PLABEL= _(0.46) R
%D @ 3 @ 2 <- sl^ .plabel= a L^T
%D @ 3 @ 2 -> sl_ .plabel= b R^T
%D ))
%D enddiagram
%D
\def\red#1{{\color{red}#1}}
\def\ph{\red}
\def\ph{\phantom}
%D
%D diagram kleisli-and-em
%D 2Dx 100 +50 +50
%D 2D 100 / k1
%D 2D // - /\
%D 2D // | \\
%D 2D // v \\
%D 2D +20 // k2 \\
%D 2D // // \\ \\
%D 2D \/ // \\ \\
%D 2D +20 r1 <================= o1
%D 2D - \\// \\ //-
%D 2D | /\\ \// |
%D 2D v \/ \\ //v v
%D 2D +20 r2 ===\\=========//=> o2
%D 2D \\ \\ // /\
%D 2D \\ \/ \/ //
%D 2D +20 \\ em1 //
%D 2D \\ - //
%D 2D \\ | //
%D 2D \/ v //
%D 2D +20 em2
%D 2D
%D (( k1 .tex= \KOBJ{A}{RLA} BOX
%D k2 .tex= \KOBJ{C}{RLC} BOX k1 place k2 place
%D em1 .tex= \EMOBJ{RLA}{RLRLA}{\mu_A} BOX
%D em2 .tex= \EMOBJ{RLC}{RLRLC}{\mu_C} BOX em1 place em2 place
%D r1 .tex= LA o1 .tex= A
%D r2 .tex= LC o2 .tex= RLC
%L comp_KL, comp_KR, comp_EML, comp_EMR = 9, 6, 16, 14
%D k1 there+xy: -comp_KL 0 k1L .tex= \ph{A}
%D k2 there+xy: -comp_KL 0 k2L .tex= \ph{C}
%D k1 there+xy: comp_KR 0 k1R .tex= \ph{RLA}
%D k2 there+xy: comp_KR 0 k2R .tex= \ph{RLC}
%D em1 there+xy: -comp_EML 0 em1L .tex= \ph{RLA}
%D em2 there+xy: -comp_EML 0 em2L .tex= \ph{RLC}
%D em1 there+xy: comp_EMR 0 em1R .tex= \ph{RLRLA}
%D em2 there+xy: comp_EMR 0 em2R .tex= \ph{RLRLC}
%D o1 o2 ->
%D r1 r2 ->
%D k1 k2 ->
%D em1 em2 ->
%D k1R o1 <-| k2R o2 |->
%D r1 o1 <-| r2 o2 |->
%D em1R o1 <-| em2R o2 |->
%D k1L r1 |-> k2L r2 |->
%D r1 em1L |-> r2 em2L |->
%D k1R k2R midpoint o1 o2 midpoint dharrownodes nil 20 nil <->
%D r1 r2 midpoint o1 o2 midpoint dharrownodes nil 25 nil <->
%D em1R em2R midpoint o1 o2 midpoint dharrownodes nil 15 nil <->
%D ))
%D enddiagram
%
$$\diag{comparisons}
\qquad
\diag{kleisli-and-em}
$$
%
where the functor $F_T$ acts like this on morphisms,
%:
%: [g]:\KOBJ{A}{RLA}->\KOBJ{C}{RLC}
%: --------------------------------\ren
%: g:A->RLC
%: --------------\flat
%: F_T([g]):=g^\flat:LA->LC
%:
%: ^F_T_1
%:
$$\ded{F_T_1}$$
%
and the functor $F^T$, that appears as $LA \mto
\EMOBJ{RLA}{RLRLA}{\mu_A}$ in the diagram, is actually something a bit
more general --- $B \mto \EMOBJ{RB}{RLRB}{R\ee_B}$ --- because its
action needs to be defined on all objects of $\catB$, not only on
those of the form $LA$. Compare:
%:
%: A
%: --L
%: LA B
%: -----------------\ee ------------\ee
%: \ee_{LA}:LRLA->LA \ee_B:LRB->B
%: --------------------R -------------R
%: \mu_A=R\ee_{LA}:RLRLA->RLA R\ee_B:RLRB->RB
%:
%: ^F^T_1 ^F^T_2
%:
%:
%:
%:
%:
%:
%:
%:
%:
$$\ded{F^T_1} \qquad \ded{F^T_2}$$
We need to impose the condition $ýA.(\mu_A=R\ee_{LA})$, but this
holds in any (non-proto-) category.
% --------------------
% «proto-monadicity» (to ".proto-monadicity")
% (subsec "Monadicity" "proto-monadicity")
\mysubsection {Monadicity} {proto-monadicity}
[Define proto-equivalence of categories]
[Define tripleable functor]
[Give examples?]
[Define proto-equalizer]
[Define preservation and reflection of proto-equalizers]
[Prove Theorem 1 of Beck's thesis (p.8 of the reprint)]
\url{http://www.tac.mta.ca/tac/reprints/articles/2/tr2abs.html}
\msk
% (find-angg ".emacs.papers" "beck")
% (find-beckthesispage 8 "tripleable")
% (find-beckthesistext)
DEFINITION 3. The adjoint pair $\aa:F \dashv U$ is tripleable if
$\Phi: B \to A^T$ is an equivalence of categories.
DEFINITION 3'. A functor $U: B \to A$ is tripleable if $U$ has a left adjoint $F$ and the
adjoint pair $F \dashv U$ is tripleable.
% --------------------
% «proto-beck» (to ".proto-beck")
% (subsec "Beck's Lemma" "proto-beck")
\mysubsection {Beck's Lemma} {proto-beck}
THEOREM 1. Let $\aa: F \dashv U$ be an adjoint pair.
(1) If $B$ has coequalizers, then there exists a left adjoint
$\hat\Phi \dashv \Phi$.
Assuming the existence of $\hat\Phi$:
(2) If $U$ preserves coequalizers, then the unit of $\hat\Phi \dashv
\Phi$ is an isomorphism $AT \ton{\equiv} \hat\Phi\Phi$.
(3) If $U$ reflects coequalizers, then the counit is an isomorphism
$\Phi \hat\Phi \ton{\equiv} B$.
Finally, in the presence of (2), (3) can be replaced by:
(3') If $U$ reflects isomorphisms, then the counit is an isomorphism
$\Phi \hat\Phi \ton{\equiv} B$.
% --------------------
% «proto-universals» (to ".proto-universals")
% (sec "Universals" "proto-universals")
\mysection {Universals} {proto-universals}
In an adjunction, each morphism $A \to RLA$ induces a natural
transformation $B \TNto ((A \to B) \to (A \to RB))$, by:
%
%D diagram adj-universal-1
%D 2Dx 100 +30
%D 2D 100 D0
%D 2D | \
%D 2D +15 | |
%D 2D v |
%D 2D +15 D1 |--> D2 |
%D 2D | | |
%D 2D +15 | |--> | /
%D 2D v vv
%D 2D +15 D3 |--> D4
%D 2D
%D 2D +20 \catB \catA
%D 2D
%D (( D0 .tex= A
%D D1 .tex= LA D2 .tex= RLA
%D D3 .tex= B D4 .tex= RB
%D D0 D2 -> .plabel= r f
%D D1 D2 |->
%D D1 D3 -> .plabel= l g
%D D2 D4 -> .plabel= r Rg
%D D0 D4 -> .slide= 16pt .plabel= r f;Rg
%D D1 D4 harrownodes nil 20 nil |->
%D D3 D4 |->
%D ))
%D (( \catB \catA <- sl^ .plabel= a L
%D \catB \catA -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\diag{adj-universal-1}$$
%
and for $f=\eta_A$ the natural transformation is a natural iso. The
notion of ``universal'' generalizes this, and makes sense when we only
have the functor $R: \catB \to \catA$.
A {\sl preuniversal} for a functor $R: \catB \to \catA$ is a triple
$(A:\catA_0, B:\catB_0, f:A \to RB)$, that we will draw as:
%
%D diagram preuniversal-1
%D 2Dx 100 +25
%D 2D 100 A
%D 2D |
%D 2D |f
%D 2D v
%D 2D +25 B |--> RB
%D 2D
%D (( A RB -> .plabel= r f
%D B RB |->
%D ))
%D enddiagram
%D
$$\diag{preuniversal-1}$$
%
or as $(A, LA, f)$ i.e.,
%
%D diagram preuniversal-2
%D 2Dx 100 +25
%D 2D 100 A
%D 2D |
%D 2D |f
%D 2D v
%D 2D +25 LA |-> RLA
%D 2D
%D (( A RLA -> .plabel= r f
%D LA RLA |->
%D ))
%D enddiagram
%D
$$\diag{preuniversal-2}$$
%
where the `$LA$' is just a ``long name'' for an object of $\catB$ (see
section \ref{dn-simple}) --- we don't have a functor $L$ anymore, so
$L$ is just a letter.
A {\sl universal} is a preuniversal plus ``universality'', where {\sl
universality} is the assertion that the induced natural
transformation is a natural iso. In the syntactical world universality
looks more like extra structure than like a property: a
(proto-)universal is a (proto-)preuniverse $(A, LA, f:A \to RLA)$ plus
a proto-inverse for its induced natural transformation.
The idea --- let me make it clearer --- is that in the syntactical
world we ``prove'' than an $(A, LA, f)$ is a universal by {\sl
constructing a proto-inverse for it}, where the proto-inverse is an
operation that behaves ``syntactically'' (i.e., in the types) as an
inverse to the natural transformation, and checking that this
proto-inverse is a real inverse is something that is left to a later
stage --- the ``lifting''.
An example should make this clearer. Any diagram $A \ton{i} C \otn{i'}
B$ (mnemonic: $C$ will ``deserve the name'' $A+B$, as we will see in
the next section) induces a natural transformation $X \TNto ((C \to X)
\to (A \to X)×(B \to X))$, by:
%
%D diagram adj-universal-+
%D 2Dx 100 +40
%D 2D 100 D0
%D 2D | \
%D 2D +15 | |
%D 2D v |
%D 2D +15 D1 |--> D2 |
%D 2D | | |
%D 2D +15 | |--> | /
%D 2D v vv
%D 2D +15 D3 |--> D4
%D 2D
%D 2D +20 \Set \Set×\Set
%D 2D
%D (( D0 .tex= (A,B)
%D D1 .tex= C D2 .tex= (C,C)
%D D3 .tex= X D4 .tex= (X,X)
%D D0 D2 -> .plabel= r (i,i')
%D D1 D2 |->
%D D1 D3 -> .plabel= l g
%D D2 D4 -> .plabel= r (g,g)
%D D0 D4 -> .slide= 22pt .plabel= r (i;g,i';g)
%D D1 D4 harrownodes nil 20 nil |->
%D D3 D4 |->
%D ))
%D (( \Set \Set×\Set
%D @ 0 @ 1 <. sl^ .plabel= a (+)
%D @ 0 @ 1 -> sl_ .plabel= b \Delta
%D ))
%D enddiagram
%D
$$\diag{adj-universal-+}$$
[...]
[$X \TNto (\Hom(C,X) \to \Hom(A,X)×\Hom(B,X))$]
[$X \TNto (\Hom(C,X) \to \Hom((A,B),(X,X))$]
[$X \TNto (\Hom_\Set(L(A,B), X) \to \Hom_{\Set×\Set}((A,B),RX)$]
[...]
\newpage
% --------------------
% «proto-yoneda» (to ".proto-yoneda")
% (sec "The Yoneda Lemma" "proto-yoneda")
\mysection {The Yoneda Lemma} {proto-yoneda}
% (find-LATEX "2009dnc-in-coq.tex" "yoneda")
% (find-angg ".emacs" "caderno")
% (find-caderno2page 45 "(Yoneda in 6 diagrams)")
% (find-angg ".emacs.papers" "barr")
% (find-books "__cats/__cats.el" "awodey")
%\def\pdiagwithboxes#1{\left(\diagprep{#1}\diag{#1}\right)}
%\def\fdiagwithboxes#1{\fbox{\!\!\!$\diagprep{#1}\diag{#1}$}}
%\def\pdiagwithboxes#1{\left(\diag{#1}\right)}
%\def\fdiagwithboxes#1{\fbox{\!\!\!$\diag{#1}$}}
\def\pdiag#1{\left(\diag{#1}\right)}
\def\fdiag#1{\fbox{\!\!\!$\diag{#1}$}}
%D diagram pdiagluniv
%D 2Dx 100 +18
%D 2D 100 #1
%D 2D -
%D 2D #4|
%D 2D v
%D 2D +16 #2 ==> #3
%D 2D
%D (( #1 #3 |-> .plabel= l #4
%D #2 #3 =>
%D ))
%D enddefpdiagram 4
\def\pdiagpreuniv#1#2#3{\pdiagluniv{#1}{#2}{#3}{}}
\def\pdiagetauniv#1#2#3{\pdiagluniv{#1}{#2}{#3}{\eta}}
\def\pdiaguniv #1#2#3{\pdiagluniv{#1}{#2}{#3}{\text{univ}}}
\def\piso{\scriptscriptstyle\text{(iso)}}
%D diagram pdiagntvv
%D 2Dx 100 +15 +15
%D 2D 100 #2 #4
%D 2D - -
%D 2D +8 #1 -.> | |-> |
%D 2D v v
%D 2D +8 #3 #5
%D 2D
%D (( #1 #2 #3 #4 #5
%D @ 1 @ 2 |-> @ 3 @ 4 |->
%D @ 0 @ 1 @ 2 midpoint -> .plabel= a *
%D @ 1 @ 4 harrownodes nil 16 nil |-> .plabel= a #6
%D ))
%D enddefpdiagram 6
%D diagram pdiagntve
%D 2Dx 100 +15 +15
%D 2D 100 #2
%D 2D -
%D 2D +8 #1 -.> | |-> #4
%D 2D v
%D 2D +8 #3
%D 2D
%D (( #1 #2 #3 #4
%D @ 1 @ 2 |->
%D @ 0 @ 1 @ 2 midpoint -> .plabel= a *
%D @ 1 @ 2 midpoint #4 |-> .plabel= a #5
%D ))
%D enddefpdiagram 5
%D diagram eta-sharp-in-adjunctions
%D 2Dx 100 +60
%D 2D 100 preuniv ntvv
%D 2D
%D (( preuniv .tex= \pdiagetauniv{a}{a^L}{a^{LR}} BOX
%D ntvv .tex= \pdiagntvv{c}{a^L}{c}{a}{c^R}{\piso} BOX
%D @ 0 @ 1 <->
%D ))
%D # OUTBOXES
%D enddiagram
%D
% $$\fdiagwithboxes{eta-sharp-in-adjunctions}$$
%D diagram lemma-on-preuniversals
%D 2Dx 100 +60
%D 2D 100 preuniv ntvv
%D 2D
%D (( preuniv .tex= \pdiagpreuniv{a}{b}{b^R} BOX
%D ntvv .tex= \pdiagntvv{c}{b}{c}{a}{c^R}{} BOX
%D @ 0 @ 1 <->
%D ))
%D # OUTBOXES
%D enddiagram
%D
% $$\fdiagwithboxes{lemma-on-preuniversals}$$
%D diagram def-of-univ-arrow
%D 2Dx 100 +60
%D 2D 100 preuniv ntvv
%D 2D
%D (( preuniv .tex= \pdiaguniv{a}{b}{b^R} BOX
%D ntvv .tex= \pdiagntvv{c}{b}{c}{a}{c^R}{\piso} BOX
%D @ 0 @ 1 <->
%D ))
%D OUTBOXES
%D enddiagram
%D
% $$\fdiagwithboxes{def-of-univ-arrow}$$
%D diagram yoneda-lemma
%D 2Dx 100 +60
%D 2D 100 preuniv ntvv
%D 2D
%D 2D +40 b^R ntve
%D 2D
%D (( preuniv .tex= \pdiagpreuniv{*}{b}{b^R} BOX
%D ntvv .tex= \pdiagntvv{c}{b}{c}{*}{c^R}{} BOX
%D b^R
%D ntve .tex= \pdiagntve{c}{b}{c}{c^R}{} BOX
%D @ 0 @ 1 <->
%D @ 0 @ 2 <->
%D @ 1 @ 3 <->
%D ))
%D OUTBOXES
%D enddiagram
%D
% $$\fdiagwithboxes{yoneda-lemma}$$
\def\ctabular#1{\begin{tabular}{c}#1\end{tabular}}
\def\ltabular#1{\begin{tabular}{c}#1\end{tabular}}
%\def\fdiagwithboxest#1#2{\ltabular{#2 \\ \fdiag{#1}}}
\def\fdiagest #1#2{\ltabular{#2 \\ \fdiag{#1}}}
%D diagram def-of-univ-arrow-and-elt
%D 2Dx 100 +60
%D 2D 100 preuniv ntvv
%D 2D
%D 2D +45 b^R ntve
%D 2D
%D (( preuniv .tex= \pdiaguniv{*}{b}{b^R} BOX
%D ntvv .tex= \pdiagntvv{c}{b}{c}{*}{c^R}{\piso} BOX
%D b^R .tex= \ctabular{$b^R$\\(universal\\element)}
%D ntve .tex= \ctabular{$\pdiagntve{c}{b}{c}{c^R}{\piso}$\\($R$"is"representable\\and"is"represented"by"$B$)} BOX
%D @ 0 @ 1 <->
%D @ 0 @ 2 <->
%D @ 1 @ 3 <->
%D ))
%D OUTBOXES
%D enddiagram
%D
% $$\fdiagwithboxes{def-of-univ-arrow-and-elt}$$
%D diagram yoneda-corollary
%D 2Dx 100 +62
%D 2D 100 preuniv ntvv
%D 2D
%D 2D +40 a|->b ntve
%D 2D
%D (( preuniv .tex= \pdiagpreuniv{*}{b}{a|->b} BOX
%D ntvv .tex= \pdiagntvv{c}{b}{c}{*}{a|->c}{} BOX
%D a|->b
%D ntve .tex= \pdiagntvv{c}{b}{c}{a}{c}{} BOX
%D @ 0 @ 1 <->
%D @ 0 @ 2 <->
%D @ 1 @ 3 <->
%D ))
%D OUTBOXES
%D enddiagram
%D
% $$\fdiagwithboxes{yoneda-corollary}$$
%D diagram yoneda-and-friends
%D 2Dx 100 +125
%D 2D 100 eta-sharp
%D 2D
%D 2D +60 pre-univs univ-arrow
%D 2D
%D 2D +80 yoneda-L univ-elt
%D 2D
%D 2D +100 yoneda-C
%D 2D
%D (( eta-sharp .tex= \fdiagest{eta-sharp-in-adjunctions}{$(\eta<->\sharp)$"in"adjunctions:} BOX
%D pre-univs .tex= \fdiagest{lemma-on-preuniversals}{Lemma"on"preuniversals:} BOX
%D yoneda-L .tex= \fdiagest{yoneda-lemma}{Yoneda"Lemma:} BOX
%D yoneda-C .tex= \fdiagest{yoneda-corollary}{Corollary:} BOX
%D univ-arrow .tex= \fdiagest{def-of-univ-arrow}{Definition"of"universal"arrow:} BOX
%D univ-elt .tex= \fdiagest{def-of-univ-arrow-and-elt}{Definitions"of"universal"element\\and"representable"functor:} BOX
%D y+= 2.5
%D @ 0 @ 1 |->
%D @ 1 @ 2 |->
%D @ 2 @ 3 |->
%D @ 0 @ 4 |->
%D @ 4 @ 5 |->
%D ))
%D OUTBOXES
%D enddiagram
%D
$$\thinmtos
\diag{yoneda-and-friends}
$$
\newpage
% \ref{proto-universals}
%D diagram pdiagLUNIV
%D 2Dx 100 +18
%D 2D 100 #1
%D 2D |
%D 2D #4|
%D 2D v
%D 2D +16 #2 |-> #3
%D 2D
%D (( #1 #3 -> .plabel= l #4
%D #2 #3 |->
%D ))
%D enddefpdiagram 4
%D diagram pdiagNTVV
%D 2Dx 100 +15 +15
%D 2D 100 #2 #4
%D 2D | |
%D 2D +8 #1 -.> | --> |
%D 2D v v
%D 2D +8 #3 #5
%D 2D
%D (( #1 #2 #3 #4 #5
%D @ 1 @ 2 -> @ 3 @ 4 ->
%D @ 0 @ 1 @ 2 midpoint -> .plabel= a .
%D @ 1 @ 4 harrownodes nil 16 nil -> .plabel= a #6
%D ))
%D enddefpdiagram 6
The diagram above starts from the idea of universal,
A preuniversal (for the functor $R: \bbB \to \bbA$, on an object $A$;
but let's consider $R$ and $A$ fixed) is a pair $(BÝ\bbB,\, f:A \to
RB)$. We will write a preuniversal $B,f$ in diagrammatic form as
%
$$\pdiagLUNIV{A}{B}{RB}{f} \qquad \text{or as} \qquad \pdiagluniv{a}{b}{b^R}{} \quad,$$
%
where the notation at the right is a downcasing for the (more)
standard notation on the left.
We will denote the space of preuniversals for $R$ on $A$ by:
%
$$\pdiagLUNIV{A}{B}{RB}{}$$
As $A$ and $R$ are fixed, then for each object $B$ of $\bbB$ we can
form the functors $\Hom_\bbB(B,-), \Hom_bbA(A,F-): \bbB \to \Set$; we
can write their actions on objects as $C \mto (B \to C)$ and $C \mto
(A \to RC)$.
We can also form the space of natural transformations between these
two functors, the we can write as:
$$\Nat(\Hom_\bbB(B,-), \Hom_\bbA(A,F-)) \qquad\text{or as}$$
$$\Hom_{\bbB \to \Set}(\Hom_\bbB(B,-), \Hom_\bbA(A,F-)) \qquad\text{or as}$$
$$ ((C \mto (B \to C)) \to (C \mto (A \to RC))) \qquad\text{or as}$$
$$\Hom_{\bbB \to \Set}((C \mto (B \to C)), (C \mto (A \to RC))) \qquad\text{or as}$$
$$C \TNto ((B \to C) \to (A \to RC)) \qquad\text{or as}$$
$$\pdiagNTVV{C}{B}{C}{A}{RC}{}$$
Our convention (section ???) is that $X \to Y$ is a hom-set and $X
\ton{f} Y$ is a specific arrow in $X \to Y$. Using this idea, we can
denote a specific natural (or proto-natural) transformation, $T$, by:
$$C \TNto ((B \to C) \ton{T_C} (A \to RC))$$
$$((B \ton{f} C) \mton{T_C} (A \ton{T_C(f)} RC))$$
Each preuniversal $B \mto RB \otn{f} A$ induces a proto-natural
transformation
%
$$C \TNto ((B \ton{g} C) \mton{ðg.(f;Rg)} (A \ton{f;Rg} RC))$$
%
whose action can be defined more formally as $ðC.ðg.(f;Rg)$; it turns
out to be a natural transformation, but in the syntactical world that
doesn't matter. And each proto-natural transformation
%
$$C \TNto ((B \to C) \ton{T} (A \to RC))$$
%
induces a preuniversal $(B, \, T_B(\id_B):A \to RB)$.
These two operations form a proto-bijection
%
%D diagram yoneda-proto-bij-1
%D 2Dx 100 +100
%D 2D T:=ðC.ðg.(f;Rg)
%D 2D 100 PREUNIV |---------------> PROTOTN
%D 2D <---------------|
%D 2D f:=T_B(\id_B)
%D 2D
%D (( PREUNIV .tex= \pdiagLUNIV{A}{B}{RB}{f} BOX
%D PROTOTN .tex= \pdiagNTVV{C}{B}{C}{A}{RC}{T} BOX
%D @ 0 @ 1 |-> sl^ .plabel= a T\;:=\;ðC.ðg.(f;Rg)
%D @ 0 @ 1 <-| sl_ .plabel= b f\;:=\;T_B(\id_B)
%D ))
%D OUTBOXES
%D enddiagram
%D
$$\diag{yoneda-proto-bij-1}$$
%
that we downcase as:
%
$$\diag{lemma-on-preuniversals}$$
This is the ``lemma on preuniversals''; note that the mechanics of the
construction are exactly the same as the idea, from adjunctions, that
we can define $\eta$ from $\sharp$ and vice-versa --- and so the big
diagram indicates that the lemma on preuniversals comes from $(\eta
\bij \sharp)$.
When $\bbA = \Set$ we can take $A = 1 = \{*\}$; this particular case
is the horizontal bijection in the Yoneda Lemma.
For any object $BÝ\bbB$, each arrow $1 \to RB$ selects an element of
$RB$ (a ``$b^R$''); and as the set $1 \to RC$ is isomorphic to $RC$
the functor $C \mto (1 \to RC)$ can be replaced by $C \mto RC$ in $C
\TNto ((B \to C) \to (1 \to RC))$; the details are:
%
%D diagram yoneda-V1
%D 2Dx 100 +90
%D 2D 100 1->RB T
%D 2D
%D 2D
%D 2D
%D 2D +30 b^RÝRB T'
%D 2D
%D (( 1->RB .tex= (1->^{f}RB)
%D b^RÝRB
%D T .tex= C-.->((B->C)->^{T}(1->RC))
%D T' .tex= C-.->((B->C)->^{T'}RC)
%D @ 0 @ 1 <-| sl_ .plabel= l ðb^R.ð*.b^R
%D @ 0 @ 1 |-> sl^ .plabel= r ðf.f(*)
%D @ 2 @ 3 <-| sl_ .plabel= l T\;:=\;ðC.ðf.ð*.((T'C)f)
%D @ 2 @ 3 |-> sl^ .plabel= r T'\;:=\;ðC.ðf.TCf*
%D ))
% D OUTBOXES
%D enddiagram
%D
$$\diag{yoneda-V1}$$
we can downcase all this --- the two ``vertical'' proto-bijections
that we just defined, plus the ``horizontal'' proto-bijection that we
defined before --- as:
%
$$\diag{yoneda-lemma}$$
The best way to think of the formalization of the diagram above is
that it is a big uple, with many components, where each of these
components can be accessed by name; for example,
$$b^R \mto \pdiagntve{c}{b}{c}{c^R}{}$$
is the composite of three of the lambda-terms that we have just
defined --- this composite turns out to be, after many
$\bb$-reductions,
%
$$ðb^R.ðC.ðg.((Rg)(b^R))$$
%
and its (proto-)inverse is:
%
$$ðT.((T_B)(\id_B))$$
This is the Yoneda Lemma.
\msk
Now we specialize again. Fix an object $A$ of $\bbB$ (note that in the
lemma on preuniversals we had $A \in \catA$!) and take $R :=
\Hom_\catB(A,-)$, i.e., $R$ is now $C \mto (A \to C)$. Each element of
$RB$ is an arrow from $A$ to $B$, and we can replace the functor $C
\mto (1 \to (A \to C))$ by $C \mto (A \to C)$. We get this:
%D diagram yoneda-V2
%D 2Dx 100 +90
%D 2D 100 1->(A->B) T
%D 2D
%D 2D
%D 2D
%D 2D +30 A->B T'
%D 2D
%D (( 1->(A->B) .tex= (1->^{f}RB)
%D A->B .tex= A->^{f'}B
%D T .tex= (C-.->((B->C)->^{T}(1->(A->C))))
%D T' .tex= (C-.->((B->C)->^{T'}(A->C)))
%D @ 0 @ 2 |-> sl^
%D @ 0 @ 2 <-| sl_
%D @ 0 @ 1 <-| sl_
%D @ 0 @ 1 |-> sl^
%D @ 2 @ 3 <-| sl_
%D @ 2 @ 3 |-> sl^
%D ))
% D OUTBOXES
%D enddiagram
%D
$$\diag{yoneda-V2}$$
% (find-angg ".emacs" "find-epalette")
% (find-epalette my-palette)
% (eev-glyphs-set-face 'eev-glyph-face-shortverb "magenta" "darkolivegreen")
% (eev-glyphs-set-face 'eev-glyph-face-shortverb "magenta" "gray15")
% (eev-set-glyph ?\C-V ?V 'eev-glyph-face-shortverb)
% (find-es "tex" "shortvrb")
[Coq demo:]
{\MakeShortVerb{}
\ttchars
\par(a,b) := «$(1\ton{f}RB)$», «$\pdiagLUNIV{A}{B}{RB}{f}$»;
\DeleteShortVerb{}
}
% --------------------
% «proto-products» (to ".proto-products")
% (sec "Products" "proto-products")
\mysection {Products} {proto-products}
\def\twolinehorizNT#1#2#3#4#5#6#7#8{
\begin{array}[t]{ccrcl}
#1 & #2 & (#3 & #4 & #5) \\
& & #6 & #7 & #8
\end{array}
}
\def\pdiag#1{\left(\diag{#1}\right)}
If $B$ and $C$ are two objects of a category $\bbC$, $B×C$ is their
product, and $:B×C \to B$ and $':B×C \to C$ the projection maps,
then we can regard the diagram
%
%D diagram fatslim-prod-1
%D 2Dx 100 +30 +30
%D 2D 100 A
%D 2D
%D 2D +30 B <--- B×C ---> C
%D 2D
%D (( A B B×C C
%D @ 0 @ 1 -> .plabel= a f
%D @ 0 @ 2 -> .plabel= m \ang{f,g}
%D @ 0 @ 3 -> .plabel= a g
%D @ 1 @ 2 <- .plabel= b \pi
%D @ 2 @ 3 -> .plabel= b \pi'
%D ))
%D enddiagram
%D
$$\diag{fatslim-prod-1}$$
as ``being'' the tuple $(B, C, B×C, \pi, \pi', (\ang{,}))$, where
$\ang,$ is the inverse for the natural transformation
$$\twolinehorizNT
{A^\op} {\tnto} {\Hom_\bbC(A,B×C)} {\to} {\Hom_{\bbC×\bbC}((A,A),(B,C))}
h {\mto} {(h;\pi,\,h;pi')}
$$
A {\sl pre-product diagram} in a category $\bbC$ is a 5-uple:
$$B \otn{p} B×C \ton{p'} C \quad \equiv \quad (B, C, P, p:P \to B, p':P \to C)$$
Any pre-product diagram induces a natural transformation
$$\twolinehorizNT
{A^\op} {\tnto} {\Hom_\bbC(A,P)} {\to} {\Hom_{\bbC×\bbC}((A,A),(B,C))}
h {\mto} {(h;p,\,h;p')}
$$
that we can draw as:
%D diagram fatslim-prod-2
%D 2Dx 100 +40
%D 2D 100 (A,A) <-----| A
%D 2D | |
%D 2D | <-| |
%D 2D v v
%D 2D +30 (B,C) |- - -> P
%D 2D
%D (( (A,A) A (B,C) P
%D @ 0 @ 1 <-|
%D @ 0 @ 2 -> .plabel= m (h;p,\,h;p')
%D @ 1 @ 3 -> .plabel= r h
%D @ 2 @ 3 |-->
%D @ 0 @ 3 harrownodes 10 20 nil <-|
%D ))
%D enddiagram
%D
$$A^\op \TNto \pdiag{fatslim-prod-2}$$
A {\sl product diagram} in $\bbC$ is a 6-uple, $(B, C, B×C, \pi, \pi',
(\ang{,}))$, which is a pre-product diagram plus an inverse to the
natural transformation just described:
%D diagram fatslim-prod-3
%D 2Dx 100 +40
%D 2D 100 (A,A) <-----| A
%D 2D | |
%D 2D | |-> |
%D 2D v v
%D 2D +30 (B,C) |- - -> P
%D 2D
%D (( (A,A) A (B,C) P
%D @ 0 @ 1 <-|
%D @ 0 @ 2 -> .plabel= l (f,g)
%D @ 1 @ 3 -> .plabel= r \ang{f,g}
%D @ 2 @ 3 |-->
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$A^\op \TNto \pdiag{fatslim-prod-3}$$
We will draw a product diagram like this:
$$\diag{fatslim-prod-1}$$
Note that from the middle arrow we can infer the name of the inverse
of the original natural transformation; the operation `$\ang,$'
factors the pair $(f,g)$ through the product.
When $B \otn{p} B×C \ton{p'} C$ is a product diagram we will say that
$P$ ``deserves the name'' $B×C$, and that the projections $p$ and $p'$
``deserve the names'' $$ and $'$.
An object $B×C$ can only deserve the `$×$' in its name if we also have
projections $:B×C \to B$ and $':B×C \to C$ also deserving their
names. A product ``comes together'' with its projections --- but we
are somehow shifting this notion to the dictionary.
A ``dictionary'' --- in the real, non-mathematical world --- maps
``names'' to ``definitions''. In our case, this part of a dictionary
corresponds to the ``interpretation function'' of a model: a model $M$
for a language $L$ maps each name (...) But dictionaries, in the
non-mathematical world, also have other parts --- for example, they
may have forewords in which some features of the language are
discussed, and where some conventions are explained ---, and within
the conventions we may have that whenever we have an entry for `$B×C$'
we will also have entries for $:B×C \to B$ and $':B×C \to C$ (or
maybe `$_{BC}$' for and `$'_{BC}$' instead --- $$ and $'$ may be
shorthands), and then the tuple $(B, C, B×C, , ')$ will have
properties such and such...
Note that in the ``real world'' (now I'm using ``real world'' in the
sense of section [...]) the natural transformation $\ang,$ is an {\sl
inverse} for
%
$$(-;,-;') \;\; = \;
\twolinehorizNT
{A^\op} {\TNto} {\Hom_\bbC(A,B×C)} {\to} {\Hom_{\bbC×\bbC}((A,A),(B,C))}
h {\mto} {(h;\pi,\,h;pi')}
$$
%
and so we could as well have just required that $(-;,-;')$ be
inversible. But the right corresponding notion in the syntactical
world is that $(\ang,)$ should be a proto-inverse for $(-;,-;')$.
And so:
%D diagram fatslim-nt-1
%D 2Dx 100 +25 +30
%D 2D 100 #2 #4
%D 2D | |
%D 2D +15 #1 -.> | --> |
%D 2D v v
%D 2D +15 #3 #5
%D 2D
%D (( #1 .tex= A^\op #2 .tex= (A,A) #3 .tex= (B,C) #4 .tex= A #5 .tex= B×C
%D @ 1 @ 2 -> @ 3 @ 4 ->
%D @ 0 @ 1 @ 2 midpoint -> .plabel= a .
%D @ 1 @ 4 harrownodes nil 20 nil -> .plabel= a {}
%D ))
%D enddiagram
$$\diag{fatslim-nt-1}$$
% --------------------
% «to-deserve-a-name» (to ".to-deserve-a-name")
% (sec "To Deserve a Name" "to-deserve-a-name")
\mysection {To Deserve a Name} {to-deserve-a-name}
In a diagram $A \ton{i} C \otn{i'} B$ we say that the `$C$' {\sl
deserves the name} `$A+B$', and that $i$ and $i'$ deserve the names
$\iota$ and $\iota'$, when $A \ton{i} C \otn{i'} B$ is a coproduct
diagram.
[Similarly for products, pullbacks, etc...]
We say that the `$C$' is a {\sl candidate for} `$A+B$' when... [This
is similar to stating: ``{\sl Proposition: Foo}'', and then
proceeding to a proof of Foo.]
% --------------------
% «mad-names» (to ".mad-names")
% (subsec "Mad Names" "mad-names")
\mysubsection {Mad Names} {mad-names}
In section \ref{dn-simple} we hint to a definition for ``downcasing''
and ``uppercasing'' that is much stricter than the one that is really
useful...
``Downcasing'' and ``uppercasing'' should {\sl not} be precise
syntactical transformations on names! Instead, what works well is to
keep a set of loosely-defined guidelines for downcasings and
uppercasing, that need not be followed very rigorously, and to keep a
``dictionary of uppercasings and downcasings'' with several entries
like ``$a' \mto b : A \to B$', `$f \equiv a \mto b$' (I use `$\equiv$'
to mean ``change of notation'', usually from standard to downcased)...
if this dictionary can be reconstructed from very hints, the better.
There is {\sl nothing} --- apart from the desire to think clearly and
to communicate our thoughts --- that prevents us, in the formalization
of some construction or theorem in Coq with \LaTeX{} chunks (section
\ref{dn-simple}), from using ``mad names'' like, say, `$\$_\#^\%$'
instead of `$a \mto b$'. The language of long names and downcasings
presented here is not like an internal language, like the ones that we
use for toposes (see \cite{BellLST}, \cite{LambekScott}, etc); rather,
it is more like {\sl half} of an internal language: a corpus of
sentences and diagrams, as they are ``spoken'', but without a fixed
grammar --- we've split the {\sl use of a language} from its {\sl
formalization}.
By the way, we can use the idea of ``diagrams as dictionaries between
notations'' (see section \ref{notes-and-further}) to change from the
$n$-th attempt to a good notation to the ($n+1$)-th attempt; the
diagrams keep the same shape...
% --------------------
% «proto-exponentials» (to ".proto-exponentials")
% (sec "Exponentials" "proto-exponentials")
\mysection {Exponentials} {proto-exponentials}
% --------------------
% «proto-terminals» (to ".proto-terminals")
% (sec "Terminals" "proto-terminals")
\mysection {Terminals} {proto-terminals}
% --------------------
% «proto-cart-cats» (to ".proto-cart-cats")
% (sec "Cartesian Categories" "proto-cart-cats")
\mysection {Cartesian Categories} {proto-cart-cats}
% --------------------
% «proto-CCCs» (to ".proto-CCCs")
% (sec "Cartesian Closed Categories" "proto-CCCs")
\mysection {Cartesian Closed Categories} {proto-CCCs}
% --------------------
% «proto-ind-fib-hyp» (to ".proto-ind-fib-hyp")
% (sec "Indexed Categories, Fibrations, Hyperdoctrines" "proto-ind-fib-hyp")
\mysection {Indexed Categories, Fibrations, Hyperdoctrines} {proto-ind-fib-hyp}
% --------------------
% «proto-subobjects» (to ".proto-subobjects")
% (subsec "Subobjects" "proto-subobjects")
\mysubsection {Subobjects} {proto-subobjects}
If $B$ is an object of a category $\bbB$, a {\sl subobject of $B$} is
a pair $(B', \bb:B' \Monicto B)$; we will often abbreviate $(B'. \bb)$
as $B' \Monicto B$. We say that two subobjects of $B$, $B' \Monicto B$
and $B'' \Monicto B$, are {\sl isomorphic} when there is an iso $B'
\bij B''$ making the obvious diagram commute.
For every category $\bbB$ we can define the category $\Sub(\bbB)$
whose objects are the subobjects of objects of $\bbB$. A morphism
$(f',f): (A' \monicto A) \to (B' \Monicto B)$ in $\Sub(\bbB)$ is a
pair of morphisms in $\bbB$, $f':A' \to B'$ and $f:A \to B$, making
the obvious square commute.
When the category $\bbB$ is $\Set$ the following definition makes
sense:
\begin{quote}
A {\sl canonical subobject} is the inclusion of a subset in its
ambient set.
\end{quote}
We will write canonical subobjects like this:
%
$$\sst{bÝB}{Q(b)} \Monicto B$$
%
and we will sometimes abbreviate that as:
%
$$\ssst{bÝB}{Q(b)}$$
We will denote by $\CanSub(\Set)$ the subcategory of $\Sub(\Set)$ made
by the canonical subobjects of $\Set$ and the morphisms between them.
Note that a morphism
%
$$(f', f): \ssst{aÝA}{P(a)} \to \ssst{bÝB}{Q(b)}$$
%
in $\CanSub(\Set)$ is in fact a pair of morphisms in $\Set$:
%D diagram CanSubSet
%D 2Dx 100 +60
%D 2D f'
%D 2D 100 A' -----> B'
%D 2D v v
%D 2D | |
%D 2D v f v
%D 2D +30 A ------> B
%D 2D
%D (( A' .tex= \sst{aÝA}{P(a)}
%D B' .tex= \sst{bÝB}{Q(b)}
%D A B
%D @ 0 @ 1 -> .plabel= a f'
%D @ 0 @ 2 >->
%D @ 1 @ 3 >->
%D @ 2 @ 3 -> .plabel= a f'
%D
%D ))
%D enddiagram
%D
$$\diag{CanSubSet}$$
We will think of subobjects of $B$ as being, or representing,
propositions over~$B$. Each subobject of a set $B$ is isomorphic to a
unique canonical subobject of~$B$:
{\myttchars
\footnotesize
\begin{verbatim}
B' <--> {b|Îb'ÝB'.\bb(b')=b}
v v
\ /
v v
B
\end{verbatim}
}
% --------------------
% «proto-arch-fibration» (to ".proto-arch-fibration")
% (subsec "Our archetypal fibration" "proto-arch-fibration")
\mysubsection {Our archetypal fibration} {proto-arch-fibration}
$\Cod: \CanSub(\Set) \to \Set$ is a fibration:
{\myttchars
\footnotesize
\begin{verbatim}
{a||Pa} ------------
\ \
ýa.Pa⊃Rgfa \ _ \ ýa.Pa⊃Rha
v g_R v
{b||Rgb} ---> {c||Rc}
<--|
g^*
A --------------
\ \ h
f \ \
v g v
B ----------> C
\end{verbatim}
}
The change-of-base functor $f^*$ associated to a morphism $f:A \to B$
in $\bbB$ acts as $\ssst{b}{Qb} \mto \ssst{a}{Qfa}$.
$\CanSub(\Set)$ has a lot of structure. Each fiber $\bbE_A$ is a BiCCC:
{\myttchars
\footnotesize
\begin{verbatim}
-- {a||Pa} -- {a||Pa} {a||Pa∧Qa} <--| {a||Pa}
/ | \ | | |
/ | \ | | <--> |
v v v v v v
{a||Qa} <- {a||Qa∧Ra} -> {a||Ra} {a||§} {a||Ra} |--> {a||Qa⊃Ra}
{a||Pa} -> {a||Pa∧Qa} <- {a||Qa} {a||®}
\ | / |
\ | / |
\ v / v
-> {a||Ra} <- {a||Pa}
\end{verbatim}
}
Each change-of-base functor has both a left adjoint, $Î_f \equiv
(\ssst{a}{Pa} \mto \ssst{b}{Îa.fa=b∧Pa})$, and a right adjoint, $ý_f
\equiv (\ssst{a}{Ra} \mto \ssst{b}{ýa.fa=b⊃Ra})$:
{\myttchars
\footnotesize
\begin{verbatim}
{a||Pa} |---> {b||Îa.fa=b∧Pa}
| |
| <-> |
v v
{a||Qfa} <---| {b||Qb}
| |
| <-> |
v v
{a||Ra} |---> {b||ýa.fa=b⊃Ra}
f
A -----------> B
\end{verbatim}
}
The diagram above specializes to:
{\myttchars
\footnotesize
\begin{verbatim}
{a,b||Pab} |---> {a||Îb.Pab} {a,b||Pab} |---> {a,b,b'||b=b'∧Pab}
| | | |
| <-> | | <-> |
v v v v
{a,b||Qa} <------| {a||Qa} {a,b||Qabb} <---| {a,b,b'||Qabb'}
| | | |
| <-> | | <-> |
v v v v
{a,b||Rab} |---> {a||ýb.Rab} {a,b||Rab} |---> {a,b,b'||b=b'⊃Rab}
A×B ------------> A A×B -------------> A×B×B
\end{verbatim}
}
The preservation rules $\Pand$, $\Ptrue$, $\Pimp$ hold trivially in
$\CanSub(\Set)$ --- the objects that they require to be isomorphic are
actually the same, for syntactical reasons (examples?)... Same for
$\BCCex$, $\BCCfa$. Frobenius holds too, albeit for less trivial
reasons.
$\CanSub(\Set)$ is also a {\sl comprehension category with unit}
(\cite{Jacobs}, definition\ 10.4.7):
{\myttchars
\footnotesize
\begin{verbatim}
{a||Pa} ---> {b||§} --------> {c||Qc}
- ^ ^ ^ -
| | | | /
v v - v v
A --------> B ---> {c|Qc}
\end{verbatim}
}
% (find-books "__cats/__cats.el" "jacobs")
% --------------------
% «proto-indexed-cats» (to ".proto-indexed-cats")
% (subsec "Indexed Categories" "proto-indexed-cats")
\mysubsection {Indexed Categories} {proto-indexed-cats}
% (find-books "__cats/__cats.el" "jacobs")
% (find-jacobspage (+ 19 27) "fibred category")
% (find-jacobspage (+ 19 50) "indexed category")
%D diagram indexed-cat-1
%D 2Dx 100 +45 +35 +30
%D 2D 100 (f;g;h)^*P @0
%D 2D
%D 2D +20 (f;g)^*h^*P @1
%D 2D
%D 2D +20 f^*g^*h^*P g^*h^*P h^*P P @2 @5 @7 @8
%D 2D
%D 2D +20 f^*(g;h)^*P (g;h)^*P @3 @6
%D 2D
%D 2D +30 (f;g;h)^*P{} @4
%D 2D
%D 2D +20 A B C D
%D 2D
%D (( (f;g;h)^*P (f;g)^*h^*P f^*g^*h^*P f^*(g;h)^*P (f;g;h)^*P{}
%D g^*h^*P (g;h)^*P h^*P P
%D @ 0 @ 1 <-> @ 1 @ 2 <-> @ 2 @ 3 <-> @ 3 @ 4 <->
%D @ 5 @ 6 <->
%D @ 0 @ 8 <-|
%D @ 1 @ 7 <-|
%D @ 2 @ 5 <-| @ 5 @ 7 <-| @ 7 @ 8 <-|
%D @ 3 @ 6 <-| @ 6 @ 8 <-|
%D @ 4 @ 8 <-|
%D ))
%D (( A B -> .plabel= a f
%D B C -> .plabel= a g
%D C D -> .plabel= a h
%D ))
%D enddiagram
%D diagram indexed-cat-2
%D 2Dx 100 +35 +30
%D 2D 100 (f;\id)^*P
%D 2D
%D 2D +20 f^*\id^*P \id^*P P
%D 2D
%D 2D +20 f^*P P{}
%D 2D
%D 2D +20 A B B{}
%D 2D
%D (( (f;\id)^*P
%D f^*\id^*P \id^*P P
%D f^*P P{}
%D @ 0 @ 1 <-> @ 1 @ 4 <->
%D @ 2 @ 5 <->
%D @ 0 @ 3 <-|
%D @ 1 @ 2 <-| @ 2 @ 3 <-|
%D @ 4 @ 5 <-|
%D ))
%D (( A B -> .plabel= a f
%D B B{} -> .plabel= a \id
%D ))
%D enddiagram
%D diagram indexed-cat-3
%D 2Dx 100 +35 +30
%D 2D 100 (\id;f)^*P
%D 2D
%D 2D +20 \id^*f^*P f^*P P
%D 2D
%D 2D +20 f^*P{}
%D 2D
%D 2D +20 A A{} B
%D 2D
%D (( (\id;f)^*P
%D \id^*f^*P f^*P P
%D f^*P{}
%D @ 0 @ 1 <-> @ 1 @ 4 <->
%D @ 3 @ 5 <->
%D @ 0 @ 3 <-|
%D @ 1 @ 2 <-| @ 2 @ 3 <-|
%D ))
%D (( A A{} -> .plabel= a \id
%D A{} B -> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{indexed-cat-3} \qquad \diag{indexed-cat-2}$$
\msk
$$\diag{indexed-cat-1}$$
% --------------------
% «proto-cart-morphs» (to ".proto-cart-morphs")
% (subsec "Cartesian Morphisms" "proto-cart-morphs")
\mysubsection {Cartesian Morphisms} {proto-cart-morphs}
A ``vee'' in a category $\bbA$ is a pair of maps $(h:A \to C, \, g:B
\to C)$ with the same codomain; we will draw vees as:
%
%D diagram vee-1
%D 2Dx 100 +15 +15
%D 2D 100 A B
%D 2D
%D 2D +20 C
%D 2D
%D (( A C -> .plabel= l h
%D B C -> .plabel= r g
%D ))
%D enddiagram
%
%D diagram vee-2
%D 2Dx 100 +15 +20
%D 2D 100 A
%D 2D
%D 2D +20 B C
%D 2D
%D (( A C -> .plabel= a h
%D B C -> .plabel= b g
%D ))
%D enddiagram
%
$$\diag{vee-1} \qquad \text{or as:} \quad \diag{vee-2} \quad \text{.}$$
A {\sl completion} for a vee $(h:A \to C, \, g:B \to C)$ is a map $f:
A \to B$ such that $f;g=h$. Let's draw the set of all completions for
the vee $(h:A \to C, \, g:B \to C)$ as this:
%
%D diagram all-completions-1
%D 2Dx 100 +15 +20
%D 2D 100 A
%D 2D
%D 2D +20 B C
%D 2D
%D (( A C -> .plabel= a h
%D B C -> .plabel= b g
%D A B --> .plabel= l f
%D ))
%D enddiagram
%
%D diagram all-completions-2
%D 2Dx 100 +15 +20
%D 2D 100 FA
%D 2D
%D 2D +20 FB FC
%D 2D
%D (( FA FC -> .plabel= a Fh
%D FB FC -> .plabel= b Fg
%D FA FB --> .plabel= l f'
%D ))
%D enddiagram
%
$$\diag{all-completions-1} \qquad .$$
The standard notation for that, using slice categories (see
\cite{BarrWells}, p.3, or \cite{Awodey}, p.15), would be:
%
$$\Hom_{\bbA/C}(h:A \to C, \, g:B \to C).$$
% (find-awodeyctpage (+ 10 15) "slice category")
% (find-tttpage (+ 13 3) "slice category")
A functor $F: \bbA \to \bbB$ takes vees in $\bbA$ to vees in $\bbB$,
%
$$(h:A \to C, \, g:B \to C) \; \mto \; (Fh:FA \to FC, \, Fg:FB \to FC)$$
%
and induces functions from sets of completions to sets of completions:
%
%D diagram F-on-completions
%D 2Dx 100 +85 +70
%D 2D 100 \usebox{\myboxa} {f:A->B} f
%D 2D
%D 2D +45 \usebox{\myboxb} {f':FA->FB} Ff
%D 2D
%D (( \usebox{\myboxa} \usebox{\myboxb} ->
%D {f:A->B} .tex= \sst{f:A->B}{f;g=h}
%D {f':FA->FB} .tex= \sst{f':FA->FB}{f';Fg=Fh}
%D ->
%D f Ff |->
%D ))
%D enddiagram
%D
$$\savebox{\myboxa}{$\diag{all-completions-1}$}
\savebox{\myboxb}{$\diag{all-completions-2}$}
\diag{F-on-completions}
$$
\def\pdiag#1{\diag{#1}}
\def\pdiag#1{\left(\diag{#1}\right)}
When a map $\pdiag{all-completions-1} \to \pdiag{all-completions-2}$
is a bijection there is a unique completion $f: A \to B$ corresponding
to each completion $f': FA \to FB$. We will then say that this $f$ is
the {\sl lifting} of the corresponding $f'$, and we will say that the
vee $(h,g)$ {\sl has unique liftings} (for the functor $F$; but let's
think of $F$ as fixed).
When a map $g:B \to C$ has the property that all vees of the form
$(h,g)$ have unique liftings --- note that this must hold for all
possible choices of domains for $h$, i.e., now the `$A$' is free ---
then we will say that $g$ is {\sl cartesian}. This property is not so
rare as it might seem.
{\sl Fact.} If $F: \Set^\to \to \Set$ is the ``codomain'' functor,
$\Cod$, then pullbacks in $\Set$ --- regarded as morphisms in
$\Set^\to$ --- are cartesian morphisms for $F$.
The diagram below is the core of the proof. Each completion $(f',f)$
``above'' is mapped to a completion $f$ ``below''; each completion $f$
below lifts to a completion $(\ang{a;f,h'},f)$ above.
%
\def\poo#1#2#3{\begin{pmatrix}
#1 \\
\scriptstyle{#2} \dnto \phantom{\scriptstyle{#2}} \\
#3 \\
\end{pmatrix}
}
\def\poom#1#2{(#1,#2)}
\def\poom#1#2{\begin{smallmatrix}#1,\\#2\end{smallmatrix}}
\def\poom#1#2{\left(\begin{smallmatrix}#1,\\#2\end{smallmatrix}\right)}
\def\poom#1#2{\begin{smallmatrix}#1\\#2\end{smallmatrix}}
%
%D diagram pullbacks-are-cartesian
%D 2Dx 100 +40 +50
%D 2D 100 AA
%D 2D
%D 2D +30 BB CC
%D 2D
%D 2D +15 A
%D 2D
%D 2D +30 B C
%D 2D
%D (( AA .tex= \poo{A'}{a}{A}
%D BB .tex= \poo{B×_{C}C'}{\pi}{B}
%D CC .tex= \poo{C'}{c}{C}
%D AA BB -> .plabel= l \poom{\ang{a;f,h'}}{f}
%D BB CC -> .plabel= b \poom{\pi'}{g}
%D AA CC -> sl^^ .plabel= a \poom{h'}{h}
%D A B -> .plabel= l f
%D B C -> .plabel= b g
%D A C -> .plabel= a h
%D ))
%D enddiagram
%D
$$\diag{pullbacks-are-cartesian}$$
% --------------------
% «proto-cleavages» (to ".proto-cleavages")
% (subsec "Cleavages" "proto-cleavages")
\mysubsection {Cleavages} {proto-cleavages}
Now let's clean up the notation. The functor $F: \bbA \to \bbB$ will
become the ``projection functor'' $p: \bbE \to \bbB$, going from the
``entire category'' $\bbE$ to the ``base category''. Projection
functors are just normal functors, but they are downcased in a funny
way, as we shall see soon.
The objects of $\bbB$ will be called $A$, $B$, $C$, $D$, $\ldots$. the
objects of $\bbE$ will be called $P$, $Q$, $R$, $S$, $\ldots$; in the
archetypal case --- namely, $p \equiv \Cod: \Sub(\Set) \to \Set$ ---
they will stand for {\sl propositions} over {\sl sets}. For example,
an object $Q$ of $\bbE$ over an object $B$ of $\bbB$ will stand for
the subobject $\sst{bÝB}{Q(b)} \monicto B$:
%
%D diagram p-on-subobjs
%D 2Dx 100 +70
%D 2D 100 \Sub(\Set) Q
%D 2D
%D 2D +20 \Set pQ=\Cod"Q=B
%D 2D
%D (( \Sub(\Set) \Set |-> .plabel= l p==\Cod
%D Q .tex= Q==(\sst{bÝB}{Q(b)}>->B)
%D pQ=\Cod"Q=B |->
%D ))
%D enddiagram
%D
$$\diag{p-on-subobjs}$$
An object $Q$ of $\bbE$ is said to be {\sl over} its projection $pQ$;
similarly, morphisms in $\bbE$ are said to be {\sl over} their images.
For each object $B$ of $\bbB$ the subcategory of $\bbE$ formed by the
objects and morphisms over $B$ and $\id_B$ is called the {\sl fiber
over $B$}, and denoted by $\bbE_B$. Also, we will tend to draw
objects and morphisms of $\bbE$ over their images and omit the funtor
arrows for $p$. So
%
%D diagram p-omit-1
%D 2Dx 100 +30
%D 2D 100 Q --> R
%D 2D
%D 2D +20 B --> C
%D 2D
%D (( Q R -> .plabel= a g'
%D B C -> .plabel= a g
%D ))
%D enddiagram
%
%D diagram p-omit-2
%D 2Dx 100 +45 +25
%D 2D 100 Q ----> R \bbE
%D 2D
%D 2D +20 B=pQ --> C=pR \bbB
%D 2D
%D (( Q R -> .plabel= a g'
%D B=pQ C=pR -> .plabel= a g=pg'
%D Q B=pQ |-> R C=pR |->
%D \bbE \bbB -> .plabel= r p
%D ))
%D enddiagram
%
$$\diag{p-omit-1}
\qquad \text{is shorthand for} \quad
\diag{p-omit-2} \quad .
$$
Morphisms in a fiber are said to be {\sl vertical}.
\msk
A {\sl cleavage} for a projection funtor $p$ is a pair of operations,
$(·^*, \ov·)$, that produces, for each morphism $g: B \to C$ in $\bbB$
and for each $R$ in $\bbE$ over $C$, a cartesian morphism $\ov g_R:
g^*R \to R$ over $g$.
A {\sl cartesian lifting} for $g: B \to C$ at an object $R$ over $C$
is a cartesian morphism $Q \to R$ over $g$ with codomain $R$. A
cleavage $(·^*, \ov·)$ chooses a particular cartesian lifting for each
pair $(R,\, g:B \to pR)$.
A {\sl cloven fibration} is a projection functor $p: \bbE \to \bbB$
plus a cleavage $(·^*, \ov·)$. A {\sl fibration} is slightly less than
this: a projection functor $p:\bbE \to \bbB$ plus the guarantee that
each pair $(R,\, g:B \to pR)$ has at least one cartesian lifting.
We will not use ``plain'' fibrations here; cleavages are too
convenient.
\msk
The following fact may at first look too technical to be useful.
{\sl Fact (technical).} In a cloven fibration $p: \bbE \to \bbB$, for each object
$R$ in $\bbE$ the ``projection'' operation $p_R: \bbE/R \to \bbB/pR$
is left adjoint to the ``cartesian lifting'' operation $\ov·_R:
\bbB/pR \to \bbE/R$. In diagrams:
%D diagram p-|cart
%D 2Dx 100 +25 +20 +25 +30 +50
%D 2D 100 P -------\
%D 2D +10 \bbE/R -> v P->R ---> g^*R->R
%D 2D +10 |^ g^*R --> R - ^
%D 2D || | |
%D 2D +10 v| pP -------\ v -
%D 2D +10 \bbB/pR -> v pP->pR ---> B->pR
%D 2D +10 B --> pR
%D 2D
%D (( \bbE/R \bbB/pR
%D @ 0 @ 1 -> sl_ .plabel= l p_R
%D @ 0 @ 1 <- sl^ .plabel= r \ov·_R
%D ))
%D (( P g^*R R
%D pP B pR
%D @ 0 @ 1 --> .plabel= b f'
%D @ 1 @ 2 -> .plabel= b \ov"g_R
%D @ 0 @ 2 -> .plabel= a h'
%D @ 3 @ 4 --> .plabel= b f
%D @ 4 @ 5 -> .plabel= b g
%D @ 3 @ 5 -> .plabel= a ph'
%D
%D ))
%D (( P->R .tex= (P->^{h'}R) g^*R->R .tex= (g^*R->^{\ov"g_R}R)
%D pP->pR .tex= (pP->^{ph'}pR) B->pR .tex= (B->^{g}pR)
%D @ 0 @ 1 -> .plabel= a f'
%D @ 0 @ 2 |-> .plabel= l p_R
%D @ 1 @ 3 |-> .plabel= r \ov·_R
%D @ 2 @ 3 -> .plabel= b f
%D @ 0 @ 3 varrownodes nil 20 nil |-> sl_ .plabel= l \flat
%D @ 0 @ 3 varrownodes nil 20 nil <-| sl^ .plabel= r \sharp
%D ))
%D enddiagram
%D
$$\diag{p-|cart}$$
The transposition `$\flat$' is a familiar operation: it take each $f'$
to its projection $pf'$. The inverse transposition, `$\sharp$', is
something new, and extremely important --- it factors $h'$ through the
cartesian morphism $\ov g_R$, returning a morphism $f'$ over $f$.
In a vee $(h':P \to R,\, g':Q \to R)$ over $(h:A \to C,\, g:B \to C)$
in which $g'$ is cartesian each completion $f:A \to B$ of the lower
vee lifts in a unique way to a completion $f':P \to Q$ of the upper
vee. When the upper vee is clear from the context we will denote this
$f'$ by $f^\sharp$, and we will call $f^\sharp$ the ``factorization of
$h'$ through $g'$ (over $f$)''. Note that here $g'$ is any cartesian
morphism --- not necessarily one returned by the cleavage.
%D diagram cart-factorization
%D 2Dx 100 +20 +25
%D 2D 100 P -------\
%D 2D +10 -> v
%D 2D +10 Q ---> R
%D 2D
%D 2D +10 A -------\
%D 2D +10 -> v
%D 2D +10 B ---> C
%D 2D
%D (( P Q --> .plabel= l f^\sharp
%D Q R -> .plabel= b g'
%D P R -> .plabel= a h'
%D A B -> .plabel= l f
%D B C -> .plabel= b g
%D A C -> .plabel= a h
%D ))
%D enddiagram
%D
$$\diag{cart-factorization}$$
For any morphism $g:B \to C$ in the base, the operation $R \mto g^* R$
given by the cleavage is the action of a functor on objects. To
construct the action of the functor $g^*:\bbE_C \to \bbE_B$ on
morphisms we use the factorization `$\sharp$': if $r:R' \to R$ is a
morphism in $\bbE_C$, then $g^*r: g^*R' \to g^*R$ is the factorization
of $\ov g_{R'};r$ through $\ov g_R$ (over $\id_B$).
%D diagram g*-on-morphisms
%D 2Dx 100 +40
%D 2D 100 g^*R' R'
%D 2D
%D 2D +25 g^*R R
%D 2D
%D 2D +15 B C
%D 2D
%D (( g^*R' R' g^*R R
%D @ 0 @ 1 -> .plabel= a \ov"g_{R'}
%D @ 0 @ 2 -> .plabel= l \sm{g^*R\;:=\\{\id_B}^\sharp}
%D @ 1 @ 3 -> .plabel= r r
%D @ 2 @ 3 -> .plabel= a \ov"g_{R}
%D B C -> .plabel= a g
%D ))
%D enddiagram
%D
$$\diag{g*-on-morphisms}$$
Each $g^*$ turned out to be a functor; it turns also out that each
$\ov g$ is a natural transformation. More precisely: for each morphism
$g:B \to C$ in the base the operation $R \mto (g^*R \ton{\ov g_R} \ov
g)$ is the action of a natural transformation $\ov g$ from $g^*:
\bbE_C \to \bbE_B$ to $\id_{\bbE_C}: \bbE_C \to \bbE_C$.
% --------------------
% «proto-cleavages-2» (to ".proto-cleavages-2")
% (subsec "Proto-cleavages" "proto-cleavages-2")
\mysubsection {Proto-cleavages} {proto-cleavages-2}
Let's see what all this becomes in the syntactical world.
A {\sl proto-vee} is just a vee.
A {\sl proto-completion} for a vee $(h:A \to C,\, g:B \to C)$ is just
a morphism $f:A \to B$.
A morphism $f':P \to Q$ is {\sl proto-above} a morphism $f:A \to B$ if
$pP=A$ and $pQ=B$. This is like being above, but here we check only
the domain and the codomain; the condition $pf'=f$ has been dropped.
The condition of ``having unique liftings'' for a vee becomes an
operation in the syntactical world: a proto-inverse for the (...)
\msk
A {\sl vee with proto-unique liftings} is a vee $(h:A \to C,\, g:B \to
C)$ plus an operation that takes each proto-completion $f'$ of $(Fh:FA
\to FC,\, Fg:FB \to FC)$ to a proto-completion $f$ of $(h:A \to C,\,
g:B \to C)$. Note that there may be many more proto-completions of
$(Fh,Fg)$ than completions. We may draw a proto-unique lifiting for
$(h,g)$ as
%
$$\pdiag{all-completions-1} \ot \pdiag{all-completions-2}$$
%
i.e., as a proto-inverse for the natural arrow `$\to$' from the first
set of proto-completions to the second.
A {\sl proto-cartesian arrow} $g:B \to C$ is an arrow $g: B \to C$
plus an operation
%
$$(A,\, A \ton{h}C) \mto (\pdiag{all-completions-1} \ot \pdiag{all-completions-2})$$
%
that takes the each possible other leg for the vee and returns a
corresponding proto-unique lifting.
A {\sl proto-projection functor} is just a proto-functor.
A {\sl proto-cleavage} for a proto-projection functor $p:\bbE \to
\bbB$
[Missing: proto-above]./
% --------------------
% «proto-change-of-base» (to ".proto-change-of-base")
% (subsec "Change-of-Base Functors" "proto-change-of-base")
\mysubsection {Change-of-Base Functors} {proto-change-of-base}
% --------------------
% «proto-fibers» (to ".proto-fibers")
% (subsec "The Logical Structure in Each Fiber" "proto-fibers")
\mysubsection {The Logical Structure in Each Fiber} {proto-fibers}
% --------------------
% «proto-preservations» (to ".proto-preservations")
% (subsec "Preservations" "proto-preservations")
\mysubsection {Preservations} {proto-preservations}
For $f:A \to B$ a morphism in the base category and $P$, $Q$, $R$
objects over $B$:
%:
%: f f
%: ===========\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
%:
$$\index{preservation!of `true'!rules}
\ded{Ptruenat-short-std} \qquad \ded{Ptrue-std}
$$
$$\index{preservation!of `and'!rules}
\ded{Pandnat-short-std} \qquad \ded{Pand-std}
$$
$$\index{preservation!of `implies'!rules}
\ded{Pimpnat-short-std} \qquad \ded{Pimp-std}
$$
%D diagram Ptrue-std
%D 2Dx 100 +30
%D 2D 100 T0 <==== T1
%D 2D -
%D 2D |
%D 2D v
%D 2D +20 T2
%D 2D
%D 2D +15 ta |---> tb
%D 2D
%D (( T0 .tex= f^*§_B T1 .tex= §_B
%D T2 .tex= §_A
%D ta .tex= A tb .tex= B
%D T0 T1 <-|
%D T0 T2 -> sl_ .plabel= l \Ptruenat
%D T0 T2 <- sl^ .plabel= r \Ptrue
%D ta tb -> .plabel= a f
%D ))
%D enddiagram
%:
%: B
%: ---§
%: f §_B
%: ------·^*
%: f^*§_B
%: -----------!
%: f^*§_B|-§_A
%:
%: ^Ptruenat-std
%D diagram Pand-std
%D 2Dx 100 +45 +45
%D 2D 100 A0 <============ A1
%D 2D ^ ^ ^
%D 2D | \ <-| |
%D 2D - - -
%D 2D +20 A2 <--| A3 <==== A4
%D 2D - - -
%D 2D | / <-| |
%D 2D v v v
%D 2D +20 A5 <============ A6
%D 2D
%D 2D +15 aa |-----------> ab
%D 2D
%D (( A0 .tex= f^*P A1 .tex= P
%D A2 .tex= f^*P&f^*Q A3 .tex= f^*(P&Q) A4 .tex= P&Q
%D A5 .tex= f^*Q A6 .tex= Q
%D aa x+= 10 .tex= A ab .tex= B
%D A0 A1 <-|
%D A0 A2 <- A0 A3 <-
%D A1 A4 <-
%D A0 A3 midpoint A1 A4 midpoint harrownodes nil 20 nil <-|
%D A2 A3 <- sl^ .plabel= a {î} A2 A3 -> sl_ .plabel= b \Pand A3 A4 <-|
%D A2 A5 -> A3 A5 ->
%D A4 A6 ->
%D A3 A5 midpoint A4 A6 midpoint harrownodes nil 20 nil <-|
%D A5 A6 <-|
%D aa ab -> .plabel= a f
%D ))
%D enddiagram
%:
%: P Q P Q
%: ------ -----'
%: f P∧Q|-P P∧Q|-Q
%: -------------·^* -------------·^*
%: f^*(P∧Q)|-f^*P f^*(P∧Q)|-f^*Q
%: ----------------------------------\ang{,}
%: f^*(P∧Q)|-f^*P∧f^*Q
%:
%: ^Pandnat-std
Here is the construction for $\Ptruenat$:
%
$$\index{preservation!of `true'!standard diagram}
\diag{Ptrue-std}
\qquad \qquad
\index{preservation!of `true'!standard tree}
\cded{Ptruenat-std}
$$
% Where $\Ptruenat$, $\Pandnat$, $\Pimpnat$ are:
Here is the construction for $\Pandnat$:
%
$$\index{preservation!of `and'!standard diagram}
\diag{Pand-std}
\qquad
\index{preservation!of `and'!standard tree}
\cded{Pandnat-std}
$$
%D diagram Pimp-std
%D 2Dx 100 +60 +55 +60
%D 2D 100 B0 <-> B0' <============== B1
%D 2D -/\ -/\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\==================== B3 \\
%D 2D \\ \\ \\ \\
%D 2D +25 \\ B4 <===================== B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \/v Vv
%D 2D +20 B6 B7
%D 2D
%D 2D +0 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= f^*(P⊃Q)&f^*P B0' .tex= f^*((P⊃Q)&P) B1 .tex= (P⊃Q)&P
%D B2 .tex= f^*Q B3 .tex= Q
%D B4 .tex= f^*(P⊃Q) B5 .tex= P⊃Q
%D B6 .tex= f^*P⊃f^*Q B7 .tex= P⊃Q
%D B0 B0' <- sl^ .plabel= a {î}
%D B0 B0' -> sl_ .plabel= b ÐP&
%D B0' B1 <-| B0 B2 -> B0' B2 -> B1 B3 -> B2 B3 <-|
%D B0 B4 <-| B2 B6 |->
%D B1 B5 <-| B3 B7 |->
%D B4 B5 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l î B4 B6 <- sl^ .plabel= r ÐP⊃
%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 b2 midpoint .TeX= A b1 b3 midpoint .TeX= B -> .plabel= a f
%D ))
%D enddiagram
%:
%: Q R
%: ----⊃
%: Q⊃R
%: ---\id
%: Q R Q⊃R|-Q⊃R
%: -----⊃ --------\Uncur
%: f Q⊃R Q f (Q⊃R)∧Q|-R
%: ---------------------------\Pand ------------·^*
%: f^*(Q⊃R)∧f^*Q|-f^*((Q⊃R)∧Q) f^*((Q⊃R)∧Q)|-f^*R
%: ------------------------------------------------------;
%: f^*(Q⊃R)∧f^*Q|-f^*R
%: -------------------\Cur
%: f^*(Q⊃R)|-f^*Q⊃f^*R
%:
%: ^Pimpnat-std
%:
%:
And here is the construction for $\Pimpnat$. Note that it uses
$\Pand$.
%
$$\index{preservation!of `implies'!standard diagram}
\diag{Pimp-std}
$$
$$\index{preservation!of `implies'!standard tree}
\ded{Pimpnat-std}
$$
% --------------------
% «proto-frobenius» (to ".proto-frobenius")
% (subsec "Frobenius" "proto-frobenius")
\mysubsection {Frobenius} {proto-frobenius}
For $f:A \to B$ a morphism in the base category, $P$ an object over
$A$ and $Q$ an object over $B$:
%:
%: 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{Frobnat-short-std} \qquad \ded{Frob-std}$$
How to build $\Frobnat$:
%
%D diagram Frob-std
%D 2Dx 100 +45 +35 +10
%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 ((
%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 B1 |-> B2 B0 -> B3 B1 -> B3' B1 ->
%D B4 B5 <-| B2 B4 -> B3 B5 -> B3' B5 ->
%D B2 B3 |-> B3 B3' -> sl^ .plabel= a î 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 .tex= A b1 .tex= B b0 b1 -> .plabel= a f
%D ))
%D enddiagram
%
$$\index{Frobenius!generic!standard diagram}
\diag{Frob-std}
$$
%:
%: f Q f Q
%: ---·^* ----·^*
%: 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
%:
$$\index{Frobenius!generic!tree}
\ded{Frobnat-std}
$$
% --------------------
% «proto-BCC» (to ".proto-BCC")
% (subsec "Beck-Chevalley" "proto-BCC")
\mysubsection {Beck-Chevalley} {proto-BCC}
% (to "dn-bcc-for-exists")
For any arrows $c:C \to B$ and $f:A \to B$, arrows $c'$ and $f'$
completing a pullback in the base category, and any object $P$ over
$C$:
%:
%: c f c' f' P c f c' f' P
%: ===========================\BCCLnat ---------------------------\BCCL
%: Î_{c'}f^{\prime*}P|-f^*Î_cP f^*Î_cP|-Î_{c'}f^{\prime*}P
%:
%: ^BCCL-short-std ^BCCL-std
%:
%: c f c' f' P c f c' f' P
%: ===========================\BCCRnat ---------------------------\BCCR
%: f^*ý_cP|-ý_{c'}f^{\prime*}P ý_{c'}f^{\prime*}P|-f^*ý_cP
%:
%: ^BCCR-short-std ^BCCR-std
%:
$$\ded{BCCL-short-std} \qquad \ded{BCCL-std}$$
$$\ded{BCCR-short-std} \qquad \ded{BCCR-std}$$
The following diagram shows how to build the $\BCCLnat$ arrow:
% (and also the $\BCCeqnat$ arrow --- see the sections
% \ref{dn-bcc-for-exists} and \ref{dn-bcc-for-equality})
%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= c^{\prime*}f^*Î_cP B2' .tex= f^{\prime*}c^*Î_cP B3 .tex= c^*Î_cP
%D B4 .tex= Î_{c'}f^{\prime*}P B5 .tex= Î_cP
%D B6 .tex= f^*Î_cP B7 .tex= Î_cP
%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= A×_{B}C b1 .tex= C b2 .tex= A b3 .tex= B
%D b0 b1 -> .plabel= b f'
%D b0 b2 -> .plabel= l c'
%D b1 b3 -> .plabel= r c
%D b2 b3 -> .plabel= b f
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$% \index{Beck-Chevalley!for `exists'!standard diagram}
% \index{Beck-Chevalley!for equality!standard diagram}
\index{Beck-Chevalley!left!standard diagram}
\diag{BCCL-std}
$$
%D diagram BCCR-std
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <-> B0' <============== B1
%D 2D -/\ -/\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\==================== B3 \\
%D 2D \\ \\ \\ \\
%D 2D +15 \\ B4 <===================== B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \/v Vv
%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= c^{\prime*}f^*ý_cP B0' .tex= f^{\prime*}c^*ý_cP B1 .tex= c^*ý_cP
%D B2 .tex= f^{\prime*}P B3 .tex= P
%D B4 .tex= f^*ý_cP B5 .tex= ý_cP
%D B6 .tex= ý_{c'}f^{\prime*}P B7 .tex= ý_cP
%D B0 B0' <-> B0' B1 <-| B0 B2 -> B0' B2 -> B1 B3 -> B2 B3 <-|
%D B0 B4 <-| B2 B6 |->
%D B1 B5 <-| B3 B7 |->
%D B4 B5 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l î B4 B6 <- sl^ .plabel= r \BCCR
%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= A×_{B}C b1 .tex= C b2 .tex= A b3 .tex= B
%D b0 b1 -> .plabel= b f'
%D b0 b2 -> .plabel= l c'
%D b1 b3 -> .plabel= r c
%D b2 b3 -> .plabel= a f
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\index{Beck-Chevalley!right!standard diagram}
\diag{BCCR-std}
$$
%:
%: P c
%: ----Î_0
%: Î_cP
%: ----\id
%: Î_cP|-Î_cP
%: ----------Î^\sharp
%: f' P|-c^*Î_cP (f';c)=(c';f) Î_cP
%: --------------------------------·^* ======================================
%: f^{\prime*}P|-f^{\prime*}c^*Î_cP f^{\prime*}c^*Î_cP|-c^{\prime*}f^*Î_cP
%: ---------------------------------------------------------------------------;
%: f^{\prime*}P|-c^{\prime*}f^*Î_cP
%: --------------------------------Î^\flat
%: Î_{c'}f^{\prime*}P|-f^*Î_cP
%:
%: ^BCCLnat-std
%:
%: P c
%: ----ý_0
%: ý_cP
%: ----\id
%: ý_cP|-ý_cP
%: ----------ý^\flat
%: (f';c)=(c';f) ý_cP f' c^*ý_cP|-P
%: ====================================== --------------------------------·^*
%: c^{\prime*}f^*ý_cP|-f^{\prime*}c^*ý_cP f^{\prime*}c^*ý_cP|-f^{\prime*}P
%: ------------------------------------------------------------------------;
%: c^{\prime*}f^*ý_cP|-f^{\prime*}P
%: --------------------------------ý^\sharp
%: f^*ý_cP|-ý_{c'}f^{\prime*}P
%:
%: ^BCCRnat-std
%:
$$\index{Beck-Chevalley!left!standard tree}
\ded{BCCLnat-std}
$$
$$\index{Beck-Chevalley!right!standard tree}
\ded{BCCRnat-std}
$$
% --------------------
% «proto-adjs-to-cobs» (to ".proto-adjs-to-cobs")
% (subsec "Adjoints to Change-of-Base Functors" "proto-adjs-to-cobs")
\mysubsection {Adjoints to Change-of-Base Functors} {proto-adjs-to-cobs}
% --------------------
% «dn-intro» (to ".dn-intro")
% (chap "Downcasing Types" "dn-intro")
\mychapter {Downcasing Types} {dn-intro}
% --------------------
% «dn-simple» (to ".dn-simple")
% (sec "Simple Proofs" "dn-simple")
\mysection {Simple Proofs} {dn-simple}
In the BHK interpretation propositions $P$, $Q$ $R$ are seen as the
sets of their proofs, and a proof of $P∧Q$ is a pair made of a proof
of $P$ and a proof of $Q$ and a proof of $P⊃Q$ is a function that
receives proofs of $P$ and returns proofs of $Q$.
As $P$, $Q$ and $R$ are sets the default choices for names of
variables ranging over them are $p$, $q$ and $r$. Let's forget
temporarily the syntactical distinctions between variables and terms,
and let their names also stand for names when needed; also, let's
allow ``long names'': ``$p,q$'' will be our default choice of name for
a term or variable whose type is $P×Q = P∧Q$, ``$p \mto q$'' the
default for a term or variable in $P \to Q = Q^P = P⊃Q$. We call the
passage from $P∧Q \to R$ to $p,q \mto r$ ``downcasing'', and the
opposite direction ``uppercasing''.
The tree at the left below is a proof of $Q⊃R \vdash P∧Q ⊃ P∧R$ in
Natural Deduction; the tree at the right is its downcasing,
%:
%: [P∧Q]^1 [p,q]^1
%: ------- -------
%: [P∧Q]^1 Q Q⊃R [p,q]^1 q q|->r
%: ------- --------- ------- ---------
%: P R p r
%: --------------- ---------------
%: P∧R p,r
%: -------1 -------1
%: P∧Q⊃P∧R p,q|->p,r
%:
%: ^foo1 ^foo2
%:
$$\ded{foo1} \qquad \ded{foo2}$$
%
and we may interpret each of its bars in a way that parallels the
logic: for example,
%:
%: Q Q⊃R
%: ------
%: R
%:
%: ^foo3
%:
$$\ded{foo3}$$
%
can be read as: ``if we know that $Q$ and that $Q⊃R$ (i.e., that both
$Q$ and $Q⊃R$ are true) then we know that $R$ (is true too)''; in the
downcased tree, this is: ``if we know $q$ and $q \mto r$ (in the sense
that we have values/definitions/meanings for these terms, i.e., we
know that their corresponding types are inhabited), then we know $r$
(we have a ``natural definition'' for an $r:R$ in terms $q$ and $q
\mto r$, and so we know that $R$ is inhabited)''.
The downcased tree induces these definitions:
%
$$\begin{array}{rcl}
p &:=& \pi \, (p,q) \\
q &:=& \pi' \, (p,q) \\
r &:=& (q \mto r) \, q \\
p,r &:=& \ang{p,r} \\
p,q \mto p,r &:=& ð(p,q)¨(P∧Q).\ang{p,r} \\
\end{array}
$$
%
and we can formalize this in Coq as:
%
$$(...)$$
The ``$\angg{\ldots}$''s above are long names, in their ascii form. A
simple preprocessor reads files with these ``$\angg{\ldots}$''s and
converts them to tokens that Coq can treat, like:
$$(...)$$
The same translator generates another kind of output, in which a few
ascii abbreviations within ``$\angg{\ldots}$''s are expanded, ---
`\verb.|->.' becomes `\verb.\mapsto .', etc; we can add more, and the
result of these expansions is treated as \LaTeX{} input in
mathematical mode, and the rest is typeset in verbatim mode. By \LaTeX
ing this output we get:
$$(...)$$
We will use this pretty-printed representation in this paper. Note
that we can put arbitrary \TeX{} code in long names --- even macros
that generate diagrams.
If $A$, $B$, $C$ are sets, a similar downcasing interprets:
%:
%: [a,b]^1 [p:A×B]^1
%: ------- ---------
%: [a,b]^1 b b|->c [p:A×B]^1 'p:B f:B->C
%: ------- --------- --------- ----------------
%: a c p:A f('p):C
%: --------------- -----------------------
%: a,c \ang{p,f('p)}:A×C
%: -------1 --------------------
%: a,b|->a,c ðp:A×B.\ang{p,f('p)}:A×B->A×C
%:
%: ^bar1 ^bar2
%:
$$\ded{bar1} \qquad \ded{bar2}$$
% --------------------
% «dn-functors» (to ".dn-functors")
% (sec "Functors" "dn-functors")
\mysection {Functors} {dn-functors}
Now fix a set $A$. The functor $(A×):\Set \to \Set$ takes each set $B$
to the set $A×B$, and each function $f:B \to C$ to $(A×)f:A×B \to
A×C$, where $(A×)f = ðp:A×B.\ang{p,f('p)}$.
We downcase the diagram of the functor,
%
%D diagram functor1
%D 2Dx 100 +30
%D 2D 100 B |---> A×B
%D 2D | |
%D 2D | |-> |
%D 2D v v
%D 2D +30 C |---> A×C
%D 2D
%D (( B A×B C A×C
%D @ 0 @ 1 |-> .plabel= a A×
%D @ 2 @ 3 |-> .plabel= b A×
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D @ 0 @ 2 -> .plabel= l f
%D @ 1 @ 3 -> .plabel= r \sm{(A×)f\;:=\hfill\\ðp:A×B.\ang{p,f('p)}}
%D ))
%D enddiagram
%D
$$\diag{functor1}$$
%
as:
%
%D diagram downfunctor1
%D 2Dx 100 +30
%D 2D 100 b ===> a,b
%D 2D
%D 2D +30 c ===> a,c
%D 2D
%D (( b a,b c a,c
%D @ 0 @ 1 => @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$\diag{downfunctor1}$$
We use the arrow `$\funto$' for functors to suggest that functors have
two actions --- one on objects, one on morphisms.
It is also useful to think that a functor $b \funto a,b$ has a
``syntactical action'', which is to prepend an `$a,$' to the names of
objects. The functor $b \funto a,b$ takes the ``space of `$b$'s'' to
the ``space of `$a,b$'s'', and takes each arrow $b \mto c$ to an arrow
$a,b \mto a,c$ (here we applied its syntactical action to both the
source and the target).
% --------------------
% «dn-cats» (to ".dn-cats")
% (sec "Categories" "dn-cats")
\mysection {Categories} {dn-cats}
Now let $A$, $B$, $C$ be objects in a category $\catC$ --- which no
longer needs to be $\Set$. If $\catC$ has products, we can speak of
objects $A×B$ and $A×C$, and now we have:
$$b \mto c : B \to C = \Hom_\catC(B, C)$$
$$a,b \mto a,c : A×B \to A×C = \Hom_\catC(B, C)$$
We still have a construction for $a,b \to a,c$ starting from $b \mto
c$, but now it's a different one:
%:
%: A B
%: -------\pi'
%: A B a,b|->b b|->c
%: -------\pi ------------------;
%: a,b|->a a,b|->c
%: --------------------
%: a,b|->a,c
%:
%: ^bla1
%:
%: A B
%: --------------
%: A B '_{AB}:A×B->B f:B->C
%: ------------- -----------------------
%: _{AB}:A×B->A '_{AB};f:A×B->C
%: -----------------------------------
%: A×f:=\ang{_{AB},'_{AB};f}:A×B->A×C
%:
%: ^bla2
%:
$$\ded{bla1}$$
%
that uppercases to:
%
$$\ded{bla2}$$
Note that if someone says ``take {\sl the} functor whose downcasing is
$b \funto a,b$'' then we just have to understand its action on objects
(which is $A×$) and its action on morphisms (that we have just
constructed, in slightly different ways, in $\Set$ and in $\catC$);
the other person is assuring us, through the ``the'', that these
actions exist, are not too hard to find, are functorial, and are
well-defined; if we were just conjecturing that a functor named ``$b
\funto a,b$'' should exist we would have to do all the steps. And in
the syntactical world some of the steps --- functoriality,
well-definedness --- are simply not relevant; the introduction of the
syntactical world permits stating results that are mathematical
precise and coherent doing only a fraction of the work that is needed
for results in the real world --- and proving functorialities,
naturalities, etc, can be seen as a separate step.
% --------------------
% «dn-pseudopoints» (to ".dn-pseudopoints")
% (sec "Pseudopoints" "dn-pseudopoints")
\mysection {Pseudopoints} {dn-pseudopoints}
If $\catC$ is an arbitrary category with finite products and $A$, $B$,
$C$ are objects of $\catC$ then we have clear meanings for $b \mto c$
and $a,b \mto a,c$ --- as seen above --- but what are ``$b$'',
``$a,b$'', etc? Does the typing $a:A$ mean something?
One solution is to say that `$b$', `$a,b$', etc are ``pseudopoints'',
and treat them as syntactical devices that we can use in building
larger expressions, which do have meaning (or: ``have semantics'' ---
$b \mto c$ and $a,b \mto a,c$ have semantics because they can appear
in the Coq code as variables, constants or terms).
In the case where $A$, $B$ $C$ were sets we could say:
\msk
``$a$ is an element of $A$'',
``$A$ is the space of `$a$'s'',
``an `$a,b$' is a pair made of an `$a$' and a `$b$'\,'',
``$A×B$ is the space of `$a,b$'s'',
``a $b \mto c$ is a function that takes `$b$'s to `$c$'s''
(Note that we tend to use indefinite articles when we speak of
downcasings!)
\msk
but when $A$, $B$ and $C$ are objects of $\catC$ it is better to say:
\msk
``a $b \mto c$ is a morphism from $B$ to $C$'',
``$\Hom_\catC(B, C)$ is the space of `$b \mto c$'s'',
``$B$ is the object of `$b$'s'',
``$B×C$ is the object of `$b,c$'s'',
``a $b,c$ is a pseudopoint of $B×C$''.
\msk
So the idea of ``pseudopoints'' exists only to let us have a name for
the syntactical function of the `$a,b$' and the `$a,c$' in a morphism
$a,b \mto a,c$.
Pseudopoints may have a concrete semantics in the archetypal category
that motivates certain kinds of categories; but that will be treated
in section \_\_\_.
Here's one example in which pseudopoints have no reasonable semantics.
Let $A^\op$ and $B^\op$ be objects of $\Set^op$; an arrow $A^\op \to
B^\op$ is an arrow $B \to A$ in disguise. If we downcase $f:A^\op \to
B^\op$ to $a^\op \mto b^\op$, then what is an $a^\op$?
% (find-books "__cats/__cats.el" "kromer")
% (find-kromerpage (+ 34 83) "The diagrams incorporate a large amount of information.")
% (find-kromerpage (+ 34 152) "absence of elements" "painfully difficult")
% (find-kromerpage (+ 33 218) "objects cannot be penetrated")
% (find-angg ".emacs.papers" "freyd")
% (find-freydabcatspage (+ 27 9) "painfully difficult")
% (find-books "__cats/__cats.el" "mclarty")
% --------------------
% «dn-NTs» (to ".dn-NTs")
% (sec "Natural Transformations" "dn-NTs")
\mysection {Natural Transformations} {dn-NTs}
% --------------------
% «dn-adjunctions» (to ".dn-adjunctions")
% (sec "Adjunctions" "dn-adjunctions")
\mysection {Adjunctions} {dn-adjunctions}
% --------------------
% «dn-CCCs» (to ".dn-CCCs")
% (sec "CCCs" "dn-CCCs")
\mysection {CCCs} {dn-CCCs}
% http://en.wikipedia.org/wiki/Wreath_product
% (find-books "__cats/__cats.el" "lambek-scott")
% (find-lambekscottpage (+ 8 49) "the following two derived rules of inference")
These are the rules for both the ``big presentation'' and the ``short
presentation'' for CCCs. In the ``big presentation'' all the rules
below are primitive; in the ``short presentation'' only the ones with
a single bar are primitive, and the double bar rules are derived rules.
%:
%: B C B C B C a|-b a|-c b|-c b'|-c'
%: ----× ------ ------' ----------\ang{,} ============×_1
%: B×C b,c|-b b,c|-c a|-b,c b,b'|-c,c'
%:
%: ^CCC-shd-p1 ^CCC-shd-p2 ^CCC-shd-p3 ^CCC-shd-p4 ^CCC-shd-prod1
%:
%: B C B C a,b|-c a|-(b|->c) A B
%: ----"-> ------------\ev ----------\cur ==========\uncur ============\eta
%: B{->}C (b|->c),b|-c a|-(b|->c) a,b|-c a|-(b|->a,b)
%:
%: ^CCC-shd-e1 ^CCC-shd-e2 ^CCC-shd-e3 ^CCC-shd-uncur ^CCC-shd-eta
%:
%: b'|-b c|-c' a|-b a|-(b|->c)
%: ============{->}_1 ================\app
%: (b|->c)|-(b'|->c') a|-c
%:
%: ^CCC-shd-->1 ^CCC-shd-app
%:
%: A a|-b *|-(a|->b)
%: -1 ----! ==========\lnameof{} ==========\wr
%: 1 a|-* *|-(a|->b) a|-b
%:
%: ^CCC-shd-!1 ^CCC-shd-!2 ^CCC-shd-nameof ^CCC-shd-*app
%:
%:
$$\ded{CCC-shd-p1} \qquad \ded{CCC-shd-p2} \qquad \ded{CCC-shd-p3} \qquad \ded{CCC-shd-p4} \qquad \ded{CCC-shd-prod1}$$
$$\ded{CCC-shd-e1} \qquad \ded{CCC-shd-e2} \qquad \ded{CCC-shd-e3} \qquad \ded{CCC-shd-uncur} \qquad \ded{CCC-shd-eta}$$
$$\ded{CCC-shd-->1} \qquad \ded{CCC-shd-app}$$
$$\ded{CCC-shd-!1} \qquad \ded{CCC-shd-!2} \qquad \ded{CCC-shd-nameof} \qquad \ded{CCC-shd-*app}$$
Here's how to expand the derived rules:
%:
%: B C B C
%: ------ ------'
%: b,c|-b b|-b' b,c|-c c|-c'
%: --------------; --------------;
%: b,c|-b' b,c|-c'
%: -----------------------\ang{,}
%: b,c|-b',c'
%:
%: ^CCC-lod-prod1
%:
%: a|-(b|->c) B B C
%: ============== ------------\ev
%: a,b|-(b|->c),b (b|->c),b|-c
%: ------------------------------;
%: a,b|-c
%:
%: ^CCC-lod-uncur
%:
%: A B
%: ========
%: a,b|-a,b
%: ------------\cur
%: a|-(b|->a,b)
%:
%: ^CCC-lod-eta
%:
%: B C
%: ------"->
%: B{->}C b'|-b B C
%: ===================== ------------\ev
%: (b|->c),b'|-(b|->c),b (b|->c),b|-c c|-c'
%: ---------------------------------------------;;
%: (b|->c),b'|-c'
%: --------------\cur
%: (b|->c)|-(b'|->c')
%:
%: ^CCC-lod-->1
%:
%: a|-(b|->c) a|-b B C
%: ----------------\ang{,} ------------\ev
%: a|-(b|->c),b (b|->c),b|-c
%: --------------------------------------;
%: a|-c
%:
%: ^CCC-lod-app
%:
%: 1 A
%: ------'
%: *,a|-a a|-b
%: ------------;
%: *,a|-b
%: ----------\cur
%: *|-(a|->b)
%:
%: ^CCC-lod-nameof
%:
%: A A
%: ----! ----\id
%: a|-* a|-a *|-(a|->b)
%: -----------\ang{,} ========\uncur
%: a|-*,a *,a|-b
%: -------------------------
%: a|-b
%:
%: ^CCC-lod-*app
%:
%:
$$\def\foo#1#2{\ded{#1} &:=& \ded{#2} \\ \\}
\begin{array}{rcl}
\foo{CCC-shd-prod1} {CCC-lod-prod1}
\foo{CCC-shd-uncur} {CCC-lod-uncur}
\end{array}
$$
$$\def\foo#1#2{\ded{#1} &:=& \ded{#2} \\ \\}
\begin{array}{rcl}
\foo{CCC-shd-eta} {CCC-lod-eta}
\foo{CCC-shd-->1} {CCC-lod-->1}
\foo{CCC-shd-app} {CCC-lod-app}
\end{array}
$$
$$\def\foo#1#2{\ded{#1} &:=& \ded{#2} \\ \\}
\begin{array}{rcl}
\foo{CCC-shd-nameof} {CCC-lod-nameof}
\foo{CCC-shd-*app} {CCC-lod-*app}
\end{array}
$$
\bsk
% --------------------
% «dn-contexts» (to ".dn-contexts")
% (sec "Contexts" "dn-contexts")
\mysection {Contexts} {dn-contexts}
% --------------------
% «dn-contexts-single» (to ".dn-contexts-single")
% (subsec "Single Hypothesis: CCs" "dn-contexts-single")
\mysubsection {Single Hypothesis: CCs} {dn-contexts-single}
In a cartesian category we have a natural way to interpret judgments
involving only pairings and projections, like, for example,
$$p:A×B, q:A×C \vdash \ang{\ang{q,p},\ang{'p,'p}} : (A×A)×(B×B)$$
They become clearer with our long names and dictionaries:
$$(a,b):A×B, (a',c):A×C \vdash ((a',a),(b,b))$$
$$\begin{array}[t]{rcl}
p &\equiv& a,b \\
q &\equiv& a',c \\
\end{array}
%
\begin{array}[t]{rcl}
a &:=& \,(a,b) \\
a' &:=& \,(a',c) \\
b &:=& '\,(a,b) \\
a',a &:=& \ang{a',a} \\
b,b &:=& \ang{b,b} \\
(a',a),(b,b) &:=& \ang{(a',a),(b,b)} \\
\end{array}
$$
We can omit the types, as they can be reconstructed from the
downcasings. We can reduce the judgment above to:
$$(a,b),(a',c) \vdash (a',a),(b,b)$$
A standard trick in Categorical Semantics is to represent the context
as the product of the types of its variables, and the `$\vdash$' as a
morphism from that product to the type of the result. So our judgment
becomes this:
$$\begin{array}{rcl}
(A×B)×(A×C) & \to & (A×A)×(B×B) \\
(a,b),(a',c) & \mto & (a',a),(b,b) \\
& & \text{where} \\
& & (a,b) := \,((a,b),(a',c)) \\
& & (a',c) := '\,((a,b),(a',c)) \\
& & \text{etc...} \\
\end{array}
$$
In a cartesian category we have projection maps,
%
$$ \projdiag{A×B}{(A×B)}{(C×D)}{C×D}{500}{500} $$
$$ \projdiag{A}{A}{B}{B}{200}{200}
\qquad
\qquad
\qquad
\qquad
\projdiag{A}{A}{C}{C}{200}{200}
$$
%
and factorizations through products, like:
%
%D diagram fact-thorugh-prod
%D 2Dx 100 +30 +30
%D 2D 100 A
%D 2D
%D 2D +30 B <--- B×C ---> C
%D 2D
%D (( A B B×C C
%D @ 0 @ 1 -> .plabel= a f
%D @ 0 @ 2 -> .plabel= m \ang{f,g}_{ABC}
%D @ 0 @ 3 -> .plabel= a g
%D @ 1 @ 2 <- @ 2 @ 3 ->
%D ))
%D enddiagram
%D
$$\diag{fact-thorugh-prod}$$
The construction for the map $(A×B)×(A×C) \to (A×A)×(B×B)$ can be
extracted from these trees:
%:
%: --------_{(A×B)(A×C)} ----_{AB}
%: (a,b),(a',c)|-a,b a,b|-a
%: -------------------------------;
%: (a,b),(a',c)|-a
%:
%: ^CC-1
%:
%: --------'_{(A×B)(A×C)} ------_{AC}
%: (a,b),(a',c)|-a',c a',c|-a'
%: -------------------------------;
%: (a,b),(a',c)|-a'
%:
%: ^CC-2
%:
%: --------_{(A×B)(A×C)} ------'_{AB}
%: (a,b),(a',c)|-a,b a,b|-b
%: -------------------------------;
%: (a,b),(a',c)|-b
%:
%: ^CC-3
%:
%: ================ ===============
%: (a,b),(a',c)|-a' (a,b),(a',c)|-a
%: ---------------------------------\ang{,}_{((A×B)×(A×C))AA}
%: (a,b),(a',c)|-a',a
%:
%: ^CC-4
%:
%: ================ ===============
%: (a,b),(a',c)|-b (a,b),(a',c)|-b
%: ---------------------------------\ang{,}_{((A×B)×(A×C))BB}
%: (a,b),(a',c)|-b,b
%:
%: ^CC-5
%:
%: ================== =================
%: (a,b),(a',c)|-a',a (a,b),(a',c)|-b,b
%: -------------------------------------\ang{,}_{((A×B)×(A×C))(A×A)(B×B)}
%: (a,b),(a',c)|-(a',a),(b,b)
%:
%: ^CC-6
%:
$$\ded{CC-1}$$
$$\ded{CC-2}$$
$$\ded{CC-3}$$
$$\ded{CC-4}$$
$$\ded{CC-5}$$
$$\ded{CC-6}$$
The final result is this, if we omit the typings in the `$_{\_\_}$'s,
`$'_{\_\_}$'s and `$\ang{,}_{\_\_\_}$'s to make it smaller:
$$\begin{array}{rcl}
\ang{\ang{';,;'},\ang{';,;'}}: (A×B)×(A×C) & \to& (A×A)×(B×B) \\
((a,b),(a',c)) &\mto& ((a',a),(b,b)) \\
\end{array}
$$
What matters here is: with the downcasings and the operations in a
proto-cartesian category --- projections, pairing --- we can build the
categorical interpretations of judgments like
%
$$\begin{array}{rcl}
(a',a):(A×B),(b,b):(A×C) &\vdash& ((a',a),(b,b)):(A×A)×(B×B) \\
(a,b),(a',c) &\vdash& (a',a),(b,b) \\
\end{array}
$$
These categorical constructions behave as expected. For example, the
composite of two ``flip'' functions,
%:
%: ========== ==========
%: a,a'|-a',a a',a|-a,a'
%: -----------------------
%: a,a'|-a,a'
%:
%: ^flipflip
%:
$$\ded{flipflip}$$
%
is the identity --- but the proof of this lives in the real world.
% --------------------
% «dn-context-morphs» (to ".dn-context-morphs")
% (subsec "Context Morphisms" "dn-context-morphs")
\mysubsection {Context Morphisms} {dn-context-morphs}
% --------------------
% «dn-contexts-multi» (to ".dn-contexts-multi")
% (subsec "Several Hypotheses: CCs (With a Trick)" "dn-contexts-multi")
\mysubsection {Several Hypotheses: CCs (With a Trick)} {dn-contexts-multi}
We can also construct the term for $(a,b),(a',c) \vdash (a',a),(b,b)$
from a tree in Natural Deduction-style, to which we add the contexts:
%:
%: ----------\id ----------\id
%: a,b a,b (a,b)|-a,b (a,b)|-a,b
%: --- --- ----------;' ----------;'
%: b b (a,b)|-b (a,b)|-b
%: ------- ------------------------\ang{,}
%: b,b (a,b)|-b,b
%:
%: ^nd-cc-1 ^nd-cc-2
%:
$$\ded{nd-cc-1} \quad \squigto \quad \ded{nd-cc-2}$$
({\sl Note:} think of trees with judgments at the nodes as being in
``sequent calculus style''... so for us ``Natural Deduction'' is when
the contexts are hidden, and ``sequent calculus'' is when they are
explicit.)
This is easy to do when all the nodes have exactly the same single
hypothesis --- we would have that in the case $\gamma:(A×B)×(A×C)
\vdash \ldots$, but not in the case $p:(A×B),q:(A×C) \vdash \ldots$,
where we have some cases where contexts have to be merged; a nice way
to handle the mergings is to represent them as extra steps in the tree
of judgments:
%:
%: ------------\id ----------\id
%: (a',c)|-a',c (a,b)|-a,b
%: ----------; ----------;
%: a',c a,b (a',c)|-a' (a,b)|-a
%: ---- --- ---------------'; ---------------;
%: a' a (a,b),(a',c)|-a' (a,b),(a',c)|-a
%: --------\ang{,} ------------------------------------\ang{,}
%: a',a (a,b),(a',c)|-a',a
%:
%: ^nd-cc-1 ^nd-cc-2
%:
$$\ded{nd-cc-1} \qquad \ded{nd-cc-2}$$
The order of the variables in the context is immaterial, in a sense
--- the ND tree at the left above can also be expanded to a sequent
calculus ``proof'' (i.e., construction) of $(a',c),(a,b) \vdash a',a$,
[But one can be obtained from the other one by composing with
(iso)morphisms that scramble the variables in the context...]
[Explain the convention for parentheses in the context: $(a,b),(a',c)
\vdash \ldots$ is $(a,b):A×B,(a',c):A×C \vdash \ldots$,
$((a,b),(a',c)) \vdash \ldots$ is $((a,b),(a',c)):(A×B)×(AxC) \vdash
\ldots$, and $a,b,a',c \vdash \ldots$ is $a:A,b:B,a':A,c:C \vdash
\ldots$.]
[The internal language: examples]
[Adding $+$ and $·$ to the language with morphisms $+:A×A \to A$ and
$·:A×A \to A$, that we downcase to $a,a' \mto a+a$ and $a,a' \mto
aa'$; the downcasing of the composite of $x,y \mto xy,y$ and $z,w
\mto z+w$ is $x,y \mto xy+y$]
% (find-books "__cats/__cats.el" "lambek-scott")
% (find-lambekscottpage (+ 8 75) "internal language L(A) of a cartesian closed category")
% --------------------
% «dn-discharges» (to ".dn-discharges")
% (subsec "Discharges: CCCs" "dn-discharges")
\mysubsection {Discharges: CCCs} {dn-discharges}
% --------------------
% «dn-subsets» (to ".dn-subsets")
% (sec "Subsets" "dn-subsets")
\mysection {Subsets} {dn-subsets}
% --------------------
% «dn-subobjects» (to ".dn-subobjects")
% (sec "Subobjects" "dn-subobjects")
\mysection {Subobjects} {dn-subobjects}
% --------------------
% «dn-proj-functors» (to ".dn-proj-functors")
% (sec "Projection Functors" "dn-proj-functors")
\mysection {Projection Functors} {dn-proj-functors}
A {\sl prefibration} is just a functor $p: \bbE \to \bbB$ --- a
``projection functor'' going from the ``entire category'' to the
``base category''. A {\sl fibration} is a prefibration with enough
``cartesian morphisms'' in $\bbE$, as we will see.
We say that an object $X$ of $\bbE$ is ``above'' its image $pX$, and
the same for morphisms. Usually when we draw a morphism $X \ton{f} Y$
of $\bbE$ above a morphism $I \ton{u} J$ of $\bbB$ this means that
$u=pf:pX \to pY$. For each object I of $\bbB$ we call the subcategory
$p^{-1}(I)$ of $\bbE$ the {\sl fiber above} (or ``{\sl of}'') $I$, and
we write $\bbE_I$ for $p^{-1}(I)$.
Each object $Z$ of $\bbE$ induces a functor $p/Z: \bbE/Z \to \bbB/pZ$
between slice categories. We say that a morphism $g:Y \to Z$ of $\bbE$
is {\sl cartesian} when for each object $f:X \to Y$ of $\bbE/Z$ the
mapping $\Hom_{\bbE/Z}(f,g) \to \Hom_{\bbB/pZ}(pf, pg)$ --- that takes
each $h:X \to Y$ to $ph:pX \to pY$ --- is a bijection.
%D diagram cart-std
%D 2Dx 100 +20 +30
%D 2D 100 e0 ----_
%D 2D \ \
%D 2D v v
%D 2D +25 e1 -> e2
%D 2D
%D 2D +10 b0 ----_
%D 2D \ \
%D 2D v v
%D 2D +25 b1 -> b2
%D 2D
%D (( e0 .tex= P
%D e1 .tex= Q
%D e2 .tex= R
%D b0 .tex= pP
%D b1 .tex= pQ
%D b2 .tex= pR
%D e0 e2 -> .plabel= a f
%D e1 e2 -> .plabel= b g
%D e0 e1 .> .plabel= l h
%D b0 b2 -> .plabel= a pf
%D b1 b2 -> .plabel= b pg
%D b0 b1 .> .plabel= l ph
%D ))
%D enddiagram
%D
%D diagram cart-std2
%D 2Dx 100 +20 +30
%D 2D 100 e0 ----_
%D 2D \ \
%D 2D v v
%D 2D +25 e1 -> e2
%D 2D
%D 2D +10 b0 ----_
%D 2D \ \
%D 2D v v
%D 2D +25 b1 -> b2
%D 2D
%D (( e0 .tex= P
%D e1 .tex= v^*R
%D e2 .tex= R
%D b0 .tex= pP
%D b1 .tex= B
%D b2 .tex= C
%D e0 e2 -> .plabel= a f
%D e1 e2 -> .plabel= b \ov{v}R
%D e0 e1 .> .plabel= l h
%D b0 b2 -> .plabel= a pf
%D b1 b2 -> .plabel= b v
%D b0 b1 .> .plabel= l ph
%D ))
%D enddiagram
%D
%D diagram cart-dnc
%D 2Dx 100 +20 +30
%D 2D 100 e0 ----_
%D 2D \ \
%D 2D v v
%D 2D +25 e1 -> e2
%D 2D
%D 2D +10 b0 ----_
%D 2D \ \
%D 2D v v
%D 2D +25 b1 -> b2
%D 2D
%D (( e0 .tex= a||P
%D e1 .tex= b||Q
%D e2 .tex= c||R
%D b0 .tex= a
%D b1 .tex= b
%D b2 .tex= c
%D e0 e2 |--> e1 e2 |-> .plabel= a ñ e0 e1 |->
%D b0 b2 |-> b1 b2 |-> b0 b1 |.>
%D ))
%D enddiagram
%D
$$\diag{cart-std} \qquad \diag{cart-std2} \qquad \diag{cart-dnc}$$
This can be made much clearer. Our archetypical fibration is $\cod:
\Sub(\Set) \to \Set$ [that we sometimes call just $\Sub(\Set)$]. An
object of $\Sub(\Set)$ is a monic $A' \monicto A$, and $\cod(A'
\monicto A)$ is its codomain, $A$. Let's restrict our attention to
subobjects where $A'$ is a subset of $A$ and `$\monicto$' is the
inclusion; better yet, let's regard $A'$ as the set of the `$a$'s in
$A$ that obey some property $P$. So our subobject $A' \monicto A$
becomes:
%
$$ \sst{aÝA}{P(a)} \monicto A$$
Now let's contract it further, by the use of a double vertical bar in
the `$\{\;\}$'. This
%
$$ \ssst{a}{P(a)} $$
%
will be our notation for the whole monic/subobject, and a morphism
%
$$ \ssst{a}{P(a)} \to \ssst{b}{Q(b)} $$
%
in $\Sub(\Set)$ is in fact a commuting square in $\Set$:
%
%D diagram a||P->b||Q
%D 2Dx 100 +60
%D 2D 100 A' ---> B'
%D 2D v v
%D 2D | |
%D 2D v v
%D 2D +20 A ----> B
%D 2D
%D (( A' .tex= \sst{aÝA}{P(a)}
%D B' .tex= \sst{bÝB}{Q(b)}
%D A' B' -> A' A >-> B' B >-> A B ->
%D ))
%D enddiagram
%D
$$\diag{a||P->b||Q}$$
%
The projection functor $\cod$ says that $$\ssst{a}{P(a)} \to
\ssst{b}{Q(b)}$$ is over $A \to B$ in the fibration $\cod:\Sub(\Set)
\to \Set$:
%
%D diagram a||P->b||Q-over
%D 2Dx 100 +60 +60
%D 2D 100 A' ---> B' \bbE=\Sub(\Set)
%D 2D |
%D 2D |p=\cod
%D 2D v
%D 2D +30 A ----> B \bbB=\Set
%D 2D
%D (( A' .tex= \ssst{aÝA}{P(a)}
%D B' .tex= \ssst{bÝB}{Q(b)}
%D A' B' -> A B ->
%D \bbE=\Sub(\Set) \bbB=\Set -> .plabel= r p=\cod
%D ))
%D enddiagram
%D
$$\diag{a||P->b||Q-over}$$
Each map $f:A \to B$ in $\B$ induces a ``change-of-base functor'',
$f^*:\bbE_B \to \bbE_A$:
%
%D diagram change-of-base-1
%D 2Dx 100 +60 +60
%D 2D 100 \bbE_A <----- \bbE_B
%D 2D
%D 2D +20 {a||Q} <----| {b||Q}
%D 2D | |
%D 2D +15 | <-| | \bbE
%D 2D v v |
%D 2D +15 {a||Q'} <---| {b||Q'} |
%D 2D |
%D 2D f v
%D 2D +20 A ----------> B \bbB
%D 2D
%D (( \bbE_A \bbE_B <- .plabel= a f^*
%D \bbE \bbB -> .plabel= r p
%D A B -> .plabel= a f
%D ))
%D (( {a||Q} .tex= \ssst{a}{Q(f(a))}
%D {b||Q} .tex= \ssst{b}{Q(b)}
%D {a||Q'} .tex= \ssst{a}{Q'(f(a))}
%D {b||Q'} .tex= \ssst{a}{Q'(b)}
%D @ 0 @ 1 <-| .plabel= a f^*
%D @ 0 @ 2 -> .plabel= l \sma
%D @ 1 @ 3 -> .plabel= r \smb
%D @ 2 @ 3 <-| .plabel= b f^*
%D @ 0 @ 3 harrownodes nil 20 nil <-|
%D ))
%D enddiagram
%D
$$\def\sma{\sm{ýaÝA.\,Q(f(a))⊃Q'(f(a)) \\
\text{or} \\
a;Q(f(a))\vdash Q'(f(a)) \\
}}
\def\smb{\sm{baÝB.\,Q(b)⊃Q'(b) \\
\text{or} \\
b;Q(b)\vdash Q'(b) \\
}}
\diag{change-of-base-1}
$$
and also a natural transformation, that produces for each object
$\ssst{b}{Q(b)}$ over $B$ a ``horizontal'' map (we will define
``horizontality'' and ``verticality'' in $\bbE$ precisely very soon),
$\ssst{a}{Q(f(a))} \to \ssst{b}{Q(b)}$, in $\bbE$. If we expand this
``horizontal'' map into a square in $\Set$ we see that what we've got
is a pullback:
%D diagram cart-pb-1
%D 2Dx 100 +35 +55 +45 +65
%D 2D 100 {a|Q} ----> {b|Q}
%D 2D v _| v
%D 2D +10 \bbE {a||Q} <---> {b||Q} | |
%D 2D | v v
%D 2D +10 | {}A ------> {}B
%D 2D v
%D 2D +20 \bbB A ---------> B {A} ------> {B}
%D 2D
%D (( \bbE \bbB ->
%D ))
%D (( {a||Q} .tex= \ssst{a}{Q(f(a))}
%D {b||Q} .tex= \ssst{b}{Q(b)}
%D A B
%D @ 0 @ 1 -> sl^
%D @ 0 @ 1 <-| sl_ .plabel= b f^*
%D @ 2 @ 3 ->
%D ))
%D (( {a|Q} .tex= \sst{aÝA}{Q(f(a))}
%D {b|Q} .tex= \sst{bÝB}{Q(b)}
%D {}A {}B
%D {A} {B}
%D @ 0 @ 1 -> @ 0 @ 2 >-> @ 1 @ 3 >-> @ 2 @ 3 ->
%D @ 0 relplace 15 7 \pbsymbol{7}
%D @ 4 @ 5 ->
%D @ 0 @ 3 harrownodes 10 25 nil <-| .plabel= m f^*
%D ))
%D enddiagram
%D
$$\diag{cart-pb-1}$$
It is these ``maps in $\Sub(\Set)$ that correspond to pullbacks in
$\Set$'' that we will call ``cartesian'' --- but the actual formal
definition of cartesianness is more abstract; it is the one using a
universal property, that we saw at the beginning of this section.
Before proceeding let's see some further shorthands, and their
downcasings. Let's write $\ssst{c}{R(c)}$ as just $\sst{c}{R}$, and
$\ssst{b}{R(g(b))}$ as just $\sst{b}{R}$; we will say that in a
diagram
%
%D diagram cart-deserve
%D 2Dx 100 +40
%D 2D 100 {b||Q} --> {c||R}
%D 2D
%D 2D +20 B -------> C
%D 2D
%D (( {b||Q} .tex= \ssst{b}{Q}
%D {c||R} .tex= \ssst{c}{R}
%D B C
%D @ 0 @ 1 -> @ 2 @ 3 -> .plabel= a g
%D ))
%D enddiagram
%D
$$\diag{cart-deserve}$$
the object $\ssst{b}{Q}$ {\sl deserves the name $\ssst{b}{R}$} when
the arrow $\ssst{b}{Q} \to \ssst{c}{R}$ is cartesian. We will downcase
$\ssst{c}{R}$ to $c||R$, and we will drop the `$c||$' in diagrams when
we can deduce it from the projections below. Also, we will write
$\ov{f}$ for the natural transformation that returns cartesian
morphisms, we will shrink ``$\ssst{c}{R}$'' even more to just `$R$'
(now we've reached the ``standard'' level of abstraction: $R$ is an
object over $C$), and we will use a `$ñ$' in the downcased notation to
stress that a morphism is cartesian. So:
%D diagram cart-shorthands
%D 2Dx 100 +50 +40 +40 +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 +30 D0 <-> D1 E0 <-> E1 F0 <-> F1
%D 2D
%D 2D +20 D2 |-> D3 E2 |-> E3 F2 |-> F3
%D 2D
%D (( A0 .tex= \ssst{b}{R(g(b))}
%D A1 .tex= \ssst{c}{R(c)}
%D A2 .tex= B A3 .tex= C
%D @ 0 @ 1 -> sl^ .plabel= a \ov{f}R
%D @ 0 @ 1 <-| sl_ .plabel= b f^*
%D @ 2 @ 3 -> .plabel= a g
%D ))
%D (( B0 .tex= \ssst{b}{R}
%D B1 .tex= \ssst{c}{R}
%D B2 .tex= B B3 .tex= C
%D @ 0 @ 1 -> sl^ .plabel= a \ov{f}R
%D @ 0 @ 1 <-| sl_ .plabel= b f^*
%D @ 2 @ 3 -> .plabel= a g
%D ))
%D (( C0 .tex= f^*R
%D C1 .tex= R
%D C2 .tex= B C3 .tex= C
%D @ 0 @ 1 -> sl^ .plabel= a \ov{f}R
%D @ 0 @ 1 <-| sl_ .plabel= b f^*
%D @ 2 @ 3 -> .plabel= a g
%D ))
%D (( D0 .tex= b\;||\;R(g(b))
%D D1 .tex= c\;||\;R(c)
%D D2 .tex= b D3 .tex= c
%D @ 0 @ 1 <-| sl^ .plabel= a {ñ}
%D @ 0 @ 1 => sl_
%D @ 2 @ 3 |->
%D ))
%D (( E0 .tex= b\;||\;R
%D E1 .tex= c\;||\;R
%D E2 .tex= b E3 .tex= c
%D @ 0 @ 1 <-| sl^ .plabel= a {ñ}
%D @ 0 @ 1 => sl_
%D @ 2 @ 3 |->
%D ))
%D (( F0 .tex= R
%D F1 .tex= R
%D F2 .tex= b F3 .tex= c
%D @ 0 @ 1 <-| sl^ .plabel= a {ñ}
%D @ 0 @ 1 => sl_
%D @ 2 @ 3 |->
%D ))
%D enddiagram
%D
$$\diag{cart-shorthands}$$
[Cartesian liftings]
[The adjunction]
[Cleavage]
[Change-of-base functors]
[$\ov{v}$ as a natural transformation]
[Vertical and horizontal; mention ``prone'']
[Every morphism in $\bbE$ factors as `vertical;horizontal']
[Archetypical case 1: $\cod: \Sub(\Set) \to \Set$. Subobjects]
[Archetypical case 2: $\cod: \Set^\to \to \Set$. Display maps]
[Archetypical case 3: $\Set//\Set$. Simplified display maps]
% (find-books "__cats/__cats.el" "lambek-scott")
% (find-books "__cats/__cats.el" "jacobs")
% --------------------
% «dn-uc-intro» (to ".dn-uc-intro")
% (sec "Some Uppercasings" "dn-uc-intro")
\mysection {Some Uppercasings} {dn-uc-intro}
% --------------------
% «dn-uc-semi-logical» (to ".dn-uc-semi-logical")
% (subsec "A Semi-Logical Notation" "dn-uc-semi-logical")
\mysubsection {A Semi-Logical Notation} {dn-uc-semi-logical}
% --------------------
% «dn-uc-lawvere» (to ".dn-uc-lawvere")
% (subsec "Lawvere" "dn-uc-lawvere")
\mysubsection {Lawvere} {dn-uc-lawvere}
% --------------------
% «dn-uc-seely» (to ".dn-uc-seely")
% (subsec "Seely" "dn-uc-seely")
\mysubsection {Seely} {dn-uc-seely}
% --------------------
% «dn-uc-jacobs» (to ".dn-uc-jacobs")
% (subsec "Jacobs" "dn-uc-jacobs")
\mysubsection {Jacobs} {dn-uc-jacobs}
% --------------------
% «dn-uc-maclane» (to ".dn-uc-maclane")
% (subsec "Maclane" "dn-uc-maclane")
\mysubsection {Maclane} {dn-uc-maclane}
% --------------------
% «dn-uc-awodey» (to ".dn-uc-awodey")
% (subsec "Awodey" "dn-uc-awodey")
\mysubsection {Awodey} {dn-uc-awodey}
\cite{Awodey}
% --------------------
% «dn-change-of-base» (to ".dn-change-of-base")
% (sec "Change-of-base" "dn-change-of-base")
\mysection {Change-of-base} {dn-change-of-base}
(Transcribed from the back of p.246 in ``On Property-Like Structures'').
In the archetypical hyperdoctrine, $\Sub(\Set)$ --- and thus also in
the downcased notation --- the adjoints to weakening ($\pi^*$) and
contraction ($\delta^*$) functors take particularly simple forms,
while the adjoints to arbitrary substitution functors ($f^*$) look
more complex, and indeed can be (re)constructed from the adjoints to
weakening and contraction.
This makes more sense in the diagrams. If $\pi \equiv (a,b \mto a)$ is
a projection, its associated change-of-base functor is a ``weakening''
rule because its weakens the context by introducing a new hypothesis:
%D diagram weakening-functor
%D 2Dx 100 +50
%D 2D 100 a,b||Pa <=== a||Pa
%D 2D - -
%D 2D | <-| |
%D 2D v v
%D 2D +25 a,b||Qa <=== a||Qa
%D 2D
%D 2D +20 a,b |-----> a
%D 2D
%D (( a,b||Pa a||Pa
%D a,b||Qa a||Qa
%D a,b a
%D @ 0 @ 1 <=
%D @ 0 @ 2 |-> .plabel= l a,b||Pa|-Qa
%D @ 1 @ 3 |-> .plabel= r a||Pa|-Qa
%D @ 2 @ 3 <=
%D @ 0 @ 3 harrownodes nil 20 nil <-| .plabel= a \pi^*
%D @ 0 @ 3 harrownodes nil 20 nil <-| .plabel= b \text{weakening}
%D @ 4 @ 5 |-> .plabel= a \pi
%D @ 4 @ 5 |-> .plabel= b \text{projection}
%D ))
%D enddiagram
%D
$$\diag{weakening-functor}$$
If $\delta \equiv (a,b \mton{b':=b} a,b,b')$ is a ``duplication'' (or
``diagonal''), the associated change-of-base functor is a
``contraction'' rule, that collapses two hypotheses of the same type
into one:
%D diagram contraction-functor
%D 2Dx 100 +60
%D 2D 100 a,b||Pabb <=== a,b,b'||Pabb'
%D 2D - -
%D 2D | <-| |
%D 2D v v
%D 2D +25 a,b||Qabb <=== a,b,b'||Qabb'
%D 2D
%D 2D +20 a,b |--------> a,b,b'
%D 2D
%D (( a,b||Pabb a,b,b'||Pabb'
%D a,b||Qabb a,b,b'||Qabb'
%D a,b a,b,b'
%D @ 0 @ 1 <=
%D @ 0 @ 2 |-> .plabel= l a,b||Pabb|-Qabb
%D @ 1 @ 3 |-> .plabel= r a,b,b'||Pabb'|-Qabb'
%D @ 2 @ 3 <=
%D @ 0 @ 3 harrownodes nil 20 nil <-| .plabel= a \delta^*
%D @ 0 @ 3 harrownodes nil 20 nil <-| .plabel= b \text{contraction}
%D @ 4 @ 5 |-> .plabel= a \delta
%D @ 4 @ 5 |-> .plabel= b \sm{\text{duplication/}\\\text{diagonal}\\(b':=b)}
%D ))
%D enddiagram
%D
$$\diag{contraction-functor}$$
In the case of an arbitrary morphism, say, $f \equiv (a \mto b)$, we
will say that the associated change of base functor, $f^*$, is just a
``substitution'':
%D diagram substitution-functor
%D 2Dx 100 +50
%D 2D 100 a||P(fa) <=== b||P(b)
%D 2D - -
%D 2D | <-| |
%D 2D v v
%D 2D +25 a||Q(fa) <=== b||Q(b)
%D 2D
%D 2D +20 a |---------> b
%D 2D
%D (( a||P(fa) b||P(b)
%D a||Q(fa) b||Q(b)
%D a b
%D @ 0 @ 1 <=
%D @ 0 @ 2 |-> .plabel= l a||P(fa)|-Q(fa)
%D @ 1 @ 3 |-> .plabel= r b||P(b)|-Q(b)
%D @ 2 @ 3 <=
%D @ 0 @ 3 harrownodes nil 20 nil <-| .plabel= a f^*
%D @ 0 @ 3 harrownodes nil 20 nil <-| .plabel= b \text{substitution}
%D @ 4 @ 5 |-> .plabel= a f
%D @ 4 @ 5 |-> .plabel= b b:=fa
%D ))
%D enddiagram
%D
$$\diag{substitution-functor}$$
Note that we are claiming that these change-of-base functors, $\pi^*$,
$\delta^*$, $f^*$, deserve the names ``$a,b||Qa \funot a||Qa$'',
``$a,b||Qabb \funot a,b,b'||Qabb'$'', ``$a||Q(fa) \funot b||Q(b)$'';
to check that these names are adequate (in the archetype, of course!)
we need to check that the implied cartesian morphisms
%
$$a,b||Qa \mton{ñ} a||Qa$$
%
are really cartesian, which amounts to checking that these diagrams
represent adjunction:
{\myttchars
\footnotesize
\begin{verbatim}
a||Pa |---------------------\
| - > v
b,c||Qb |-cart?-> b||Qb
a |-----------------------\
| - - - > v
b,c |-----------> b
\end{verbatim}
}
% (Transcribed from the back of p.244 in ``On Property-Like Structures'').
We say that a morphism $b||Q \mto c||R$ in $\bbE$ is {\sl
pre-cartesian} when it is ``on the way to becoming cartesian''; this
means that we have not yet constructed the universal condition that
proves that it is cartesian, but we are going towards that.
Note that this terminology --- ``on the way to becoming'', ``not
yet'', ``towards that'' --- imply that there are underlying notions of
{\sl time} and {\sl aim}; they refer to a mathematician (or a proof
assistant) who is working on a proof.
We can picture the situation as this:
{\myttchars
\footnotesize
\begin{verbatim}
statement
+ proof |- - ->
S+P^-
<- - -|
statement
+ witness
\end{verbatim}
}
Take a statement $S$; for example, ``$b,c||Rc \mto c||Rc$ is
cartesian''. We may have a witness, $W$, for ``$\sigma$ is true''; in
our everyday practice a ``witness'' may be a mathematician --- in
flesh and bones; or a book; or an article, an e-mail, etc --- who says
that $\sigma$ is true; in a purely mathematical world, however, a
witness for $\sigma$ may be something as abstract as a point in the
set
%
$$\sst{xÝ\{*\}}{\text{$\sigma$ is true}},$$
%
which is a singleton if $\sigma$ is true, or the empty set if $\sigma$
is false.
Starting from $S$ and $W$ --- or even from just $S$, if we are brave
--- we may try to work towards a situation where we have even more
information: $S+P$, where $P$ is a proof of the statement $S$. In our
example, a proof is an inverse for a certain natural map.
If you, reader, are a strictly classical mathematician, I urge you to
skip the rest of this paragraph; for those who are still reading, an
inverse for the natural transformation
{\myttchars
\footnotesize
\begin{verbatim}
a||P |--------\
|-> v
b||Q |-> c||R
a |----------\
|-> v
b |-----> c
\end{verbatim}
}
is a {\sl construction} that receives triples $(\sof{a||P}, (a||P \mto
c||R), (a \mto b))$ obeying a certain commutativity condition and
return the unique corresponding $a||P \mto b||Q$.
[And constructions are lambda-terms.]
% --------------------
% «dn-arch-hyperdoctrine» (to ".dn-arch-hyperdoctrine")
% (sec "Our archetypal hyperdoctrine" "dn-arch-hyperdoctrine")
\mysection {Our archetypal hyperdoctrine} {dn-arch-hyperdoctrine}
% (find-LATEX "2008bcc.tex" "adjs-of-change-of-base")
%D diagram adjs-to-change-of-base-dnc
%D 2Dx 100 +30 +30 +35 +30 +40
%D 2D 100 A0 ===> A1 B0 ===> B1 C0 ===> C1
%D 2D - - - - - -
%D 2D | <-> | | <-> | | <-> |
%D 2D v v v v v v
%D 2D +20 A2 <=== A3 B2 <=== B3 C2 <=== C3
%D 2D - - - - - -
%D 2D | <-> | | <-> | | <-> |
%D 2D v v v v v v
%D 2D +20 A4 ===> A5 B4 ===> B5 C4 ===> C5
%D 2D
%D 2D +20 a0 |--> a1 b0 |--> b1 c0 |--> c1
%D 2D
%D (( A0 .tex= Pab A1 .tex= Îb.Pab
%D A2 .tex= Qa A3 .tex= Qa
%D A4 .tex= Rab A5 .tex= ýb.Rab
%D a0 .tex= a,b a1 .tex= a
%D A0 A1 =>
%D A0 A2 |-> A1 A3 |-> A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <=
%D A2 A4 |-> A3 A5 |-> A2 A5 harrownodes nil 20 nil <->
%D A4 A5 =>
%D a0 a1 |->
%D ))
%D (( B0 .tex= Pab B1 .tex= b=b'∧Pabb
%D B2 .tex= Qabb B3 .tex= Qabb'
%D B4 .tex= Rab B5 .tex= b=b'⊃Rab
%D b0 .tex= a,b b1 .tex= a,b,b'
%D B0 B1 =>
%D B0 B2 |-> B1 B3 |-> B0 B3 harrownodes nil 20 nil <->
%D B2 B3 <=
%D B2 B4 |-> B3 B5 |-> B2 B5 harrownodes nil 20 nil <->
%D B4 B5 =>
%D b0 b1 |->
%D ))
%D (( C0 .tex= Pa C1 .tex= Îa.a=fb∧Pa
%D C2 .tex= Qfa C3 .tex= Qb
%D C4 .tex= Ra C5 .tex= ýa.a=fb⊃Pa
%D c0 .tex= a c1 .tex= b
%D C0 C1 =>
%D C0 C2 |-> C1 C3 |-> C0 C3 harrownodes nil 20 nil <->
%D C2 C3 <=
%D C2 C4 |-> C3 C5 |-> C2 C5 harrownodes nil 20 nil <->
%D C4 C5 =>
%D c0 c1 |-> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{adjs-to-change-of-base-dnc}$$
% --------------------
% «dn-preservations» (to ".dn-preservations")
% (sec "Preservations" "dn-preservations")
\mysection {Preservations} {dn-preservations}
% (find-LATEX "2008hyp.tex" "preservations-overview")
% (find-LATEX "2008hyp.tex" "pres-of-true-and-and")
% (find-LATEX "2008bcc.tex" "first-preservations")
[Explain these diagrams:]
%D diagram new-pres-T-and-AND-dnc
%D 2Dx 100 +30 +30 +45 +45
%D 2D 100 A0 <============ A1
%D 2D ^ ^ ^
%D 2D | \ <-| |
%D 2D - - -
%D 2D +20 T0 <==== T1 A2 <--| A3 <==== A4
%D 2D - - - -
%D 2D | | / <-| |
%D 2D v v v v
%D 2D +20 T2 A5 <============ A6
%D 2D
%D 2D +15 ta |---> tb aa |-----------> ab
%D 2D
%D (( T0 .tex= § T1 .tex= §
%D T2 .tex= §
%D ta .tex= a tb .tex= b
%D T0 T1 <= T0 T2 |-> sl_ .plabel= l î T0 T2 <-| sl^ .plabel= r ÐP§
%D ta tb |->
%D ))
%D (( A0 .tex= P A1 .tex= P
%D A2 .tex= P&Q A3 .tex= P&Q A4 .tex= P&Q
%D A5 .tex= Q A6 .tex= Q
%D aa x+= 10 .tex= a ab .tex= b
%D A0 A1 <=
%D A0 A2 <-| A0 A3 <-|
%D A1 A4 <-|
%D A0 A3 midpoint A1 A4 midpoint harrownodes nil 20 nil <-|
%D A2 A3 <-| sl^ .plabel= a {î} A2 A3 |-> sl_ .plabel= b ÐP& A3 A4 <=
%D A2 A5 |-> A3 A5 |->
%D A4 A6 |->
%D A3 A5 midpoint A4 A6 midpoint harrownodes nil 20 nil <-|
%D A5 A6 <=
%D aa ab |->
%D ))
%D enddiagram
$$\index{preservation!of `true'!DNC diagram}
\index{preservation!of `and'!DNC diagram}
\diag{new-pres-T-and-AND-dnc}
$$
% (find-LATEX "2008hyp.tex" "pres-of-true-and-and")
% (find-LATEX "2008bcc.tex" "first-preservations")
[Explain these diagrams:]
% (find-LATEX "2008hyp.tex" "pres-of-imp")
% (find-LATEX "2008bcc.tex" "first-preservations")
%D diagram Pimp-DNC
%D 2Dx 100 +45 +55 +45
%D 2Dx 100 +60 +55 +60
%D 2D 100 B0 <-> B0' <============== B1
%D 2D -/\ -/\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\==================== B3 \\
%D 2D \\ \\ \\ \\
%D 2D +15 \\ B4 <===================== B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \/v Vv
%D 2D +20 B6 B7
%D 2D
%D 2D +0 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= (P⊃Q)&P B0' .tex= (P⊃Q)&P B1 .tex= (P⊃Q)&P
%D B2 .tex= Q B3 .tex= Q
%D B4 .tex= P⊃Q B5 .tex= P⊃Q
%D B6 .tex= P⊃Q B7 .tex= P⊃Q
%D B0 B0' <-| sl^ .plabel= a {î}
%D B0 B0' |-> sl_ .plabel= b ÐP&
%D B0' B1 <= B0 B2 |-> B0' B2 |-> B1 B3 |-> B2 B3 <=
%D B0 B4 <= B2 B6 =>
%D B1 B5 <= B3 B7 =>
%D B4 B5 <= B5 B7 |-> .plabel= r \id
%D B4 B6 |-> sl_ .plabel= l î B4 B6 <-| sl^ .plabel= r ÐP⊃
%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 b2 midpoint .TeX= a b1 b3 midpoint .TeX= b |->
%D ))
%D enddiagram
%
$$\diag{Pimp-DNC}$$
% --------------------
% «dn-display-maps» (to ".dn-display-maps")
% (sec "Display Maps" "dn-display-maps")
\mysection {Display Maps} {dn-display-maps}
% --------------------
% «dn-quantifiers» (to ".dn-quantifiers")
% (sec "Quantifiers" "dn-quantifiers")
\mysection {Quantifiers} {dn-quantifiers}
% --------------------
% «dn-equality» (to ".dn-equality")
% (sec "Equality" "dn-equality")
\mysection {Equality} {dn-equality}
% --------------------
% «dn-bcc-for-exists» (to ".dn-bcc-for-exists")
% (sec "Beck-Chevalley for `Exists'" "dn-bcc-for-exists")
\mysection {Beck-Chevalley for `Exists'} {dn-bcc-for-exists}
% (to "proto-BCC")
%D diagram bcc-for-exists-dnc0
%D 2Dx 100 +45 +55 +45
%D 2D 100 ac;d <=============== bc;d
%D 2D -\\ - - \\
%D 2D | \\ \ | \\
%D 2D v \\ v v \\
%D 2D +20 ac;cd <\\> ac;cd' <=== bc;cd \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ a;cd \\ b;cd
%D 2D \\ - \\ -
%D 2D \\ | \\ |
%D 2D \\ v \\ v
%D 2D +20 a;cd' <============= b;cd'
%D 2D
%D 2D +10 ac |----------------> bc
%D 2D |---> |-->
%D 2D +35 a |----------------> b
%D 2D
%D (( ac;d .tex= P bc;d .tex= P
%D ac;cd .tex= Îc.P ac;cd' .tex= Îc.P bc;cd .tex= Îc.P
%D a;cd .tex= Îc.P b;cd .tex= Îc.P
%D a;cd' .tex= Îc.P b;cd' .tex= Îc.P
%D ac;d bc;d <= ac;d ac;cd |-> ac;d ac;cd' |-> bc;d bc;cd |-> ac;cd ac;cd' <-> ac;cd' bc;cd <=
%D ac;d a;cd => bc;d b;cd =>
%D ac;cd a;cd' <= bc;cd b;cd' <=
%D a;cd' b;cd' <= b;cd b;cd' |-> .plabel= r \id
%D a;cd a;cd' |-> sl_ .plabel= l î a;cd a;cd' <-| sl^ .plabel= r Ð{BCC}Î
%D ac;d ac;cd' midpoint bc;d bc;cd midpoint harrownodes nil 20 nil <-|
%D ac;d ac;cd midpoint a;cd a;cd' midpoint dharrownodes nil 20 nil |->
%D bc;d bc;cd midpoint b;cd b;cd' midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( ac .tex= ac bc .tex= bc a .tex= a b .tex= b
%D ac bc |-> ac a |-> bc b |-> a b |->
%D ac relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\index{Beck-Chevalley!for `exists'!DNC diagram}
\diag{bcc-for-exists-dnc0}
$$
% :*p'*p*
%D diagram bcc-for-exists-dnc1
%D 2Dx 100 +75 +10 +85 +55
%D 2Dx 100 +65 +20 +85 +55
%D 2Dx 100 +55 +30 +85 +55
%D 2D 100 ac;d <=============== bc;d
%D 2D -\\ - - \\
%D 2D | \\ \ | \\
%D 2D v \\ v v \\
%D 2D +20 ac;cd <\\> ac;cd' <=== bc;cd \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ a;cd \\ b;cd
%D 2D \\ - \\ -
%D 2D \\ | \\ |
%D 2D \\ v \\ v
%D 2D +20 a;cd' <============= b;cd'
%D 2D
%D 2D +20 ac |----------------> bc
%D 2D |---> |-->
%D 2D +45 a |----------------> b
%D 2D
%D ((
%D ac;d .tex= d:D_{bc}[b{:=}fa] bc;d .tex= d:D_{bc}
%D ac;cd .tex= p':(Æc¨C_b.D_{bc})[b{:=}fa] ac;cd' .tex= p:(Æc¨C_b.D_{bc})[b{:=}fa] bc;cd .tex= p:Æc¨C_b.D_{bc}
%D a;cd .tex= p:(Æc¨C_b[b{:=}fa].D_{bc}[b{:=}fa]) b;cd .tex= p:Æc¨C_b.D_{bc}
%D a;cd' .tex= p':(Æc¨C_b.D_{bc})[b{:=}fa] b;cd' .tex= p':Æc¨C_b.D_{bc}
%D ac;d bc;d <= ac;d ac;cd |-> ac;d ac;cd' |-> bc;d bc;cd |-> ac;cd ac;cd' <-> ac;cd' bc;cd <=
%D ac;d a;cd => bc;d b;cd =>
%D ac;cd a;cd' <= bc;cd b;cd' <=
%D a;cd' b;cd' <= b;cd b;cd' |-> .plabel= r \id
%D a;cd a;cd' |-> sl_ .plabel= l î a;cd a;cd' <-| sl^ .plabel= r Ð{BCC}Î
%D ac;d ac;cd' midpoint bc;d bc;cd midpoint harrownodes nil 20 nil <-|
%D ac;d ac;cd midpoint a;cd a;cd' midpoint dharrownodes nil 20 nil |->
%D bc;d bc;cd midpoint b;cd b;cd' midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( ac .tex= a:A,c:C_b[b{:=}fa] bc .tex= b:B,c:C_b
%D a .tex= a:A b .tex= b:B
%D ac bc |-> .plabel= a b:=fa
%D ac a |-> bc b |->
%D a b |-> .plabel= a b:=fa
%D ac relplace 28 10 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\index{Beck-Chevalley!for sums!term model diagram}
\diag{bcc-for-exists-dnc1}
$$
\def\unp{\operatorname{unp}}
\def\ren{\operatorname{ren}}
%:
%: b:B,c:C|-D_{b}:Þ
%: -----------------Æ
%: b:B|-Æc¨C.D_{b}:Þ
%: ------------------------------------\id
%: b:B;p:Æc¨C_b.D_{bc}|-p:Æc¨C_b.D_{bc}
%: -------------------------------------------Æ^\sharp
%: a:A|-fa:B b:B,c:C_b;d:D_{bc}|-\ang{c,d}:Æc¨C_b.D_{bc}
%: -------------------------------------------------------¯{cut}
%: a:A,c:C_b[b{:=}fa];d:D_{bc}[b{:=}fa]|-\ang{c,d}[b{:=}fa]:(Æc¨C_b.D_{bc})[b{:=}fa] a,c;p|-p
%: ------------------------------------------------------------------------------------------;
%: a:A,c:C_b[b{:=}fa];d:D_{bc}[b{:=}fa]|-\ang{c,d}[b{:=}fa]:(Æc¨C_b.D_{bc})[b{:=}fa]
%: ------------------------------------------------------------------------------------------Æ^\flat
%: a:A;p:Æc¨C_b[b{:=}fa].D_{bc}[b{:=}fa]|-\ang{c,d}[b{:=}fa][c,d:=\unp"p]:(Æc¨C_b.D_{bc})[b{:=}fa][c,d:=\unp"p]
%:
%: ^bcc-for-exists-dnc1
%:
%:
%:
%:
%:
%:
$$\ded{bcc-for-exists-dnc1}$$
[Explain these diagrams:]
%D diagram bcc-for-exists-dnc
%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= P B1 .tex= P
%D B2 .tex= Îc.P B2' .tex= Îc.P B3 .tex= Îc.P
%D B4 .tex= Îc.P B5 .tex= Îc.P
%D B6 .tex= Îc.P B7 .tex= Îc.P
%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 Ð{BCC}Î
%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= a,c b1 .tex= b,c b2 .tex= a b3 .tex= b
%D b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-exists-dnc}$$
% --------------------
% «dn-bcc-for-forall» (to ".dn-bcc-for-forall")
% (sec "Beck-Chevalley for `For All'" "dn-bcc-for-forall")
\mysection {Beck-Chevalley for `For All'} {dn-bcc-for-forall}
% (find-LATEX "2008hyp.tex" "bcc-for-forall")
%D diagram bcc-for-forall-dnc
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <-> B0' <============== B1
%D 2D -/\ -/\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\==================== B3 \\
%D 2D \\ \\ \\ \\
%D 2D +15 \\ B4 <===================== B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \/v Vv
%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= ýc.P B0' .tex= ýc.P B1 .tex= ýc.P
%D B2 .tex= P B3 .tex= P
%D B4 .tex= ýc.P B5 .tex= ýc.P
%D B6 .tex= ýc.P B7 .tex= ýc.P
%D B0 B0' <-> B0' B1 <= B0 B2 |-> B0' B2 |-> B1 B3 |-> B2 B3 <=
%D B0 B4 <= B2 B6 =>
%D B1 B5 <= B3 B7 =>
%D B4 B5 <= B5 B7 |-> .plabel= r \id
%D B4 B6 |-> sl_ .plabel= l î B4 B6 <-| sl^ .plabel= r Ð{BCC}ý
%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= a,c b1 .tex= b,c b2 .tex= a b3 .tex= b
%D b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-forall-dnc}$$
% --------------------
% «dn-bcc-for-equality» (to ".dn-bcc-for-equality")
% (sec "Beck-Chevalley for Equality" "dn-bcc-for-equality")
\mysection {Beck-Chevalley for Equality} {dn-bcc-for-equality}
[BCC for equality is the same, categorically; point that in
\cite{Jacobs} and in \cite{SeelyBeck} they are kept separate,
because they don't require a left adjoint to all `$f$'s in the base
--- just for projections and diagonals. The downcased diagram is
different...]
% (find-LATEX "2008hyp.tex" "bcc-for-equality")
%D diagram bcc-for-equality-dnc
%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= P B1 .tex= P
%D B2 .tex= c{=}c{&}P B2' .tex= c{=}c{&}P B3 .tex= c{=}c{&}P
%D B4 .tex= c{=}c'{&}P B5 .tex= c{=}c'{&}P
%D B6 .tex= c{=}c'{&}P B7 .tex= c{=}c'{&}P
%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 Ð{BCC}Î
%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= a,c b1 .tex= b,c b2 .tex= a,c,c' b3 .tex= b,c,c'
%D b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-equality-dnc}$$
%D diagram bcc-for-equality-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'*P B1 .tex= P
%D B2 .tex= c'*f^*\Eq_{c}P B2' .tex= f'*c^*\Eq_{c}P B3 .tex= c^*\Eq_{c}P
%D B4 .tex= \Eq_{c'}f'*P B5 .tex= \Eq_{c}P
%D B6 .tex= f^*\Eq_{c}P B7 .tex= \Eq_{c}P
%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 Ð{BCC}=
%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= A×C b1 .tex= B×C b2 .tex= A×C×C b3 .tex= B×C×C
%D b0 b1 -> .plabel= b f'
%D b0 b2 -> .plabel= l c'
%D b1 b3 -> .plabel= r c
%D b2 b3 -> .plabel= b f
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{bcc-for-equality-std}$$
% --------------------
% «dn-frob-for-exists» (to ".dn-frob-for-exists")
% (sec "Frobenius for `Exists'" "dn-frob-for-exists")
\mysection {Frobenius for `Exists'} {dn-frob-for-exists}
% (find-LATEX "2008hyp.tex" "frob-for-exists")
% (find-LATEX "2008hyp.tex" "frob-for-equality")
% (find-LATEX "2008hyp.tex" "frob-for-ex-eq")
[Explain the diagrams below, and include the diagrams that show that
in the presence of a left adjoint to change-of-base we have that
``Frobenius is equivalent to preservation of `implies'\,''.]
[Frobenius for exists:]
%D diagram frob-for-exists-dnc
%D 2Dx 100 +45 +35 +10
%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 ((
%D B0 .tex= P B1 .tex= Îc.P
%D B2 .tex= P&Q B3 .tex= Îc.(P&Q) B3' .tex= (Îc.P)&Q
%D B4 .tex= Q B5 .tex= Q
%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 î 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 .tex= b,c b1 .tex= b b0 b1 |->
%D ))
%D enddiagram
%
$$\index{Frobenius!for `exists'!DNC diagram}
\diag{frob-for-exists-dnc}
$$
% : a,b;c =============================> a;(b,c)
% : ^ ------> ^
% : | / |
% : - \ -
% : a,b;(c,d) ====> a;(b,(c,d)) |-nat-> a;((b,c),d)
% : - / <-Frob-| -
% : | \ |
% : v -------> v
% : a,b;d <============================== a;d
%:
%: a|-D a|-D
%: ====== ======
%: a,b|-C a,b|-D a,b|-C a,b|-D
%: ---------------\pi ---------------\pi'
%: a,b;(c,d)|-c a,b;(c,d)|-d
%: ------------------Æ_1 -------------Æ^\flat
%: a;(b,(c,d))|-(b,c) a;(b,(c,d))|-d
%: --------------------------------------<,>
%: a;(b,(c,d))|-((b,c),d)
%:
%: ^Frob-nat
%:
% Engraçado, o Frobenius não é uma associatividade "forte", ele tem
% restrições grandes nas dependências do D....
% --------------------
% «dn-frob-for-equality» (to ".dn-frob-for-equality")
% (sec "Frobenius for Equality" "dn-frob-for-equality")
\mysection {Frobenius for Equality} {dn-frob-for-equality}
[Frobenius for equality:]
%D diagram frob-for-equality-dnc
%D 2Dx 100 +50 +40 +15
%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 ((
%D B0 .tex= P B1 .tex= c{=}c'{&}P
%D B2 .tex= P&Q B3 .tex= c{=}c'{&}(P&Q) B3' .tex= (c{=}c'{&}P)&Q
%D B4 .tex= Q B5 .tex= Q
%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 î 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 .tex= b,c b1 .tex= b,c,c' b0 b1 |->
%D ))
%D enddiagram
%
$$\index{Frobenius!for equality!DNC}
\diag{frob-for-equality-dnc}
$$
%D diagram frob-for-equality-std
%D 2Dx 100 +45 +35 +10
%D 2Dx 100 +50 +40 +15
%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 ((
%D B0 .tex= P B1 .tex= \Eq_cP
%D B2 .tex= P&c^*Q B3 .tex= \Eq_c(P&c^*Q) B3' .tex= (\Eq_cP)&Q
%D B4 .tex= c^*Q B5 .tex= Q
%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 î 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 .tex= B×C b1 .tex= B×C×C b0 b1 -> .plabel= a c
%D ))
%D enddiagram
%
$$\index{Frobenius!for equality!standard}
\diag{frob-for-equality-std}
$$
[Frobenius for an arbitrary map:]
%D diagram frob-for-ex-eq-dnc
%D 2Dx 100 +60 +55 +25
%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 ((
%D B0 .tex= Pa B1 .tex= Îa.b=fa&Pa
%D B2 .tex= Pa&Qfa B3 .tex= Îa.b=fa&(Pa&Qfa) B3' .tex= (Îa.b=fa&Pa)&Qb
%D B4 .tex= Qfa B5 .tex= Qb
%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 î 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 .tex= a b1 .tex= b b0 b1 |->
%D ))
%D enddiagram
%
$$\index{Frobenius!generic!DNC}
\diag{frob-for-ex-eq-dnc}
$$
%D diagram frob-for-ex-eq-std
%D 2Dx 100 +60 +55 +25
%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 ((
%D B0 .tex= P B1 .tex= \Eq_fP
%D B2 .tex= P&f^*Q B3 .tex= \Eq_f(P&f^*Q) B3' .tex= (\Eq_fP)&Q
%D B4 .tex= f^*Q B5 .tex= Q
%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 î 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 .tex= A b1 .tex= B b0 b1 -> .plabel= a f
%D ))
%D enddiagram
%
$$\index{Frobenius!for equality!standard}
\diag{frob-for-ex-eq-std}
$$
% --------------------
% «dn-hyperdoctrines» (to ".dn-hyperdoctrines")
% (sec "Hyperdoctrines" "dn-hyperdoctrines")
\mysection {Hyperdoctrines} {dn-hyperdoctrines}
We say that a cloven fibration $p: \bbE \to \bbB$ is a {\sl hyperdoctrine} when:
(1) the base category $\bbB$ is a CCC,
(2) each fiber $\bbE_B$ is a CCC,
and for each $f:A \to B$ in $\bbB$ the change-of-base functor $f^*$ has:
(3) a left adjoint, $Æ_f \dashv f*$,
(4) a right adjoint, $f^* \dashv å_f$,
and each change-of base functor $f^*$ preserves, modulo iso,
(5) the terminal,
(6) binary products,
(7) exponentials,
and furthermore the following three ``technical conditions'' hold:
(8) Beck-Chevalley for ``exists'',
(9) Beck-Chevalley for ``forall'',
(10) Frobenius.
\msk
Our archetypical fibration $\cod: \Sub(\Set) \to \Set$ is a
hyperdoctrine --- it was the motivation for the definition of
hyperdoctrine, by the way --- and we can use a notation ``lifted''
from $\cod: \Sub(\Set) \to \Set$ to define each of these properties
diagramatically, an to prove a few theorems about hyperdoctrines.
% --------------------
% «dn-lawvere-70» (to ".dn-lawvere-70")
% (sec "Three Theorems from Lawvere's ``Hyperdoctrines'' Paper" "dn-lawvere-70")
\mysection {Three Theorems from Lawvere's ``Hyperdoctrines'' Paper} {dn-lawvere-70}
% (find-angg ".emacs.papers" "lawvere")
% (find-LATEX "2008hyp.tex" "frob-and-pres-imp")
% (find-xpdfpage "~/LATEX/2008hyp.pdf" 21)
% (find-dvipage "~/LATEX/2008hyp.dvi" 21)
% (find-LATEX "2008hyp.tex" "bcc-ex-iff-bcc-fa")
% (find-xpdfpage "~/LATEX/2008hyp.pdf" 22)
% (find-dvipage "~/LATEX/2008hyp.dvi" 22)
% (find-LATEX "2008hyp.tex" "frob-for-equality-2")
% (find-xpdfpage "~/LATEX/2008hyp.pdf" 34)
% (find-dvipage "~/LATEX/2008hyp.dvi" 34)
% (find-LATEX "2008hyp.tex" "dep-eq-from-simple-eq")
% (find-xpdfpage "~/LATEX/2008hyp.pdf" 35)
% (find-dvipage "~/LATEX/2008hyp.dvi" 35)
% --------------------
% «dn-frob-and-pimp» (to ".dn-frob-and-pimp")
% (subsec "Frob and Pimp" "dn-frob-and-pimp")
\mysubsection {Frob and Pimp} {dn-frob-and-pimp}
\thinmtos
%D diagram frob=pres-imp-1
%D 2Dx 100 +45 +40 +45
%D 2D 100 a,b;(c,d) ===> a;(b,(c,d)) a,b;e <========== a;e
%D 2D /\ -^ || ||
%D 2D || nat||Frob || ||
%D 2D || v- || ||
%D 2D +20 || a;((b,c),d) \/ ||
%D 2D +10 || /\ a,b;(d|->e)_B ||
%D 2D || || ^- ||
%D 2D || || nat||PImp ||
%D 2D || || -v \/
%D 2D +20 a,b;c ========> a;(b,c) a,b;(d|->e)_A <=== a;(d|->e)
%D 2D
%D (( a,b;(c,d) a;(b,(c,d))
%D a;((b,c),d)
%D a,b;c a;(b,c)
%D @ 0 @ 1 =>
%D @ 0 @ 3 <=
%D @ 1 @ 2 |-> sl_ .plabel= l \Frobnat @ 1 @ 2 <-| sl^ .plabel= r \Frob
%D @ 2 @ 4 <=
%D @ 3 @ 4 =>
%D ))
%D (( a;e a;(d|->e)
%D a,b;(d|->e)_A
%D a,b;e a,b;(d|->e)_B
%D @ 0 @ 1 =>
%D @ 0 @ 3 => @ 1 @ 2 =>
%D @ 2 @ 4 |-> sl_ .plabel= r \Pimpnat @ 2 @ 4 <-| sl^ .plabel= l \Pimp
%D @ 3 @ 4 =>
%D ))
%D enddiagram
%D
$$\diag{frob=pres-imp-1}$$
%D diagram frob=pres-imp-1-std-new
%D 2Dx 100 +45 +40 +45
%D 2D 100 a,b;(c,d) ===> a;(b,(c,d)) a,b;e <========== a;e
%D 2D /\ -^ || ||
%D 2D || nat||Frob || ||
%D 2D || v- || ||
%D 2D +20 || a;((b,c),d) \/ ||
%D 2D +10 || /\ a,b;(d|->e)_B ||
%D 2D || || ^- ||
%D 2D || || nat||PImp ||
%D 2D || || -v \/
%D 2D +20 a,b;c ========> a;(b,c) a,b;(d|->e)_A <=== a;(d|->e)
%D 2D
%D (( a,b;(c,d) .tex= C×b^*\!D
%D a;(b,(c,d)) .tex= Æ_b(C×b^*\!D)
%D a;((b,c),d) .tex= Æ_{b}C×D
%D a,b;c .tex= C
%D a;(b,c) .tex= Æ_{b}C
%D @ 0 @ 1 |-> .plabel= a Æ_b
%D @ 0 @ 3 <-| .plabel= l ×b^*\!D
%D @ 1 @ 2 -> sl_ .plabel= l \Frobnat @ 1 @ 2 <- sl^ .plabel= r \Frob
%D @ 2 @ 4 <-| .plabel= r ×D
%D @ 3 @ 4 |-> .plabel= a Æ_b
%D ))
%D (( a,b;e .tex= b^*\!E
%D a;e .tex= E
%D a,b;(d|->e)_B .tex= b^*\!D{->}b^*\!E
%D a,b;(d|->e)_A .tex= b^*(D{->}E)
%D a;(d|->e) .tex= D{->}E
%D @ 0 @ 1 <-| .plabel= a b^*
%D @ 0 @ 2 |-> .plabel= l b^*\!D{->}
%D @ 1 @ 4 |-> .plabel= r D{->}
%D @ 3 @ 4 <-| .plabel= r b^*
%D @ 2 @ 3 <- sl_ .plabel= l \Pimpnat @ 2 @ 3 -> sl^ .plabel= r \Pimp
%D ))
%D enddiagram
%D
$$\diag{frob=pres-imp-1-std-new}$$
%D diagram frob=pres-imp-1-logical-short
%D 2Dx 100 +45 +40 +45
%D 2D 100 a,b;(c,d) ===> a;(b,(c,d)) a,b;e <========== a;e
%D 2D /\ -^ || ||
%D 2D || nat||Frob || ||
%D 2D || v- || ||
%D 2D +20 || a;((b,c),d) \/ ||
%D 2D +10 || /\ a,b;(d|->e)_B ||
%D 2D || || ^- ||
%D 2D || || nat||PImp ||
%D 2D || || -v \/
%D 2D +20 a,b;c ========> a;(b,c) a,b;(d|->e)_A <=== a;(d|->e)
%D 2D
%D (( a,b;(c,d) .tex= P∧Q
%D a;(b,(c,d)) .tex= Îb.(P∧Q)
%D a;((b,c),d) .tex= (Îb.P)∧Q
%D a,b;c .tex= P
%D a;(b,c) .tex= Îb.P
%D @ 0 @ 1 |-> .plabel= a Æ_
%D @ 0 @ 3 <-| .plabel= l ×b^*\!D
%D @ 1 @ 2 -> sl_ .plabel= l \Frobnat @ 1 @ 2 <- sl^ .plabel= r \Frob
%D @ 2 @ 4 <-| .plabel= r ×D
%D @ 3 @ 4 |-> .plabel= a Æ_
%D ))
%D (( a,b;e .tex= R
%D a;e .tex= R
%D a,b;(d|->e)_B .tex= Q⊃R
%D a,b;(d|->e)_A .tex= Q⊃R
%D a;(d|->e) .tex= Q⊃R
%D @ 0 @ 1 <-| .plabel= a ^*
%D @ 0 @ 2 |-> .plabel= l b^*\!D{->}
%D @ 1 @ 4 |-> .plabel= r D{->}
%D @ 3 @ 4 <-| .plabel= r ^*
%D @ 2 @ 3 <- sl_ .plabel= l \Pimpnat @ 2 @ 3 -> sl^ .plabel= r \Pimp
%D ))
%D enddiagram
%D
$$\diag{frob=pres-imp-1-logical-short}$$
%D diagram frob=pres-imp-1-semi-logical
%D 2Dx 100 +45 +40 +45
%D 2D 100 a,b;(c,d) ===> a;(b,(c,d)) a,b;e <========== a;e
%D 2D /\ -^ || ||
%D 2D || nat||Frob || ||
%D 2D || v- || ||
%D 2D +20 || a;((b,c),d) \/ ||
%D 2D +10 || /\ a,b;(d|->e)_B ||
%D 2D || || ^- ||
%D 2D || || nat||PImp ||
%D 2D || || -v \/
%D 2D +20 a,b;c ========> a;(b,c) a,b;(d|->e)_A <=== a;(d|->e)
%D 2D
%D (( a,b;(c,d) .tex= P∧f^*Q
%D a;(b,(c,d)) .tex= Î_f(P∧f^*Q)
%D a;((b,c),d) .tex= (Î_fP)∧Q
%D a,b;c .tex= P
%D a;(b,c) .tex= Î_fP
%D @ 0 @ 1 |-> .plabel= a Æ_f
%D @ 0 @ 3 <-| .plabel= l ∧\,f^*Q
%D @ 1 @ 2 -> sl_ .plabel= l \Frobnat @ 1 @ 2 <- sl^ .plabel= r \Frob
%D @ 2 @ 4 <-| .plabel= r ∧Q
%D @ 3 @ 4 |-> .plabel= a Æ_f
%D ))
%D (( a,b;e .tex= f^*R
%D a;e .tex= R
%D a,b;(d|->e)_B .tex= f^*Q⊃f^*R
%D a,b;(d|->e)_A .tex= f^*(Q⊃R)
%D a;(d|->e) .tex= Q⊃R
%D @ 0 @ 1 <-| .plabel= a f^*
%D @ 0 @ 2 |-> .plabel= l f^*Q\,⊃
%D @ 1 @ 4 |-> .plabel= r Q⊃
%D @ 3 @ 4 <-| .plabel= a f^*
%D @ 2 @ 3 <- sl_ .plabel= l \Pimpnat @ 2 @ 3 -> sl^ .plabel= r \Pimp
%D ))
%D enddiagram
%D
$$\diag{frob=pres-imp-1-semi-logical}$$
%D diagram frob=pres-imp-2-semil
%D 2Dx 100 +80
%D 2D Æ^b
%D 2D 100 a,b;(c,d)|-e |-----> a;(b,(c,d))|-e
%D 2D -^ <-----| -^
%D 2D || Æ^# nat||Frob
%D 2D Cur||Uncur v-
%D 2D +20 || a;((b,c),d)|-e
%D 2D v- -^
%D 2D +20 a,b;c|-(d|->e)_B ||
%D 2D -^ Cur||Uncur
%D 2D nat||PImp Æ^b ||
%D 2D v- |---> v-
%D 2D +20 a,b;c|-(d|->e)_A <---| a;(b,c)|-(d|->e)
%D 2D Æ^#
%D 2D
%D 2D +20 A -------------------> B
%D 2D
%D (( a,b;(c,d)|-e .tex= a,b;P∧f^*Q|-f^*R .tex= P∧f^*Q|-f^*R
%D a;(b,(c,d))|-e .tex= a;Î_f(P∧f^*Q)|-R .tex= Î_f(P∧f^*Q)|-R
%D a;((b,c),d)|-e .tex= a,b;Î_fP∧Q|-R? .tex= Î_fP∧Q|-R?
%D a,b;c|-(d|->e)_B .tex= a,b;P|-f^*Q⊃f^*R .tex= P|-f^*Q⊃f^*R
%D a,b;c|-(d|->e)_A .tex= a,b;P|-f^*(Q⊃R) .tex= P|-f^*(Q⊃R)
%D a;(b,c)|-(d|->e) .tex= a;Î_fP|-Q⊃R .tex= Î_fP|-Q⊃R
%D @ 0 @ 1 |-> sl^ .plabel= a Æ^\flat @ 0 @ 1 <-| sl_ .plabel= b Æ^\sharp
%D @ 0 @ 3 <-| sl_ .plabel= l \Uncur @ 0 @ 3 |-> sl^ .plabel= r \Cur
%D @ 1 @ 2 -> sl_ .plabel= l \Frob; @ 1 @ 2 <- sl^ .plabel= r \Frobnat;
%D @ 2 @ 5 <-| sl_ .plabel= l \Uncur @ 2 @ 5 |-> sl^ .plabel= r \Cur
%D @ 3 @ 4 -> sl_ .plabel= l ;\Pimpnat @ 3 @ 4 <- sl^ .plabel= r ;\Pimp
%D @ 4 @ 5 |-> sl^ .plabel= a Æ^\flat @ 4 @ 5 <-| sl_ .plabel= b Æ^\sharp
%D ))
%D (( A B -> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{frob=pres-imp-2-semil}$$
% \newpage
%D diagram frob=pres-imp-2
%D 2Dx 100 +65
%D 2D Æ^b
%D 2D 100 a,b;(c,d)|-e |-----> a;(b,(c,d))|-e
%D 2D -^ <-----| -^
%D 2D || Æ^# nat||Frob
%D 2D Cur||Uncur v-
%D 2D +20 || a;((b,c),d)|-e
%D 2D v- -^
%D 2D +20 a,b;c|-(d|->e)_B ||
%D 2D -^ Cur||Uncur
%D 2D nat||PImp Æ^b ||
%D 2D v- |---> v-
%D 2D +20 a,b;c|-(d|->e)_A <---| a;(b,c)|-(d|->e)
%D 2D Æ^#
%D 2D
%D (( a,b;(c,d)|-e a;(b,(c,d))|-e
%D a;((b,c),d)|-e
%D a,b;c|-(d|->e)_B
%D a,b;c|-(d|->e)_A a;(b,c)|-(d|->e)
%D @ 0 @ 1 |-> sl^ .plabel= a Æ^\flat @ 0 @ 1 <-| sl_ .plabel= b Æ^\sharp
%D @ 0 @ 3 <-| sl_ .plabel= l \Uncur @ 0 @ 3 |-> sl^ .plabel= r \Cur
%D @ 1 @ 2 |-> sl_ .plabel= l \Frob; @ 1 @ 2 <-| sl^ .plabel= r \Frobnat;
%D @ 2 @ 5 <-| sl_ .plabel= l \Uncur @ 2 @ 5 |-> sl^ .plabel= r \Cur
%D @ 3 @ 4 |-> sl_ .plabel= l \Pimpnat @ 3 @ 4 <-| sl^ .plabel= r \Pimp
%D @ 4 @ 5 |-> sl^ .plabel= a Æ^\flat @ 4 @ 5 <-| sl_ .plabel= b Æ^\sharp
%D ))
%D enddiagram
%D
$$\diag{frob=pres-imp-2}$$
% \newpage
Let
$$\begin{array}{rcl}
A &\equiv& \E[a], \\
B &\equiv& \E[a,b], \\
b &\equiv& a,b \mto b, \\
C &\equiv& \O[a,b;c], \\
D &\equiv& \O[a;d], \\
E &\equiv& \O[a;e]. \\
\end{array}
$$
Then:
%
%D diagram frob=pres-imp-1-std
%D 2Dx 100 +40 +40 +40
%D 2D 100 a;((b,c),d) <==== a;(b,c) a;e ======> a;(d|->e)
%D 2D ^- /\ || ||
%D 2D nat||Frob || || ||
%D 2D -v || || ||
%D 2D +20 a;(b,(c,d)) || || \/
%D 2D +10 /\ || || a,b;(d|->e)_A
%D 2D || || || -^
%D 2D || || || nat||PImp
%D 2D || || \/ v-
%D 2D +20 a,b;(c,d) <====== a,b;c a,b;e ===> a,b;(d|->e)_B
%D 2D
%D (( a;((b,c),d) .tex= Æ_{b}C×D a;(b,c) .tex= Æ_{b}C
%D a;(b,(c,d)) .tex= Æ_b(C×b^*\!D)
%D a,b;(c,d) .tex= C×b^*\!D a,b;c .tex= C
%D @ 0 @ 1 <-| .plabel= a ×D
%D @ 0 @ 2 <- sl_ .plabel= l \Frobnat @ 0 @ 2 -> sl^ .plabel= r \Frob
%D @ 2 @ 3 <-| .plabel= l Æ_b @ 1 @ 4 <-| .plabel= r Æ_b
%D @ 3 @ 4 <-| .plabel= a ×b^*\!D
%D ))
%D (( a;e .tex= E a;(d|->e) .tex= D{->}E
%D a,b;(d|->e)_A .tex= b^*(D{->}E)
%D a,b;e .tex= b^*\!E a,b;(d|->e)_B .tex= b^*\!D{->}b^*\!E
%D @ 0 @ 1 |-> .plabel= a D{->}
%D @ 0 @ 3 |-> .plabel= l b^* @ 1 @ 2 |-> .plabel= r b^*
%D @ 2 @ 4 -> sl_ .plabel= l \Pimpnat @ 2 @ 4 <- sl^ .plabel= r \Pimp
%D @ 3 @ 4 |-> .plabel= b b^*\!D{->}
%D ))
%D ((
%D
%D ))
%D enddiagram
%D
$$\diag{frob=pres-imp-1-std}$$
%D diagram frob=pres-imp-2-std
%D 2Dx 100 +75
%D 2D cur^b
%D 2D 100 a;((b,c),d)|-e <----->| a;(b,c)|-(d|->e)
%D 2D -^ |-----> -^
%D 2D nat||Frob cur^# ||
%D 2D v- Æ^#||Æ^b
%D 2D +20 a;(b,(c,d))|-e ||
%D 2D -^ v-
%D 2D +20 || a,b;c|-(d|->e)_A
%D 2D Æ^b||Æ^# -^
%D 2D || cur^b nat||PImp
%D 2D v- <--------| v-
%D 2D +20 a,b;(c,d)|-e |--------> a,b;c|-(d|->e)_B
%D 2D cur^#
%D 2D
%D (( a;((b,c),d)|-e .tex= ((Æ_{b}C×D)->E) a;(b,c)|-(d|->e) .tex= (Æ_{b}C->(D{->}E))
%D a;(b,(c,d))|-e .tex= (Æ_b(C×b^*\!D)->E)
%D a,b;c|-(d|->e)_A .tex= (C->b^*(D{->}E))
%D a,b;(c,d)|-e .tex= ((C×b^*\!D)->b^*E) a,b;c|-(d|->e)_B .tex= (C->(b^*\!D{->}b^*\!E))
%D @ 0 @ 1 <- sl^ .plabel= a \Uncur @ 0 @ 1 -> sl_ .plabel= b \Cur
%D @ 0 @ 2 -> sl_ .plabel= l \Frobnat; @ 0 @ 2 <- sl^ .plabel= r \Frob;
%D @ 1 @ 3 -> sl_ .plabel= l Æ^\sharp @ 1 @ 3 <- sl^ .plabel= r Æ^\flat
%D @ 2 @ 4 -> sl_ .plabel= l Æ^\sharp @ 2 @ 4 <- sl^ .plabel= r Æ^\flat
%D @ 3 @ 5 -> sl_ .plabel= l ;\Pimpnat @ 3 @ 5 <- sl^ .plabel= r ;\Pimp
%D @ 4 @ 5 <- sl^ .plabel= a \Uncur @ 4 @ 5 -> sl_ .plabel= b \Cur
%D ))
%D enddiagram
%D
$$\diag{frob=pres-imp-2-std}$$
% --------------------
% «dn-arbitrary-cobs» (to ".dn-arbitrary-cobs")
% (subsec "Adjoints to Arbitrary Changes of Base" "dn-arbitrary-cobs")
\mysubsection {Adjoints to Arbitrary Changes of Base} {dn-arbitrary-cobs}
% --------------------
% «dn-lawvere-70-eq» (to ".dn-lawvere-70-eq")
% (subsec "Equality" "dn-lawvere-70-eq")
\mysubsection {Equality} {dn-lawvere-70-eq}
{\myttchars
% \footnotesize
\begin{verbatim}
(find-lawvere70page 6 "Substitutivity of equality")
\end{verbatim}
}
% (find-kopkadaly4page (+ 12 595) "\\textsc")
{\sl \textsc{Proposition (substitutivity of equality).} In any eed in
which, for every term $f:X \to Y$ and any two attributes $\aa$,
$\psi$ of type $Y$, the canonical deduction
%
$$f·(\aa \funto \psi) \to f·\aa \funto f·\psi$$
%
is an isomorphism, one also has, for any attribute $\psi$ of type $X$,
a canonical deduction
%
$$\Th_X \to \pi_1·\psi \funto \pi_2·\psi$$
%
over $X×X$.}
\msk
The first canonical deduction that he mentions is my derived rule
$\Pimpnat$:
%:
%:
%: f \aa \psi
%: ============================\Pimpnat
%: f·(\aa=>\psi)->f·\aa=>f·\psi
%:
%: ^law70-pimpnat-1
%: \aa \psi
%: ----------
%: \aa=>\psi
%: --------------------\id
%: \aa \psi \aa=>\psi->\aa=>\psi
%: --------- --------------------\Uncur
%: f \aa \aa=>\psi \aa∧\aa=>\psi->\psi
%: ---------------------------------\Pand -------------------------(f·)_1
%: f·\aa∧f·(\aa=>\psi)->f·(\aa∧\aa=>\psi) f·(\aa∧\aa=>\psi)->f·\psi
%: ------------------------------------------------------------------\Cur
%: f·\aa∧f·(\aa=>\psi)->f·\psi
%: ----------------------------\Cur
%: f·(\aa=>\psi)->f·\aa=>f·\psi
%:
%: ^law70-pimpnat-2
%:
$$\ded{law70-pimpnat-1}$$
which expands to:
$$\ded{law70-pimpnat-2}$$
The second deduction is this:
%:
%:
%: \phi
%: ==============
%: \phi∧1_X->\phi
%: ---------------\Cur
%: 1_X->\phi=>\phi
%: ----------------------\iso
%: 1_X->\id·\phi=>\id·\phi
%: ------------------------\ren
%: 1_X->(_1)·\phi=>(_2)·\phi _1·\psi _2·\psi
%: -------------------------------\iso --------------------------------------------------\Pimp
%: 1_X->·(_1·\psi)=>·(_2·\psi) ·(_1·\psi)=>·(_2·\psi)->·(_1·\psi=>_2·\psi)
%: -----------------------------------------------------------------------------------------;
%: 1_X->·(_1·\psi=>_2·\psi)
%: -------------------------------\Eq^\flat
%: 1_XÆ(X)->_1·\psi=>_2·\psi
%: -----------------------------\ren
%: \Th_X->_1·\psi=>_2·\psi
%:
%: ^law70-substeq1
%:
%:
$$\ded{law70-substeq1}$$
I just realized that I have never defined the ``iso'' rules... an
example:
%:
%: \aa \phi \psi
%: ===============
%: \aa<->\aa' \phi<->\phi' \psi<->\psi' \aa∧\phi=>\psi
%: -------------------------------------------------------\iso
%: (\aa∧\phi=>\psi)<->(\aa'∧\phi'=>\psi')
%:
%: ^iso-example
%:
$$\ded{iso-example}$$
% --------------------
% «notes-and-further» (to ".notes-and-further")
% (chap "Notes and Further Reading" "notes-and-further")
\mychapter {Notes and Further Reading} {notes-and-further}
I've learned hyperdoctrines from \cite{SeelyPLC}, \cite{SeelyBeck},
\cite{Jacobs}, and \cite{StreicherBenabou}, and I found the subject
very hard. The ideas from this paper can be used --- I hope! --- to
make it a bit simpler: we've seen how to split the theory in two
parts, and how to start by the syntactical part; and we can draw
diagrams with the same structure as the ones in these notes but using
the notations of other texts, and then we can compare the diagrams in
different notations and use them as dictionaries between the different
languages.
[To do: dictionaries for the papers and books above, and for
\cite{LawvereAdjFo} and \cite{LawvereEqHyp}. The most important
parts are the diagrams for the structure in $\bbB$ and $\bbE$ and
for the change-of-base functors and their adjoints --- the diagrams
for the preservations, BCCs and Frobenius don't really need to be
drawn, as they can be reconstructed from the others; we only need
the show the notation for the arrows in them that are required to be
isos.]
[I have the impression that there are very good accounts of fibrations
in \cite{TaylorPhDThesis} and \cite{Elephant1}, but I haven't read
them with enough attention yet.]
\msk
[I've learned monads from \cite{CWM}, \cite{BarrWells}, \cite{Schalk},
\cite{BeckPhDThesis} and \cite{Awodey}; compare their notations. To
do, also: create a comparison diagram for comonads (easy), discuss
the case of building $R[x]$ from $R$ when $R$ is a ring (good
references: \cite{LambekScott}, \cite{Awodey}). Try to find a
proto-proof for Lambek's theorem (that says that an initial algebra
in an Eilenberg-Moore category is an iso).]
[A medium-term goal: finish the downcasing of differential categories,
as presented in \cite{SeelyDiff}. I have crappy ascii-art
renderizations of some of the downcased diagrams here:
\url{http://angg.twu.net/2007diffcats.html} (but it may contain
errors). I don't understand enough of
\cite{SeelyCartDiff} yet.]
[I have a very nice downcasing of the best part of this: \cite{Kock77}
--- I presented it in seminars at UFF, but I'd look to clean it up
(I have better notations now), and I lost the source code for my
diagrams... (what is the URL of the PDF with the slides?)]
[This looks extremely interesting: \cite{KellyLack}, ``On
Property-Like Structures'' --- but its ideas are far above my head
now. It will be better to try to read it when I have more contact
with grown-up categorists.]
[This looks extremely interesting too: section D1.4, ``Syntactic
categories'', of \cite{Elephant2}.]
[Point to several parts of \cite{Kromer} where he discusses having
vs.\ not having elements; my `$a \mto b$' notation is like the
``internal view'' of morphisms that appears in [LawvereSchanuelCM],
p.13 (the ``internal diagram of a set''), and it's like a mix
between the usual `$x \mto f(x)$' and the `$y=y(x)$' notations.]
% (find-books "__cats/__cats.el" "lawvere")
% (chap "Abstract" "abstract")
% (chap "Introduction" "introduction")
% (sec "There Are no Theorems in This Paper" "no-theorems")
% (chap "The syntactical world" "syntactical-world")
% (sec "Categories" "proto-cats")
% (sec "Functors" "proto-functors")
% (sec "Natural Transformations" "proto-NTs")
% (sec "Isos" "proto-isos")
% (sec "Epis and Monics" "proto-epis-and-monics")
% (sec "Adjunctions" "proto-adjunctions")
% (sec "Monads" "proto-monads")
% (subsec "The Kleisli Category of a Monad" "proto-kleisli")
% (subsec "The Eilenberg-Moore Category of a Monad" "proto-EM")
% (subsec "The Comparison Theorem" "proto-comparison")
% (subsec "Monadicity" "proto-monadicity")
% (subsec "Beck's Lemma" "proto-beck")
% (sec "Universals" "proto-universals")
% (sec "The Yoneda Lemma" "proto-yoneda")
% (sec "Products" "proto-products")
% (sec "To Deserve a Name" "to-deserve-a-name")
% (subsec "Mad Names" "mad-names")
% (sec "Terminals" "proto-terminals")
% (sec "Exponentials" "proto-exponentials")
% (sec "Cartesian Categories" "proto-cart-cats")
% (sec "Cartesian Closed Categories" "proto-CCCs")
% (sec "Indexed Categories, Fibrations, Hyperdoctrines" "proto-ind-fib-hyp")
% (subsec "Subobjects" "proto-subobjects")
% (subsec "Indexed Categories" "proto-indexed-cats")
% (subsec "Cartesian Morphisms" "proto-cart-morphs")
% (subsec "Cleavages" "proto-cleavages")
% (subsec "Change-of-Base Functors" "proto-change-of-base")
% (subsec "The Logical Structure in Each Fiber" "proto-fibers")
% (subsec "Preservations" "proto-preservations")
% (subsec "Adjoints to Change-of-Base Functors" "proto-adjs-to-cobs")
% (chap "Downcasing Types" "dn-intro")
% (sec "Simple Proofs" "dn-simple")
% (sec "Functors" "dn-functors")
% (sec "Categories" "dn-cats")
% (sec "Pseudopoints" "dn-pseudopoints")
% (sec "Natural Transformations" "dn-NTs")
% (sec "Contexts" "dn-contexts")
% (subsec "Single Hypothesis: CCs" "dn-contexts-single")
% (subsec "Context Morphisms" "dn-context-morphs")
% (subsec "Several Hypotheses: CCs (With a Trick)" "dn-contexts-multi")
% (subsec "Discharges: CCCs" "dn-discharges")
% (sec "Adjunctions" "dn-adjunctions")
% (sec "Subsets" "dn-subsets")
% (sec "Subobjects" "dn-subobjects")
% (sec "Projection Functors" "dn-proj-functors")
% (sec "Some Uppercasings" "dn-uc-intro")
% (subsec "A Semi-Logical Notation" "dn-uc-semi-logical")
% (subsec "Lawvere" "dn-uc-lawvere")
% (subsec "Seely" "dn-uc-seely")
% (subsec "Jacobs" "dn-uc-jacobs")
% (subsec "Maclane" "dn-uc-maclane")
% (subsec "Awodey" "dn-uc-awodey")
% (sec "Change-of-base" "dn-change-of-base")
% (sec "Preservations" "dn-preservations")
% (sec "Display Maps" "dn-display-maps")
% (sec "Quantifiers" "dn-quantifiers")
% (sec "Equality" "dn-equality")
% (sec "Beck-Chevalley for `Exists'" "dn-bcc-for-exists")
% (sec "Beck-Chevalley for `For All'" "dn-bcc-for-forall")
% (sec "Beck-Chevalley for Equality" "dn-bcc-for-equality")
% (sec "Frobenius for `Exists'" "dn-frob-for-exists")
% (sec "Frobenius for Equality" "dn-frob-for-equality")
% (sec "Hyperdoctrines" "dn-hyperdoctrines")
% (sec "Three Theorems from Lawvere's ``Hyperdoctrines'' Paper" "dn-lawvere-70")
% (subsec "Frob and Pimp" "dn-frob-and-pimp")
% (subsec "Adjoints to Arbitrary Changes of Base" "dn-arbitrary-cobs")
% (subsec "Equality" "dn-lawvere-70-eq")
% (chap "Notes and Further Reading" "notes-and-further")
%: a,b;c ======> a;(b,c)
%: - -
%: a|-D a,b;c|-d | | a;(b,c)|-d
%: --------------Æ^\flat | | ----------Æ^\sharp
%: a;(b,c)|-d | | a,b;c|-d
%: | |
%: ^Si-flat-0 | | ^Si-sharp-0
%: | |
%: a|-D_a a,b;c|-d_{abc} | | a;p|-d_{ap}
%: ----------------------Æ^\flat | Æ^\flat | ---------------------------Æ^\sharp
%: a;p|-d_{abc}[b,c:=\unp{p}] | |---> | a,b;c|-d_{ap}[p:=\ang{b,c}]
%: | <---| |
%: ^Si-flat-1 | Æ^\sharp | ^Si-sharp-1
%: | |
%: (beta) a|-D_a a,b;c|-d_{abc} | | a;p|-d_{ap} (eta)
%: --------------------------Æ^\flat | | ---------------------------Æ^\sharp
%: a;p|-d_{abc}[b,c:=\unp{p}] | | a,b;c|-d_{ap}[p:=\ang{b,c}]
%: ------------------------------------Æ^\sharp | | ---------------------------------------Æ^\flat
%: a,b;c|-d_{abc}[b,c:=\unp{p}][p:=\ang{b,c}] | | a;p|-d_{ap}[p:=\ang{b,c}][b,c:=\unp{p}]
%: ----------------------------------------\ren | | ---------------------------------------\ren
%: a,b;c|-d_{abc}[b,c:=\unp{\ang{b,c}}] | | a;p|-d_{ap}[p:=\ang{\unp{p}}]
%: v v
%: ^Si-beta v v ^Si-eta
%: v v
%: a,b;d <======== a;d
%: - -
%: a|-D a,b;d|-e | | a;d|-(b|->e)
%: --------------å^\sharp | | ------------å^\flat
%: a;d|-(b|->e) | | a,b;d|-e
%: | |
%: ^Pi-sharp0 | | ^Pi-flat0
%: | |
%: a|-D_a a,b;d|-e_{abd} | å^\flat | a;d|-f_{ad}
%: ----------------------å^\sharp | <---| | --------------å^\flat
%: a;d|-ðb.e_{abd} | |---> | a,b;d|-f_{ad}b
%: | å^\sharp |
%: ^Pi-sharp1 | | ^Pi-flat1
%: | |
%: a|-D_a a,b;d|-e_{abd} | | a;d|-f_{ad}
%: ----------------------å^\sharp | | --------------å^\flat
%: (beta) a;d|-ðb.e_{abd} | | a,b;d|-f_{ad}b (eta)
%: --------------------å^\flat | | -----------------å^\sharp
%: a,b;d|-(ðb.e_{abd})b | | a;d|-ðb.(f_{ad}b)
%: v v
%: ^Pi-beta v v ^Pi-eta
%: v v
%: a,b;e =====> a;(b|->e)
%:
%:
%:
%:
$$\ded{Si-flat-0} \qquad \ded{Si-sharp-0}$$
$$\ded{Si-flat-1} \qquad \ded{Si-sharp-1}$$
$$\ded{Si-beta} \qquad \ded{Si-eta}$$
\bsk
$$\ded{Pi-sharp0} \qquad \ded{Pi-flat0}$$
$$\ded{Pi-sharp1} \qquad \ded{Pi-flat1}$$
$$\ded{Pi-beta} \qquad \ded{Pi-eta}$$
% (find-LATEX "2008hyp.tex" "adj-functors-as-seq-rules")
% (find-xpdfpage "~/LATEX/2008hyp.pdf" 24)
% (find-dvipage "~/LATEX/2008hyp.dvi" 24)
% (find-LATEX "2008hyp.tex" "adj-maps-as-seq-rules")
% (find-xpdfpage "~/LATEX/2008hyp.pdf" 26)
% (find-dvipage "~/LATEX/2008hyp.dvi" 26)
%D diagram adj-exfa-flsh
%D 2Dx 100 +30
%D 2D 100 Pab ===> Îb.Pab
%D 2D - |b> -
%D 2D | |
%D 2D v <#| v
%D 2D +30 Qa <====== Qa{}
%D 2D - <b| -
%D 2D | |
%D 2D v |#> v
%D 2D +30 Rab ===> ýb.Rab
%D 2D
%D 2D +15 a,b |----> a
%D 2D
%D (( Pab Îb.Pab Qa Qa{} Rab ýb.Rab a,b a
%D @ 0 @ 1 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 3 <=
%D @ 2 @ 4 |-> @ 3 @ 5 |->
%D @ 4 @ 5 =>
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl^ .plabel= a \flat
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl_ .plabel= b \sharp
%D @ 2 @ 5 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D @ 2 @ 5 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D @ 6 @ 7 |->
%D ))
%D enddiagram
$$\diag{adj-exfa-flsh}$$
% \end{document}
% (find-kopkadaly4page (+ 12 644) "title page")
% (find-kopkadaly4text)
% (find-kopkadaly4page (+ 12 52) "3.3.1 Title page")
% (find-kopkadaly4text "3.3.1 Title page")
Missing: in the fat presentation for hyps we have the three
preservations, two generic BCCs and generic frob;
% (find-es "tex" "shortvrb")
% (find-LATEX "2008filterp.tex")
% (find-LATEX "2009-planodetrabalho.tex")
% (find-LATEX "catsem.bib" "test")
% (find-LATEX "filters.bib")
% (find-zsh "makebbl 2009-planodetrabalho.bbl catsem,filters")
% (find-es "tex" "makebbl")
% \bibliographystyle{alpha}
\bibliography{catsem,filters}
\bibliographystyle{alpha}
\printindex
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: