|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2021excuse.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record --synctex=1 2021excuse.tex" :end))
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2021excuse.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2021excuse.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2021excuse.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2021excuse.pdf"))
% (defun e () (interactive) (find-LATEX "2021excuse.tex"))
% (defun l () (interactive) (find-LATEX "2021excuse.lua"))
% (defun h () (interactive) (find-angg "HASKELL/2021excuse.hs"))
% (defun u () (interactive) (find-latex-upload-links "2021excuse"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (find-pdf-page "~/LATEX/2021excuse.pdf")
% (find-xournalpp "~/LATEX/2021excuse.pdf")
% (find-sh0 "cp -v ~/LATEX/2021excuse.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2021excuse.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2021excuse.pdf
% file:///tmp/2021excuse.pdf
% file:///tmp/pen/2021excuse.pdf
% http://angg.twu.net/LATEX/2021excuse.pdf
% (find-LATEX "2019.mk")
%
% (find-lualatex-links "2021excuse")
% https://mail.google.com/mail/ca/u/0/#search/categorias+type+theory/KtbxLwGnRQxDGgTltXvbZjZCHvkdspPvlB
% «.defs» (to "defs")
% «.co» (to "co")
% «.verbatim» (to "verbatim")
% «.title-page» (to "title-page")
% «.rings» (to "rings")
% «.rings-2» (to "rings-2")
% «.conventions-CT-1» (to "conventions-CT-1")
% «.downcasing» (to "downcasing")
% «.downcasing-2» (to "downcasing-2")
% «.term-inf-proof-search» (to "term-inf-proof-search")
% «.haskell» (to "haskell")
%
% «.universals-CWM-orig» (to "universals-CWM-orig")
% «.universals-defs» (to "universals-defs")
% «.universals-CWM» (to "universals-CWM")
% «.universals-my-letters» (to "universals-my-letters")
% «.universals-rings» (to "universals-rings")
%
% «.internal-views» (to "internal-views")
% «.functors» (to "functors")
% «.functor-2» (to "functor-2")
% «.functor-3» (to "functor-3")
% «.functor-4» (to "functor-4")
% «.NTs» (to "NTs")
% «.NTs-2» (to "NTs-2")
% «.NTs-3» (to "NTs-3")
% «.yoneda» (to "yoneda")
% «.kan» (to "kan")
%
% «.intro-TT» (to "intro-TT")
% «.untyped-lambda» (to "untyped-lambda")
% «.types-after-discrete» (to "types-after-discrete")
% «.dependent-types» (to "dependent-types")
% «.typing-and-and-implies» (to "typing-and-and-implies")
% «.typing-forall-and-exists» (to "typing-forall-and-exists")
%
% «.marsden» (to "marsden")
%
% «.type-inference» (to "type-inference")
% «.typing» (to "typing")
% «.intro-to-the-hard-part» (to "intro-to-the-hard-part")
% «.some-references» (to "some-references")
% «.contexts» (to "contexts")
% «.PTSs» (to "PTSs")
% «.PTSs-2» (to "PTSs-2")
% «.judgments» (to "judgments")
%
% «.guessing-nu-CWM-1» (to "guessing-nu-CWM-1")
% «.guessing-nu-1» (to "guessing-nu-1")
% «.guessing-nu-2» (to "guessing-nu-2")
% «.guessing-nu-2-diag» (to "guessing-nu-2-diag")
\documentclass[oneside]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{stmaryrd}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15} % (find-LATEX "edrx15.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex" "defub")
%
\usepackage[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-slides.bib} % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\usepackage[paperwidth=11.5cm, paperheight=9cm,
%total={6.5in,4in},
%textwidth=4in, paperwidth=4.5in,
%textheight=5in, paperheight=4.5in,
%a4paper,
top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
]{geometry}
%
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% %L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
% \pu
% «defs» (to ".defs")
% (find-LATEX "edrx15.sty" "colors-2019")
\long\def\ColorRed #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray #1{{\color{GrayLight}#1}}
\long\def\ColorGray #1{{\color{black!30!white}#1}}
\long\def\ColorOrange#1{{\color{orange}#1}}
\long\def\ColorBrown #1{{\color{brown}#1}}
\catcode`«=13 \def«{\llangle}
\catcode`»=13 \def»{\rrangle}
\def\univ{\text{(univ)}}
\def\nameof#1{\ulcorner#1\urcorner}
\def\Rings{\mathbf{Rings}}
\def\V{\mathbf{T}}
\def\F{\mathbf{F}}
\def\smile{\ensuremath{{=})}}
\def\frown{\ensuremath{{=}(}}
\def\smirk{\ensuremath{{=}/}}
\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\def\ug#1{\und{#1}{gen}}
\def\uf#1{\und{#1}{filt}}
\def\ue#1{\und{#1}{expr}}
\def\uC#1{\und{#1}{context}}
\def\uCH#1{\und{#1}{context / hypotheses}}
\def\uvt#1{\und{#1}{v:T}}
\def\uterm#1{\und{#1}{term}}
\def\utype#1{\und{#1}{type}}
\def\uconc#1{\und{#1}{conclusion}}
\def\setofst#1#2{\{\,#1\;|\;#2\,\}}
\def\setofsc#1#2{\{\,#1\;;\;#2\,\}}
% pos-spec colors
% (find-es "tex" "xcolor")
% (find-xcolorpage 17 "2.4 Predefined colors")
% (find-xcolortext 17 "2.4 Predefined colors")
\def\Cnum#1{{\color{magenta}#1}}
\def\Cnum#1{{\color{Red1}#1}}
\def\Cnum#1{{\color{violet}#1}}
\def\Cnum#1{{\color{orange}#1}}
\def\Cstr#1{{\color{violet}#1}}
\def\Cstr#1{{\color{Red1}#1}}
\def\Csex#1{{\color{Red1}#1}}
\def\pdiag#1{\left(\diag{#1}\right)}
% «co» (to ".co")
% (find-es "tex" "co")
% \co: a low-level way to typeset code; a poor man's "\verb"
\def\cocolor{}
\def\cocolor{\color{DarkGreen!80!black}}
\def\co#1{{%
\cocolor%
\def\%{\char37}%
\def\\{\char92}%
\def\^{\char94}%
\def\~{\char126}%
\tt#1%
}}
\def\qco#1{`\co{#1}'}
\def\qqco#1{``\co{#1}''}
\def\pco#1{\par\co{#1}}
% «verbatim» (to ".verbatim")
% (find-angg "LUA/Verbatim1.lua" "Verbatim")
%\directlua{dofile "2021excuse.lua"} % (find-LATEX "2021excuse.lua")
\def\myhbox#1#2#3{\setbox0=\hbox{#3}\ht0=#1\dp0=#2\box0}
\def\verbahbox#1{\hbox{\tt#1}}
\def\verbahbox#1{\myhbox{7pt}{2pt}{{\tt#1}}}
% (find-dednat6 "tug-slides.tex" "bgcolorhbox")
\def\bgcolorhbox#1#2{{%
\setbox0\hbox{#2}%
\setbox0\vbox{\vskip\fboxsep\box0\vskip\fboxsep}%
\setbox0\hbox{\kern\fboxsep\box0\kern\fboxsep}%
{\color{#1}{\smashedvrule{\wd0}{\ht0}{\dp0}}}%
\box0%
}}
\def\bgbox#1{\bgcolorhbox{YellowOrangeLight}{#1}}
\def\myvcenter#1{\begin{matrix}#1\end{matrix}}
\catcode`\^^O=13 \def*{{\color{red}*}}
% From:
% (find-LATEX "2018-1-LA-material.tex" "defs")
\def\tabl#1{\begin{tabular}{l}#1\end{tabular}}
\def\tablt#1{\begin{tabular}[t]{l}#1\end{tabular}}
\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\textstyle #2}}
\def\subf#1{\underbrace{#1}_{}}
\def\p{\phantom{(}}
\def\cur{\operatorname{cur}}
\def\uncur{\operatorname{uncur}}
\def\ren{\operatorname{ren}}
\def\app{\operatorname{app}}
\def\pair{\operatorname{pair}}
\def\cur{\mathsf{cur}}
\def\uncur{\mathsf{uncur}}
\def\ren{\mathsf{ren}}
\def\app{\mathsf{app}}
\def\pair{\mathsf{pair}}
\def\Ran{\mathsf{Ran}}
\def\Dn {\Downarrow}
% \def∧{\&}
\def\namedfunction#1#2#3#4#5{
\begin{array}{rrcl}
#1: & #2 & → & #3 \\
& #4 & ↦ & #5 \\
\end{array}
}
\def\IPLai{\text{IPL}_{{∧}{→}}}
\def\NDai {\text{ND} _{{∧}{→}}}
%\noedrxfooter % (find-LATEX "edrxheadfoot.tex")
\def\drafturl{http://angg.twu.net/LATEX/2020-1-C2.pdf}
\def\drafturl{http://angg.twu.net/math-b.html\#2021-excuse-tt}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}
\setlength{\parindent}{0em}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title-page» (to ".title-page")
% (excp 1 "title-page")
% (exca "title-page")
% (ecop 1 "title-page")
% (eco "title-page")
\thispagestyle{empty} % (find-es "tex" "thispagestyle")
\begin{center}
\begin{tabular}{c}
\phantom{a}\\[-15pt]
{\Large {\bf Category Theory}} \\[1pt]
{\Large {\bf as An Excuse to}} \\[1pt]
{\Large {\bf Learn Type Theory}} \\[0pt]
\ColorGray{(talk @ Encontro de Categorias 2021)}\\[-5pt]
{\tiny\url{http://angg.twu.net/math-b.html#2021-excuse-tt}}\\[8pt]
\end{tabular}
\begin{tabular}[c]{r}
By: \\
Eduardo Ochs $→$ \\
\ColorGray{(main author)} \\
\\
Selana Ochs $→$ \\
\ColorGray{(friend and coauthor)} \\
\\
\\
\end{tabular}
\!\!\!\!\!\!\!
\begin{tabular}[c]{c}
$\includegraphics[height=100pt]{2021excuse-selana1.jpg}$
\end{tabular}
\phantom{mm}
% \msk
% \url{http://angg.twu.net/\#eev}
\end{center}
\newpage
% «rings» (to ".rings")
% (excp 2 "rings")
% (exca "rings")
{\bf Rings}
\ssk
A ring $R$ is a tuple $(R,0,1,+,-,·)$ in which:
\ssk
$\begin{array}{ccl}
R & \text{is} & \text{a set}, \\
0 & \in & R, \\
1 & \in & R, \\
+ & : & R×R→R, \\
- & : & R→R, \\
· & : & R×R→R \\
\end{array}
$
\ssk
and this $(R,0,1,+,-,·)$ obeys several conditions.
The part $(R,0,1,+,-,·)$ is called \ColorRed{structure},
and the conditions are called \ColorRed{properties}.
\msk
(For more on structure and properties
see\cite[section 7.5]{FavC}, \cite[p.15]{BaezShulman2007}).
% (favp 39 "ness")
% (fav "ness")
\newpage
% «rings-2» (to ".rings-2")
% (excp 3 "rings-2")
% (exca "rings-2")
{\bf Rings (2)}
\ssk
The symbols $0,1,+,-,·$ in $(R,0,1,+,-,·)$ have
standard conventions that let us infer their
arities, types, and equations --- what they have
to obey to ``deserve their names''.
\msk
Also, if $f:R→S$ is a morphism of rings then
$f$ is a function from the underlying set of $R$
to the underlying set of $S$ that obeys several
equations --- for example $f(a+b)=f(a)+f(b)$,
that is actually
%
$$∀a,b∈R.\,f(a +_R b) = f(a) +_S f(b) \; ...$$
These things can be written in several levels of detail.
\newpage
% «conventions-CT-1» (to ".conventions-CT-1")
% (excp 4 "conventions-CT-1")
% (exca "conventions-CT-1")
{\bf Conventions in Category Theory}
\ssk
Category Theory is like that too, only much, much worse.
The notation changes a lot from one text to the other.
Most diagrams are left to the reader.
Some parts of the \ColorRed{structure} are left to the reader too...
For example (see \cite[section 3]{FavC}):
\msk
Fix a set $A$. Let $(A×)$ be \ColorRed{the} functor that takes
each object $B$ to $A×B$.
\msk
This says that the \ColorRed{action on objects} of the functor $(A×)$
is $(A×)_0(B) = A×B$, and the ``\ColorRed{the}'' implies that the
reader knows how to discover that the action on morphisms is:
%
$$(A×)_1(B \ton{f} C) = A×B \xton{〈π,f∘π'〉} A×C.$$
% (favp 11 "to-deserve-a-name")
% (fav "to-deserve-a-name")
\newpage
% «downcasing» (to ".downcasing")
% (excp 5 "downcasing")
% (exca "downcasing")
{\bf A weird idea: downcasing}
\ssk
This looked very natural to me when I was starting to learn
CT and Haskell by myself... it is great as an \ColorRed{informal} tool.
\ssk
Btw, the paper \cite{IDARCT} is about how I tried to formalize
this idea for years, failed miserably, and then found a way
to use it for ``skeletons of proofs''.
%
%D diagram ??
%D 2Dx 100 +20 +30 +25
%D 2D 100 A0 B0 B1 C0
%D 2D
%D 2D +25 A1 B2 B3 C1
%D 2D
%D 2D +20 D0 D1
%D 2D
%D ren A0 B0 B1 C0 ==> b B A{×}B (a,b)
%D ren A1 B2 B3 C1 ==> c C A{×}C (a,c)
%D ren D0 D1 ==> \Set \Set
%D
%D (( A0 A1 |->
%D B0 B1 |->
%D B0 B2 -> .plabel= l f
%D B1 B3 -> .plabel= r A{×}f
%D B0 B3 harrownodes nil 20 nil |->
%D B2 B3 |->
%D C0 C1 |->
%D D0 D1 -> .plabel= a (A{×})
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
\qquad
\scalebox{0.9}{$
\begin{array}{l}
(a,b) \mapsto (a,c) \\
≡ (a,b) \mapsto (a,f(b)) \\
≡ (a,b) \mapsto (π(a,b),f(π'(a,b))) \\
≡ p \mapsto (πp, f(π'p)) \\
≡ p \mapsto (π(p), (f∘π')(p)) \\
≡ p \mapsto 〈π,f∘π'〉(p) \\
≡ 〈π,f∘π'〉 \\
\end{array}
$}
$$
\newpage
% «downcasing-2» (to ".downcasing-2")
% (excp 6 "downcasing-2")
% (exca "downcasing-2")
{\bf A weird idea: downcasing (2)}
\ssk
Downcasing and upcasing are like
lowercasing and uppercasing, but for terms and types.
\ssk
Downcasing a set gives us a name for \ColorRed{a}
``typical element'' of that set.
Downcasing a type gives us a name for a variable of that type.
\def\CO#1{\ColorOrange{\text{#1}}}
\msk
$\begin{array}{rcll}
a &:& A & \CO{(ok)} \\
a' &:& A' & \CO{(ok)} \\
a' &:& A & \CO{(ok when there's no $A'$)} \\
b &:& B & \CO{(ok)} \\
(a,b) &:& A×B & \CO{(ok?)} \\
b \mapsto c &:& B→C & \CO{(weird)} \\
(a,b) \mapsto (a,c) &:& A×B→A×C & \CO{(weird)} \\
\end{array}
$
\newpage
% «term-inf-proof-search» (to ".term-inf-proof-search")
% (excp 7 "term-inf-proof-search")
% (exca "term-inf-proof-search")
{\bf Term inference is like proof search}
\ssk
Finding \ColorRed{the} meaning of $A×f$
means finding \ColorRed{a} natural construction
for $\ColorRed{?}:A×B→A×C$ from $f:B→C$...
\ssk
``Natural constructions'' are $λ$-terms.
This is a bit quirky. Details: \cite[section 3]{FavC}.
Main diagrams:
\msk
%L addabbrevs("|->", "\\mapsto ")
%:
%: [(a,b)]^1 p
%: --------- ---
%: [(a,b)]^1 b b|->c [p]^1 π'p f
%: --------- ------------- ----- -----------
%: a c πp f(π'p)
%: ------------------- -------------------
%: b|->c (a,c) (πp,f(π'p))
%: ============= -------------1 --------------1
%: (a,b)|->(a,c) (a,b)|->(a,c) λp.(πp,f(π'p))
%:
%: ^nc-1 ^nc-2 ^nc-3
%:
%:
\pu
$\scalebox{0.9}{$
\ded{nc-1} \squigto \ded{nc-2} \squigto \;\;\; \ded{nc-3}
$}
$
% (favp 11 "to-deserve-a-name")
% (fav "to-deserve-a-name")
\newpage
%:
%:
%: [P∧Q]^1
%: ------
%: [P∧Q]^1 Q Q→R
%: ------- -----------
%: P R
%: -------------
%: Q→R P∧R
%: ======== -------------1
%: P∧Q→P∧R P∧Q→P∧R
%:
%: ^nc-log-1 ^nc-log-2
%:
%: [p:A{×}B]^1
%: ------------
%: [p:A{×}B]^1 π'p:B f:B→C
%: ------------ ---------------
%: πp:A f(π'p):C
%: ----------------------------
%: f:B→C (πp,f(π'p)):A{×}C
%: ==================== => -----------------------------------1
%: (×A)_1f:A{×}C→A{×}C (λp⠆A{×}B.(πp,f(π'p)):A{×}B→A{×}C
%:
%: ^nc-4 ^nc-5
%:
\pu
$\scalebox{0.8}{$
\ded{nc-log-1} \;\;\; \squigto \ded{nc-log-2}
$}
$
\msk
$\scalebox{0.8}{$
\ded{nc-4} \;\;\; \squigto \;\;\; \ded{nc-5}
$}
$
\newpage
% «haskell» (to ".haskell")
% (excp 9 "haskell")
% (exca "haskell")
%: [p:A{×}B]^1
%: ------------
%: [p:A{×}B]^1 π'p:B f:B→C
%: ------------ ---------------
%: πp:A f(π'p):C
%: ----------------------------
%: (πp,f(π'p)):A{×}C
%: -----------------------------------1
%: (λp⠆A{×}B.(πp,f(π'p)):A{×}B→A{×}C
%:
%: ^nc-5
%:
%: [\co{ab}:A{×}B]^1
%: -----------------
%: [\co{ab}:A{×}B]^1 \co{b}:B \co{btoc}:B→C
%: ----------------- -----------------------------
%: \co{a}:A \co{c}:C
%: --------------------------------
%: \co{ac}:A{×}C
%: -----------------------------------1
%: \co{abtoac}:A{×}B→A{×}C
%:
%: ^nc-6
%V -- Translation to Haskell:
%V -- (with help from ski @ #haskell)
%V atimes :: (b -> c) -> ((a,b) -> (a,c))
%V atimes btoc = abtoac where
%V abtoac ab = ac where
%V a = fst ab
%V b = snd ab
%V c = btoc b
%V ac = (a,c)
%L
%L verbdef "atimesHaskell"
\pu
$\hspace{-0.4cm}
\scalebox{0.72}{$
\begin{array}{c}
\ded{nc-5} \\
\\
\cded{nc-6}
\qquad
\begin{tabular}{l}
\co{a = fst ab} \\
\co{b = snd ab} \\
\co{c = btoc b} \\
\co{ac = (a,c)} \\
\co{abtoac = \\ ab -> ac} \\
\co{atimes = \\ btoc -> abtoac} \\
\end{tabular}
\\
\\
\atimesHaskell
\end{array}
$}
$
\pu
% $\vcenter{\resizebox{!}{120pt}{\foo}}
% $
\newpage
% _ _ _ _
% | | | |_ __ (_)_ _____ _ __ ___ __ _| |___
% | | | | '_ \| \ \ / / _ \ '__/ __|/ _` | / __|
% | |_| | | | | |\ V / __/ | \__ \ (_| | \__ \
% \___/|_| |_|_| \_/ \___|_| |___/\__,_|_|___/
%
% «universals-CWM-orig» (to ".universals-CWM-orig")
% (excp 10 "universals-CWM-orig")
% (exca "universals-CWM-orig")
Here's how \cite[section III.1]{CWM2} defines universals:
% (find-cwm2page (+ 13 55) "III. Universals and Limits")
% (find-cwm2text (+ 13 55) "III. Universals and Limits")
% (find-cwm2page (+ 13 55) "1. Universal Arrows")
\begin{quote}
{\bf Definition.} If $S: D→C$ is a functor and $c$ an object of $C$, a
universal arrow from $c$ to $S$ is a pair $〈r, u〉$ consisting of an
object $r$ of $D$ and an arrow $u: c→Sr$ of $C$, such that to every
pair $〈d,f〉$ with $d$ an object of $D$ and $f: c→Sd$ an arrow of $C$,
there is a unique arrow $f': r→d$ of $D$ with $S f'∘u = f$.
\end{quote}
This is too hard for my tiny brain.
\ColorRed{Solution:} I need types, diagrams,
a way to use other letters and fonts,
and examples.
% _ _ _ _ __
% | | | |_ __ (_)_ _____ _ __| | ___ / _|___
% | | | | '_ \| \ \ / / __(_) / _` |/ _ \ |_/ __|
% | |_| | | | | |\ V /\__ \_ | (_| | __/ _\__ \
% \___/|_| |_|_| \_/ |___(_) \__,_|\___|_| |___/
%
% «universals-defs» (to ".universals-defs")
% (excp 11 "universals-defs")
% (exca "universals-defs")
\def\OK#1{\ColorGreen{(ok#1)}}
\def\OK#1{\ColorOrange{(ok#1)}}
%D diagram universal-CWM
%D 2Dx 100 +25
%D 2D 100 C1
%D 2D |
%D 2D +25 C2 C3
%D 2D | |
%D 2D +25 C4 C5
%D 2D
%D 2D +15 C6 C7
%D 2D
%D ren C1 C2 C3 C4 C5 C6 C7 ==> c r Sr ∀d Sd D C
%D
%D (( C1 C3 -> .plabel= r \sm{u\\\univ}
%D C2 C3 |->
%D C2 C4 -> .plabel= l ∃!f'
%D C3 C5 -> .plabel= r Sf'
%D C2 C5 harrownodes nil 20 nil |->
%D C4 C5 |->
%D C1 C5 -> .slide= 28pt .plabel= r ∀f
%D C6 C7 -> .plabel= a R
%D ))
%D enddiagram
%D
%D diagram universal-my-letters
%D 2Dx 100 +25
%D 2D 100 C1
%D 2D |
%D 2D +25 C2 C3
%D 2D | |
%D 2D +25 C4 C5
%D 2D
%D 2D +15 C6 C7
%D 2D
%D ren C1 C2 C3 C4 C5 C6 C7 ==> A B RB ∀C RC \catB \catA
%D
%D (( C1 C3 -> .plabel= r \sm{η\\\univ}
%D C2 C3 |->
%D C2 C4 -> .plabel= l ∃!f
%D C3 C5 -> .plabel= r Rf
%D C2 C5 harrownodes nil 20 nil |->
%D C4 C5 |->
%D C1 C5 -> .slide= 28pt .plabel= r ∀g
%D C6 C7 -> .plabel= a R
%D ))
%D enddiagram
%D
%D diagram universal-ring
%D 2Dx 100 +30
%D 2D 100 C1
%D 2D |
%D 2D +25 C2 C3
%D 2D | |
%D 2D +25 C4 C5
%D 2D
%D 2D +15 C6 C7
%D 2D
%D ren C1 C2 C3 C4 C5 C6 C7 ==> 1 \Z[x] U\Z[x] ∀R UR \mathbf{Rings} \Set
%D
%D (( C1 C3 -> .plabel= r \sm{\nameof{x}\\\univ}
%D C2 C3 |->
%D C2 C4 -> .plabel= l ∃!f
%D C3 C5 -> .plabel= r Rf
%D C2 C5 harrownodes nil 20 nil |->
%D C4 C5 |->
%D C1 C5 -> .slide= 28pt .plabel= r ∀\nameof{a}
%D C6 C7 -> .plabel= a U
%D ))
%D enddiagram
%D
\pu
\def\universaltextCWM{
\begin{tabular}{rl}
If & $C,D$ are categories, \\
& $S:D→C$ is a functor, \\
& $c∈C$ is an object, \\
& $r∈D$ is an object, \\
& $u:C→Sr$ is a morphism, \\
then & $〈r,u〉$ is universal from $c$ to $S$ \\
iff & $∀d∈D$, \\
& $∀f:C→Sd$, \\
& $∃!f:r→d$ with $Sf'∘u=f$ \\
\end{tabular}
}
\def\universaltextmyletters{
\begin{tabular}{rl}
If & $\catA,\catB$ are categories, \\
& $R:\catA→\catB$ is a functor, \\
& $A∈\catA$ is an object, \\
& $B∈\catB$ is an object, \\
& $η:A→RB$ is a morphism, \\
then & $(B,η)$ is universal from $A$ to $R$ \\
iff & $∀C∈\catB$, \\
& $∀g:A→RC$, \\
& $∃!f:B→C$ with $Rf∘η=g$ \\
\end{tabular}
}
\def\universaltextRings{
\begin{tabular}{rll}
If & $\Set,\Rings$ are categories, & \OK{} \\
& $U:\Rings→\Set$ is a functor, & \OK{: $U =$ underlying set} \\
& $1∈\Set$ is an object, & \OK{: $1=\{*\}$} \\
& $\Z[x]∈\Rings$ is an object, & \OK{} \\
& $\nameof{x}:1→U\Z[x]$ is a morphism, & \OK{: $\nameof{x}(*)=x$} \\
then & $(\Z[x],\nameof{x})$ is universal from $A$ to $R$ \\
iff & $∀R∈\Rings$, \\
& $∀\nameof{a}:1→UR$, \\
& $∃!f:\Z[x]→R$ with $Uf∘\nameof{x}=\nameof{a}$ & \OK{: $f(P(x)) = P(a)$} \\
\end{tabular}
}
\newpage
% «universals-CWM» (to ".universals-CWM")
$\scalebox{0.9}{$
\myvcenter{\universaltextCWM}
\qquad
\diag{universal-CWM}
$}
$
\newpage
% «universals-my-letters» (to ".universals-my-letters")
$\scalebox{0.9}{$
\begin{array}{c}
\myvcenter{\universaltextmyletters}
\qquad
\diag{universal-my-letters}
\\
\\
\\
\ColorOrange{
\qquad
\qquad
\begin{tabular}{c}
$↑$ Looks like \\
Type Theory
\end{tabular}
\qquad
\qquad
\qquad
\begin{tabular}{c}
$↑$ Looks like \\
Freyd's notation
\end{tabular}
}
\end{array}
$}
$
\newpage
% «universals-rings» (to ".universals-rings")
$\scalebox{0.75}{$
\begin{array}{c}
\diag{universal-ring}
\\ \\
\myvcenter{\universaltextRings}
\end{array}
$}
$
\newpage
% ___ _ _ _
% |_ _|_ __ | |_ ___ _ __ _ __ __ _| | __ _(_) _____ _____
% | || '_ \| __/ _ \ '__| '_ \ / _` | | \ \ / / |/ _ \ \ /\ / / __|
% | || | | | || __/ | | | | | (_| | | \ V /| | __/\ V V /\__ \
% |___|_| |_|\__\___|_| |_| |_|\__,_|_| \_/ |_|\___| \_/\_/ |___/
%
% «internal-views» (to ".internal-views")
% (excp 13 "internal-views")
% (exca "internal-views")
{\bf Internal views}
% (favp 19 "internal-views")
% (fav "internal-views")
\ssk
The internal view of a \ColorRed{function}:
\def\ooo(#1,#2){\begin{picture}(0,0)\put(0,0){\oval(#1,#2)}\end{picture}}
\def\oooo(#1,#2){{\setlength{\unitlength}{1ex}\ooo(#1,#2)}}
%
%D diagram second-blob-function
%D 2Dx 100 +20 +20
%D 2D 100 a-1 |--> b-1
%D 2D +08 a0 |--> b0
%D 2D +08 a1 |--> b1
%D 2D +08 a2 |--> b2
%D 2D +08 a3 |--> b3
%D 2D +08 a4 |--> b4
%D 2D +14 a5 |--> b5
%D 2D +25 \N ---> \R
%D 2D
%D ren a-1 a0 a1 a2 a3 a4 a5 ==> -1 0 1 2 3 4 n
%D ren b-1 b0 b1 b2 b3 b4 b5 ==> -1 0 1 \sqrt{2} \sqrt{3} 2 \sqrt{n}
%D (( a0 a5 midpoint .TeX= \oooo(7,23) y+= -2 place
%D b-1 b5 midpoint .TeX= \oooo(7,25) y+= -2 place
%D b-1 place
%D a0 b0 |->
%D a1 b1 |->
%D a2 b2 |->
%D a3 b3 |->
%D a4 b4 |->
%D a5 b5 |->
%D \N \R -> .plabel= a \sqrt{\phantom{a}}
%D a-1 relplace -7 -7 \phantom{foo}
%D b5 relplace 7 7 \phantom{bar}
%D ))
%D enddiagram
%D
\pu
$$\scalebox{0.95}{$
\begin{array}{rrcl}
\sqrt{\;\;}: & \N &→& \R \\
& n &↦& \sqrt{n} \\
\end{array}
\qquad
\diag{second-blob-function}
$}
$$
\newpage
% _____ _
% | ___| _ _ __ ___| |_ ___ _ __ ___
% | |_ | | | | '_ \ / __| __/ _ \| '__/ __|
% | _|| |_| | | | | (__| || (_) | | \__ \
% |_| \__,_|_| |_|\___|\__\___/|_| |___/
%
% «functors» (to ".functors")
% (excp 15 "functors")
% (exca "functors")
{\bf The internal view of a functor}
% (favp 8 "the-conventions")
% (fav "the-conventions")
% (favp 17 "internal-view-functor")
% (fav "internal-view-functor")
\ssk
{\sl Above} usually means {\sl inside}. (CAI)
The image of a diagram above $\catA$ by a functor $F:\catA→\catB$
is a a diagram {\sl with the same shape} above $\catB$. (CFSh)
%
%D diagram internal-view-functor-0
%D 2Dx 100 +12 +12 +25 +12 +12
%D 2D 100 A1 ____ B1 ____
%D 2D +12 | ____ A3 | ____ B3
%D 2D +12 A2 ____ | B2 ____ |
%D 2D +12 A4 B4
%D 2D
%D 2D +15 \catA ------> \catB
%D 2D
%D ren A1 A2 A3 A4 ==> A_1 A_2 A_3 A_4
%D
%D (( A1 A2 -> .plabel= l f
%D A2 A3 -> .plabel= m g
%D A3 A4 -> .plabel= r h
%D A1 A3 -> .plabel= a k
%D A2 A4 -> .plabel= b m
%D \catA \catB -> .plabel= a F
%D ))
%D enddiagram
%D
%$$\pu
% \diag{internal-view-functor-0}
%$$
%
%D diagram internal-view-functor-1
%D 2Dx 100 +12 +12 +25 +16 +16
%D 2D 100 A1 ____ B1 ____
%D 2D +12 | ____ A3 | ____ B3
%D 2D +12 A2 ____ | B2 ____ |
%D 2D +12 A4 B4
%D 2D
%D 2D +15 \catA ------> \catB
%D 2D
%D ren A1 A2 A3 A4 ==> A_1 A_2 A_3 A_4
%D ren B1 B2 B3 B4 ==> FA_1 FA_2 FA_3 FA_4
%D
%D (( A1 A2 -> .plabel= l f
%D A2 A3 -> .plabel= m g
%D A3 A4 -> .plabel= r h
%D A1 A3 -> .plabel= a k
%D A2 A4 -> .plabel= b m
%D \catA \catB -> .plabel= a F
%D
%D B1 B2 -> .plabel= l Ff
%D B2 B3 -> .plabel= m Fg
%D B3 B4 -> .plabel= r Fh
%D B1 B3 -> .plabel= a Fk
%D B2 B4 -> .plabel= b Fm
%D ))
%D enddiagram
%D
$$\pu
\scalebox{0.9}{$
\diag{internal-view-functor-1}
$}
$$
In this case we don't draw the arrows like $A_1 \mapsto FA_1$ because
there would be too many of them --- we leave them implicit.
\newpage
% «functor-2» (to ".functor-2")
{\bf The internal view of a functor (2)}
\ssk
We say that the diagram in the previous slide is \ColorRed{an}
internal view of the functor $F$. To draw \ColorRed{the} internal view
of the functor $F: \catA → \catB$ we start with a diagram in $\catA$
that is made of two generic objects and a generic morphism between
them. We get this:
%D diagram internal-view-functor-2
%D 2Dx 100 +20
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> C FC D FD \catA \catB
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l g
%D A1 A3 -> .plabel= r Fg
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-2}
$$
% Compare this with the diagram with blob-sets in Section
% \ref{internal-views}, in which the `$n \mapsto \sqrt{n}$' says where
% a generic element is taken.
\newpage
% «functor-3» (to ".functor-3")
{\bf The internal view of a functor (3)}
%\ssk
Any arrow of the form $α \mapsto β$ above a functor arrow $\catA
\ton{F} \catB$ is interpreted as saying that $F$ takes $α$ to $β$, or,
that $Fα$ \ColorRed{reduces} to $β$. So this diagram
%
%D diagram internal-view-functor-3
%D 2Dx 100 +25
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> B A{×}B C A{×}C \Set \Set
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l f
%D A1 A3 -> .plabel= r λp.(πp,f(π'p))
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a (A{×})
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-3}
$$
%
\ColorRed{defines} $(A×)$ as:
%
$$\begin{array}{rcl}
(A×)_0 &:=& λB.\,A×B,\\
(A×)_1 &:=& λf.λp.(πp,f(π'p)).\\
\end{array}
$$
\newpage
% «functor-4» (to ".functor-4")
% (excp 18 "functor-4")
% (exca "functor-4")
{\bf The internal view of a functor (4)}
\ssk
Here the codomain of $F$ is $\Set$, and so we can also use the
internal view of $(A×)f$ to define $(A×)_1$...
%
%D diagram internal-view-functor-4
%D 2Dx 100 +25 +30 +35
%D 2D 100 A0 A1 C0 D0
%D 2D
%D 2D +20 A2 A3 C1 D1
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> B A{×}B C A{×}C \Set \Set
%D ren C0 C1 ==> (a,b) (a,f(b))
%D ren D0 D1 ==> p (πp,f(π'p))
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l f
%D A1 A3 -> .plabel= r (A{×})f
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a (A{×})
%D C0 C1 |->
%D D0 D1 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-4}
$$
\newpage
% _ _ _____
% | \ | |_ _|__
% | \| | | |/ __|
% | |\ | | |\__ \
% |_| \_| |_||___/
%
% «NTs» (to ".NTs")
% (excp 19 "NTs")
% (exca "NTs")
% (favp 22 "internal-view-NT")
% (fav "internal-view-NT")
{\bf How to draw the internal view of a NT}
\ssk
If $F,G:\catA \to \catB$ are functors from $\catA$ to $\catB$,
$T:F \to G$ is a natural transformation from $F$ to $G$, and
$h:C \to D$ is a morphism in $\catA$,
then \ColorRed{$Th$ is a commutative square in $\catB$.}
\msk
How do we visualise this?
How do we visualise this with all details?
\newpage
% «NTs-2» (to ".NTs-2")
% (excp 20 "NTs-2")
% (exca "NTs-2")
%D diagram NT-img-T-only
%D 2Dx 100 +40
%D 2D 100 C0 ---_
%D 2D \ v
%D 2D +20 ---> C3
%D 2D
%D ren C0 C3 ==> \catA \catB
%D
%D (( C0 C3 -> .curve= _12pt .PLABEL= _(0.2) F
%D C0 C3 -> .curve= ^12pt .PLABEL= ^(0.8) G
%D newnode: TL at: tow(@C0,@C3)+v(-7,1.5)
%D newnode: TR at: tow(@C0,@C3)+v(9,1.5) TL TR => .plabel= a T
%D ))
%D enddiagram
%D
%D diagram NT-img-h-only
%D 2Dx 100
%D 2D 100 C
%D 2D +20 D
%D 2D +15 \catA
%D 2D
%D # ren ==>
%D
%D (( C D -> .plabel= l h
%D \catA place
%D ))
%D enddiagram
%D
%D
%D
%D
%D diagram NT-img-full
%D 2Dx 100 +20 +20 +20
%D 2D 100 A0 -------_
%D 2D | -> v
%D 2D +20 | A1 ---> A2
%D 2D v | |
%D 2D +20 B0 -|-----_ |
%D 2D ->v v v
%D 2D +20 B1 ---> B2
%D 2D
%D 2D +17 C0 ---_
%D 2D \ v
%D 2D +20 ---> C3
%D 2D
%D ren A0 A1 A2 ==> C FC GC
%D ren B0 B1 B2 ==> D FD GD
%D ren C0 C3 ==> \catA \catB
%D
%D (( A0 A1 |->
%D A0 A2 |->
%D B0 B1 |->
%D B0 B2 |->
%D C0 C3 -> .curve= _12pt .PLABEL= _(0.2) F
%D C0 C3 -> .curve= ^12pt .PLABEL= ^(0.8) G
%D
%D A0 B0 -> .plabel= l h
%D A1 B1 -> .plabel= m Fh
%D A2 B2 -> .plabel= m Gh
%D A1 A2 -> .plabel= m TC
%D B1 B2 -> .plabel= m TD
%D
%D newnode: FL at: tow(tow(@A0,@B0),tow(@A1,@B1),0+0.17)
%D newnode: FR at: tow(tow(@A0,@B0),tow(@A1,@B1),1-0.17) FL FR |->
%D newnode: GL at: tow(tow(@A0,@B0),tow(@A2,@B2),0+0.37)
%D newnode: GR at: tow(tow(@A0,@B0),tow(@A2,@B2),1-0.19) GL GR |->
%D newnode: TCL at: tow(@A0,tow(@A1,@A2),0.4)
%D newnode: TCR at: tow(@A0,tow(@A1,@A2),0.8) TCL TCR |->
%D newnode: TDL at: tow(@B0,tow(@B1,@B2),0.5)
%D newnode: TDR at: tow(@B0,tow(@B1,@B2),0.85) TDL TDR |->
%D
%D newnode: TL at: tow(@C0,@C3)+v(-7,1.5)
%D newnode: TR at: tow(@C0,@C3)+v(9,1.5) TL TR => .plabel= a T
%D ))
%D enddiagram
%D
$\pu
\pdiag{NT-img-T-only}
\pdiag{NT-img-h-only} =
\left(
\;\; \diag{NT-img-full}
\;\;
\right)
$
\newpage
% «NTs-3» (to ".NTs-3")
% (excp 21 "NTs-3")
% (exca "NTs-3")
%D diagram ??
%D 2Dx 100 +25 +25
%D 2D 100 A0 B0 B1
%D 2D
%D 2D +25 A1 B2 B3
%D 2D
%D 2D +20 C0 C1
%D 2D
%D ren A0 B0 B1 ==> C FC GC
%D ren A1 B2 B3 ==> D FD GD
%D ren C0 C1 ==> \catA \catB
%D
%D (( A0 A1 -> .plabel= l h
%D B0 B1 -> .plabel= a TC
%D B2 B3 -> .plabel= a TD
%D B0 B2 -> .plabel= l Fh
%D B1 B3 -> .plabel= r Fg
%D C0 C1 -> .plabel= a T
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\newpage
% __ __ _
% \ \ / /__ _ __ ___ __| | __ _
% \ V / _ \| '_ \ / _ \/ _` |/ _` |
% | | (_) | | | | __/ (_| | (_| |
% |_|\___/|_| |_|\___|\__,_|\__,_|
%
% «yoneda» (to ".yoneda")
% (excp 22 "yoneda")
% (exca "yoneda")
{\bf Trailer: Yoneda in a particular case}
(With a representable functor... \cite[section 7.7]{FavC})
% (favp 40 "representable-functors")
% (fav "representable-functors")
% (favp 42 "representable-functor-ex")
% (fav "representable-functor-ex")
%D diagram 2.3.4._Z[x]
%D 2Dx 100 +55
%D 2D 100 A1
%D 2D +20 A2 A3
%D 2D +20 A4 A5
%D 2D +15 B0 B1
%D 2D +15 C1 C2
%D 2D +20 C3
%D 2D
%D ren A1 ==> 1
%D ren A2 A3 ==> \Z[x] U(\Z[x])
%D ren A4 A5 ==> R UR
%D ren B0 B1 ==> \Rings \Set
%D ren C1 C2 ==> \Rings(\Z[x],-) \Set(1,U-)
%D ren C3 ==> U
%D
%D (( A1 A3 -> .plabel= r \sm{\nameof{x}\\\univ}
%D A2 A3 |->
%D A2 A4 -> .plabel= l ϕ
%D A3 A5 -> .plabel= r Uϕ
%D A4 A5 |->
%D A1 A5 -> .slide= 25pt .plabel= r \nameof{ϕ(x)}
%D A2 A5 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a U
%D C1 C2 <-> .plabel= b T
%D C1 C3 <-> .plabel= b T'
%D C2 C3 <->
%D ))
%D enddiagram
%D
$$\pu
\scalebox{0.9}{$
\diag{2.3.4._Z[x]}
$}
$$
\newpage
% _ __
% | |/ /__ _ _ __
% | ' // _` | '_ \
% | . \ (_| | | | |
% |_|\_\__,_|_| |_|
%
% «kan» (to ".kan")
% (excp 23 "kan")
% (exca "kan")
{\bf Trailer: (right) Kan Extensions}
(From \cite[section 7.9]{FavC})
% (favp 45 "kan-extensions")
% (fav "kan-extensions")
% (favp 33 "basic-example-full")
% (fav "basic-example-full")
%D diagram kan-1
%D 2Dx 100 +35
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +20 A2 - A3
%D 2D |
%D 2D +20 A4
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> GF ∀G
%D ren A2 A3 ==> RF R{:=}\Ran_FH
%D ren A4 ==> H
%D ren B0 B1 ==> \catC^\catA \catC^\catB
%D ren C0 C1 ==> \catA \catB
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l GU
%D A1 A3 -> .plabel= r ∃!U
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l T
%D A0 A4 -> .slide= -20pt .plabel= l ∀V
%D B0 B1 <- sl^ .plabel= a ∘F
%D B0 B1 -> sl_ .plabel= b \Ran_F
%D C0 C1 -> .plabel= a F
%D ))
%D enddiagram
%D
%D diagram kan-2-cells-1
%D 2Dx 100 +25 +25 +20 +25 +25 +20 +25 +25
%D 2D 100 A1 B1 C1
%D 2D / \ / \ / \\
%D 2D +25 A0 ---- A2 B0 ---- B2 C0 ---- C2
%D 2D
%D ren A0 A1 A2 ==> \catA \catB \catC
%D
%D (( A0 A1 -> .plabel= a F
%D A1 A2 -> .curve= _10pt .plabel= m R
%D A1 A2 -> .curve= ^20pt .plabel= a ∀G
%D A0 A2 -> .plabel= b H
%D A0 A2 midpoint relplace -4 -8 \Dn{T}
%D A1 A2 midpoint relplace 2 -3 \Dn{∃!U}
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-1}
\qquad
\quad
\diag{kan-2-cells-1}
$$
\newpage
% ___ _ _____ _____
% |_ _|_ __ | |_ _ __ ___ |_ _|_ _|
% | || '_ \| __| '__/ _ \ | | | |
% | || | | | |_| | | (_) | | | | |
% |___|_| |_|\__|_| \___/ |_| |_|
%
% «intro-TT» (to ".intro-TT")
% (excp 24 "intro-TT")
% (exca "intro-TT")
\thispagestyle{empty} % (find-es "tex" "thispagestyle")
\begin{center}
\vspace*{1.5cm}
\begin{tabular}{c}
{\Large {\bf Introduction}} \\[1pt]
{\Large {\bf to Type Theory}} \\[1pt]
\end{tabular}
\end{center}
\newpage
% «untyped-lambda» (to ".untyped-lambda")
% (excp 25 "untyped-lambda")
% (exca "untyped-lambda")
{\bf A bit of untyped $λ$-calculus}
\ssk
If $h = (λa.a·a+4)$ then...
% (lam181p 5 "lambda")
% (lam181 "lambda")
%D diagram reduce-h
%D 2Dx 100 +35 +35 +40 +30
%D 2D 100 A ----> B
%D 2D | |
%D 2D v v
%D 2D +20 CL ---> DL
%D 2D | |
%D 2D v |
%D 2D +20 CS ---> DS
%D 2D | |
%D 2D v |
%D 2D +20 E |
%D 2D | \ |
%D 2D | v |
%D 2D +20 | F |
%D 2D | \ |
%D 2D v v v
%D 2D +20 G ----> H -> I -> J
%D 2D
%D ren A B ==> h(2+3) h(5)
%D ren CL DL ==> (λa.\,a·a+4)(2+3) (λa.\,a·a+4)(5)
%D ren CS DS ==> (a·a+4)[a:=2+3] (a·a+4)[a:=5]
%D ren E F ==> (2+3)·(2+3)+4 (2+3)·5+4
%D ren G H ==> 5·(2+3)+4 5·5+4
%D ren I J ==> 25+4 29
%D (( A B -> CS DS -> CL DL -> E F -> F H -> G H ->
%D A CL -> CL CS -> CS E -> E G ->
%D B DL -> DL DS -> DS H -> H I -> I J ->
%D ))
%D enddiagram
%D
$$\pu
\scalebox{0.80}{$
\diag{reduce-h}
$}
$$
\newpage
% «types-after-discrete» (to ".types-after-discrete")
% (excp 26 "types-after-discrete")
% (exca "types-after-discrete")
{\bf Types after Discrete Mathematics}
\ssk
% (lam181p 9 "typed-L1-trees")
% (lam181 "typed-L1-trees")
$\begin{array}{l}
\text{If:} \\
A = \{1,2\}, \\
B = \{3,4\}, \\
C = \{30,40\}, \\
D = \{10,20\}, \\[5pt]
\text{Then:} \\
A×B = \cmat{(1,3),(1,4),\\(2,3),(2,4)} \\[8pt]
B→C = \cmat{
\csm{(3,30),\\(4,30)},
\csm{(3,30),\\(4,40)},
\csm{(3,40),\\(4,30)},
\csm{(3,40),\\(4,40)}\\
} \\
\end{array}
$
\newpage
If we know \ColorOrange{(the values of)} $a$, $b$, $f$
then we know \ColorOrange{(the value of)} $(a,f(b))$.
If $(a,b)=(2,3)$ and $f=\csm{(3,30),\\(4,40)}$
then $(a,f(b))=(2,30)$.
\msk
In trees:
%:
%: (a,b) (2,3)
%: -----π' -----π'
%: (a,b) b f (2,3) 3 \csm{(3,30),\\(4,40)}
%: -----π --------\app -----π --------------------------\app
%: a f(b) 2 30
%: --------------\pair -----------------\pair
%: (a,f(b)) (2,30)
%:
%: ^idxf1 ^idxf2
%:
$$\pu
\scalebox{0.9}{$
\ded{idxf1} \qquad \ded{idxf2}
$}
$$
\newpage
\scalebox{0.8}{%
\begin{tabular}{l}
If we know the {\sl types} of $a$, $b$, $f$ \\
we know the type of $(a,f(b))$. \\
If we know the types of $p$, $f$ \\
we know the type of $(πp,f(π'p))$. \\
If we know the types of $p$, $f$ \\
we know the type of $(λp:A×B.(πp,f(π'p)))$. \\
\end{tabular}
}
\msk
%:
%: (a,b):A×B p:A×B
%: ---------π' -----π'
%: (a,b):A×B b:B f:B→C p:A×B π'p:B f:B→C
%: ---------π ---------------\app ------π ----------------\app
%: a:A f(b):C πp:A f(π'p):C
%: ----------------------\pair ----------------------\pair
%: (a,f(b)):A×C (πp,f(π'p)):A×C
%:
%: ^idxf3 ^idxf4
%:
%:
%: p:A×B
%: -----π'
%: p:A×B π'p:B f:B→C
%: ------π ----------------\app
%: πp:A f(π'p):C
%: ----------------------\pair
%: (πp,f(π'p)):A×C
%: -----------------------------λ
%: (λp:A×B.(πp,f(π'p))):A×B→A×C
%:
%: ^idxf5
\pu
$$\scalebox{0.8}{$
\begin{array}{l}
\ded{idxf3}
\\ \\
\ded{idxf5}
\end{array}
$}
$$
% $$\ded{idxf4}$$
% $$\ded{idxf3} \qquad \ded{idxf4}$$
\newpage
% «type-inference» (to ".type-inference")
% (excp 29 "type-inference")
% (exca "type-inference")
\def\und#1#2{\underbrace{#1}_{#2}}
% {\bf Type inference}
% The usual way to type all subexpressions in via trees...
Compare:
\msk
% (lam181p 8 "types")
% (lam181 "types")
% (lam181p 11 "type-inference")
% (lam181 "type-inference")
%UB λ p : A×B. (π p , f (π' p ))
%UB ---- ---- ---- ----
%UB :A×B :A×B :B→C :A×B
%UB ------ -------
%UB :A :B
%UB ---------------
%UB :C
%UB -------------------------
%UB :A×C
%UB --------------------------------------
%UB :A×B→A×C
%L
%L defub "Axf 1"
%
$\pu
\scalebox{0.9}{$
\begin{array}{c}
\ded{idxf5}
\\ \\
\ub{Axf 1}
\end{array}
$}
$
\newpage
% «typing» (to ".typing")
% (excp 30 "typing")
% (exca "typing")
{\bf Typing}
\def\Co#1{{\color{orange}(#1)}} % Constraint
\def\Bc#1{{\color{Red} #1 }} % Bad constraint (not yet satisfied)
\def\Gc#1{{\color{Green}#1 }} % Good constraint (satisfied)
\def\Gc#1{{\color{SpringGreen4}#1 }} % Good constraint (satisfied)
\ssk
Idea: start with lots of type variables,
look at the constraints induced by the underbraces,
try to find a substitution that works...
\msk
%UB λ p . (π p , f (π' p ))
%UB ---- ---- ---- ----
%UB :A :A :B :A
%UB ------ -------
%UB :C :D
%UB ---------------
%UB :E
%UB -------------------------
%UB :F
%UB --------------------------------------
%UB :G
%L
%L defub "Axf 2"
%
$\pu
\myvcenter{\ub{Axf 2}}
\qquad
\begin{array}{rc}
\Co{C⇒} & \Bc{A = C×▁} \\
\Co{D⇒} & \Bc{A = ▁×D} \\
\Co{E⇒} & \Bc{B = D→E} \\
\Co{F⇒} & \Bc{F = C×E} \\
\Co{G⇒} & \Bc{G = A→F} \\
\end{array}
$
\msk
First step: $[A:=C×D]$
\newpage
In the previous slide all the constraints
were red, meaning ``not satisfied yet''.
Let's mark the ones that are satisfied in green
and perform more substituions if needed...
\msk
%UB λ p . (π p , f (π' p ))
%UB ---- ---- ---- ----
%UB :C×D :C×D :B :C×D
%UB ------ -------
%UB :C :D
%UB ---------------
%UB :E
%UB -------------------------
%UB :F
%UB --------------------------------------
%UB :G
%L
%L defub "Axf 3"
%
$\pu
\myvcenter{\ub{Axf 3}}
\qquad
\begin{array}{rc}
\Co{C⇒} & \Gc{C×D = C×▁} \\
\Co{D⇒} & \Gc{C×D = ▁×D} \\
\Co{E⇒} & \Bc{B = D→E} \\
\Co{F⇒} & \Bc{F = C×E} \\
\Co{G⇒} & \Bc{G = C×D→F} \\
\end{array}
$
\msk
Next step: $\bmat{B:=D→E \\ F:=C×E}$
\newpage
Let's
do
it
again...
\msk
%UB λ p . (π p , f (π' p ))
%UB ---- ---- ---- ----
%UB :C×D :C×D :D→E :C×D
%UB ------ -------
%UB :C :D
%UB ---------------
%UB :E
%UB -------------------------
%UB :C×E
%UB --------------------------------------
%UB :G
%L
%L defub "Axf 4"
%
$\pu
\scalebox{0.85}{$
\myvcenter{\ub{Axf 4}}
\qquad
\begin{array}{rc}
\Co{C⇒} & \Gc{C×D = C×▁} \\
\Co{D⇒} & \Gc{C×D = ▁×D} \\
\Co{E⇒} & \Gc{D→E = D→E} \\
\Co{F⇒} & \Gc{C×E = C×E} \\
\Co{G⇒} & \Bc{G = C×D→C×E} \\
\end{array}
$}
$
\msk
Next step: $[G := C×D→C×E]$
\newpage
Done! Note that:
1) $C,D,E$ are {\sl type variables},
2) this typing is {\sl universal} --- all other valid typing
are substitution instances of this one. For example...
(see the next page)
\bsk
\bsk
\ColorBrown{
\footnotesize
Exercise:
Compare our naïve approach here
with the ones in \cite[chapter 22]{Pierce}.
% (find-books "__comp/__comp.el" "pierce")
% (find-taplpage (+ 22 317) "22 Type Reconstruction")
% (find-tapltext (+ 22 317) "22 Type Reconstruction")
% (find-taplpage (+ 22 317) "22.1 Type Variables and Substitutions")
% (find-taplpage (+ 22 319) "22.2 Two Views of Type Variables")
% (find-taplpage (+ 22 321) "22.3 Constraint-Based Typing")
% (find-taplpage (+ 22 326) "22.4 Unification")
% (find-taplpage (+ 22 329) "22.5 Principal Types")
% (find-taplpage (+ 22 330) "22.6 Implicit Type Annotations")
% (find-taplpage (+ 22 331) "22.7 Let-Polymorphism")
% (find-taplpage (+ 22 336) "22.8 Notes")
}
\newpage
%UB λ p . (π p , f (π' p ))
%UB ---- ---- ---- ----
%UB :C×D :C×D :D→E :C×D
%UB ------ -------
%UB :C :D
%UB ---------------
%UB :E
%UB -------------------------
%UB :C×E
%UB --------------------------------------
%UB :C×D→C×E
%L
%L defub "Axf 5"
%
%UB λ p . (π p , f (π' p ))
%UB ---- ---- ---- ----
%UB :A×B :A×B :B→C :A×B
%UB ------ -------
%UB :A :B
%UB ---------------
%UB :C
%UB -------------------------
%UB :A×C
%UB --------------------------------------
%UB :A×B→A×C
%L
%L defub "Axf 6"
%
$\pu
\scalebox{0.85}{$
\begin{array}{c}
\left(\myvcenter{\ub{Axf 5}}\right) \bmat{C:=A \\ D:=B \\ E:=C} =
\\ \\
\left(\myvcenter{\ub{Axf 6}}\right)
\end{array}
$}
$
\newpage
{\bf Very very concrete types}
\msk
%UB λ p :\A×\B . (π p , f (π' p ))
%UB ------ ------ ------ ------
%UB :\A×\B :\A×\B :\B→\C :\A×\B
%UB -------- ---------
%UB :\A :\B
%UB -----------------
%UB :\C
%UB ------------------------------
%UB :\A×\C
%UB ----------------------------------------------------
%UB :\A×\B→\A×\C
%L
%L defub "Axf concrete 1"
%
$\pu
\def\AA{\{0,1\}}
\def\BB{\{2,3\}}
\def\CC{\{4,5\}}
\scalebox{0.80}{$
\begin{array}{c}
{\def\A{A}
\def\B{B}
\def\C{C}
\left(\myvcenter{\ub{Axf concrete 1}}\right)
}
\bmat{A:=\AA \\ B:=\BB \\ C:=\CC} =
\\ \\
{\def\A{\AA}
\def\B{\BB}
\def\C{\CC}
\left(\myvcenter{\ub{Axf concrete 1}}\right)
}
\end{array}
$}
$
% (find-books "__logic/__logic.el" "damas")
% (find-damasphdpage (+ 8 72) "2.4. The type assignment algorithm W")
% (find-books "__comp/__comp.el" "pierce")
% (find-taplpage (+ 22 317) "22 Type Reconstruction")
% https://papl.cs.brown.edu/2014/Type_Inference.html
\newpage
% «intro-to-the-hard-part» (to ".intro-to-the-hard-part")
% (excp 36 "intro-to-the-hard-part")
% (exca "intro-to-the-hard-part")
\thispagestyle{empty} % (find-es "tex" "thispagestyle")
\begin{center}
\vspace*{1.0cm}
\begin{tabular}{c}
{\Large {\bf Introduction}} \\[1pt]
{\Large {\bf to the Hard Part}} \\[1pt]
{\Large {\bf of Basic Type Theory}} \\[1pt]
\end{tabular}
\end{center}
\newpage
% «some-references» (to ".some-references")
% (excp 37 "some-references")
% (exca "some-references")
Girard:
\cite{GLT} and \cite{GirardBlind}
\msk
Benjamin Pierce's book, Haskell:
\cite{Pierce}, \cite{HaskellCore}, \cite{Hutton}
\msk
HOTT, Kamareddine:
\cite{HOTT}, \cite{Kamareddine}
\msk
Also:
\cite{Sommaruga}, \cite{BauerGDDTT}
\msk
Some of them don't even mention $Σ$-types...
``$Σ$-types can be constructed from $Π$-types''
\ColorRed{This is not trivial at all! \frown}
\newpage
% ____ _ _
% / ___|___ _ __ | |_ _____ _| |_ ___
% | | / _ \| '_ \| __/ _ \ \/ / __/ __|
% | |__| (_) | | | | || __/> <| |_\__ \
% \____\___/|_| |_|\__\___/_/\_\\__|___/
%
% «contexts» (to ".contexts")
% (excp 38 "contexts")
% (exca "contexts")
% (ntyp 60 "judgments-2")
% (nty "judgments-2")
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
{\bf Contexts}
$\setofsc {\uC{\ug{a∈\{1,2\}}, \ug{b∈\{2,3\}}, \uf{a<b}}} {\ue{10a+b}}$
here the context has ``generators'' (``{\sl var} $∈$ {\sl set}'')
and ``filters'' (``{\sl this expression must be true}'').
\msk
In
$\uC{\uvt{A⠆Θ}, \uvt{B⠆Θ}, \uvt{C⠆Θ}, \uvt{p:A×B}, \uvt{g:B→C}} ⊢
\uconc{\uterm{(πp,g(π'p))}:\utype{A×C}}
$
the context is made of several declarations of the form
``variable : type''...
\newpage
% ____ _____ ____
% | _ \_ _/ ___| ___
% | |_) || | \___ \/ __|
% | __/ | | ___) \__ \
% |_| |_| |____/|___/
%
% «PTSs» (to ".PTSs")
% (excp 39 "PTSs")
% (exca "PTSs")
{\bf Derivations in Pure Type Systems}
Derivations in a PTS have {\sl lots} of bureaucracy.
This is what we need to derive $A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ$:
\msk
%: (fooi-t ":" "⠆")
%:
%: ----a ----a ----a ----a ----a
%: ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□
%: ----a ----a ----a -----------w -------v -----------w
%: ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□ A⠆Θ⊢Θ⠆□ A⠆Θ⊢A⠆Θ A⠆Θ⊢Θ⠆□
%: -----------w -------v -----------------------w -----------v
%: A⠆Θ⊢Θ⠆□ A⠆Θ⊢A⠆Θ A⠆Θ,B⠆Θ⊢A⠆Θ A⠆Θ,B⠆Θ⊢B⠆Θ
%: -----------------------w ---------------------------------w
%: A⠆Θ,B⠆Θ⊢A⠆Θ A⠆Θ,B⠆Θ,a⠆A⊢B⠆Θ
%: ----------------------------------------------Π_{ΘΘΘ}
%: A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ
%:
%: ^depprod1
%:
%: ----a ----a ----a ----a ----a
%: ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□
%: ----a ----a ----a -----------w_□ -------v_□ -----------w_□
%: ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□ A⠆Θ⊢Θ⠆□ A⠆Θ⊢A⠆Θ A⠆Θ⊢Θ⠆□
%: -----------w_□ -------v_□ -----------------------w_□ -----------v_□
%: A⠆Θ⊢Θ⠆□ A⠆Θ⊢A⠆Θ A⠆Θ,B⠆Θ⊢A⠆Θ A⠆Θ,B⠆Θ⊢B⠆Θ
%: -----------------------w_□ ---------------------------------w_Θ
%: A⠆Θ,B⠆Θ⊢A⠆Θ A⠆Θ,B⠆Θ,a⠆A⊢B⠆Θ
%: --------------------------------------------------Π_{ΘΘΘ}
%: A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ
%:
%: ^depprod1
%:
%:
%: ----a ----a ----a
%: ⊢Θ⠆□ ⊢Θ⠆□ ⊢Θ⠆□
%: ======= -------v_□ -----------w_□
%: A⠆Θ⊢Θ⠆□ A⠆Θ⊢A⠆Θ A⠆Θ⊢Θ⠆□
%: -----------------------w_□ -----------v_□
%: A⠆Θ,B⠆Θ⊢A⠆Θ A⠆Θ,B⠆Θ⊢B⠆Θ
%: =========== ---------------------------------w_Θ
%: A⠆Θ,B⠆Θ⊢A⠆Θ A⠆Θ,B⠆Θ,a⠆A⊢B⠆Θ
%: ---------------------------------------------------Π_{ΘΘΘ}
%: A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ
%:
%: ^depprod2
%:
\pu
\resizebox{1.0\textwidth}{!}{%
$\ded{depprod1}
$}
\msk
i.e.:
\resizebox{1.0\textwidth}{!}{%
$\ded{depprod2}
$}
\newpage
% ____ _____ ____ ____
% | _ \_ _/ ___| _____ __ |___ \
% | |_) || | \___ \ / _ \ \/ / __) |
% | __/ | | ___) | | __/> < / __/
% |_| |_| |____/ \___/_/\_\ |_____|
%
% «PTSs-2» (to ".PTSs-2")
% «pts-derivation-2» (to ".pts-derivation-2")
{\bf Pure Type Systems: a derivation (2)}
This is what we need to derive $A⠆Θ⊢(λa⠆A.a)⠆(Πa⠆A.A)$:
\msk
%:
%:
%: ----a
%: ⊢Θ⠆□
%: ======= -------v_□
%: A⠆Θ⊢A⠆Θ A⠆Θ⊢A⠆Θ
%: ======= ======= -----------------w_Θ
%: A⠆Θ⊢A⠆Θ A⠆Θ⊢A⠆Θ A⠆Θ,a⠆A⊢A⠆Θ
%: -----------v_Θ -----------------------Π_{ΘΘΘ}
%: A⠆Θ,a⠆A⊢a⠆A A⠆Θ⊢(Πa⠆A.A)⠆Θ
%: -------------------------------------λ
%: A⠆Θ⊢(λa⠆A.a)⠆(Πa⠆A.A)
%:
%: ^depprod3
%:
\pu
\resizebox{1.0\textwidth}{!}{%
$\ded{depprod3}
$}
\bsk
\bsk
\ColorBrown{
\footnotesize
Exercise:
Read the presentation of PTSs in \cite[section 4c]{Kamareddine}.
Translate these trees to the notation of the book.
You will need a few tiny changes.
% (find-books "__logic/__logic.el" "typetheory")
% (find-mpottpage (+ 12 116) "4c Pure Type Systems")
% (find-mpottpage (+ 12 118) "4c1 The Barendregt cube")
% (find-mpottpage (+ 12 121) "4c2 Metaproperties of PTSs")
}
\newpage
% _ _ _ _____
% | |_ _ __| | __ _ _ __ ___ ___ _ __ | |_ ___ |___ /
% _ | | | | |/ _` |/ _` | '_ ` _ \ / _ \ '_ \| __/ __| |_ \
% | |_| | |_| | (_| | (_| | | | | | | __/ | | | |_\__ \ ___) |
% \___/ \__,_|\__,_|\__, |_| |_| |_|\___|_| |_|\__|___/ |____/
% |___/
%
% «judgments» (to ".judgments")
% (excp 37 "judgments")
% (exca "judgments")
% (ntyp 61 "judgments-3")
% (nty "judgments-3")
{\bf Judgments}
If we think --- \ColorRed{informally} --- that
$Θ$ is the ``set of all sets'' (mnemonic: Theta for ``Theths''),
then we can put these judgments for $λ$-calculus in
a very homogeneous form...
\msk
$\uC{\uvt{A⠆Θ}, \uvt{B⠆Θ}, \uvt{C⠆Θ}, \uvt{p:A×B}, \uvt{g:B→C}} ⊢
\uconc{\uterm{(πp,g(π'p))}:\utype{A×C}}
$
\msk
the context is a series of declarations of the form ``var : type'',
and the conclusion is of the form ``term : type''.
\newpage
% ____ _
% | _ \ ___ _ __ | |_ _ _ _ __ ___ ___
% | | | |/ _ \ '_ \ | __| | | | '_ \ / _ \/ __|
% | |_| | __/ |_) | | |_| |_| | |_) | __/\__ \
% |____/ \___| .__/ \__|\__, | .__/ \___||___/
% |_| |___/|_|
%
% «dependent-types» (to ".dependent-types")
% (excp 42 "dependent-types")
% (exca "dependent-types")
% (find-books "__logic/__logic.el" "hott")
% (find-hottpage (+ 12 25) "1.4 Dependent function types (-types)")
% (find-hottpage (+ 12 26) "1.5 Product types")
% (find-hottpage (+ 12 30) "1.6 Dependent pair types (-types)")
{\bf Dependent types for children}
\ssk
\def\ato#1#2{\csm{(0,#1),\\(1,#2)}}
\def\ABCD{
\begin{array}[t]{c}
A = \{0,1\}, \\
B = \{2,3\}, \\
C_0 = \{4,5\}, \\
C_1 = \{6,7\} \\
\\
f:A→B \\
f(a)∈B \\[5pt]
g:(a⠆A)→C_a \\
g(a)∈C_a \\[5pt]
p∈A×B \\
π'p∈B \\[5pt]
q∈(a⠆A)×C_a \\
π'q∈C_{πq} \\[5pt]
\end{array}}
\def\Examples{
\begin{array}[t]{rcl}
\multicolumn{3}{l}{\text{Function types and}} \\
\multicolumn{3}{l}{\text{dependent function types ($Π$-types):}} \\[5pt]
A→B & = & \cmat{\ato22, \ato23, \ato32, \ato44} \\[10pt]
(a:A)→C_a & = \\
Πa:A.C_a & = & \cmat{\ato46, \ato47, \ato56, \ato57} \\
\\
\multicolumn{3}{l}{\text{Product types and}} \\
\multicolumn{3}{l}{\text{dependent pair types ($Σ$-types):}} \\[5pt]
A×B & = & \{ (0,2),\, (0,3), \, (1,2), \, (1,3) \} \\[5pt]
(a:A)×C_a & = & \\
Σa:A.C_a & = & \{ (0,4),\, (0,5), \, (1,6), \, (1,7) \} \\
\end{array}}
$\scalebox{0.75}{$
\begin{array}{l}
\ABCD \quad \Examples \\
\\
\begin{tabular}{l}
Note: ``$(a:A)→C_a$'' and ``$(a:A)×C_a$'' are Agda-isms. \\
Many places use the terms ``dependent products'' and ``dependent sums''. \\
\end{tabular}
\end{array}
$}
$
\newpage
% _ _ _ _
% / \ _ __ __| | __ _ _ __ __| | (_)_ __ ___ _ __
% / _ \ | '_ \ / _` | / _` | '_ \ / _` | | | '_ ` _ \| '_ \
% / ___ \| | | | (_| | | (_| | | | | (_| | | | | | | | | |_) |
% /_/ \_\_| |_|\__,_| \__,_|_| |_|\__,_| |_|_| |_| |_| .__/
% |_|
%
% «typing-and-and-implies» (to ".typing-and-and-implies")
% (excp 43 "typing-and-and-implies")
% (exca "typing-and-and-implies")
{\bf Typing proofs of ``and'' and ``implies''}
$«Q»$ is a proof of $Q$.
$⟦Q⟧$ is the set of all proofs of $Q$.
\msk
$⟦Q∧R⟧$ is the set of all proofs of $Q∧R$.
\ColorRed{A} $«Q∧R»$ is a proof of $Q∧R$.
\ColorRed{A} $«Q∧R»$ is a pair $(«Q»,«R»)$,
so $⟦Q∧R⟧$ = $⟦Q⟧×⟦R⟧$.
\msk
$⟦Q→R⟧$ is the set of all proofs of $Q→R$.
\ColorRed{A} $«Q→R»$ is a proof of $Q→R$.
\ColorRed{A} $«Q→R»$ is an operation that takes $«Q»$s to $«R»$s,
so $⟦Q→R⟧$ = $⟦Q⟧→⟦R⟧$.
\newpage
% _____ _ _____
% | ___|_ _ __ _ _ __ __| | | ____|_ __
% | |_ / _` | / _` | '_ \ / _` | | _| \ \/ /
% | _| (_| | | (_| | | | | (_| | | |___ > <
% |_| \__,_| \__,_|_| |_|\__,_| |_____/_/\_\
%
% «typing-forall-and-exists» (to ".typing-forall-and-exists")
% (excp 44 "typing-forall-and-exists")
% (exca "typing-forall-and-exists")
{\bf Typing proofs of ``for all'' and ``exists''}
\bsk
% (find-mpottpage (+ 14 103) "II Propositions as Types, Pure Type Systems, AUTOMATH")
% (find-mpottpage (+ 12 105) "4 Propositions as Types and Pure Type Systems")
% (find-mpottpage (+ 12 106) "4a Propositions as Types and Proofs as Terms (PAT)")
% (find-mpottpage (+ 12 106) "4a1 Intuitionistic logic")
% (find-mpottpage (+ 16 123) "A universal quantification")
% (find-mpotttext (+ 16 123) "A universal quantification")
% (find-mpottpage (+ 16 147) "various ways in which PAT")
% (find-mpotttext (+ 16 147) "various ways in which PAT")
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\def\und#1#2{\underbrace{#1}_{#2}}
%UB «∀b⠆B.P(b)» = \PFA
%UB ------------ ------------
%UB :⟦∀b⠆B.P(b)⟧ :Πb⠆B.⟦P(b)⟧
%L
%L defub "forall"
%
$\pu
\def\PFA{\cmat{
(2,«P(2)»), \\
(3,«P(3)»)
}}
\scalebox{1.0}{$
\begin{array}{c}
\ub{forall}
\end{array}
$}
$
\bsk
\bsk
%UB «∃b⠆B.P(b)» = \PEX
%UB ------------ ------------
%UB :⟦∃b⠆B.P(b)⟧ :Σb⠆B.⟦P(b)⟧
%L
%L defub "forall"
%
$\pu
\def\PEX{(b,«P(b)»)}
\scalebox{1.0}{$
\begin{array}{c}
\ub{forall}
\end{array}
$}
$
%\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
% \end{document}
% \newpage
%
% % «marsden» (to ".marsden")
%
% {\bf String diagrams: Marsden}
%
% % (find-books "__cats/__cats.el" "marsden-dragging")
% % (find-books "__cats/__cats.el" "marsden-ctusd")
% % (favp 44 "2-category-of-cats")
% % (fav "2-category-of-cats")
% (find-es "haskell" "haskell-to-core")
\newpage
% ______ ____ __ ____ _ _
% / ___\ \ / / \/ | / ___|_ __| | / |
% | | \ \ /\ / /| |\/| | | | | '__| | | |
% | |___ \ V V / | | | | | |___| | | |___ | |
% \____| \_/\_/ |_| |_| \____|_| |_____| |_|
%
% «guessing-nu-CWM-1» (to ".guessing-nu-CWM-1")
% (excp 45 "guessing-nu-CWM-1")
% (exca "guessing-nu-CWM-1")
{\bf CWM: Creation of Limits, theorem V.1}
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 109) "V. Limits")
% (find-cwm2page (+ 13 109) "1. Creation of Limits")
\def\Cone{\mathrm{Cone}}
\def\Nat{\mathrm{Nat}}
\def\vcat#1#2#3{\psm{
& \\
& &↓ \\
#1&→\\}}
\def\constvcat#1{\vcat{#1}{#1}{#1}}
\def\smallvcat{{\scalebox{0.50}{$\vcat123$}}}
\def\ACB{A{×_C}B}
%D diagram nu-CWM-1
%D 2Dx 100 +30
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +20 A2 - A3
%D 2D |
%D 2D +20 A4
%D 2D
%D 2D +15 B0 - B1
%D 2D
%D ren A0 A1 ==> Δ* *
%D ren A2 A3 ==> ΔL L
%D ren A4 ==> F
%D ren B0 B1 ==> \text{Set}^J \text{Set}
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l Δg
%D A1 A3 -> .plabel= r ∃!g
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l \sm{ν\\\text{(univ)}}
%D A0 A4 -> .slide= -30pt .plabel= l ∀σ
%D B0 B1 <- sl^ .plabel= a Δ
%D B0 B1 -> sl_ .plabel= b \Lim
%D newnode: A3R at: @A3+v(28,8) .TeX= \defL place
%D ))
%D enddiagram
%D
%D diagram nu-CWM-X
%D 2Dx 100 +30
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +20 A2 - A3
%D 2D |
%D 2D +20 A4
%D 2D
%D 2D +15 B0 - B1
%D 2D
%D ren A0 A1 ==> ΔX X
%D ren A2 A3 ==> ΔL L
%D ren A4 ==> F
%D ren B0 B1 ==> \text{Set}^J \text{Set}
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l Δh
%D A1 A3 -> .plabel= r ∃!h
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l \sm{ν\\\text{(univ)}}
%D A0 A4 -> .slide= -30pt .plabel= l ∀τ
%D B0 B1 <- sl^ .plabel= a Δ
%D B0 B1 -> sl_ .plabel= b \Lim
%D ))
%D enddiagram
%D
$$\pu
\def\defL{\begin{array}{l}
:=\Cone(*,F) \\ =\Nat(Δ*,F) \\ = \Hom(Δ*,F) \\
\end{array}}
%
\scalebox{0.9}{$
\diag{nu-CWM-1}
\quad
\diag{nu-CWM-X}
$}
$$
\newpage
% «guessing-nu-1» (to ".guessing-nu-1")
% (excp 46 "guessing-nu-1")
% (exca "guessing-nu-1")
{\bf Guessing $ν$: first attempt}
%D diagram nu-1-small
%D 2Dx 100 +35
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +20 A2 - A3
%D 2D |
%D 2D +20 A4
%D 2D
%D 2D +15 B0 - B1
%D 2D
%D ren A0 A1 ==> Δ1 1
%D ren A2 A3 ==> Δ\Lim\,F \Lim\,F
%D ren A4 ==> F
%D ren B0 B1 ==> \Set^\catJ \Set
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l Δg
%D A1 A3 -> .plabel= r ∃!g
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l \sm{ν\\\text{(univ)}}
%D A0 A4 -> .slide= -30pt .plabel= l ∀σ
%D B0 B1 <- sl^ .plabel= a Δ
%D B0 B1 -> sl_ .plabel= b \Lim
%D ))
%D enddiagram
%D
%D diagram nu-1
%D 2Dx 100 +50
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +35 A2 - A3
%D 2D |
%D 2D +35 A4
%D 2D
%D 2D +25 B0 - B1
%D 2D
%D ren A0 A1 ==> \constvcat{1} 1
%D ren A2 A3 ==> \constvcat{\ACB} \ACB
%D ren A4 ==> \vcat{A}{B}{C}
%D ren B0 B1 ==> \Set^\smallvcat_{\phantom{a}} \Set
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l Δg
%D A1 A3 -> .plabel= r ∃!g
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l \sm{ν\\\text{(univ)}}
%D A0 A4 -> .slide= -45pt .plabel= l ∀σ
%D B0 B1 <- sl^ .plabel= a Δ
%D B0 B1 -> sl_ .plabel= b \Lim
%D ))
%D enddiagram
%D
$\pu
\scalebox{0.9}{$
\diag{nu-1-small}
\qquad
\diag{nu-1}
$}
$
\newpage
In this first attempt the types don't match...
A natural transformation
%
$$σ: \vcat{1}{1}{1} → \vcat{A}{B}{C}$$
is a triple $(\nameof{a}:1→A, \nameof{b}:1→B, \nameof{c}:1→C)$,
but an element of $\ACB$ is a triple $(a,b,c)$...
\bsk
\ColorRed{(I'm omitting the ``obeying certain properties''!)}
\ColorRed{(Why can I do that? Long story...)}
\newpage
% «guessing-nu-2» (to ".guessing-nu-2")
% (excp 48 "guessing-nu-2")
% (exca "guessing-nu-2")
{\bf Guessing $ν$: second attempt}
\ssk
...so let's try to guess $ν$, $g$, $h$ by finding their types,
then finding natural constructions that yield
terms of those types, and then checking if
our guesses behave as expected...
\newpage
% «guessing-nu-2-diag» (to ".guessing-nu-2-diag")
% (excp 49 "guessing-nu-2-diag")
% (exca "guessing-nu-2-diag")
% (cwmp 14 "creation-of-limits")
% (cwm "creation-of-limits")
%D diagram nu-attempt-2-1
%D 2Dx 100 +40 +35
%D 2D 100 C0 A0 - A1
%D 2D | | |
%D 2D +25 | A2 - A3
%D 2D | |
%D 2D +25 C1 A4
%D 2D
%D 2D +15 C2 B0 - B1
%D 2D
%D ren A0 A1 ==> Δ1 1
%D ren A2 A3 ==> ΔL L
%D ren A4 ==> F
%D ren B0 B1 ==> \Set^\catJ \Set
%D ren C0 C1 C2 ==> 1 FJ \Set
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l Δg
%D A1 A3 -> .plabel= r \sm{∃!g\phantom{ooo}\\:=λ*.ℓ}
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l \sm{ν:=\\λJ.λℓ.ℓJ*}\!\! # \sm{ν\\\text{(univ)}}
%D A0 A4 -> .slide= -40pt .plabel= l ∀ℓ
%D
%D newnode: A3R at: @A3+v(28,0) .TeX= =\Hom(Δ1,F) place
%D
%D B0 B1 <- sl^ .plabel= a Δ
%D B0 B1 -> sl_ .plabel= b \Lim
%D
%D C0 C1 -> .plabel= l ℓJ C2 place
%D ))
%D enddiagram
%D
%D diagram nu-attempt-2-X
%D 2Dx 100 +40 +35
%D 2D 100 C0 A0 - A1
%D 2D | | |
%D 2D +25 | A2 - A3
%D 2D | |
%D 2D +25 C1 A4
%D 2D
%D 2D +15 C2 B0 - B1
%D 2D
%D ren A0 A1 ==> ΔX ∀X
%D ren A2 A3 ==> ΔL L
%D ren A4 ==> F
%D ren B0 B1 ==> \Set^\catJ \Set
%D ren C0 C1 C2 ==> X FJ \Set
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l Δh
%D A1 A3 -> .plabel= r \sm{∃!h\phantom{oooooooooooo}\\:=λx.λJ.λ*.TJx}
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l \sm{ν:=\\λJ.λℓ.ℓJ*\\\text{(univ)}}
%D A0 A4 -> .slide= -40pt .plabel= l ∀T
%D
%D newnode: A3R at: @A3+v(28,0) .TeX= =\Hom(Δ1,F) place
%D
%D B0 B1 <- sl^ .plabel= a Δ
%D B0 B1 -> sl_ .plabel= b \Lim
%D
%D C0 C1 -> .plabel= l TJ C2 place
%D ))
%D enddiagram
%D
$\pu
\scalebox{0.60}{$
\begin{array}{r}
\diag{nu-attempt-2-1}
\\ \\ \\
\diag{nu-attempt-2-X}
\end{array}
\qquad
\begin{array}{l}
\begin{array}[t]{rcl}
ℓ &:& Δ1 → F \\
ℓJ &:& Δ1J → FJ \\
ℓJ &:& 1 → FJ \\
ℓJ* &∈& FJ \\[5pt]
ν &:& ΔL → F \\
νJ &:& ΔLJ → FJ \\
νJ &:& L → FJ \\
νJℓ &∈& FJ \\[5pt]
g &:& 1 \to L \\
g* &∈& L \\
\end{array}
\quad
\begin{array}[t]{rcl}
T &:& ΔX → F \\
TJ &:& ΔXJ → FJ \\
TJ &:& X → FJ \\
TJx &∈& FJ \\[5pt]
h &:& X → L \\
hx &∈& L \\
hx &:& Δ1 → F \\
hxJ &:& Δ1J → FJ \\
hxJ &:& 1 → FJ \\
hxJ* &∈& FJ \\[5pt]
\end{array}
\\
\\
\text{Let's try this:} \\ %[5pt]
\def\IE{\hspace{-0.75em}⇒}
\begin{array}[t]{rcll}
νJℓ &=& ℓJ* & \IE \\
νJ &=& λℓ.ℓJ* & \IE \\
ν &:=& λJ.λℓ.ℓJ* & \\[5pt]
g* &=& ℓ & \IE \\
g &:=& λ*.ℓ & \\[5pt]
hxJ* &=& TJx & \IE \\
hxJ &=& λ*.TJx & \IE \\
hx &=& λJ.λ*.TJx & \IE \\
h &:=& λx.λJ.λ*.TJx \\
\end{array}
\end{array}
$}
$
% \newpage
% (find-LATEX "catsem-slides.bib")
% \cite{Riehl}
% (find-books "__comp/__comp.el" "pierce")
% (find-taplpage (+ 22 315) "V Polymorphism")
% (find-taplpage (+ 22 317) "22 Type Reconstruction")
% (find-tapltext (+ 22 317) "22 Type Reconstruction")
% (find-taplpage (+ 22 317) "22.1 Type Variables and Substitutions")
% (find-taplpage (+ 22 319) "22.2 Two Views of Type Variables")
% (find-taplpage (+ 22 321) "22.3 Constraint-Based Typing")
% (find-taplpage (+ 22 326) "22.4 Unification")
% (find-taplpage (+ 22 329) "22.5 Principal Types")
% (find-taplpage (+ 22 330) "22.6 Implicit Type Annotations")
% (find-taplpage (+ 22 331) "22.7 Let-Polymorphism")
% (find-taplpage (+ 22 336) "22.8 Notes")
% http://angg.twu.net/2018.2-MD.html
% http://angg.twu.net/2018.2-MD/20180813_lista_1.pdf
% http://angg.twu.net/2018.2-MD/20180813_lista_2.pdf
% (favp 39 "ness")
% (fav "ness")
\newpage
\printbibliography
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% <make>
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2021excuse veryclean
make -f 2019.mk STEM=2021excuse pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "exc"
% End: