|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2020seelylccc.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020seelylccc.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2020seelylccc.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020seelylccc.pdf"))
% (defun e () (interactive) (find-LATEX "2020seelylccc.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020seelylccc"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page "~/LATEX/2020seelylccc.pdf")
% (find-sh0 "cp -v ~/LATEX/2020seelylccc.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2020seelylccc.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2020seelylccc.pdf
% file:///tmp/2020seelylccc.pdf
% file:///tmp/pen/2020seelylccc.pdf
% http://angg.twu.net/LATEX/2020seelylccc.pdf
% (find-LATEX "2019.mk")
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\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")
%
\DeclareFontFamily{U}{matha}{\hyphenchar\font45}
\DeclareFontShape{U}{matha}{m}{n}{
<5> <6> <7> <8> <9> <10> gen * matha
<10.95> matha10 <12> <14.4> <17.28> <20.74> <24.88> matha12
}{}
\DeclareSymbolFont{matha}{U}{matha}{m}{n}
\DeclareMathSymbol{\thinsubset}{3}{matha}{"80}
\DeclareMathSymbol{\thinsupset}{3}{matha}{"81}
\def\limp{\thinsupset} % See: (find-es "tex" "limp-abx")
%
% (find-es "tex" "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
% (find-LATEX "2020hyp.tex" "limp-2020")
% \def\limpbody{%
% \begin{picture}%(4,2)
% (5.1,2.5)(-0.5,-0.25)
% \Line(0,0)(3,0)
% \Line(0,2)(3,2)
% \put(3,1){\arc[-90,90]{1}}
% \end{picture}%
% }
% \def\limp{%
% \mathrel{\vcenter{\hbox{%
% \unitlength=2pt%
% \linethickness{0.4pt}%
% \limpbody%
% }}}}
\catcode`⊸=13 \def⊸{\limp}
{\setlength{\parindent}{0em}
\footnotesize
Notes on [Seely84], a.k.a.:
``Locally cartesian closed categories and type theory'', available at:
\url{http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf}
\ssk
These notes are at:
\url{http://angg.twu.net/LATEX/2020seelylccc.pdf}
}
\section*{1. The type theory ML}
% (find-books "__cats/__cats.el" "seely-lccc")
% (find-seelylcccpage (+ -32 33) "1. The type theory ML")
% (find-seelylccctext (+ -32 33) "1. The type theory ML")
% (find-seelylcccpage (+ -32 34) "Type formation rules")
% (find-seelylccctext (+ -32 34) "Type formation rules")
1.1.1. Type formation rules. The following are to be types:
(i) If $F$ is a type-valued function constant, and $a_1, ... ,
a_n$ are terms of the appropriate types, then $F(a_1, ..., a_n)$ is a
type.
(ii) 1 is a type.
(iii) If $a, b ∈ A$, then $I(a, b)$ is a type.
(iv) If $A,B[x]$ are types, $x∈A$, where $x,B$ satisfy the c.o.v.,
then $Π_{x∈A}B[x]$ and $Σ_{x∈A} B[x]$ are types. If $x$ does not in
fact occur in $B$, these are written $A ⊸ B$ and $A×B$ respectively.
\msk
% 1.1.2. Term formation rules. The following are to be terms of the
% indicated types:
%
% (vbl) For each type $A$, there are variables $x∈A$; (such $x$ could
% also be denoted $x_A$, if the type of x is not clear from the
% context.)
%
% (fen) If / is a term-valued function constant, and a1)...,an are terms of the
% appropriate types, then f(av..., an) is a term of the appropriate type.
%
% (II) * e 1 .
%
% (III) If t[x]eB[x], where xA,t (and a;^,.B) satisfy the c.o.v., then
%
%
% (also written AxA t[x] e HxA B[x]).
% (TIE) IffeYlxAB[x], aeA, thenf(a)eB[a].
% (El) If aeA,beB[a], then <a,b}e'LxeAB[x'].
% (SE) If ce'LxeAB[x], then7r(c)e4, 7T'(c)eB[n(c)].
% (=1) If aeA, then r(a)el{a, a).
%
% (= E) If a,beA, cel(a,b), deC[a,a,r(a)], where C[x,y,z] is a type depending on
% x,yeA, zeI(x,y), then a(d)[a,b,c]eC[a,b,c].
% 1-1-3. Equality rules. Using the notation of § 1-1-2, we have the following equations:
% (f eq) Any imposed equations on function constants induce the obvious equations.
% (lred) If<el,then< = *.
% (Tired) (*xeAt[x])(a) = t[a].
% (UexV)f=AxeAf(x).
% (S red) n«a,b)) = a; n'((a,b)) = b.
% (Sexp) c = (n(c),n'(c)y.
% (= red) cr(d) [a, a, r(a)] = d.
% (= exp) If/[a, b, c] e C[a, b, c], then/ = <r(f[a, a, r(a)]) [a, b, c].
% (I rule) If a[x], b[x]eA, t[x]el(a[x], b[x]), then a[x] = b[x], and t[x] = r(a[x]).
% Furthermore, an ML theory may have axioms of the form S = T for types S, T. (We
% suppose similar axioms for terms are given by function constants of the appropriate
% I-type.)
% Finally, we have the usual rules for = : for types or terms o, b, c (as appropriate):
% If a = b then c[a] = c[b]. If a -- b then b = a.
% If a = b and b = c, then a = c. a = a.
% If cea and a = b, then ce6. If aec and a = b, then 6ec.
% (hypp 7 "bcc-seely-lccc")
% (hyp "bcc-seely-lccc")
% (find-books "__cats/__cats.el" "seely-lccc")
% (find-seelylcccpage (+ -32 37) "(iv) P satisfies the Beck condition:")
% (find-seelylccctext (+ -32 37) "(iv) P satisfies the Beck condition:")
% (find-TH "dednat6" "a-big-example")
% (find-dednat6 "tug-slides.tex" "BCC")
{\bf BCC in the SeelyLCCC paper}
\def\BCCL{\mathsf{BCCL}}
%D diagram BCC-Seely-LCCC-1
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <====================== B1
%D 2D -\\ -\\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\> B2' ============== B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 A0 |---------------------> A1
%D 2D |-> |->
%D 2D +35 A2 |--------------------> A3
%D 2D
%D ((
%D B0 .tex= h^*φ B1 .tex= φ
%D B2 .tex= k^*f^*Σ_gφ B3 .tex= g^*Σ_gφ
%D B2' .tex= h^*g^*Σ_gφ
%D B4 .tex= Σ_kh^*φ B5 .tex= Σ_gφ
%D B6 .tex= f^*Σ_gφ B7 .tex= Σ_gφ
%D B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D B0 B4 |-> B1 B5 |->
%D B2 B6 <-| B3 B7 <-|
%D B6 B7 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r \BCCL
%D B0 B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( A0 .tex= D A1 .tex= C A2 .tex= A A3 .tex= B
%D A0 A1 -> .plabel= b h
%D A0 A2 -> .plabel= l k
%D A1 A3 -> .plabel= r g
%D A2 A3 -> .plabel= a f
%D A0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\pu
\diag{BCC-Seely-LCCC-1}
$$
\newpage
{\bf BCC in the SeelyLCCC paper (2)}
%D diagram BCC-Seely-LCCC-my
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <====================== B1
%D 2D -\\ -\\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\> B2' ============== B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 A0 |---------------------> A1
%D 2D |-> |->
%D 2D +35 A2 |--------------------> A3
%D 2D
%D ((
%D B0 .tex= h^*φ B1 .tex= φ
%D B2 .tex= k^*f^*Σ_gφ B3 .tex= g^*Σ_gφ
%D B2' .tex= h^*g^*Σ_gφ
%D B4 .tex= Σ_kh^*φ B5 .tex= Σ_gφ
%D B6 .tex= f^*Σ_gφ B7 .tex= Σ_gφ
%D
%D B0 .tex= \bsm{x\\b,a,c} B1 .tex= \bsm{x\\b,c}
%D B2 .tex= \bsm{c,x\\b,a,c} B3 .tex= \bsm{c,x\\b,c}
%D B2' .tex= \bsm{c,x\\b,a,c}
%D B4 .tex= \bsm{c,x\\b,a} B5 .tex= \bsm{c,x\\b}
%D B6 .tex= \bsm{c,x\\b,a} B7 .tex= \bsm{c,x\\b}
%D
%D B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D B0 B4 |-> B1 B5 |->
%D B2 B6 <-| B3 B7 <-|
%D B6 B7 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r \BCCL
%D B0 B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( A0 .tex= D A1 .tex= C A2 .tex= A A3 .tex= B
%D A0 .tex= [b,a,c] A1 .tex= [b,c] A2 .tex= [b,a] A3 .tex= [b]
%D A0 A1 -> .plabel= b h
%D A0 A2 -> .plabel= l k
%D A1 A3 -> .plabel= r g
%D A2 A3 -> .plabel= a f
%D A0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\pu
\scalebox{0.9}{$
\diag{BCC-Seely-LCCC-my}
$}
$$
\newpage
{\bf BCC in the SeelyLCCC paper (2)}
% (nmop 2 "components")
% (nmo "components")
%:
%: φ
%: ----
%: Σ_gφ
%: -------------
%: \id:Σ_gφ→Σ_gφ φ
%: ----------------- ------------- ----
%: η=\id^♯:φ→g^*Σ_gφ h^*g^*≅k^*f^* Σ_gφ
%: -------------------- -----------------------
%: h^*η:h^*φ→h^*g^*Σ_gφ α:h^*g^*Σ_gφ→k^*f^*Σ_gφ
%: -----------------------------------------------
%: α∘h^*η:h^*φ→k^*f^*Σ_gφ
%: ----------------------------
%: ♮=(α∘h^*η)^♭:Σ_kh^*φ→f^*Σ_gφ
%:
%: ^BCC-Seely-LCCC-1
%:
$$\pu
\ded{BCC-Seely-LCCC-1}
$$
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "slc"
% End: