% 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:
