% (find-angg "LATEX/istanbul-handouts.tex")
% (find-angg "LATEX/istanbul-handouts.lua")
% (defun c () (interactive) (find-LATEXsh "lualatex istanbul-handouts.tex"))
% (defun c () (interactive) (find-LATEXsh "lualatex --output-format=dvi istanbul-handouts.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/istanbul-handouts.pdf"))
% (defun d () (interactive) (find-xdvipage "~/LATEX/istanbul-handouts.dvi"))
% (defun e () (interactive) (find-LATEX "istanbul-handouts.tex"))
% (defun l () (interactive) (find-LATEX "istanbul-handouts.lua"))
% (find-xpdfpage "~/LATEX/istanbul-handouts.pdf")
% (find-xdvipage "~/LATEX/istanbul-handouts.dvi")

% «.mixedpicture-tests»	(to "mixedpicture-tests")
% «.sandwich»		(to "sandwich")
% «.J-and-connectives»	(to "J-and-connectives")
% «.J-proofs»		(to "J-proofs")
% «.HAs-and-CCCs»	(to "HAs-and-CCCs")
% «.brute-force»	(to "brute-force")

\documentclass[oneside]{book}
% (find-angg ".emacs.papers" "latexgeom")
\usepackage[a4paper, landscape, top=1cm, left=1cm]{geometry} 
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{tikz}
\usepackage{luacode}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
% (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}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

\directlua{dofile "2015logicandcats.lua"} % (find-LATEX "2015logicandcats.lua")
\directlua{dofile "istanbulall.lua"}      % (find-ist "all.lua")

% NEW:
%
%L deletecomments1 = function (line)
%L     return line:match"^([^%%]*)"
%L   end
%L deletecomments = function (bigstr)
%L     return (bigstr:gsub("([^\n]+)", deletecomments1))
%L   end

% OLD:
%
% %\input edrxrepl                     % (find-LATEX "edrxrepl.tex")
% \catcode`\^^J=10                     % (find-es "luatex" "spurious-omega")
% %\directlua{dofile "\jobname.lua"}   % (find-LATEX "2015logicandcats.lua")
% \directlua{dofile "2015logicandcats.lua"}
% \directlua{dofile "istanbulall.lua"} % (find-ist "all.lua")
% \directlua{getword = getword_utf8}   % (find-dn5 "dednat6.lua" "utf8")
% 
% \directlua{tf = TexFile.read(tex.jobname..".tex")}
% \directlua{output =  printboth}
% \directlua{output = mytexprint}
% \directlua{tf:processuntil()}
% %L output(preamble1)
% \pu


% (find-LATEX "edrx15.sty" "colors")
\edrxcolors
\def\bhbox{\bicolorhbox}

% (find-LATEX "edrx15.sty" "picture-cells")
%$$
% Hello \input /tmp/o.tex % (find-fline "/tmp/o.tex")
% \hbox{\input /tmp/o.tex } % (find-fline "/tmp/o.tex")
%\bhbox{\hbox{\input /tmp/o.tex }} % (find-fline "/tmp/o.tex")
%$$

% (find-angg ".emacs.papers" "texbook")
% (find-texbookpage (+ 12 60) "ex is the \"x-height\" of the current font")
% (find-texbooktext (+ 12 60) "ex is the \"x-height\" of the current font")
% (find-texbookpage (+ 12 151) "$\\vcenter{...}$")
% (find-texbooktext (+ 12 151) "$\\vcenter{...}$")


\def\dagHouse#1#2#3#4#5{\left(\bhbox{$\vcenter{\hbox{\unitlength=4pt%
\celllower=2.5pt%
\def\cellfont{\scriptsize}%
\begin{picture}(3,3)(-0.5,-0.5)
  \put(1,2){\cell{#1}}
  \put(0,1){\cell{#2}}
  \put(2,1){\cell{#3}}
  \put(0,0){\cell{#4}}
  \put(2,0){\cell{#5}}
\end{picture}}}$}\right)}

\def\PvSTbullets{\left(\bhbox{$\vcenter{\hbox{\unitlength=3pt%
\celllower=2pt%
\def\cellfont{\scriptsize}%
\begin{picture}(8,10)(-3.5,-0.5)
  \put(-1,9){\cell{\bullet}}
  \put(-2,6){\cell{\bullet}}
  \put(-1,7){\cell{\bullet}}
  \put(0,8){\cell{\bullet}}
  \put(-3,3){\cell{\bullet}}
  \put(-2,4){\cell{\bullet}}
  \put(-1,5){\cell{\bullet}}
  \put(0,6){\cell{\bullet}}
  \put(1,7){\cell{\bullet}}
  \put(-2,2){\cell{\bullet}}
  \put(-1,3){\cell{\bullet}}
  \put(0,4){\cell{\bullet}}
  \put(1,5){\cell{\bullet}}
  \put(2,6){\cell{\bullet}}
  \put(-1,1){\cell{\bullet}}
  \put(0,2){\cell{\bullet}}
  \put(1,3){\cell{\bullet}}
  \put(2,4){\cell{\bullet}}
  \put(3,5){\cell{\bullet}}
  \put(0,0){\cell{\bullet}}
  \put(1,1){\cell{\bullet}}
  \put(2,2){\cell{\bullet}}
  \put(3,3){\cell{\bullet}}
  \put(4,4){\cell{\bullet}}
\end{picture}}}$}\right)}

\catcode`\^^O=13 \def{\ensuremath{\bullet}}
% \catcode`=13  \def{\ensuremath{\bullet}}

a$\dagHouse54321 b \dagHouse b \PvSTbullets$c



%L drawpile = function (x, y, dy, A, B, arrow)
%L     local runstr = function (str) print(str) end
%L     local runstr = function (str) dxyrun(str) end
%L     local runf = function (fmt, ...) runstr(format(fmt, ...)) end
%L     runf "(("
%L     A = split(A)
%L     B = B and split(B)
%L     for i=1,#A do
%L       runf("node: %d,%d %s", x, y+dy*(i-1), A[i])
%L       if B then runf(".tex= %s", B[i]) end
%L       if not arrow then runf("place") end
%L     end
%L     if arrow then
%L       for i=1,#A-1 do
%L         runf("%s %s %s", A[i], A[i+1], arrow)
%L       end
%L     end
%L     runf "))"
%L   end


%D diagram piles0
%D 2Dx     100
%D 2D  100
%D 2D
%D 2D  +20
%D 2D
%L drawpile(100, 100, -15, "L1 L2 L3 L4", "1\\_ 2\\_ 3\\_ 4\\_", "<-")
%L drawpile(120, 100, -15, "R1 R2 R3 R4", "\\_1 \\_2 \\_3 \\_4")
%D (( L1 R3 -> R2 L4 <-
%D
%D ))
%D enddiagram
%D
$$\pu a \left(\diag{piles0}\right) b$$






% «mixedpicture-tests» (to ".mixedpicture-tests")
% (find-dn5 "newrect.lua" "MixedPicture-arch-tests")

%L omp = function ()
%L     print(); print("\\"..mp.lp.def..":"); print(mp)
%L     output(mp:tolatex())
%L   end
%L
%L -- (Pv) is *-functorial
%L z = ZHA.fromspec("1234R3L21L")
%L mp = MixedPicture.new({def="PvIsStarFunctorial"}, z)
%L mp:addcuts("c 5432/10 0|12|34")
%L mp:put(v"20", "P"):put(v"30", "P*", "P^*")
%L mp:put(v"11", "Q"):put(v"12", "Q*", "Q^*")
%L mp:put(v"03", "R"):put(v"14", "R*", "R^*")
%L omp()
%L 
%L -- (&R) is *-functorial
%L z = ZHA.fromspec("1234R321")
%L mp = MixedPicture.new({def="andRIsStarFunctorial"}, z)
%L mp:addcuts("c 32/10 01|23|4")
%L mp:put(v"30", "P"):put(v"31", "P*", "P^*")
%L mp:put(v"22", "Q"):put(v"33", "Q*", "Q^*")
%L mp:put(v"04", "R"):put(v"14", "R*", "R^*")
%L omp()
%L 
%L -- The (&*) cube
%L z = ZHA.fromspec("12321")
%L mp = MixedPicture.new({def="andStarCubeArchetypal"}, z)
%L mp:addcuts("c 2/10 01|2")
%L mp:put(v"20", "P"):put(v"21", "P*", "P^*")
%L mp:put(v"02", "Q"):put(v"12", "Q*", "Q^*")
%L omp()
%L 
%L -- The (v*) cube
%L z = ZHA.fromspec("12321L")
%L mp = MixedPicture.new({def="orStarCubeArchetypal"}, z)
%L mp:addcuts("c 21/0 0|12")
%L mp:put(v"10", "P"):put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q"):put(v"02", "Q*", "Q^*")
%L omp()
%L 
%L -- The (->*) cube
%L z = ZHA.fromspec("12321")
%L mp = MixedPicture.new({def="impStarCubeArchetypal"}, z)
%L mp:addcuts("c 2/10 01|2")
%L mp:put(v"10", "P")
%L mp:put(v"00", "Q")
%L omp()

$$
\pu
\PvIsStarFunctorial
\qquad
\andRIsStarFunctorial
\qquad
\andStarCubeArchetypal
\qquad
\orStarCubeArchetypal
\qquad
\impStarCubeArchetypal
$$


%\input /tmp/o.tex % (find-fline "/tmp/o.tex")
%$$a
%  \foo
%  b
%$$




%$$
%{\unitlength=10pt
%\lower2\unitlength\hbox{\begin{picture}(3,5)(1.5,3)
%\put(-1,0){\line(1,1){2}}
%\put(1,2){\line(1,-1){1}}
%\put(0,-1){\line(-1,1){2}}
%\put(-2,1){\line(1,1){2}}
%\put(0,3){\line(-1,1){1}}
%\put(-1,4){\line(1,1){1}}
%\put(0,5){\line(-1,1){2}}
%\put(-2,7){\line(1,1){3}}
%\put(1,10){\line(1,-1){1}}
%\put(2,9){\line(-1,-1){2}}
%\put(0,7){\line(1,-1){4}}
%\put(4,3){\line(-1,-1){4}}
%\end{picture}
%}}
%$$


\newpage




%                      _          _      _     
%  ___  __ _ _ __   __| |_      _(_) ___| |__  
% / __|/ _` | '_ \ / _` \ \ /\ / / |/ __| '_ \ 
% \__ \ (_| | | | | (_| |\ V  V /| | (__| | | |
% |___/\__,_|_| |_|\__,_| \_/\_/ |_|\___|_| |_|
%                                              
% «sandwich» (to ".sandwich")

{\bf The sandwich lemma}

The {\sl sandwich lemma} says that if $P≤Q≤P^*$, then $P=^*Q$:
%:  
%:                                    Q≤P^*                  
%:                                 ----------Mo  ----------M2
%:                        P≤Q      Q^*≤P^{**}    P^{**}=P^*  
%:                      -------Mo  ------------------------  
%:  P≤Q  Q≤P^*          P^*≤Q^*         Q^*≤P^*              
%:  ----------Sa        -----------------------              
%:    P^*=Q^*      :=        P^*=Q^*            
%:
%:    ^sand1                 ^sand2
%:
\pu
$$\ded{sand1} \qquad \ded{sand2}$$

Let's use the notation of closed interval, $[P,R]$, for the set of all
points between $P$ and $R$ (in the partial order $≤$ of the ZHA):
%
$$[P,R] := \setofst{Q∈Ω}{P≤Q≤R}$$

We saw that $Q∈[P,P^*]$ implies $P =^* Q$, which means that all points
in $[P,P^*]$ are ${}^*$-equal, and that the equivalence class $[P]^*$
contains at least the set $[P,P^*]$ -- which is never empty, because
$M1$ tells us that $P≤P^*$, so
%
$$\mat{P≤P  ≤P^* \to P  ∈[P,P^*], \\
       P≤P^*≤P^* \to P^*∈[P,P^*]. \\
}
$$

Let's call a non-empty set of the form $[P,R]$ a {\sl lozenge}, even
though it may inherit some dents from the ambient ZHA, as here:
%
$$[11,33] = (diagram)$$

If $P_1^* = P_2^*$, then the equivalence class $[P_1]^*$ ($= [P_2]^*$)
contains the union of the lozenges $[P_1, P_1^*]$ and $[P_2, P_2^*] =
[P_2, P_1^*]$. If $42^* = 33^* = 14^* = 56$, then
%
$$\mat{
  [42]^* = [33]^* = [14]^* ⊇ \\
  [42,56] ∪ [33,56] ∪ [14,56] \\
  }
$$
%
so each equivalence class $[P]^*$ is a union of lozenges or the form
$[\_, P^*]$; and if $[P_1]^* = \setof{P1, P_2, \ldots, P_n}$ then
$[P_1]^* = [P_1,P_1^*] ∪ [P_2,P_1^*] ∪ \ldots ∪ [P_n,P_1^*]$.

\msk

Let's go back to the example above, where $42^* = 33^* = 14^* = 56$.
We have
%
$$\begin{array}{rcl}
  ((42∧33)∧14)^* &=& \\
  (42∧33)^*∧14^* &=& \\
  (42^*∧33^*)∧14^* &=& \\
  (56∧56)∧56 &=& 56, \\
  \end{array}
$$
%
so $42∧33∧14$ is in the same equivalence class as 42, 33, and 14. We
have $[12, 56] ⊆ [42]^* = [33]^* = [14]^*$, which means this shape:
%
$$(diagram)$$

\newpage

(...)

%:
%:
%:
%:                        P_1^*=P_2^*
%:                       ==============
%:  P_1=^*P_2            P_1^*∧P_2^*=P_1^*
%:  -----------ECC∧      =================M3
%:  P_1∧P_2=^*P_1    :=  (P_1∧P_2)^*=P_1^*
%:
%:  ^Eqcand-1             ^Eqcand-2
%:                                                    ---------M1
%:                                                    P_2≤P_2^*    P_2^*=P_1^*
%:                                       ---------M1  ------------------------
%:                                       P_1≤P_1^*       P_2≤P_1^*
%:                          -----------  -------------------------
%:  P_1=^*P_2               P_1≤P_1∨P_2  P_1∨P_2≤P_1^*
%:  -------------ECC∨       --------------------------Sa
%:  P_1=^*P_1∨P_2      :=   P_1^*=(P_1∨P_2)~*
%:
%:  ^Eqcor-1                ^Eqcor-2
%:
%:
%:                        P^*=Q^*
%:                       ==========
%:  P=^*Q                P^*∧Q^*=P*
%:  -----------ECC∧      ===========M3
%:  P∧Q=^*P          :=  (P∧Q)^*=P^*
%:
%:  ^Eqcand-1             ^Eqcand-2
%:                                    -----M1
%:                                    Q≤Q^*    Q^*=P^*
%:                           -----M1  ----------------
%:                           P≤P^*       Q≤P^*
%:                    -----  -----------------
%:  P=^*Q             P≤P∨Q  P∨Q≤P^*
%:  -------ECC∨      ----------------Sa
%:  P=^*P∨Q      :=   P^*=(P∨Q)~*
%:
%:  ^Eqcor-1          ^Eqcor-2
%:
\pu
$$\begin{array}{rcl}
  \ded{Eqcand-1} &:=& \ded{Eqcand-2} \\\\
  \ded{Eqcor-1}  &:=& \ded{Eqcor-2} \\\\
  \end{array}
$$

% $$\ded{Eqcand-1} \qquad := \qquad \ded{Eqcand-2}$$
% $$\ded{Eqcor-1}  \qquad := \qquad \ded{Eqcor-2}$$



\newpage


%      _ 
%     | |
%  _  | |
% | |_| |
%  \___/ 
%        
% «J-and-connectives» (to ".J-and-connectives")

% (find-istfile "1.org" "P&Q, J(P)&Q, ...")
% (find-LATEX "2008graphs.tex")
% (find-LATEX "2008graphs.tex" "LT-modalities")
% (find-853page  21 "internal-diagram")
% (find-853page  22 "and")

%L forths["="] = function () pusharrow("=") end

%L dxyren = function (li)
%L     local a, b = li:match("^(.*) =+> (.*)$")
%L     local A, B = split(a), split(b)
%L     for i=1,#A do PP(A[i], B[i]); nodes[A[i]].tex = B[i] end
%L   end
%L forths["ren"] = function () dxyren(getrestofline()) end

%D diagram test0
%D 2Dx     100 +30 +30
%D 2D  100     A1    
%D 2D  +25 A2  A3  A4 
%D 2D  +25 A5  A6  A7 
%D 2D  +25     A8     
%D 2D
%D ren     A1      ==>       V_1   
%D ren  A2 A3 A4   ==>   V_2 V_3 V_4
%D ren  A5 A6 A7   ==>   V_5 V_6 V_7
%D ren     A8      ==>       V_8   
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D    A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D    A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%D
%D diagram test1
%D 2Dx     100 +30 +30
%D 2D  100     A1    
%D 2D  +25 A2  A3  A4 
%D 2D  +25 A5  A6  A7 
%D 2D  +25     A8     
%D 2D
%D ren     A1      ==>            (P^*∧Q^*)^*
%D ren  A2 A3 A4   ==>  (P∧Q^*)^* P^*∧Q^*  (P^*∧Q)^*
%D ren  A5 A6 A7   ==>   P∧Q^*     (P∧Q)^*  P^*∧Q   
%D ren     A8      ==>              P∧Q               
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D    A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D    A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%D
%D diagram test2
%D 2Dx     100 +30 +30
%D 2D  100     A1    
%D 2D  +25 A2  A3  A4 
%D 2D  +25 A5  A6  A7 
%D 2D  +25     A8     
%D 2D
%D ren     A1      ==>            (P^*∧Q^*)^*
%D ren  A2 A3 A4   ==>  (P∧Q^*)^* P^*∧Q^*  (P^*∧Q)^*
%D ren  A5 A6 A7   ==>   P∧Q^*     (P∧Q)^*  P^*∧Q   
%D ren     A8      ==>              P∧Q               
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D    A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D    A5 A8 <- A6 A8 <- A7 A8 <-
%D    A3 A6 =
%D ))
%D enddiagram
$$\pu \diag{test0} \qquad \diag{test1} \qquad \diag{test2}$$


%D diagram LT-and-1
%D 2Dx     100  +30  +30  +30  +30  +30  +30  +30  +30  +30
%D 2D  100      P^*  A7   Q^*            p^*  a7   q^*   
%D 2D                                                    
%D 2D  +25 P    A3   A5   A6   Q    p    a3   a5   a6   q
%D 2D                                                    
%D 2D  +25      A1   A2   A4             a1   a2   a4    
%D 2D                                                    
%D 2D  +25           A0                       a0         
%D 2D
%D (( A0 .tex= P∧Q           a0 .tex= 11
%D    A1 .tex= P∧Q^*         a1 .tex= 21      
%D    A2 .tex= (P∧Q)^*       a2 .tex=   22    
%D    A3 .tex= (P∧Q^*)^*     a3 .tex=   22  
%D    A4 .tex= P^*∧Q         a4 .tex= 12      
%D    A5 .tex= P^*∧Q^*       a5 .tex= 22    
%D    A6 .tex= (P^*∧Q)^*     a6 .tex=   22  
%D    A7 .tex= (P^*∧Q^*)^*   a7 .tex=   22
%D
%D    A0 A1 -> A0 A2 -> A1 A3 -> A2 A3 ->
%D    A4 A5 -> A4 A6 -> A5 A7 -> A6 A7 ->
%D    A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D 
%D    a0 a1 -> a0 a2 -> a1 a3 -> a2 a3 =
%D    a4 a5 -> a4 a6 -> a5 a7 =  a6 a7 =
%D    a0 a4 -> a1 a5 -> a2 a6 =  a3 a7 =
%D ))
%D (( p .tex= 31 p^* .tex= 32 q^* .tex= 23 q .tex= 13
%D    P P^* ->  Q Q^* ->
%D    p p^* ->  q q^* ->
%D ))
%D enddiagram
%D
%:
%:
%:
%:                     ----------M2  ----------M2
%:                     P^*=P^{**}    Q^*=Q^{**}
%:                     ---------------------(∧)_1  -------------------------M3
%:                     P^*∧Q^*=P^{**}∧Q^{**}       P^{**}∧Q^{**}=(P^*∧Q^*)^*
%:  ---------------M3  -----------------------------------------------------
%:  (P∧Q)^*=P^*∧Q^*                 P^*∧Q^*=(P^*∧Q^*)^*
%:  ---------------------------------------------------
%:              (P∧Q)^*=P^*∧Q^*=(P^*∧Q^*)^*
%:
%:                     ----------M2  ----------M2
%:                     P^*=P^{**}    Q^*=Q^{**}
%:                     ---------------------(∧)_1  -------------------------M3
%:                     P^*∧Q^*=P^{**}∧Q^{**}       P^{**}∧Q^{**}=(P^*∧Q^*)^*
%:                     -----------------------------------------------------
%:                                  P^*∧Q^*=(P^*∧Q^*)^*
%:
%:                                  ^J-and-lozenge-1
%:
%:  ---------------M3   ===================
%:  (P∧Q)^*=P^*∧Q^*     P^*∧Q^*=(P^*∧Q^*)^*
%:  ---------------------------------------
%:       (P∧Q)^*=P^*∧Q^*=(P^*∧Q^*)^*
%:
%:       ^J-and-lozenge-2
%:
\pu
$$\diag{LT-and-1}
  \qquad
  \mat{
  \ded{J-and-lozenge-1} \\ \\ \\
  \ded{J-and-lozenge-2} \\
  }
$$


%D diagram LT-or-1
%D 2Dx     100  +30  +30  +30  +30  +30  +30  +30  +30  +30
%D 2D  100           A7                       a7           
%D 2D              /  |  \                                 
%D 2D  +25      A3   A5   A6             a3   a5   a6      
%D 2D           |  X    X                                  
%D 2D  +25      A1   A2   A4             a1   a2   a4      
%D 2D              \  | /                                  
%D 2D  +25 P^*       A0        Q^*  p^*       a0        q^*
%D 2D                                                      
%D 2D  +25      P         Q              p         q       
%D 2D
%D (( P P^* ->
%D    Q Q^* ->
%D    p .tex= 10 p^* .tex= 20 ->
%D    q .tex= 01 q^* .tex= 02 ->
%D ))
%D (( A0 .tex= P∨Q           a0 .tex= 11
%D    A1 .tex= P∨Q^*         a1 .tex= 21
%D    A2 .tex= (P∨Q)^*       a2 .tex= 33
%D    A3 .tex= (P∨Q^*)^*     a3 .tex= 33
%D    A4 .tex= P^*∨Q         a4 .tex= 02
%D    A5 .tex= P^*∨Q^*       a5 .tex= 22
%D    A6 .tex= (P^*∨Q)^*     a6 .tex= 33
%D    A7 .tex= (P^*∨Q^*)^*   a7 .tex= 33
%D    A0 A1 -> A0 A2 -> A1 A3 -> A2 A3 ->
%D    A4 A5 -> A4 A6 -> A5 A7 -> A6 A7 ->
%D    A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D
%D    a0 a1 -> a0 a2 -> a1 a3 -> a2 a3 =
%D    a4 a5 -> a4 a6 -> a5 a7 -> a6 a7 =
%D    a0 a4 -> a1 a5 -> a2 a6 =  a3 a7 =
%D ))
%D enddiagram
%D
%:
%:     ------           ------
%:     P≤P∨Q           Q≤P∨Q
%:  ------------Mo   ------------Mo
%:  J(P)≤J(P∨Q)     J(Q)≤J(P∨Q)
%:  ---------------------------
%:       J(P)∨J(Q)≤J(P∨Q)
%:    -----------------------Mo   ----------------M2
%:    J(J(P)∨J(Q))≤J(J(P∨Q))     J(J(P∨Q))=J(P∨Q)
%:    --------------------------------------------
%:               J(J(P)∨J(Q))≤J(P∨Q)
%:
%:               ^J-or-lozenge
%:
%:
%:     ------          ------
%:     P≤P∨Q           Q≤P∨Q
%:  ------------Mo  -----------Mo
%:  P^*≤(P∨Q)^*     Q^*≤(P∨Q)^*
%:  ---------------------------
%:       P^*∨Q^*≤(P∨Q)^*
%:    ----------------------Mo   ----------------M2
%:    (P^*∨Q^*)^*≤(P∨Q)^{**}     (P∨Q)^{**}=(P∨Q)^*
%:    --------------------------------------------
%:               (P^*∨Q^*)^*≤(P∨Q)^*
%:
%:               ^J-or-lozenge
%:
\pu
$$\diag{LT-or-1}
  % \qquad
  \ded{J-or-lozenge}
$$


%D diagram LT-imp-1
%D 2Dx     100  +30  +30  +30  +30  +30  +30  +30
%D 2D  100      A7                  A7           
%D 2D                                            
%D 2D  +25 A3   A5   A6        A3   A5   A6      
%D 2D                                            
%D 2D  +25 A1   A2   A4        A1   A2   A4      
%D 2D                                            
%D 2D  +25      A0                  A0           
%D 2D
%D ((
%D    A0 .tex= P^*{→}Q
%D    A1 .tex= P^*{→}Q^*
%D    A2 .tex= (P^*{→}Q)^*
%D    A3 .tex= (P^*{→}Q^*)^*
%D    A4 .tex= P{→}Q
%D    A5 .tex= P{→}Q^*
%D    A6 .tex= (P{→}Q)^*
%D    A7 .tex= (P{→}Q^*)^*
%D    A0 A1 -> A0 A2 -> A1 A3 -> A2 A3 ->
%D    A4 A5 -> A4 A6 -> A5 A7 -> A6 A7 ->
%D    A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%D
\pu
$$\diag{LT-imp-1}$$


% «J-proofs» (to ".J-proofs")
% (find-istfile "1.org" "P&Q, J(P)&Q, ...")
% (find-LATEX "2008graphs.tex")
% (find-LATEX "2008graphs.tex" "LT-modalities")
% (find-853page  21 "internal-diagram")
% (find-853page  22 "and")


Extras:

%:   01=_J23    45=_J67
%:  ---------  ---------
%:  0\_=_L2\_  \_5=_R\_7
%:  --------------------
%:        05=_W27
%:  
%:        ^JLRW
%:
%:
%:  P≤^*Q                        Q≤^*R                      
%:  -------def                   -------def                 
%:  P^*≤Q^*                      Q^*≤R^*                    
%:  -----------(∧R)_1            -----------(P∨)_1          
%:  P^*∧R≤Q^*≤R                  P∨Q^*≤P∨R^*                
%:  ----------------(*)_1        -------------------(*)_1   
%:  (P^*∧R)^*≤(Q^*≤R)^*          (P∨Q^*)^*≤(P∨R^*)^*        
%:  -------------------∧-cube    -------------------∨-cube  
%:  (P∧R)^*≤(Q∧R)^*              (P∨Q)^*≤(P∨R)^*            
%:  --------------- def          ---------------def         
%:  P∧R≤^*Q∧R                    P∨Q≤^*P∨R                  
%:                                                          
%:  ^and-R-is-star-functorial    ^P-or-is-star-functorial   
%:
\pu
$$\ded{JLRW}$$
$$\ded{and-R-is-star-functorial} \qquad \ded{P-or-is-star-functorial}$$


%:                     ----------M2  ----------M2
%:                     P^*=P^{**}    Q^*=Q^{**}
%:                     ---------------------(∧)_1  -------------------------M3
%:                     P^*∧Q^*=P^{**}∧Q^{**}       P^{**}∧Q^{**}=(P^*∧Q^*)^*
%:                     -----------------------------------------------------
%:                                  P^*∧Q^*=(P^*∧Q^*)^*
%:
%:                                  ^J-and-lozenge-1


% There the "="s get into the rule name:
% =================∧-cube





%\end{document}
\newpage



% «HAs-and-CCCs» (to ".HAs-and-CCCs")

\par Logic and Categories, or: Heyting Algebras for Children
\par Eduardo Ochs - UniLog 2015, Istanbul
\par \url{http://angg.twu.net/math-b.html#istanbul}
\msk
\par \bf{1. A comparison between HAs and Cartesian Closed Categories:}


%  _   _    _                          _    ____ ____ ____     
% | | | |  / \   ___    __ _ _ __   __| |  / ___/ ___/ ___|___ 
% | |_| | / _ \ / __|  / _` | '_ \ / _` | | |  | |  | |   / __|
% |  _  |/ ___ \\__ \ | (_| | | | | (_| | | |__| |__| |___\__ \
% |_| |_/_/   \_\___/  \__,_|_| |_|\__,_|  \____\____\____|___/
%                                                              

%: 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-[,]
%:  

\pu

\def\BiHArules{{
\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\BiCCCrules{{
\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-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}
}

\def\BiCCCeqs{
\begin{array}{rl}
(id)   & \id_A ∈ \Hom(A,A)                  \\
(comp) & (;)_{A,B,C}: \Hom(A,B)×\Hom(B,C)→\Hom(A,C) \\
                                     \\
(⊤)    & ∀A.(\Hom(A,1)≃1)            \\
(⊥)    & ∀A.(\Hom(0,A)≃1)            \\
(∧)    & ∀A,B,C.(\Hom(A,B×C)≃\Hom(A,B)×\Hom(A,C)) \\
(∨)    & ∀A,B,C.(\Hom(A+B,C)≃\Hom(A,C)×\Hom(B,C)) \\
(→)    & ∀A,B,C.(\Hom(A,C^B)≃\Hom(A×B,C)      \\
\end{array}
}


% (find-854file "" "fdiagest")
% (find-854file "" "%D diagram yoneda-and-friends")
% (find-dn4 "experimental.lua" "BOX")
\def\ctabular#1{\begin{tabular}{c}#1\end{tabular}}
\def\ltabular#1{\begin{tabular}{c}#1\end{tabular}}
% \def\fdiagwithboxest#1#2{\ltabular{#2 \\ \fdiagwithboxes{#1}}}
\def\fdiagest#1#2{\ltabular{#2 \\ \fdiag{#1}}}

\savebox{\myboxa}{$\diag{BiHAdiag}$}   \def\BiHAdiag {\usebox{\myboxa}}
\savebox{\myboxb}{$\diag{BiCCCdiag}$}  \def\BiCCCdiag{\usebox{\myboxb}}

% (find-es "tex" "savebox")

$$\begin{array}{rcl}
    \fbox{$\BiHAeqs$}    && \fbox{$\BiCCCeqs$}  \\\\
    \fbox{$\BiHArules$}  && \fbox{$\BiCCCrules$} \\\\
    \fbox{\BiHAdiag}     && \fbox{\BiCCCdiag}   \\
  \end{array}
$$







%  _                _          __                    
% | |__  _ __ _   _| |_ ___   / _| ___  _ __ ___ ___ 
% | '_ \| '__| | | | __/ _ \ | |_ / _ \| '__/ __/ _ \
% | |_) | |  | |_| | ||  __/ |  _| (_) | | | (_|  __/
% |_.__/|_|   \__,_|\__\___| |_|  \___/|_|  \___\___|
%                                                    
% «brute-force» (to ".brute-force")

% (find-LATEX "2015logicandcats.lua" "processzrect")
\def\processzrect#1{\directlua{tf:processuntil() processzrect"#1 out"}}
\def\zr#1{\processzrect{#1}}

% NEW:
%
\end{document}

%R  ra := 1/   0   \    rb := 1/   0   \    rc := 1/   0   \    
%R         |  0 0  |           |  0 0  |           |  0 0  |    
%R         | 0 0 0 |           | 0 0 0 |           | 0 0 0 |    
%R         |0 1 0 0|           |0 0 1 0|           |0 0 0 0|    
%R         | 1 1 0 |           | 0 1 1 |           | 0 1 0 |    
%R         |  1 1  |           |  1 1  |           |  1 1  |    
%R         \   1   /           \   1   /           \   1   /    
%R
\pu
\def\ra{\mat{λP.P≤21 = \\ \zr{ra script 7pt}}}
\def\rb{\mat{λP.P≤12 = \\ \zr{rb script 7pt}}}
\def\rc{\mat{λP.P≤21∧P≤12 = \\ \zr{rc script 7pt}}}
\def\rd{\mat{λP.P≤?  = \\ \zr{rc script 7pt}}}
%
%  (P≤Q & R) <-> (P≤Q )&(P≤R )
%     21 12         21     12
%     -----      -----  ------
%       ?          \ra    \rb
%   -------      -------------
%     \rd             \rc
%
%L ubs_brute_force_and = ubs [[
%L   P Q 21 u R 12 u ∧ bin ? u ≤ bin \rd u ()
%L   P Q 21 u ≤ bin \ra u ()
%L   P R 12 u ≤ bin \rb u () ∧ bin \rc u
%L   ↔ bin
%L   ∀P. pre
%L ]]
   
%R  Ra := 2/      21      \    Rb := 1/   0   \
%R         |    21  21    |           |  0 0  |
%R         |  21  21  11  |           | 0 0 1 |
%R         |20  21  11  01|           |0 0 1 1|
%R         |  20  11  01  |           | 0 1 1 |
%R         |    10  01    |           |  1 1  |
%R         \      00      /           \   1   /
%R
\pu
\def\Ra{\mat{λP.P∧21      = \\ \zr{Ra script 9pt}}}
\def\Rb{\mat{λP.(P∧21)≤12 = \\ \zr{Rb script 7pt}}}
\def\Rc{\mat{λP.P≤?       = \\ \zr{Rb script 7pt}}}

%
%  (P≤Q -> R) <-> (P&Q ≤ R )
%     21  12         21  12
%     ------      -----
%       ?          \Ra
%   --------      ----------
%     \Rc             \Rb
%
%
%   P   Q 21 u R 12 u → bin ? u    ≤ bin \Rc    u ()
%   P Q 21 u ∧ bin    \Ra u   R 12 u ≤ bin    \Rb u ()
%
%L ubs_brute_force_imp = ubs [[
%L   P   Q 21 u R 12 u → bin ? u    ≤ bin \Rc    u ()
%L   P Q 21 u ∧ bin    \Ra u   R 12 u ≤ bin    \Rb u ()
%L   ↔ bin
%L ]]

\par Logic and Categories, or: Heyting Algebras for Children
\par Eduardo Ochs - UniLog 2015, Istanbul
\par \url{http://angg.twu.net/math-b.html#istanbul}
\msk
\par \bf{2. Calculating $21∧12$ and $21{→}12$ by brute force:}

\bsk

$$\Expr{ubs_brute_force_and}
  \qquad
  \qquad
  \Expr{ubs_brute_force_imp}
$$
   







\end{document}






   





\end{document}


% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End:
