|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% -*- 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}$''.