% -*- coding: raw-text -*-
% This is the file `examples/eedemo2.tex' of dednat4.
% The target "demo2" of the makefile copies this to
% "demos/ee.tex" and then runs dednat41 and latex on
% "demos/tmp.tex", that will be a wrapper around "ee.tex".
% Usage:
%   cd ~/dednat4/
%   make demo2
%   xdvi demos/tmp.dvi
% See:
%   http://angg.twu.net/dednat4.html
%   http://angg.twu.net/dednat4/examples/eedemo2.tex
%   http://angg.twu.net/dednat4/examples/eedemo2.tex.html

% (find-dn4 "Makefile")

% Author: Eduardo Ochs <eduardoochs@gmail.com>
% Version: 2008jul06
% Public Domain.


% �.comprcat�		(to "comprcat")
% �.midpoint�		(to "midpoint")
% �.harrownodes�	(to "harrownodes")
% �.presheaf�		(to "presheaf")
% �.color�		(to "color")
% �.beta-reductions�	(to "beta-reductions")




% �comprcat�  (to ".comprcat")

A construction from Bart Jacobs' ``Categorical Logic and Type Theory''
book (sec. 10.4.7, pp.616--617):

%D diagram ccwu-pb
%D 2Dx     100    +30 -15 +15 +15  +15     +30
%D 2D  100                    a0
%D 2D                         /\/
%D 2D                         || \
%D 2D                         ||  v
%D 2D  +25            a1 |--> a2   a3
%D 2D                   -       -  ||/
%D 2D                    \       \ || \
%D 2D                     v       v\/  \
%D 2D  +25                a4 |---> a5   \
%D 2D                       -        -   v
%D 2D  +25 a6 |-> a7 |------------------> a8
%D 2D      /\     /\           \       // ||
%D 2D      ||     ||            \     //  ||
%D 2D      ||     ||             v   \/   \/
%D 2D  +25 a9 |-> a10 |---------> a11 |-> a12
%D 2D
%D ((                   a0 .tex= 1I
%D    a1 .tex= \{1I\}  a2 .tex= I        a3 .tex= X
%D                      a4 .tex= \{X\}    a5 .tex= pX
%D    a6 .tex= 1I  a7 .tex= 1\{Y\}                      a8 .tex= Y
%D    a9 .tex=  I  a10 .tex=  \{Y\}   a11 .tex=   \{Y\} a12 .tex=  pY
%D    a0 a1 |-> a0 a2 <-|
%D    a3 a4 |-> a3 a5 |->
%D    a6 a9 <-| a7 a10 <-| a8 a11 |-> a8 a12 |->
%D    a1 a2 -> sl_ .plabel= b \pi_{1I}
%D    a1 a2 <- sl^ .plabel= a \eta_I
%D    a1 a4 -> .plabel= l \{g\}
%D    a2 a4 -> .plabel= m g^\vee
%D    a0 a3 -> .plabel= a g
%D    a2 a5 -> .plabel= m u
%D    a4 a5 -> .plabel= b \pi_X
%D    a3  a8 -> .PLABEL= ^(0.33) f
%D    a4 a11 -> .PLABEL= ^(0.33) \{f\}
%D    a5 a12 -> .PLABEL= ^(0.33) pf
%D    a6  a7 -> .plabel= b 1v
%D    a7  a8 -> .PLABEL= _(0.5) \ee_Y
%D    a9  a10 -> .plabel= b v
%D    a10 a11 -> .plabel= b \id
%D    a11 a12 -> .plabel= b \pi_Y
%D ))
%D enddiagram

%D diagram ccwu-pb-dnc
%D 2Dx     100    +30 -15 +15 +15  +15     +30
%D 2D  100                    a0
%D 2D                         /\/
%D 2D                         || \
%D 2D                         ||  v
%D 2D  +25            a1 |--> a2   a3
%D 2D                   -       -  ||/
%D 2D                    \       \ || \
%D 2D                     v       v\/  \
%D 2D  +25                a4 |---> a5   \
%D 2D                       -        -   v
%D 2D  +25 a6 |-> a7 |------------------> a8
%D 2D      /\     /\           \       // ||
%D 2D      ||     ||            \     //  ||
%D 2D      ||     ||             v   \/   \/
%D 2D  +25 a9 |-> a10 |---------> a11 |-> a12
%D 2D
%D ((                   a0 .tex= \s[i|*]
%D    a1 .tex= i,*      a2 .tex=    i       a3 .tex= \s[a|b]
%D                      a4 .tex=    a,b     a5 .tex=    a
%D    a6 .tex= \s[i|*]  a7 .tex= \s[c,d|*]                   a8 .tex= \s[c|d]
%D    a9 .tex=    i     a10 .tex=    c,d    a11 .tex=   c,d   a12 .tex=    c
%D    a0 a2 <= a0 a1 =>
%D    a3 a4 => a3 a5 =>
%D    a6 a9 <= a7 a10 <= a8 a11 => a8 a12 =>
%D    a0 a3 |->
%D    a1 a2 <-> a1 a4 |-> a2 a4 |->
%D    a2 a5 |-> a3 a8 |-> .plabel= a \Box a4 a5 |->
%D    a4 a11 |-> a5 a12 |->
%D    a6 a7 |-> a7 a8 |->
%D    a9 a10 |-> a10 a11 |-> a11 a12 |->
%D ))
%D enddiagram

$$\diag{ccwu-pb} \quad \diag{ccwu-pb-dnc}$$

\medskip

Two examples of diagrams with phantom nodes:

% �midpoint�  (to ".midpoint")

%D diagram T:F->G
%D 2Dx    100   +20  +20
%D 2D 100       A
%D 2D         \ - /  
%D 2D        /  |  \
%D 2D       v   v   v
%D 2D +25 FA ------> GA
%D 2D          TA
%D 2D
%D (( A FA |-> A GA |->
%D    FA GA -> .plabel= b TA
%D    A FA GA midpoint
%D      |->
%D ))
%D enddiagram

$$\diag{T:F->G}
  \qquad
  \def\red#1{{\color{red}#1}}
  \def\phantom{\red}
  \diag{T:F->G}
$$

% �harrownodes�  (to ".harrownodes")

%D diagram harrowdemo
%D 2Dx     100       +40
%D 2D  100 A |-----> FA
%D 2D	   |          -
%D 2D	 f |   |->    | Ff
%D 2D	   v          v
%D 2D  +30 B |-----> FB
%D 2D
%D ((  A FA |->
%D     A  B -> .plabel= l f
%D    FA FB -> .plabel= r Ff
%D     B FB |->
%D    A FB harrownodes nil 20 nil |->
%D ))
%D enddiagram

$$\diag{harrowdemo}
  \qquad
  \def\red#1{{\color{red}#1}}
  \def\phantom{\red}
  \diag{harrowdemo}
$$

\newpage

% �presheaf�  (to ".presheaf")

\def\emp{\emptyset}
\def\ph#1{\phantom{#1}}

A diagram with relative phantom nodes:

%L thereplusxy = function (dx, dy, tag)
%L     ds[1] = storenode({x = ds[1].x + dx, y = ds[1].y + dy, tag = tag})
%L     return ds[1]
%L   end
%L forths["there+xy:"] = function ()
%L     thereplusxy(getword(), getword(), getword())
%L   end

%D diagram a-presheaf-that-is-not-a-sheaf
%D 2Dx     100 +15 +15  +30 +15  +15  
%D 2D  100     X            X'     
%D 2D        /   \        /   \    
%D 2D  +20 U       V    U'      V'  
%D 2D        \   /        \   /    
%D 2D  +20     W            W'      
%D 2D          |            |      
%D 2D  +20   \emp         \emp{}
%D 2D
%D ((         X .tex= P(X)          
%D    U .tex= P(U)    V .tex= P(V)  
%D            W .tex= P(W)
%D         \emp .tex= P(\emp)          
%D    @ 0 @ 1 -> @ 0 @ 2 ->
%D    @ 1 @ 3 -> @ 2 @ 3 ->
%D    @ 3 @ 4 ->
%D ))
%D (( X' there+xy: -6 0 X'L .tex= \ph{p_X}
%D    X' there+xy:  6 0 X'R .tex= \ph{p'_X}
%D    V' there+xy: -6 0 V'L .tex= \ph{p_V}
%D    V' there+xy:  6 0 V'R .tex= \ph{p'_V}
%D ))
%D ((          X' .tex= \{p_X,p'_X\}
%D    U' .tex= \{p_U\}   V' .tex= \{p_V,p'_V\}
%D             W' .tex= \{p_W\}
%D         \emp{} .tex= \{p_\emp\}       
%D    # @ 0 @ 1 -> @ 0 @ 2 ->
%D    # @ 1 @ 3 -> @ 2 @ 3 ->
%D    # @ 3 @ 4 ->
%D                         X' place
%D    X'L U' -> X'R U' ->           X'L V'L -> X'R V'L ->
%D                                    V' place
%D                U' W' ->         V'L W' -> V'R W' ->
%D                       W' \emp{} ->
%D ))
%D enddiagram
%D
$$\diag{a-presheaf-that-is-not-a-sheaf}$$

Same, but with the relative phantom nodes in red:

$$\def\ph#1{{\color{red}#1}}
  \diag{a-presheaf-that-is-not-a-sheaf}
$$

\bsk

% �color�  (to ".color")

\def\colorpush#1#2#3{\special{color push rgb #1 #2 #3}}
\def\colorpop{\special{color pop}}

%L arrowwrap = function (arrow)
%L     return format(arrow.wrapin, arrowtoTeX(arrow, ""))
%L   end
%L setwrap = function (fmtstr)
%L     ds[1].special = arrowwrap
%L     ds[1].wrapin = fmtstr
%L   end
%L setcolor = function (rgb)
%L     setwrap("\\colorpush "..rgb.."%s \\colorpop")
%L   end
%L forths[".wrap="]  = function () setwrap(getword()) end
%L forths[".color="] = function () setcolor(getword()) end

%D diagram colors-pushing
%D 2Dx     100   +15  +15
%D 2D  100       red
%D 2D
%D 2D  +25 green      blue
%D 2D
%D (( red   .tex= {\color{red}\text{red}}
%D    green .tex= {\color{green}\text{green}}
%D    blue  .tex= {\color{blue}\text{blue}}
%D    red   green <-> .color= 110
%D    red   blue  <-> .color= 101
%D    green blue  <-> .color= 011
%D ))
%D enddiagram

Coolored nodes and arrows:
$\diag{colors-pushing}$


\newpage

% �beta-reductions�  (to ".beta-reductions")

Some $\bb$-reductions from Bierman and de Paiva's

``On an intuitionistic modal logic'' paper:

% To do: change \fst, \snd, \inl, \inr to use \operatorname
% (but in the sans-serif font)
\def\fst{\textsf{fst}}
\def\snd{\textsf{snd}}
\def\inl{\textsf{inl}}
\def\inr{\textsf{inr}}

\def\unbox #1{\textsf{unbox $#1$}}
\def\unboxp#1{\textsf{unbox($#1$)}}
\def\caseofinlinr#1#2#3#4#5{
  \textsf{case $#1$ of $\inl(#2) \to #3 \;||\; \inr(#4) \to #5$}}
\def\boxwithfor#1#2#3{\textsf{box $#1$ with $#2$ for $#3$}}
\def\letppinwithfor#1#2#3#4#5{
  \textsf{let $\poss#1 \funot \poss#2$ in $#3$ with $#4$ for $#5$}}

\def\poss{\lozenge}
\def\I{\mathcal{I}}
\def\E{\mathcal{E}}
\def\betaquad{\quad \rightsquigarrow_\beta \quad}

% Note that the characters �, , � are \def'd to \land, \lor,
% and \limp (and \limp looks somewhat like \supset). See:
% (find-dn4ex "edrx08.sty" "glyphs")
% (find-dn4ex "edrx08.sty" "limp")

%:\vec\vec 
%:[]\Box 
%:<>\poss 

%:       [x:A]^1  \GG
%:         :::::::::
%:           M:B
%:       -------------{�\I};1
%:  N:A  (�x:A.M):A->B           N:A   \GG
%:  ------------------{�\E}        :::::
%:     (�x:A.M)N:B           ->  M[x:=N]:B
%:  
%:     ^betared-imp-1            ^betared-imp-2
%:  
%:      M:A   N:B
%:    -------------{�\I}
%:    \ang{M,N}:A�B
%:  -----------------{�\E}_1
%:  \fst\ang{M,N}:A�B        ->   M:A
%:  
%:  ^betared-and1-1               ^betared-and1-2
%:  
%:     M:A            [x:A]^1  \GG   [y:B]^1  \DD
%:  -----------\I_1       :::::          :::::
%:  \inl(M):A+B             N:C            P:C        M:A  \GG
%:  ------------------------------------------\E       ::::
%:    \caseofinlinr{\inl(M)}{x}{N}{y}{P}             N[x:=M]:C
%:  
%:    ^betared-or-1                                  ^betared-or-2
%:
%:  \GG      [\vecx:[]\vecA]^1
%:   :               :
%:  \vecM:[]\vecA   N:B                                   \GG
%:  --------------------------------[]\I;1                :::
%:  \boxwithfor{N}{\vecM}{\vecx}:[]B                 \vecM:[]\vecA
%:  -----------------------------------------[]\E         :::
%:  \unboxp{\boxwithfor{N}{\vecM}{\vecx}:[]B}       N[\vecx:=\vecM]:B
%:
%:  ^betared-box-1                                  ^betared-box-2
%:
%:                   \DD
%:                   :::
%:   \GG             N:B      [\vecx:[]\vecA\;y:B]^1      \GG       \DD
%:   :::           -----<>\I         :::                  :::       :::
%:  \vecM:[]\vecA  <>N:<>B          P:<>C            \vecM:[]\vecA  N:B
%:  -------------------------------------<>\E;1                  ::::
%:      P[\vecx:=\vecM,<>y:=<>N]:<>C               P[\vecx:=\vecM,y:=N]:<>C
%:
%:      ^betared-poss-1                            ^betared-poss-2
%:

$$\ded{betared-imp-1} \qquad \ded{betared-imp-2}$$

$$\ded{betared-and1-1} \betaquad \ded{betared-and1-2}$$

$$\ded{betared-or-1} \betaquad \ded{betared-or-2}$$

$$\ded{betared-box-1} \betaquad \ded{betared-box-2}$$

$$\ded{betared-poss-1} \betaquad \ded{betared-poss-2}$$

\bigskip

``$P[\vec x := \vec M, \poss y := \poss N]$'' is a shorthand for

``$\letppinwithfor y N P {\vec M} {\vec x}$''.


