|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2012minicats.tex")
% (find-angg ".emacs" "minicats")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (find-angg "bin/dednat5")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && dednat5 -t 2012minicats.tex && latex 2012minicats.tex" 1 '(eek "M->")))
% (defun cp () (interactive) (find-zsh "cd ~/LATEX/ && dednat5 -t 2012minicats.tex && pdflatex 2012minicats.tex" 1 '(eek "M->")))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2012minicats.tex && latex 2012minicats.tex"))
% (defun cp () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2012minicats.tex && pdflatex 2012minicats.tex"))
% (eev "cd ~/LATEX/ && Scp 2012minicats.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2012minicats.dvi"))
% (defun dp () (interactive) (find-xpdfpage "~/LATEX/2012minicats.pdf"))
% (find-dvipage "~/LATEX/2012minicats.dvi")
% (find-pspage "~/LATEX/2012minicats.ps")
% (find-pspage "~/LATEX/2012minicats.pdf")
% (find-xpdfpage "~/LATEX/2012minicats.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvipdf 2012minicats.dvi 2012minicats.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2012minicats.ps 2012minicats.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2012minicats.ps 2012minicats.dvi && ps2pdf 2012minicats.ps 2012minicats.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2012minicats.pdf" (ee-twupfile "LATEX/2012minicats.pdf") 'over)
% (ee-cp "~/LATEX/2012minicats.pdf" (ee-twusfile "LATEX/2012minicats.pdf") 'over)
% (ee-cp "~/LATEX/2012minicats.dvi" (ee-twusfile "LATEX/2012minicats.dvi") 'over)
% (find-twusfile "LATEX/" "2012minicats")
% http://angg.twu.net/LATEX/2012minicats.pdf
% http://angg.twu.net/LATEX/2012minicats.dvi
% (find-TH "2012-unb")
% The format will be the same as:
% (find-angg "LATEX/2010unilog-current.tex")
% «.defs-sections» (to "defs-sections")
% «.defs-other» (to "defs-other")
% «.program-1» (to "program-1")
% «.program-2» (to "program-2")
% «.functions-explicitly» (to "functions-explicitly")
% «.functions-ret-functions» (to "functions-ret-functions")
% «.groups-as-sp» (to "groups-as-sp")
% «.groups-as-sp-2» (to "groups-as-sp-2")
% «.groups-as-sp-3» (to "groups-as-sp-3")
% «.cats-as-sp» (to "cats-as-sp")
% «.cats-as-sp-2» (to "cats-as-sp-2")
% «.Set-as-cat» (to "Set-as-cat")
% «.explicit-subcats» (to "explicit-subcats")
% «.wellpos-subsets-of-N2» (to "wellpos-subsets-of-N2")
% «.wellpos-subsets-of-N2-2» (to "wellpos-subsets-of-N2-2")
% «.BPMK-not-protocat» (to "BPMK-not-protocat")
% «.BPM*K-as-protocat» (to "BPM*K-as-protocat")
% «.BPM*K-as-cat» (to "BPM*K-as-cat")
% «.cats-from-graphs» (to "cats-from-graphs")
% «.commutative-diags» (to "commutative-diags")
% «.coherence» (to "coherence")
% «.terminal-in-Set» (to "terminal-in-Set")
% «.prods-in-set» (to "prods-in-set")
% «.terminals-categorically» (to "terminals-categorically")
% «.products-categorically» (to "products-categorically")
% «.without-products» (to "without-products")
% «.terminals-are-isomorphic» (to "terminals-are-isomorphic")
% «.terminals-are-isomorphic» (to "terminals-are-isomorphic")
% «.cat-without-1-and-prod» (to "cat-without-1-and-prod")
% «.cats-with-1-and-prod» (to "cats-with-1-and-prod")
% «.Ax-in-Set» (to "Ax-in-Set")
% «.a-NT-in-Set» (to "a-NT-in-Set")
% «.exponentials-in-Set» (to "exponentials-in-Set")
% «.exponentials-categorically» (to "exponentials-categorically")
% «.adjunctions» (to "adjunctions")
% «.adjoints-are-isomorphic» (to "adjoints-are-isomorphic")
% «.lambda-intro» (to "lambda-intro")
% «.lambda-reductions» (to "lambda-reductions")
% «.lambda-calc-in-a-CCC» (to "lambda-calc-in-a-CCC")
% «.videos» (to "videos")
\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\usepackage[x11names]{xcolor} % (find-es "tex" "xcolor")
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\input 2012minicats.dnt
\begin{document}
%\input 2012minicats.dnt
% (find-LATEX "2011ebl-slides.tex")
% (find-dn4 "dednat4.lua" "lplacement")
% (find-dn4file "dednat4.lua" "When lplacement")
% (find-dn5grep "grep -nH -e placement *.lua")
% (find-dn5 "parse.lua")
% (find-dn5 "dednat5.lua")
% (find-dn5file "dednat5.lua")
% (find-dn5file "dednat5.lua" "local lplace =")
% (find-dn5 "build.lua")
% (defun m () (interactive) (find-dn5sh "lua51 build.lua"))
%
%L forths["sl^^"] = function () ds:pick(0).slide = "5pt" end
%L forths["sl^"] = function () ds:pick(0).slide = "2.5pt" end
%L forths["sl_"] = function () ds:pick(0).slide = "-2.5pt" end
%L forths["sl__"] = function () ds:pick(0).slide = "-5pt" end
%L forths["<-"] = function () pusharrow("<-") end
%L forths["<-|"] = function () pusharrow("<-|") end
%L forths["<--"] = function () pusharrow("<--") end
%L forths[".PLABEL="] = function ()
%L ds:pick(0).lplacement = PP(getword())
%L ds:pick(0).label = PP(getword())
%L end
%%L forths[".PLABEL="] = function () PP(getword(), getword()) end
% (find-es "lua5" "setvbuf")
%L io.stdout:setvbuf("no")
%L _arrow_to_TeX = function (arrow)
%L local node1 = nodes[arrow.from]
%L local node2 = nodes[arrow.to]
%L local x1, y1 = realxy(node1.x, node1.y)
%L local x2, y2 = realxy(node2.x, node2.y)
%L local dx, dy = x2 - x1, y2 - y1
%L local N1 = node_to_TeX(node1)
%L local N2 = node_to_TeX(node2)
%L local Label = arrow.Label or (arrow.label and unabbrev(arrow.label))
%L local L = Label and "{"..Label.."}" or ""
%L --
%L local p = arrow.placement and "|"..arrow.placement.."|" or ""
%L local shape = arrow.shape or "->"
%L local slide = arrow.slide and "@<"..arrow.slide..">"
%L local curve = arrow.curve and "@/"..arrow.curve.."/"
%L -- local lplace = arrow.lplacement and arrow.lplacement.."{"..label.."}"
%L local lplace = arrow.lplacement and arrow.lplacement..L
%L -- PP(lplace)
%L local sh
%L if slide or curve or lplace then
%L sh = format("/{@{%s}%s%s%s}/", shape,
%L (lplace or ""), (slide or ""), (curve or ""))
%L else
%L sh = "/"..shape.."/"
%L end
%L if lplace then p = "||"; L = "" end
%L --
%L return format("\\morphism(%d,%d)%s%s<%d,%d>[%s`%s;%s]",
%L x1, y1, p, sh, dx, dy, N1, N2, L)
%L end
%*->*\to *
%*|-*\vdash *
% «defs-sections» (to ".defs-sections")
% (find-dn4ex "edrx08.sty" "slides")
%
\mylosopen{tmp.los}
\def\mylosadd #1{\addtocontents{mylos}{#1}}
\def\anchorto #1#2#3{\hypertarget{#1}{\href{\##2}{#3}}}
%
% Pseudocode:
%
% \toctag {tag}
% -> % <tag> (to "tag")
% \toclinetext {Slide name}
% -> \textcolor {Firebrick4} {Slide name}
% \tocline {Slide name} {pagen}
% -> \par
% \anchorto {.pagen} {pagen} {
% \toclinetext {Slide name}
% } \dotfill pagen
%
% \myslidetext {Slide name}
% -> \textcolor {Firebrick4} {\bf Slide name}
% \myslide {Slide name} {tag}
% -> \newpage
% \mylosadd {\protect\toctag {tag}}
% \mylosadd {\protect\tocline {Slide name} {\thispagen}}
% \anchorto {\thispagen} {.\thispagen} {
% \myslidetext{Slide name}
% }
%
\def\thispagen{\the\count0}
\def\toctag#1{}
\def\toclinetext#1{#1}
\def\tocline#1#2{
\par
\anchorto {.#2} {#2} {\toclinetext{#1}}
\dotfill #2
}
\def\myslidetext#1{{\bf #1}}
\def\myslide#1#2{
\newpage
%\mylosadd{\protect\toctag {#2}}
\mylosadd {\protect\tocline {#1} {\thispagen}}
% \anchorto {\thispagen} {.\thispagen} {\myslidetext{#2}}
\anchorto {\thispagen} {.\thispagen} {\myslidetext{\thispagen. #1}}
}
% «defs-other» (to ".defs-other")
\def\Sets{Ð{Sets}}
\def\BPM{\mathsf{BPM}}
\def\Re{\mathfrak{Re}}
\def\Im{\mathfrak{Im}}
\def\idLR{\mathsf{idLR}}
\def\SetBdC{\Set^{B \ot * \to C}}
\def\onemto#1#2{\sm{#1 \mto #2}}
\def\twomtos#1#2#3#4{\sm{#1 \mto #2 \\ #3 \mto #4}}
\def\threemtos#1#2#3#4#5#6{\sm{#1 \mto #2 \\ #3 \mto #4 \\ #5 \mto #6}}
\def\fourmtos#1#2#3#4#5#6#7#8{\sm{#1 \mto #2 \\ #3 \mto #4 \\ #5 \mto #6 \\ #7 \mto #8}}
\def\ph#1{\leavevmode\phantom{#1}}
%*
% (eedn4-51-bounded)
Index of the slides:
\msk
% To update the list of slides uncomment this line:
%\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\tocline {Program (1)} {2}
\tocline {Program (2)} {3}
\tocline {Functions, explicitly} {4}
\tocline {Functions that return functions} {5}
\tocline {Groups as structure plus properties} {6}
\tocline {Groups as structure plus properties (2)} {7}
\tocline {Groups as structure plus properties (3)} {8}
\tocline {Categories as structure plus properties} {9}
\tocline {Categories as structure plus properties (2)} {10}
\tocline {$\mathbf {Set}$ as a category} {11}
\tocline {Finite subcategories of $\mathbf {Set}$, explicitly} {12}
\tocline {Well-positioned subsets of $\mathbb {N}^2$} {13}
\tocline {Well-positioned subsets of $\mathbb {N}^2$ (2)} {14}
\tocline {$\mathsf {BPM}(K)$ is not a protocategory} {15}
\tocline {$\mathsf {BPM}^*(K)$ is a protocategory} {16}
\tocline {BPM*(K) is a category} {17}
\tocline {Two categories generated by graphs} {18}
\tocline {Commutative diagrams} {19}
\tocline {Coherence} {20}
\tocline {A terminal object in $\mathbf {Set}$} {21}
\tocline {Products in Set} {22}
\tocline {Terminals, categorically} {23}
\tocline {Products, categorically} {24}
\tocline {A category without products} {25}
\tocline {Terminals are isomorphic} {26}
\tocline {Products are isomorphic} {27}
\tocline {A category without terminals and products} {28}
\tocline {Categories with terminals and products} {29}
\tocline {A functor in Set: Ax} {30}
\tocline {A natural transformation in Set} {31}
\tocline {Exponentials in Set} {32}
\tocline {Exponentials, categorically} {33}
\tocline {Adjunctions} {34}
\tocline {Adjoints are isomorphic} {35}
\par
%*
% --------------------
% «program-1» (to ".program-1")
% (s "Program (1)" "program-1")
\myslide {Program (1)} {program-1}
\msk
\par (Original draft, oct/2011...)
{\myttchars
\footnotesize
\begin{verbatim}
(1) Categorias como "estrutura" (objetos, Hom, identidade, composição)
e "propriedades" (a composição é associativa, identidades se
comportam como deveriam). Comparação com grupos, anéis, etc;
"dependent types".
(2) Nossas categorias preferidas: Set, categorias finitas dadas
explicitamente, posets, categorias de grupos, anéis, espaços
topológicos, categorias de subobjetos.
(3) Funtores e transformações naturais. Diagramas e condições de
coerência. Introdução ao lambda-cálculo tipado (em Set). Notação
lambda para morfismos. Beta-redução (para composição). Produtos de
objetos. Produtos como "estrutura" + "propriedades". Prova de que
dois produtos P e P' são isomorfos. Como deixar em segundo plano a
prova de que as compostas P->P'->P e P'->P->P' são identidades.
Como isolar as "construções". Análise de provas do MacLane, do
Awodey e do Beck.
(4) Categorias cartesianas. A linguagem interna de uma categoria
cartesiana: uplas e projeções. Tradução entre linguagem interna e
linguagem categórica.
(5) Uma categoria cartesiana abstrata: a CC livre gerada pelos objetos
A_1,...,A_n. A definição formal (categórica) de "livre".
(6) Os funtores (×B) e (B->) em Set. A adjunção (×B)-|(B->). Adjunções
como "estrutura" e "propriedades". Proto-adjunções (só a parte
"estrutura" das adjunções). Unidades e counidades. O teorema sobre
vários modos equivalentes de especificar uma adjunção. Categorias
cartesianas fechadas ("CCC"s). A linguagem interna de uma CCC.
Tradução entre linguagem interna e linguagem categórica. Em que
sentido esta tradução é "fiel".
\end{verbatim}
}
% --------------------
% «program-2» (to ".program-2")
% (s "Program (2)" "program-2")
\myslide {Program (2)} {program-2}
{\myttchars
\footnotesize
\begin{verbatim}
(7) Adjunções em posets. Como calcular "P->Q" num certo poset. Posets
como espaços de valores de verdade. Cálculo proposicional num
poset. Como calcular a "coimplicação" neste poset. A relação entre
adjunções e produtos.
(8) A tradução entre cálculo de seqüentes, dedução natural e operações
numa CCC. Uma tradução correspondente para lambda-cálculo.
Curry-Howard. Reduções em demonstrações em dedução natural.
(9) Outros posets nos quais podemos fazer cálculo proposicional
(intuicionista). Categorias de funtores. Categorias da forma 2^D,
onde D é um poset finito "plano". Representação gráfica explícita
dos objetos destas categorias. Valores de verdade como subobjetos.
Lógica modal (S4) nestas categorias. "Necessário" como "interior".
Cálculo proposicional num espaço topológico qualquer.
(10) Introdução à noção de "feixe": coberturas, colagens, duas noções
de saturação. Categorias da forma Set^D ("prefeixes"). Exemplos de
prefeixes que são e que não são feixes.
(11) O classificador de subobjetos em categorias da forma Set^D.
Introdução à linguagem interna de um topos.
(12) O lema de Yoneda (versão "proto"). Funtores representáveis.
(13) Mônadas e álgebras. As categorias de Kleisli e Eilenberg-Moore de
uma mônada. O teorema da comparação (versão "proto").
(14) Mônadas em linguagens funcionais.
(15) Morfismos geométricos num caso particular. Feixificação num caso
particular.
\end{verbatim}
}
% --------------------
% «functions-explicitly» (to ".functions-explicitly")
% (s "Functions, explicitly" "functions-explicitly")
\myslide {Functions, explicitly} {functions-explicitly}
\msk
\par The two functions below,
\msk
\par
$
\begin{array}{rcccl}
f &:& \N & \to & \N \\
&& n & \mto & 3+n \\
\end{array}
$
\msk
\par and
\msk
\par
$
\begin{array}{rcccl}
g &:& \N & \to & \N \\
&& n & \mto & 1+(n+2) \\
\end{array}
$
\msk
\par are mathematically the \und{same} function,
\par even though they are \und{syntactically different}
\par and they correspond to {\sl different algorithms}...
\msk
\par Mathematicians tend to think that functions
\par \und{are} their graphs --- i.e., sets of ordered pairs.
\msk
\par For example, if
$$
\begin{array}{rcccl}
h &:& \N & \to & \N \\
&& n & \mto & 10n \\
\end{array}
$$
\par Then $h = \{(2,20),(3,30)\}$.
\par We will often write this as $\twomtos 2{20} 3{30}$
\par or as $\left\{\twomtos 2{20} 3{30}\right\}$.
% --------------------
% «functions-ret-functions» (to ".functions-ret-functions")
% (s "Functions that return functions" "functions-ret-functions")
\myslide {Functions that return functions} {functions-ret-functions}
\msk
\par We will often have to deal with {\sl functions that return functions}.
\par For example:
\msk
\par
$
\def\ma{
\begin{array}{rcccl}
m_a &:& \{10,100\} & \to & \N \\
&& b & \mto & ab \\
\end{array}
}
%
\begin{array}{rcccl}
m &:& \{2,3\} & \to & \N^{\{10,100\}} \\
&& a & \mto & \left(\ma\right) \\
\end{array}
$
\msk
\par Then $(m(2))(10) = m_2(10) = 2·10 = 20$,
\par $m = \{(2, m_2), (3, m_3)\}$,
\par $m = \{(2, \{(10, 20),(100,200)\}),
(3, \{(10, 20),(100,200)\})\}$.
\msk
\par Using the other notation,
\par $
\def\mtwo {\{\twomtos {10}{20} {100}{200}\}}
\def\mthree{\{\twomtos {10}{30} {100}{300}\}}
\def\mtwo {\left\{\twomtos {10}{20} {100}{200}\right\}}
\def\mthree{\left\{\twomtos {10}{30} {100}{300}\right\}}
m = \left\{ \twomtos 2{\mtwo} 3{\mthree} \right\}
$
% --------------------
% «groups-as-sp» (to ".groups-as-sp")
% (s "Groups as structure plus properties" "groups-as-sp")
\myslide {Groups as structure plus properties} {groups-as-sp}
\msk
\par A group $G$ is (formally) a tuple, whose components are:
\par * an underlying set, usually also called $G$,
\par * a binary operation, $·:G×G \to G$,
\par * an identity element, $eÝG$,
\par * a unary operation, $(·)³:G \to G$,
\par * the guarantee that $e$ ``behaves as expected'',
\par * the guarantee that $·$ ``behaves as expected'',
\par * the guarantee that $(·)³$ ``behaves as expected''.
\msk
\par So: $G = (G, ·, e, (·)³; Ð{idLR}, Ð{assoc}, Ð{invLR})$,
\par where:
\par $Ð{idLR} \equiv (ýaÝG.\, ea=a) ∧ (ýaÝG.\, ae=a)$,
\par $Ð{assoc} \equiv (ýaÝG.\, ýbÝG.\, ýcÝG.\, a(bc)=(ab)c)$,
\par $Ð{invLR} \equiv (ýaÝG.\, aa³=e) ∧ (ýaÝG.\, a³a=e)$,
\bsk
\par Let's clean this up...
\par $G = (G_0, ·, e, (·)³; Ð{idLR}, Ð{assoc}, Ð{invLR})$,
\par where:
\par * $G_0 : \Sets$,
\par * $e : G_0$,
\par * $· : G_0×G_0 \to G_0$,
\par * $(·)³ : G_0 \to G_0$,
\par * $Ð{idLR}$ is a proof of $(ýaÝG_0.\, ea=a) ∧ (ýaÝG_0.\, ae=a)$,
\par * $Ð{assoc}$ is a proof of $(ýaÝG_0.\, ýbÝG_0.\, ýcÝG_0.\, a(bc)=(ab)c)$,
\par * $Ð{invLR}$ is a proof of $(ýaÝG_0.\, aa³=e) ∧ (ýaÝG_0.\, a³a=e)$.
\bsk
\par More generally:
\par $G = (G_0, ·_G, e_G, (·)³_G; Ð{idLR}_G, Ð{assoc}_G, Ð{invLR}_G)$.
% --------------------
% «groups-as-sp-2» (to ".groups-as-sp-2")
% (s "Groups as structure plus properties (2)" "groups-as-sp-2")
\myslide {Groups as structure plus properties (2)} {groups-as-sp-2}
\msk
\par $G = (G_0, ·, e, (·)³; Ð{idLR}, Ð{assoc}, Ð{invLR})$,
\par where:
\par * $G_0 : \Sets$,
\par * $e : G_0$,
\par * $· : G_0×G_0 \to G_0$,
\par * $(·)³ : G_0 \to G_0$,
\par * $Ð{idLR}$ is a proof of $(ýaÝG_0.\, ea=a) ∧ (ýaÝG_0.\, ae=a)$,
\par * $Ð{assoc}$ is a proof of $(ýaÝG_0.\, ýbÝG_0.\, ýcÝG_0.\, a(bc)=(ab)c)$,
\par * $Ð{invLR}$ is a proof of $(ýaÝG_0.\, aa³=e) ∧ (ýaÝG_0.\, a³a=e)$.
\bsk
\par {\sl Constructing} ({\sl exhibiting}) a group $G$ means:
\par * {\sl choosing} a set $G_0$,
\par * {\sl choosing} an element $e:G_0$
\par * {\sl choosing} a function $·:G_0×G_0 \to G_0$
\par * {\sl choosing} a function $(·)³:G_0 \to G_0$,
\par * {\sl proving} that $(ýaÝG_0.\, ea=a) ∧ (ýaÝG_0.\, ae=a)$,
\par * {\sl proving} that $(ýaÝG_0.\, ýbÝG_0.\, ýcÝG_0.\, a(bc)=(ab)c)$,
\par * {\sl proving} that $(ýaÝG_0.\, aa³=e) ∧ (ýaÝG_0.\, a³a=e)$.
\bsk
\par Note:
\par `:' is roughly the same as `$Ý$', so
\par $e : G_0$ is roughly the same as $e Ý G_0$;
\par $\Sets$ is the class of all sets (the ``set of all sets''), so
\par $G_0:\Sets$ means that $G_0$ is a set;
\par $A \to B$ will be regarded as the set $B^A$, so
\par $f: A \to B$ means $f Ý B^A$, i.e.,
\par $f$ is an element of the set of all functions from $A$ to $B$.
% --------------------
% «groups-as-sp-3» (to ".groups-as-sp-3")
% (s "Groups as structure plus properties (3)" "groups-as-sp-3")
\myslide {Groups as structure plus properties (3)} {groups-as-sp-3}
\msk
\par Fact 1: when we see the {\sl name} of an object
\par we often know which {\sl type} it is expected to have.
\par (We will not formalize this!)
\msk
\par Fact 2: it is possible to define
\par the set of proofs of $(ýaÝG_0.\, ea=a) ∧ (ýaÝG_0.\, ae=a)$,
\par and then say: $Ð{idLR} : Ð{Proofs}[(ýaÝG_0.\, ea=a) ∧ (ýaÝG_0.\, ae=a)]$.
\par (We will not formalize this, either.)
\msk
\par Fact 3: it is {\sl sometimes} sufficient to say just this,
\par $G = (G_0, ·, e, (·)³; Ð{idLR}, Ð{assoc}, Ð{invLR})$,
\par and our interlocutors will be able to figure out by themselves
\par the (implicit) types of all the components.
\bsk
\par The first four components of the tuple
\par $G = (G_0, ·, e, (·)³; Ð{idLR}, Ð{assoc}, Ð{invLR})$
\par will be called the ``structure'' part of $G$; their types
\par involve just known objects (the class $\Sets$), and `:', `$×$', `$\to$'.
\msk
\par Note that after `$G_0: \Sets$' the value of $G_0$ is a ``known object'',
\par and the declaration `$·:G_0×G_0 \to G_0$' makes sense.
\msk
\par The last three components of the tuple
\par $G = (G_0, ·, e, (·)³; Ð{idLR}, Ð{assoc}, Ð{invLR})$
\par will be called the ``properties'' part of $G$; their types
\par involve `$Ð{Proofs}$', quantifiers, {\bf equalities}, {\bf equations}...
\bsk
\par Conventions:
\par * a `;' separates the ``structure'' from the ``properties''
\par * $G = (G_0, ·, e, (·)³; Ð{idLR}, Ð{assoc}, Ð{invLR})$ is a group,
\par * $G^- = (G_0, ·, e, (·)³)$ is a {\bf proto-group};
\par * each definition of a structure will have a corresponding proto-structure.
% --------------------
% «cats-as-sp» (to ".cats-as-sp")
% (s "Categories as structure plus properties" "cats-as-sp")
\myslide {Categories as structure plus properties} {cats-as-sp}
\msk
\par Informally, a {\sl Category} is a directed graph
\par in which the arrows can be composed (when they ``match''),
\par the composition is associative,
\par and we have identity arrows, that behave as expected.
\msk
\par A bit more formally:
\par $\catC = \{\catC_0, \Hom_\catC, ¢_\catC, \id_\catC; \assoc_\catC, \idLR_\catC\}$
\par where:
\par * $\catC_0$ is the set of vertices,
\par * $\Hom_\catC(A,B)$ is the set of arrows from $A$ to $B$,
\par * for any $A, B, C Ý \catC_0$ we have
%
$$\begin{array}{rcccl}
¢_{\catC\,ABC} &:& \Hom_\catC(B,C)×\Hom_\catC(A,B) &\to& \Hom_\catC(A,C) \\
& & (g_{BC},\;f_{AB}) &\mto& g_{BC}¢f_{AB} \\
\end{array} \quad
$$
%D diagram comp
%D 2Dx 100 +30 +30
%D 2D 100 A ---> B ---> C
%D 2D
%D (( A B -> .plabel= a f_{AB}
%D B C -> .plabel= a g_{BC}
%D A C -> .slide= 15pt .plabel= a g_{BC}¢f_{AB}
%D A C -> .slide= -12pt .plabel= b f_{AB};g_{BC}
%D ))
%D enddiagram
%D
$$\diag{comp}$$
\par * for any $AÝ\catC_0$ we have an ``identity arrow'' $\id_\catC(A) Ý \Hom_\catC(A,B)$,
\par * for any $A, B, C, D Ý \catC_0$ and arrows $f_{AB}$, $g_{BC}$, $h_{CD}$ we have:
%D diagram assoc
%D 2Dx 100 +30 +30 +30
%D 2D 100 A ---> B ---> C ---> D
%D 2D
%D (( A B -> .plabel= a f_{AB}
%D B C -> .plabel= a g_{BC}
%D C D -> .plabel= a h_{CD}
%D A C -> .slide= 15pt .plabel= a f_{AB};g_{BC}
%D B D -> .slide= -12pt .plabel= b g_{BC};h_{CD}
%D A D -> .slide= -27pt .plabel= b f_{AB};(g_{BC};h_{CD})=(f_{AB};g_{BC});h_{CD}
%D ))
%D enddiagram
%D
$$\diag{assoc}$$
\par * for any $A, B Ý \catC_0$ and $f_{AB}$ we have $\id_A;f_{AB} = f_{AB} = f_{AB};\id_B$.
% \par $\catC = \{\catC_0, \Hom, ¢, \id; \assoc, \idLR\}$
%D diagram ids
%D 2Dx 100 +30
%D 2D 100 A --> B
%D 2D
%D (( A B -> .plabel= a f_{AB}
%D A loop (dl,ul)^{\id_A}
%D B loop (ur,dr)^{\id_B}
%D ))
%D enddiagram
%D
$$\diag{ids}$$
% --------------------
% «cats-as-sp-2» (to ".cats-as-sp-2")
% (s "Categories as structure plus properties (2)" "cats-as-sp-2")
\myslide {Categories as structure plus properties (2)} {cats-as-sp-2}
\msk
\par $\catC = \{\catC_0, \Hom, ¢, \id; \assoc, \idLR\}$,
\par where:
\par * $\catC_0 : \Sets$ \qquad (in our ``small categories'')
\par * $\Hom : \catC_0×\catC_0 \to \Set$
\par * for any $A$, $B$, $C$ we have $¢_{ABC} : \Hom(B,C) \to \Hom(A,B) \to \Hom(A,C)$
\par * for any $A$ we have $\id(A) : \Hom(A,A)$
\par * $\assoc$ is a proof of
%
$$ýA,B,C,D,f_{AB},g_{BC},h_{CD}.\, (f_{AB};g_{BC});h_{CD} = f_{AB};(g_{BC};h_{CD})$$
\par * $\idLR$ is a proof of $ýA,B,f_{AB}.\, \id_A;f_{AB} = f_{AB} = f_{AB};\id_B$
% --------------------
% «Set-as-cat» (to ".Set-as-cat")
% (s "$Set$ as a category" "Set-as-cat")
\myslide {$\Set$ as a category} {Set-as-cat}
\msk
\par Our archetypical category is $\Set$.
\par * $\Set_0 = \Sets$ (the objects of $\Set$ are sets),
\par * $\Hom_\Set(A,B) =$ the set of all functions from $A$ to $B$,
\par * $f ¢_\Set g$ is the composition of functions, $f¢g$
\par * $\id_\Set(A)$ is the identity map $\id_A: A \to A$.
\msk
\par [EXERCISE: prove $\assoc_\Set$ and $\idLR_\Set$].
\msk
\par When we look at $\Set$ as a graph (with composition and ids),
\par it is a HUGE graph --- to many vertices, too many arrows.
\par Let's see two simple ways to define smaller categories.
% --------------------
% «explicit-subcats» (to ".explicit-subcats")
% (s "Finite subcategories of Set, explicitly" "explicit-subcats")
\myslide {Finite subcategories of $\Set$, explicitly} {explicit-subcats}
\msk
\par A subcategory of $\catC \subset \Set$ is one in which:
\par * $\catC_0 \subset \Set_0$,
\par * for any $A, B Ý \catC_0$ we have $\Hom_\catC(A,B) \subset \Hom_\Set(A,B)$,
\par * the operations $¢_\catC$ and $\id_\catC$ and ``inherited'' from $\Set$.
\msk
\par For example, let $\catC$ be:
%D diagram subcat
%D 2Dx 100 +60
%D 2D 100 A B
%D 2D
%D 2D +50 C
%D 2D
%D (( A .tex= \{2,3\}
%D B .tex= \{4,5,6\}
%D C .tex= \{7,8\}
%D A B -> sl^ .plabel= a \twomtos2435
%D A B -> sl_ .plabel= b \twomtos2534
%D B C -> sl^ .plabel= r \threemtos475768
%D B C -> sl_ .plabel= l \threemtos475767
%D A C -> .plabel= l \twomtos2737
%D ))
%D enddiagram
%D
$$\diag{subcat}$$
\par (The identity maps are not shown).
\msk
\par In this example $\catC_0 = \setof{ \{2,3\}, \{4,5,6\}, \{7,8\} }$,
\par $\Hom_\catC(\{2,3\}, \{4,5,6\}) = \{\twomtos2435, \twomtos2534\}$,
\par $\Hom_\catC(\{2,3\}, \{2,3\}) = \{\twomtos2233\}$,
\par etc.
% --------------------
% «wellpos-subsets-of-N2» (to ".wellpos-subsets-of-N2")
% (s "Well-positioned subsets of N2" "wellpos-subsets-of-N2")
\myslide {Well-positioned subsets of $\N^2$} {wellpos-subsets-of-N2}
\msk
\par By abuse of language, let's write
\par `$\N^2$' for $\N+i\N$ and
\par `$\Z^2$' for $\Z+i\Z$.
\msk
\par Example:
\par $\aa = 1+3i$
\par $\bb = 0+2i$
\par $\cc = 2+2i$
\par $\dd = 1+1i$
\par $\ee = 1+0i$
\msk
\par Let $K = \setof{\aa, \bb, \cc, \dd, \ee} \subset \N^2$
\par (mnemonic: $\und{K}$ite).
%D diagram kite-0
%D 2Dx 100 +20 +20 +40 +20 +20
%D 2D 100 \aa' \aa
%D 2D
%D 2D +20 \bb' \cc' \bb \cc
%D 2D
%D 2D +20 \dd' \dd
%D 2D
%D 2D +20 \ee' \ee
%D 2D
%D (( \aa' .tex= (1+3i)
%D \bb' .tex= (0+2i)
%D \cc' .tex= (2+2i)
%D \dd' .tex= (1+1i)
%D \ee' .tex= (1+0i)
%D ))
%D (( \aa' \bb' -> \aa' \cc' ->
%D \bb' \dd' -> \cc' \dd' ->
%D \dd' \ee' ->
%D ))
%D (( \aa \bb -> \aa \cc ->
%D \bb \dd -> \cc \dd ->
%D \dd \ee ->
%D ))
%D enddiagram
%D
$$\diag{kite-0}$$
\par We will say that a subset $D \subset \Z^2$ is {\sl well-positioned}
\par when $\inf(\Re(D)) = 0$ and $\inf(\Im(D))=0$.
\msk
\par
$\begin{array}{rcl}
\inf(\Re(K)) &=& \inf(\Re(\{\aa,\bb,\cc,\dd,\ee\})) \\
&=& \inf(\{1, 0, 2, 1, 1\}) \\
&=& 0 \\
\inf(\Im(K)) &=& \inf(\Im(\{\aa,\bb,\cc,\dd,\ee\})) \\
&=& \inf(\{3, 2, 2, 1, 0\}) \\
&=& 0
\end{array}
$
\msk
\par $K$ is well-positioned.
% --------------------
% «wellpos-subsets-of-N2-2» (to ".wellpos-subsets-of-N2-2")
% (s "Well-positioned subsets of N2 (2)" "wellpos-subsets-of-N2-2")
\myslide {Well-positioned subsets of $\N^2$ (2)} {wellpos-subsets-of-N2-2}
\msk
\par Def: an {\sl $\N^2$-set} is a finite, well-positioned subset of $\N^2$.
\par We will denote $\N^2$-sets (with few elements) by bullet diagrams:
\par $K = \dagKite*****$, \qquad $V = \dagVee***$.
\msk
\par Def: to list the elements of an $\N^2$-set {\sl in reading order}
\par is to list them from top to bottom, and from left to right.
\par Example: $K = \setof{\aa, \bb, \cc, \dd, \ee}$.
$$\diag{kite-0}$$
\par We are interested in regarding $\N^2$-sets
\par as (the vertices of) directed (acyclical) graphs.
\msk
\par Def: an arrow $z \to w$ between points of $\N^2$ is a {\sl black pawn's move}
\par when it moves at most one unit horizontally and exactly one unit down;
\par black pawn's moves are short arrows of shape $\swarrow$, $\downarrow$ or $\searrow$.
\msk
\par The set of black pawn's moves \und{on a subset} $D \subset \N^2$, $\BPM(D)$,
\par is defined in the obvious way:
$$\BPM(D) = \setofst{(z,w) Ý D^2}{z \to w \text{ is a black pawn's move}}.$$
\par Example:
\par $\BPM(K) = \{\aa\to\bb, \; \aa\to\cc, \; \bb\to\dd, \; \cc\to\dd, \; \dd\to\ee\}$.
% --------------------
% «BPMK-not-protocat» (to ".BPMK-not-protocat")
% (s "BPM(K) is not a protocategory" "BPMK-not-protocat")
\myslide {$\BPM(K)$ is not a protocategory} {BPMK-not-protocat}
\msk
\par ...because $\BPM(K)$ is just a set of arrows,
\par not a tuple of the form $\{K_0, \Hom, ¢, \id; \assoc, \idLR\}$...
\par What happens when we try to fix this?
\msk
\par Let's try:
\par * $K_0 = \{\aa,\bb,\cc,\dd,\ee\}$
\par * $\Hom_K(\aa,\bb) = \{(\aa,\bb)\}$, $\Hom_K(\aa,\dd) = \{\;\}$, ...
% --------------------
% «BPM*K-as-protocat» (to ".BPM*K-as-protocat")
% (s "BPM*(K) is a protocategory" "BPM*K-as-protocat")
\myslide {$\BPM^*(K)$ is a protocategory} {BPM*K-as-protocat}
% --------------------
% «BPM*K-as-cat» (to ".BPM*K-as-cat")
% (s "BPM*(K) is a category" "BPM*K-as-cat")
\myslide {BPM*(K) is a category} {BPM*K-as-cat}
% --------------------
% «cats-from-graphs» (to ".cats-from-graphs")
% (s "Two categories generated by graphs" "cats-from-graphs")
\myslide {Two categories generated by graphs} {cats-from-graphs}
% (find-books "__cats/__cats.el" "awodey")
% (find-awodeypage (+ 10 20) "The free category on a graph")
% (find-awodeytext (+ 10 20) "The free category on a graph")
% --------------------
% «commutative-diags» (to ".commutative-diags")
% (s "Commutative diagrams" "commutative-diags")
\myslide {Commutative diagrams} {commutative-diags}
% --------------------
% «coherence» (to ".coherence")
% (s "Coherence" "coherence")
\myslide {Coherence} {coherence}
\par In a linear diagram like
%D diagram coherence-linear
%D 2Dx 100 +30 +30 +30 +30
%D 2D 100 A --> B --> C --> D --> E
%D 2D
%D (( A B -> .plabel= a f_{AB}
%D B C -> .plabel= a f_{BC}
%D C D -> .plabel= a f_{CD}
%D D E -> .plabel= a f_{DE}
%D A loop (dl,ul)^{\id_A}
%D B loop (dl,dr)_{\id_B}
%D C loop (dl,dr)_{\id_C}
%D D loop (dl,dr)_{\id_D}
%D E loop (ur,dr)^{\id_E}
%D ))
%D enddiagram
%D
$$\diag{coherence-linear}$$
\par all ways to define an arrow that ``deserves the name $f_{AE}$''
\par give the same result.
\msk
\par [EXPLAIN WD]
\msk
\par In a planar diagram like the one below,
\par in which each cell commutes, i.e., $\welld[f_{AE}]$, $\welld[f_{BF}]$, $\welld[f_{DH}]$, $\welld[f_{EI}]$,
\par all ways to define an arrow that ``deserves the name $f_{AI}$''
\par give the same result.
%D diagram coherence-planar
%D 2Dx 100 +30 +30
%D 2D 100 A --> B --> C
%D 2D
%D 2D +30 D --> E --> F
%D 2D
%D 2D +30 G --> H --> I
%D 2D
%D (( A B -> .plabel= a f_{AB} B C -> .plabel= a f_{BC}
%D D E -> .plabel= a f_{DE} E F -> .plabel= a f_{EF}
%D G H -> .plabel= a f_{GH} H I -> .plabel= a f_{HI}
%D
%D A D -> .plabel= l f_{AD} D G -> .plabel= l f_{DG}
%D B E -> .plabel= l f_{BE} E H -> .plabel= a f_{EH}
%D C F -> .plabel= l f_{CF} F I -> .plabel= a f_{FI}
%D
%D
%D ))
%D enddiagram
%D
$$\diag{coherence-planar}$$
[EXERCISES]
% --------------------
% «terminal-in-Set» (to ".terminal-in-Set")
% (s "A terminal object in Set" "terminal-in-Set")
\myslide {A terminal object in $\Set$} {terminal-in-Set}
\msk
\par Standard definition:
\par A {\sl terminal object} in $\catC$ is an object $T Ý \catC$
\par such that for each object $AÝ\catC$ there is exactly one map
\par (called $t_A$) from $A$ to $T$.
\msk
\par Equivalent definition:
\par A {\sl terminal} in $\catC$ is a triple $(T, t; Ð{uniq})$ where:
\par * $T Ý \catC$,
\par * for each $AÝ\catC$ we have that $t(A)$ is a map from $A$ to $T$,
\par * $Ð{uniq}$ is a proof for $ýA.\,ýf_{AT}.\,f_{AT}=t(A)$.
\msk
\par Fact 1: $\{200\}$ is a terminal object in $\Set$.
\par EXERCISE: find the unique map from $\{2,3,4\}$ to $\{200\}$.
\par EXERCISE:
% (find-awodeyctpage (+ 10 28) "2.2 Initial and terminal objects")
% (find-awodeycttext (+ 10 28) "2.2 Initial and terminal objects")
T, t, uniq
$\setof{8}$ is a terminal in $\Set$.
% --------------------
% «prods-in-set» (to ".prods-in-set")
% (s "Products in Set" "prods-in-set")
\myslide {Products in Set} {prods-in-set}
%D diagram meta-prod
%D 2Dx 100 +40 +40
%D 2D 100 A
%D 2D
%D 2D +40 B P C
%D 2D
%D (( A .tex= \prodA
%D B .tex= \prodB
%D C .tex= \prodC
%D P .tex= \prodP
%D A B -> .plabel= l \prodf
%D A P -> .plabel= m \prodh
%D A C -> .plabel= r \prodg
%D P B -> .plabel= b \prodpl
%D P C -> .plabel= b \prodpr
%D ))
%D enddiagram
%D
$$\def\prodA{\{1,2\}}
\def\prodB{\{3,4\}}
\def\prodC{\{5,6\}}
\def\prodP{\{\sm{35,36\\45,46}\}}
\def\prodf{f}
\def\prodf{\twomtos1324}
\def\prodg{f}
\def\prodg{\twomtos1525}
\def\prodh{\ang{f,g}}
\def\prodh{\twomtos1{35}2{45}}
\def\prodpl{p_1}
\def\prodpl{\fourmtos{35}3{36}3{45}4{46}4}
\def\prodpr{p_2}
\def\prodpr{\fourmtos{35}5{36}6{45}5{46}6}
\diag{meta-prod}
$$
% --------------------
% «terminals-categorically» (to ".terminals-categorically")
% (s "Terminals, categorically" "terminals-categorically")
\myslide {Terminals, categorically} {terminals-categorically}
% --------------------
% «products-categorically» (to ".products-categorically")
% (s "Products, categorically" "products-categorically")
\myslide {Products, categorically} {products-categorically}
% --------------------
% «without-products» (to ".without-products")
% (s "A category without products" "without-products")
\myslide {A category without products} {without-products}
% --------------------
% «terminals-are-isomorphic» (to ".terminals-are-isomorphic")
% (s "Terminals are isomorphic" "terminals-are-isomorphic")
\myslide {Terminals are isomorphic} {terminals-are-isomorphic}
% --------------------
% «terminals-are-isomorphic» (to ".terminals-are-isomorphic")
% (s "Products are isomorphic" "terminals-are-isomorphic")
\myslide {Products are isomorphic} {terminals-are-isomorphic}
% --------------------
% «cat-without-1-and-prod» (to ".cat-without-1-and-prod")
% (s "A category without terminals and products" "cat-without-1-and-prod")
\myslide {A category without terminals and products} {cat-without-1-and-prod}
% --------------------
% «cats-with-1-and-prod» (to ".cats-with-1-and-prod")
% (s "Categories with terminals and products" "cats-with-1-and-prod")
\myslide {Categories with terminals and products} {cats-with-1-and-prod}
% --------------------
% «Ax-in-Set» (to ".Ax-in-Set")
% (s "A functor in Set: Ax" "Ax-in-Set")
\myslide {A functor in Set: Ax} {Ax-in-Set}
% --------------------
% «a-NT-in-Set» (to ".a-NT-in-Set")
% (s "A natural transformation in Set" "a-NT-in-Set")
\myslide {A natural transformation in Set} {a-NT-in-Set}
% --------------------
% «exponentials-in-Set» (to ".exponentials-in-Set")
% (s "Exponentials in Set" "exponentials-in-Set")
\myslide {Exponentials in Set} {exponentials-in-Set}
% --------------------
% «exponentials-categorically» (to ".exponentials-categorically")
% (s "Exponentials, categorically" "exponentials-categorically")
\myslide {Exponentials, categorically} {exponentials-categorically}
% --------------------
% «adjunctions» (to ".adjunctions")
% (s "Adjunctions" "adjunctions")
\myslide {Adjunctions} {adjunctions}
See [Awodey, pp.179ff]
% (find-books "__cats/__cats.el" "awodey")
% (find-awodeyctpage (+ 10 179) "9" "ADJOINTS")
% (find-awodeycttext (+ 10 179) "9" "ADJOINTS")
% --------------------
% «adjoints-are-isomorphic» (to ".adjoints-are-isomorphic")
% (s "Adjoints are isomorphic" "adjoints-are-isomorphic")
\myslide {Adjoints are isomorphic} {adjoints-are-isomorphic}
% --------------------
% «lambda-intro» (to ".lambda-intro")
% (s "lambda-calculus: introduction" "lambda-intro")
\myslide {lambda-calculus: introduction} {lambda-intro}
\msk
\par Many slides ago we defined a function that returned functions...
$
\def\ma{
\begin{array}{rcccl}
m_a &:& \{10,100\} & \to & \N \\
&& b & \mto & a·b \\
\end{array}
}
%
\begin{array}{rcccl}
m &:& \{2,3\} & \to & \N^{\{10,100\}} \\
&& a & \mto & \left(\ma\right) \\
\end{array}
$
\msk
\par Then $(m(2))(10) = m_2(10) = 2·10 = 20$.
\msk
\par The `$ð$' lets us create {\sl anonymous functions}.
\par Example 1: $m_2 = ðb¨\{10,100\}.(a·b)$
\par Example 2: $m = ða¨\{2,3\}.ðb¨\{10,100\}.(a·b)$
\par Example 3: $m = ða¨\{2,3\}.ðb¨\{10,100\}.(((·)a)b)$
\par Example 4: $m = ða.ðb.(·)a\,b$
\msk
\par Convention: $(m(2))(10) = m\,2\,10$
\par $f\,x\,y = (f\,x)\,y$
\msk
\par Syntax:
\par * (function) (argument)
\par * $ð$ (var) . (expression)
\par * $ð$ (var) : (type) . (expression)
\par * (expr) [(var) := (vexpr)] \qquad (special)
% --------------------
% «lambda-reductions» (to ".lambda-reductions")
% (s "lambda-calculus: reductions" "lambda-reductions")
\myslide {$ð$-calculus: reductions} {lambda-reductions}
\msk
\par Reductions:
\par * $\bb$-reduction: $((ðy.(-)y\,2)5) \squigto (-)5\,2$
\par \ph{* }(formally: $(ðx.a)b \squigto a[x:=b]$)
\par * $\aa$-conversion: change the name of a variable
\par * $\kk$-reduction (non-standard): $(-)5\, 2 \squigto 3$
\msk
%D diagram lambda-reductions
%D 2Dx 100 +30 +30 +70 +30
%D 2D 100 A
%D 2D
%D 2D +20 B
%D 2D
%D 2D +20 C D
%D 2D
%D 2D +20 E
%D 2D
%D 2D +20 F
%D 2D
%D 2D +20 G H
%D 2D
%D 2D +20 I J K
%D 2D
%D (( A .tex= (ðx.(+)x\,x)((ðy.(-)y\,2)5)
%D B .tex= (+)((ðy.(-)y\,2)5)((ðy.(-)y\,2)5)
%D C .tex= (+)((ðy.(-)y\,2)5)((ðz.(-)z\,2)5)
%D D .tex= (ðx.(+)x\,x)((-)5\,2)
%D E .tex= (+)((ðy.(-)y\,2)5)((-)5\,2)
%D F .tex= (+)((-)5\,2)((ðz.(-)z\,2)5)
%D G .tex= (+)((-)5\,2)((-)5\,2)
%D H .tex= (+)((-)5\,2)3
%D I .tex= (+)3((-)5\,2)
%D J .tex= (+)3\,3
%D K .tex= 6
%D ))
%D (( A B -> A D ->
%D B C -> .plabel= l \aa
%D C E -> C F ->
%D D G -> E G -> F G ->
%D G H -> .plabel= a \kk
%D G I -> .plabel= l \kk
%D H J -> .plabel= r \kk
%D I J -> .plabel= a \kk
%D J K -> .plabel= a \kk
%D ))
%D enddiagram
%D
$$\diag{lambda-reductions}$$
% (find-tesemestrpage (+ 7 20) "((-)5 2)")
% (find-tesemestrtext (+ 7 20) "((-)5 2)")
% (ee-page-parameters "tesemestr" 7)
% --------------------
% «lambda-calc-in-a-CCC» (to ".lambda-calc-in-a-CCC")
% (s "$ð$-calculus in a CCC" "lambda-calc-in-a-CCC")
\myslide {$ð$-calculus in a CCC} {lambda-calc-in-a-CCC}
% (find-unilogcurrpage 87 "Lambda-calculus in a hyperdoctrine")
% (find-unilogcurr "" "lambda-calc-in-a-hyp")
\par (Compare with:
[LambekScott, p.75],
% (find-books "__cats/__cats.el" "lambek-scott")
% (find-lambekscottpage (+ 8 75) "internal language L(A) of a cartesian closed category")
[Awodey, pp.119--122])
% (find-books "__cats/__cats.el" "awodey")
% (find-awodeyctpage (+ 10 119) "6.5 lambda-calculus")
% (find-awodeycttext "\n6.5" "-calculus")
%D diagram app-new
%D 2Dx 100 +60 +60 +40
%D 2D 100 A A'
%D 2D / | \
%D 2D / | \
%D 2D v v v
%D 2D +40 B <- BCB <- BC
%D 2D | |
%D 2D | |
%D 2D v v
%D 2D +40 C |-> BC' C'
%D 2D
%D (( BCB .tex= (B{->}C){×}B
%D BC .tex= B{->}C
%D BC' .tex= B{->}C
%D A B -> .plabel= l a|-b
%D # A BCB -> .plabel= m a|-(f,b)
%D A BCB -> .plabel= m \sm{(a|-(f,b))\;:=\\\ang{(a|-f),(a|-b)}}
%D A BC -> .plabel= r a|-f
%D # BCB B -> .plabel= a '_{B(B{->}C)}
%D BCB B -> .PLABEL= _(0.52) '_{B(B{->}C)}
%D BCB BC -> sl^ .plabel= a _{B(B{->}C)}
%D BCB BC <-| sl_ .plabel= b (×B)
%D BCB C -> .plabel= l \sm{\ev_{BC}\;:=\\(\id_{B{->C}})^\flat}
%D BC BC' -> .plabel= r \id_{B{->}C}
%D C BC' -> .plabel= b (B{->})
%D BCB BC' harrownodes nil 20 nil <-| .plabel= a \flat
%D A' .tex= A
%D C' .tex= C
%D A' C' --> .plabel= m \sm{(a|-fb)\;:=\\(a|-(f,b));\ev_{BC}}
%D ))
%D enddiagram
%D
$$\diag{app-new}$$
%D diagram CCC-HL1
%D 2Dx 100 +30 +30 +25 +30 +30
%D 2D 100 P0 T0 E0 E1
%D 2D
%D 2D +30 P1 P2 P3 T1 E2 E3
%D 2D
%D (( P0 .tex= A P1 .tex= B P2 .tex= B×C P3 .tex= C
%D P0 P1 -> .plabel= a f
%D P0 P2 -> .plabel= m \ang{f,g}
%D P0 P3 -> .plabel= a g
%D P1 P2 <- .plabel= b \pi
%D P2 P3 -> .plabel= b \pi'
%D ))
%D (( T0 .tex= A T1 .tex= 1 -> .plabel= l !
%D ))
%D (( E0 .tex= A×B E1 .tex= A
%D E2 .tex= C E3 .tex= B{->}C
%D E0 E1 <-|
%D E0 E2 -> .PLABEL= _(0.43) \uncur"g
%D E0 E2 -> .PLABEL= _(0.57) f
%D E1 E3 -> .PLABEL= ^(0.43) g
%D E1 E3 -> .PLABEL= ^(0.57) \cur"f
%D E0 E3 harrownodes nil 20 nil <-| sl^ .plabel= a \flat
%D E0 E3 harrownodes nil 20 nil |-> sl_ .plabel= b \sharp
%D E2 E3 |->
%D ))
%D enddiagram
%D
$$\diag{CCC-HL1}$$
%D diagram CCC-HL2
%D 2Dx 100 +30 +30 +25 +30 +30 +35
%D 2D 100 P0 T0 E0 E1 E0'
%D 2D
%D 2D +30 P1 P2 P3 T1 E2 E3 E2'
%D 2D
%D (( P0 .tex= A P1 .tex= B P2 .tex= B{×}C P3 .tex= C
%D P0 P1 -> .plabel= a a|-b
%D P0 P2 -> .plabel= m a|-(b,c)
%D P0 P3 -> .plabel= a a|-c
%D P1 P2 <- .plabel= b p|-b
%D P2 P3 -> .plabel= b p|-b'
%D ))
%D (( T0 .tex= A T1 .tex= 1 -> .plabel= l a|-*
%D ))
% %D (( E0' .tex= (B{->}C){×}B E2' .tex= C
% %D E0' E2' -> .plabel= c \ev_{BC}
% %D ))
%D (( E0 .tex= A×B E1 .tex= A
%D E2 .tex= C E3 .tex= B{->}C
%D E0 E1 <-|
%D E0 E2 -> .PLABEL= _(0.43) a,b|-fb
%D E0 E2 -> .PLABEL= _(0.57) a,b|-c
%D E1 E3 -> .PLABEL= ^(0.43) a|-f
%D E1 E3 -> .PLABEL= ^(0.57) a|-ðb¨B.c
%D E0 E3 harrownodes nil 20 nil <-| sl^
%D E0 E3 harrownodes nil 20 nil |-> sl_
%D E2 E3 |->
%D ))
%D enddiagram
%D
$$\diag{CCC-HL2}$$
%L print("1284 ok")
%L registerhead "%:" {
%L action = function ()
%L allsegments[nline] = tosegments(linestr, nline)
%L for _,seg in ipairs(allsegments[nline]) do
%L local name = seg.t:match("^%^(.*)")
%L if name then
%L local rootnode = seg:rootnode() or Error(seg.t.." points to nothing")
%L -- if not rootnode then
%L -- print("At line "..nline..": "..seg.t.." points to nothing")
%L -- error()
%L -- end
%L -- PP(name, rootnode)
%L output(rootnode:totreenode():TeX_deftree(name))
%L -- output(seg:rootnode():totreenode():TeX_deftree(name))
%L end
%L end
%L end,
%L }
In a sequent-calculus-like form:
%:
%: B C a|-b a|-c B C B C
%: ----×_0 ------------\ang{,} ---- -----'
%: B×C a|-\ang{b,c} p|-p p|-'p
%:
%: ^HL-x0 ^HL-ang ^HL-pi ^HL-pi'
%:
%: A
%: -1 ----!
%: 1 a|-*
%:
%: ^HL-1 ^HL-!
%:
%: B C B C a,b|-c
%: ----{->}_0 ----\ev ---------ð
%: B{->}C b,f|-fb a|-ðb¨B.c
%:
%: ^HL-->0 ^HL-ev ^HL-cur
%:
$$\begin{array}{cccc}
\ded{HL-x0} & \ded{HL-ang} & \ded{HL-pi} & \ded{HL-pi'} \\ \\
\ded{HL-1} & \ded{HL-!} \\ \\
\ded{HL-->0} & \ded{HL-ev} & \ded{HL-cur} \\
\end{array}
$$
%L print("1313 ok")
% (find-LATEXfile "proof.sty" "\\def\\DeduceSym")
\makeatletter
\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
\vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
\vbox{\hbox{.}\hbox{.}}\hbox{.}}}
\makeatother
In natural deduction form (in downcased notation):
%:
%: a a
%: : :
%: b c b,c b,c
%: ----\ang{,} --- ---'
%: b,c b c
%:
%: ^HLD-1 ^HLD-2 ^HLD-3
%:
%: a
%: -!
%: *
%:
%: ^HLD-4
%:
%: a a a [b]^1
%: : : ::::
%: b b|->c c
%: ---------\app -----ð;1
%: c b|->c
%:
%: ^HLD-5 ^HLD-6
%:
$$\begin{array}{cccc}
\ded{HLD-1} & \ded{HLD-2} & \ded{HLD-3} \\ \\
\ded{HLD-4} \\ \\
\ded{HLD-5} & \ded{HLD-6} \\
\end{array}
$$
% (find-unilogcurr "" "product-property")
% (find-unilogcurrpage 47)
% (find-unilogcurrtext 47)
%L print("1360 ok")
\end{document}
% «videos» (to ".videos")
% (find-minicatsvideo "aula_1/" "DSC_0143" "30-second test")
% (find-minicatsframe "aula_1/" "DSC_0143" "30-second test")
% (find-minicatsvideo "aula_1/" "DSC_0144" "5-second test")
% (find-minicatsframe "aula_1/" "DSC_0144" "5-second test")
% (find-minicatsvideo "aula_1/" "DSC_0145" "1:15" "Functions, explicitly")
% (find-minicatsvideo "aula_1/" "DSC_0145" "3:40" "Functions are sets")
% (find-minicatsvideo "aula_1/" "DSC_0145" "5:48" "Preambulo ao que sao cats (grupos)")
% (find-minicatsframe "aula_1/" "DSC_0145" "3:40")
% (find-minicatsvideo "aula_1/" "DSC_0146" "0:20" "apresentacao by Claus (40 secs)")
% (find-minicatsframe "aula_1/" "DSC_0146")
% (find-minicatsvideo "aula_1/" "DSC_0148" "4:34" "; e bola")
% (find-minicatsframe "aula_1/" "DSC_0148")
% (find-minicatsvideo "aula_1/" "DSC_0149")
% (find-minicatsframe "aula_1/" "DSC_0149")
% (find-minicatsvideo "aula_1/" "DSC_0150")
% (find-minicatsframe "aula_1/" "DSC_0150")
% (find-minicatsvideo "aula_1/" "DSC_0151")
% (find-minicatsframe "aula_1/" "DSC_0151")
% (find-minicatsvideo "aula_1/" "DSC_0155")
% (find-minicatsframe "aula_1/" "DSC_0155")
% (find-minicatsvideo "aula_1/" "DSC_0156")
% (find-minicatsframe "aula_1/" "DSC_0156")
% (find-minicatsvideo "aula_1/" "DSC_0158")
% (find-minicatsframe "aula_1/" "DSC_0158")
% (find-minicatsvideo "aula_2/" "DSC_0002")
% (find-minicatsframe "aula_2/" "DSC_0002")
% (find-minicatsvideo "aula_2/" "DSC_0003")
% (find-minicatsframe "aula_2/" "DSC_0003")
% (find-minicatsvideo "aula_2/" "DSC_0004")
% (find-minicatsframe "aula_2/" "DSC_0004")
% (find-minicatsvideo "aula_2/" "DSC_0005")
% (find-minicatsframe "aula_2/" "DSC_0005")
% (find-minicatsvideo "aula_2/" "DSC_0006")
% (find-minicatsframe "aula_2/" "DSC_0006")
% (find-minicatsvideo "aula_2/" "DSC_0007")
% (find-minicatsframe "aula_2/" "DSC_0007")
% (find-minicatsvideo "aula_2/" "DSC_0008")
% (find-minicatsframe "aula_2/" "DSC_0008")
% (find-minicatsvideo "aula_2/" "DSC_0009")
% (find-minicatsframe "aula_2/" "DSC_0009")
% (find-minicatsvideo "aula_2/" "DSC_0010")
% (find-minicatsframe "aula_2/" "DSC_0010")
% (find-minicatsvideo "aula_3/" "DSC_0001")
% (find-minicatsframe "aula_3/" "DSC_0001")
% (find-minicatsvideo "aula_3/" "DSC_0002")
% (find-minicatsframe "aula_3/" "DSC_0002")
% (find-minicatsvideo "aula_3/" "DSC_0003")
% (find-minicatsframe "aula_3/" "DSC_0003")
% (find-minicatsvideo "aula_3/" "DSC_0004")
% (find-minicatsframe "aula_3/" "DSC_0004")
% (find-minicatsvideo "aula_3/" "DSC_0005")
% (find-minicatsframe "aula_3/" "DSC_0005")
% (find-minicatsvideo "aula_3/" "DSC_0006")
% (find-minicatsframe "aula_3/" "DSC_0006")
% (find-minicatsvideo "aula_3/" "DSC_0007")
% (find-minicatsframe "aula_3/" "DSC_0007")
% (find-minicatsvideo "aula_4/" "DSC_0001")
% (find-minicatsframe "aula_4/" "DSC_0001")
% (find-minicatsvideo "aula_4/" "DSC_0002")
% (find-minicatsframe "aula_4/" "DSC_0002")
% (find-minicatsvideo "aula_4/" "DSC_0004")
% (find-minicatsframe "aula_4/" "DSC_0004")
% (find-minicatsvideo "aula_4/" "DSC_0005")
% (find-minicatsframe "aula_4/" "DSC_0005")
% (find-minicatsvideo "aula_4/" "DSC_0006")
% (find-minicatsframe "aula_4/" "DSC_0006")
% (find-minicatsvideo "aula_4/" "DSC_0007")
% (find-minicatsframe "aula_4/" "DSC_0007")
% (find-minicatsvideo "aula_4/" "DSC_0008")
% (find-minicatsframe "aula_4/" "DSC_0008")
% (find-minicatsvideo "aula_5/" "DSC_0003")
% (find-minicatsframe "aula_5/" "DSC_0003")
% (find-minicatsvideo "aula_5/" "DSC_0004")
% (find-minicatsframe "aula_5/" "DSC_0004")
% (find-minicatsvideo "aula_5/" "DSC_0006")
% (find-minicatsframe "aula_5/" "DSC_0006")
% (find-minicatsvideo "aula_5/" "DSC_0007")
% (find-minicatsframe "aula_5/" "DSC_0007")
% (find-minicatsvideo "aula_5/" "DSC_0010")
% (find-minicatsframe "aula_5/" "DSC_0010")
% (find-minicatsvideo "aula_5/" "DSC_0011")
% (find-minicatsframe "aula_5/" "DSC_0011")
% (find-minicatsvideo "aula_5/" "DSC_0012")
% (find-minicatsframe "aula_5/" "DSC_0012")
Coherence, linearly
Coherence, planarly
;; (find-efunction 's)
(load "eev-template.el")
lambda
% (s "Internal diagrams" "internal
(a|->b|->b) = (a|->b)
% (s "Categories and protocategories" "cats-sp")
% (find-sh "lua51 ~/LUA/toctag.lua < tmp.los")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
Scp -v ~/LATEX/2012minicats.pdf edrx@angg.twu.net:slow_html/MINICATS/
Scp -v ~/LATEX/2012minicats.dvi edrx@angg.twu.net:slow_html/MINICATS/
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: