|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% Logic and Categories
% (Minicourse slides)
% For UniLog 2015, Istanbul
% By Eduardo Ochs
% (find-angg "LATEX/2014istanbul-a.tex")
% (find-xpdfpage "~/LATEX/2014istanbul-a.pdf")
% http://www.uni-log.org/start5.html
% http://www.uni-log.org/tutorials5.html
% http://www.uni-log.org/t5-cat.html
% (find-TH "tmp")
% (find-angg "LATEX/2015logicandcats.tex")
% (find-angg "LATEX/2015logicandcats.lua")
% (defun c () (interactive) (find-LATEXsh "lualatex 2015logicandcats.tex"))
% (defun c () (interactive) (find-LATEXsh "lualatex --output-format=dvi 2015logicandcats.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2015logicandcats.pdf"))
% (defun d () (interactive) (find-xdvipage "~/LATEX/2015logicandcats.dvi"))
% (defun e () (interactive) (find-LATEX "2015logicandcats.tex"))
% (defun l () (interactive) (find-LATEX "2015logicandcats.lua"))
% (find-xpdfpage "~/LATEX/2015logicandcats.pdf")
% (find-xdvipage "~/LATEX/2015logicandcats.dvi")
\documentclass[oneside,landscape]{article}
\usepackage[utf8]{inputenc}
% (find-angg ".emacs.papers" "latexgeom")
%\usepackage[%total={6.5in,4in},
% textwidth=4in, paperwidth=4.5in, textheight=5in, paperheight=4.5in,
% top=0.05in, left=0.2in]{geometry}
\usepackage[a4paper, landscape]{geometry}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
% \usepackage{tikz}
\usepackage{luacode}
% (find-dn5file "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 istanbuldefs % (find-ist "defs.tex")
\begin{document}
% (find-angg "LATEX/2014istanbul-a.tex")
% (find-xpdfpage "~/LATEX/2014istanbul-a.pdf")
\input edrxrepl % (find-LATEX "edrxrepl.tex")
\catcode`\^^J=10 % (find-es "luatex" "spurious-omega")
\directlua{dofile "\jobname.lua"} % (find-LATEX "2015logicandcats.lua")
\directlua{dofile "istanbulall.lua"} % (find-ist "all.lua")
\directlua{getword = getword_utf8} % (find-dn5 "dednat6.lua" "utf8")
% \directlua{dofile "/home/edrx/LUA/picture.lua"} % (find-angg "LUA/picture.lua")
% (find-angg "LUA/picture.lua" "getrect")
% (find-dn5 "tests/6a.tex")
\directlua{tf = TexFile.read(tex.jobname..".tex")}
\directlua{output = print}
\directlua{output = tex.print}
\directlua{output = printboth}
\directlua{output = mytexprint}
%L output(preamble1)
\directlua{tf:processuntil()}
\def\pu{\directlua{tf:processuntil()}}
\def\Diag#1{\directlua{tf:processuntil()}\diag{#1}}
\def\Ded #1{\directlua{tf:processuntil()}\ded{#1}}
\def\Exec#1{\directlua{tf:processuntil() #1}}
\def\Expr#1{\directlua{tf:processuntil() output(#1)}}
\def\Expr#1{\directlua{tf:processuntil() output(tostring(#1))}}
%
% (find-LATEX "2015logicandcats.lua" "processzrect")
\def\processzrect#1{\directlua{tf:processuntil() processzrect"#1 out"}}
\def\zr#1{\processzrect{#1}}
% (find-es "tex" "underbrace")
%:*|->*\mapsto *
%L forths["<="] = function () pusharrow("<=") end
\def\ang#1{\langle #1 \rangle}
A diagram:
%
%D diagram foo
%D 2Dx 100 +20
%D 2D 100 a,b <=== a
%D 2D - -
%D 2D | <-> |
%D 2D v v
%D 2D +20 c ==> b|->c
%D 2D
%D (( a,b a c b|->c
%D @ 0 @ 1 <=
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 3 =>
%D ))
%D enddiagram
%D
$$\Diag{foo}$$
%L print("hello")
A tree:
%:
%:*a*(a)*
%:*abc*(abc)*
%:
%: 1 2 3
%: =======
%: 1+2+3
%: --------ababc
%: f(1+2+3)
%:
%: ^f(1+2+3)
%:
$$\Ded{f(1+2+3)}$$
\directlua{output = printboth}
%:*"* *
%: HA rules:
%:
%: P∧Q≤R
%: -----π -----π' -----♯
%: Q∧R≤Q Q∧R≤R P≤Q{→}R
%:
%: ^P-pi ^P-pi' ^P-sharp
%:
%: P≤Q P≤R P≤Q{→}R
%: ---! --------\ang{,} -----♭
%: P≤⊤ P≤Q∧R P∧Q≤R
%:
%: ^P-T ^P-ang ^P-flat
%:
%:
%: -----ι -----ι'
%: P≤P∨Q Q≤P∨Q
%:
%: ^P-iota ^P-iota'
%:
%: P≤R Q≤R
%: ---¡ --------[,]
%: ⊥≤P P∨Q≤R
%:
%: ^P-F ^P-[,]
%:
%: CCC rules:
%: f:A×B→C
%: -------π --------π' -----------♯
%: π:B×C→B π':B×C→C f^♯:A→B{→}C
%:
%: ^F-pi ^F-pi' ^F-sharp
%:
%: f:A→B g:A→C g:A→B{→}C
%: ------¡ ---------------\ang{,} ---------♭
%: !:A→1 \ang{f,g}:A→B×C g^♭:A×B→C
%:
%: ^F-T ^F-ang ^F-flat
%:
%: -------ι --------ι'
%: ι:A→A+B ι':B→A+B
%:
%: ^F-iota ^F-iota'
%:
%: f:A→B g:A→C
%: ------¡ ---------------\ang{,}
%: ¡:0→A \ang{f,g}:A→B×C
%:
%: ^F-F ^F-[,]
%:
\def\mat#1{\begin{matrix}#1\end{matrix}}
\pu
\def\BiCCCrules{{
\def\PT {\ded{P-T}}
\def\PPA{\ded{P-pi}}
\def\PPB{\ded{P-pi'}}
\def\PPC{\ded{P-ang}}
\def\PEA{\ded{P-sharp}}
\def\PEB{\ded{P-flat}}
\def\PF {\ded{P-F}}
\def\PCA{\ded{P-iota}}
\def\PCB{\ded{P-iota'}}
\def\PCC{\ded{P-[,]}}
\mat{ & \PPA \qquad \PPB & \PEA \\\\
\PT & \PPC & \PEB \\\\
& \PCA \qquad \PCB & \\\\
\PF & \PCC &
}
}}
\def\BiHArules{{
\def\PT {\ded{F-T}}
\def\PPA{\ded{F-pi}}
\def\PPB{\ded{F-pi'}}
\def\PPC{\ded{F-ang}}
\def\PEA{\ded{F-sharp}}
\def\PEB{\ded{F-flat}}
\def\PF {\ded{F-F}}
\def\PCA{\ded{F-iota}}
\def\PCB{\ded{F-iota'}}
\def\PCC{\ded{F-[,]}}
\mat{ & \PPA \qquad \PPB & \PEA \\\\
\PT & \PPC & \PEB \\\\
& \PCA \qquad \PCB & \\\\
\PF & \PCC &
}
}}
% (find-854 "" "more-on-wd" "is a tuple:")
% (find-854 "" "dn-functors" "fcded")
% (find-854page 27 "dn-functors")
% (find-854page 87 "is a tuple:")
\newpage
% (find-dn4 "dednat4.lua" "lplacement")
%L forths[".PLABEL="] = function ()
%L ds[1].lplacement = getword()
%L ds[1].label = getword()
%L end
%D diagram BiHAdiag
%D 2Dx 100 +15 +25 +25 +15 +25
%D 2D 100 T1 PB <- PBC -> PC EC |--> EB->C
%D 2D ^ ^ ^ ^ ^ ^
%D 2D | \ | / | |
%D 2D +25 TA PA EAxB <-| EA
%D 2D
%D 2D +15 IA CC
%D 2D ^ ^ ^ ^
%D 2D | / | \
%D 2D +25 I0 CA -> CAB <- CB
%D 2D
%D (( T1 .tex= ⊤ TA .tex= P
%D @ 0 @ 1 <-
%D ))
%D (( PB .tex= Q PBC .tex= Q∧R PC .tex= R PA .tex= P
%D @ 0 @ 1 <- @ 1 @ 2 ->
%D @ 0 @ 3 <- @ 1 @ 3 <- @ 2 @ 3 <-
%D ))
%D (( EC .tex= R EB->C .tex= Q{→}R EAxB .tex= P∧Q EA .tex= P
%D @ 0 @ 1 |->
%D @ 0 @ 2 <- @ 1 @ 3 <-
%D @ 2 @ 3 <-|
%D ))
%D (( IA .tex= P I0 .tex= ⊥
%D @ 0 @ 1 <-
%D ))
%D (( CC .tex= R CA .tex= P CAB .tex= P∨Q CB .tex= Q
%D @ 0 @ 1 <- @ 0 @ 2 <- @ 0 @ 3 <-
%D @ 1 @ 2 -> @ 2 @ 3 <-
%D ))
%D enddiagram
%D
%D diagram BiCCCdiag
%D 2Dx 100 +15 +25 +25 +15 +25
%D 2D 100 T1 PB <- PBC -> PC EC |--> EB->C
%D 2D ^ ^ ^ ^ ^ ^
%D 2D | \ | / | |
%D 2D +25 TA PA EAxB <-| EA
%D 2D
%D 2D +15 IA CC
%D 2D ^ ^ ^ ^
%D 2D | / | \
%D 2D +25 I0 CA -> CAB <- CB
%D 2D
%D (( T1 .tex= 1 TA .tex= A
%D @ 0 @ 1 <- .plabel= l !
%D ))
%D (( PB .tex= B PBC .tex= B{×}C PC .tex= C PA .tex= A
%D @ 0 @ 1 <- .plabel= a π @ 1 @ 2 -> .plabel= a π'
%D @ 0 @ 3 <- .plabel= l f @ 2 @ 3 <- .plabel= r g
%D @ 1 @ 3 <- .plabel= m <f,g>
%D ))
%D (( EC .tex= C EB->C .tex= B{→}C EAxB .tex= A{×}B EA .tex= A
%D @ 0 @ 1 |-> .plabel= a (B{→})
%D @ 0 @ 2 <- .plabel= l \sm{f\\g^♭}
%D @ 1 @ 3 <- .plabel= r \sm{f^♯\\g}
%D @ 2 @ 3 <-| .plabel= r (×B)
%D @ 0 @ 3 harrownodes nil 20 nil |-> sl^
%D @ 0 @ 3 harrownodes nil 20 nil <-| sl_
%D # @ 0 @ 2 <- .PLABEL= _(0.43) g^\flat
%D # @ 0 @ 2 <- .PLABEL= _(0.57) f
%D # @ 1 @ 3 <- .PLABEL= ^(0.43) g
%D # @ 1 @ 3 <- .PLABEL= ^(0.57) f^\sharp
%D ))
%D (( IA .tex= A I0 .tex= 0
%D @ 0 @ 1 <- .plabel= l ¡
%D ))
%D (( CC .tex= C CA .tex= A CAB .tex= A{+}B CB .tex= B
%D @ 0 @ 1 <- .plabel= l f @ 0 @ 3 <- .plabel= r g
%D @ 0 @ 2 <- .plabel= m [f,g]
%D @ 1 @ 2 -> .plabel= b ι @ 2 @ 3 <- .plabel= b ι'
%D ))
%D enddiagram
%D
\pu
\def\BiHAeqs{
\begin{array}{rl}
(id) & ∀P.(P≤P) \\
(comp) & ∀P,Q,R.(P≤Q)∧(Q≤R)→(P≤R) \\
\\
(⊤) & ∀P.(P≤⊤) \\
(⊥) & ∀P.(⊥≤P) \\
(∧) & ∀P,Q,R.(P≤Q∧R)↔(P≤Q)∧(P≤R) \\
(∨) & ∀P,Q,R.(P∨Q≤R)↔(P≤R)∧(Q≤R) \\
(→) & ∀P,Q,R.(P≤Q→R)↔(P∧Q≤R) \\
\\
(¬) & ¬P := P→⊥ \\
(↔) & P↔Q := (P→Q)∧(Q→P) \\
\end{array}
}
% $$\diag{BiHAdiag}$$
% $$\diag{BiCCCdiag}$$
$$\mat{
& \BiHAeqs \\\\
\diag{BiHAdiag} & \BiCCCrules \\\\
\diag{BiCCCdiag} & \BiHArules \\
}
$$
% (find-854file "")
% (find-854page 2)
% (find-854 "" "adjunctions")
% (find-854page 28 "adjunctions")
% $\ang{f,g}$
% \enddocument
% (find-es "tex" "resizebox")
% \resizebox{10cm}!{Hello}
%\savebox{\myboxa}{$\Diag{foo}$}
%\usebox{\myboxa}
%R a := 2/ 11 \ b := 1/a b c \foo
%R |10 01| | d e f|
%R \ 00 / \ g /
%R
%R c := 2/ 23 \bar
%R | 22 13
%R | 12 03
%R | 11 02
%R |10 01
%R \ 00
%R
%R d := 2/ 54 \ D := 2/ aa \
%R |53 44 |bb cc
%R | 43 34 | dd ee
%R | 33 \ ff
%R | ab
%R | 22 cd
%R | 21 12
%R |20 11
%R | 10
%R \ 00
%R
%
% (find-dn5 "heads6.lua" "zrect-head")
% \directlua{PP(zrects.a)}
\directlua{tf:processuntil()}
\directlua{PP(zrects.a)}
% \directlua{print(zrects.a)}
% \directlua{tf:processuntil() print(zrects.a)}
hey $\zr{a 12pt}$ you
hey $\zr{a 10pt ()}$ you
hey $\zr{a foot 7pt ()}$ you
8: $\zr{a 8pt bul}$
6: $\zr{a 6pt bul}$
4: $\zr{a 4pt bul}$
xy: $\zr{c 14pt (x,y), {}}$
Xy: $\zr{c 14pt (X,y), {}}$
lr: $\zr{c 14pt (l,r), {}}$
bord: $\zr{d 10pt bord}$
bord: $\zr{d 10pt}$
cuts: $\zr{d 10pt lcuts:02 bord}$
% \directlua{print(zrects.d)}
% Test ``cell'':
% $
% \def\cell#1{\hbox to 0pt{\hss \footnotesize#1\hss}}
% \def\cell#1{\raise 1.5pt\hbox to 0pt{\hss \footnotesize#1\hss}}
% \left({\unitlength=7pt
% \lower1\unitlength\hbox{\begin{picture}(3,3)(-1.5,0)
% \put(0,0){\cell{11}}
% \put(1,1){\cell{01}}
% \put(-1,1){\cell{10}}
% \put(0,2){\cell{00}}
% \put(0,-0.5){\line(1,1){2}}
% \put(0,-0.5){\line(-1,1){2}}
% \put(0,3.5){\line(1,-1){2}}
% \put(0,3.5){\line(-1,-1){2}}
% \end{picture}
% }}\right)
% $
Cuts:
{\unitlength=10pt
\lower4.5\unitlength\hbox{\begin{picture}(5,10)(-2.5,0)
\put(0,0){\hbox to 0pt{\hss 00\hss}}
\put(-1,1){\hbox to 0pt{\hss 10\hss}}
\put(0,2){\hbox to 0pt{\hss 11\hss}}
\put(1,3){\hbox to 0pt{\hss 12\hss}}
\put(2,4){\hbox to 0pt{\hss 13\hss}}
\put(-2,2){\hbox to 0pt{\hss 20\hss}}
\put(-1,3){\hbox to 0pt{\hss 21\hss}}
\put(0,4){\hbox to 0pt{\hss 22\hss}}
\put(1,5){\hbox to 0pt{\hss 23\hss}}
\put(0,6){\hbox to 0pt{\hss 33\hss}}
\put(1,7){\hbox to 0pt{\hss 34\hss}}
\put(-1,7){\hbox to 0pt{\hss 43\hss}}
\put(0,8){\hbox to 0pt{\hss 44\hss}}
\put(-2,8){\hbox to 0pt{\hss 53\hss}}
\put(-1,9){\hbox to 0pt{\hss 54\hss}}
\put(-1,0){\line(1,1){1}}
\put(-2,1){\line(1,1){4}}
\put(2,3){\line(-1,1){2}}
\put(1,6){\line(-1,1){3}}
\end{picture}
}}
\newpage
{\basicttchars
%\footnotesize
\begin{verbatim}
For Alice, Classical Propositional Logic is this,
(Ω,⊤,⊥,∧,∨,→,¬,↔) =
({0,1}, 1, 0, {(0,0)↦0, {(0,0)↦0, {(0,0)↦1, {0↦1, {(0,0)↦1, }
(0,1)↦0, (0,1)↦1, (0,1)↦1, 1↦0}, (0,1)↦0,
(1,0)↦0, (1,0)↦1, (1,0)↦0, (1,0)↦0,
(1,1)↦1 }, (1,1)↦1 }, (1,1)↦1 }, (1,1)↦1 }
In Bob's book, Classical Propositional Logic is
(Ω,⊤,∧,¬) = ...
\end{verbatim}
}
\newpage
$$
\underbrace{
\underbrace{
\neg (\underbrace{
\underbrace{
P
}_{10} \&
\underbrace{
Q
}_{01}
}_{00})
}_{32} \to
(\underbrace{
\underbrace{
\neg \underbrace{
P
}_{10}
}_{02} \lor
\underbrace{
\neg \underbrace{
Q
}_{01}
}_{20}
}_{22})
}_{22}
$$
$$
\left\{
\sm{
(1,3)\mto 1 \\
(0,2)\mto 2 \\
(2,2)\mto 3 \\
(1,1)\mto 4 \\
(1,0)\mto 5 \\
}
\right\}
%
\quad
%
\csm{ (1,3)\mto1 \\
(0,2)\mto2 \quad (2,2)\mto3 \\
(1,1)\mto4 \\
(1,0)\mto5 }
%
\quad
%
\csm{ ((1,3),1), \\
((0,2),2), \quad ((2,2),3), \\
((1,1),4), \\
((1,0),5) }
$$
%L myfoo = "barbar"
\Expr{myfoo}
% (find-ist "all.lua" "ubs-tests")
%L ubs_DeMorgan = ubs [[
%L P 10 u Q 01 u \& bin 00 u () \neg pre 32 u
%L P 10 u \neg pre 02 u Q 01 u \neg pre 20 u \lor bin 22 u ()
%L \to bin 22 u
%L ]]
$$\Expr{ubs_DeMorgan}$$
%R
%R a := 1/ · \ b := 2/ 21 \ c := 1/ 0 \
%R | · · | | 21 21 | | 0 0 |
%R | · · → | | 21 21 11 | | 0 0 1 |
%R |· Q R ·| |20 21 11 01| |0 0 1 1|
%R | · ∧ · | | 20 10 01 | | 0 1 1 |
%R | · · | | 10 01 | | 1 1 |
%R \ · / \ 00 / \ 1 /
%R
\def\ra{\zr{a 10pt}}
\def\rb{\zr{b 10pt}}
\def\rc{\zr{c 10pt}}
% \ra \rb \rc
% raise(cell(dollar(contents)))
\end{document}
-- Local Variables:
-- coding: utf-8-unix
-- End: