Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% This is the `eqfibs.metatex' file of dednat4.
% Copyright 2005 Eduardo Ochs <edrx@mat.puc-rio.br>
% Author:        Eduardo Ochs <edrx@mat.puc-rio.br>
% Version:       2005feb24
% License: GPL (I'll add the complete headers later)
% Latest: http://angg.twu.net/dednat4/eqfibs.metatex
% This is a "real-world" test for the diagrams feature of dednat4.

% (code-c-d "tese" "/oldfs/7/pandahome/edrx/LATEX/dout/")
% (find-tesefile "")
% (find-tesefile "tscats.metatex")
% (find-tesefile "tscats.metatex" "b=b''")
% (find-tesefile "defs-dnt.tex")
% (find-angg "LATEX/edrx.sty")
% (eebg-xdvi "/oldfs/7/pandahome/edrx/LATEX/dout/chapters.dvi")
% (eebg-xdvi "/oldfs/7/pandahome/edrx/LATEX/2002h.dvi")
% (eebg-xdvi "/oldfs/7/pandahome/edrx/LATEX/2003a.dvi")
% (eebg-xdvi "/oldfs/7/pandahome/edrx/LATEX/2003d.dvi")

% (find-tesefile "../2002h.tex")
% (find-tesefile "../2003a.tex")
% (find-tesefile "../2003d.tex")


\documentclass[oneside]{book}

\usepackage{amsmath}
\usepackage{amssymb}

\usepackage{proof}
\input diagxy
\input demodefs.tex
% \xyoption{curve}

\begin{document}
\input eqfibs.dnt

\def\id{\mathrm{id}}
\def\nat{\natural}
\def\Frob{\mathrm{Frob}}
\def\BCC{\mathrm{BCC}}

\def\newpage{\vfill\break}

%L standardabbrevs()
%L require "experimental.lua"
%L forths["sl_"] = macro(".slide= -2.5pt")
%L forths["sl^"] = macro(".slide= 2.5pt")
%:*.=*{=}*
%:*&* \land *
%:*&*{\land}*

% (find-tesefile "defs-dnt.tex" "_|")
%
\def\pbsymbol#1{%
  \begin{picture}(#1,#1)
  \put(0,0){\line(1,0){#1}}
  \put(#1,#1){\line(0,-1){#1}}
  \end{picture}}
% (find-dednat "experimental.lua")
%L emitTeX = function (arrow)
%L     return arrow.TeX
%L   end
%L forths["relplace"] = function ()
%L     local x, y = ds[1].x, ds[1].y
%L     local dx, dy = getwordasluaexpr(), getwordasluaexpr()
%L     local TeX = getword()
%L     storearrow {special=emitTeX, TeX = format(
%L         "\\place(%d,%d)[{%s}]", realx(x+dx), realy(y+dy), TeX
%L       )}
%L   end
%L forths["_|"] = macro "relplace 7 7 \\pbsymbol{7}"
%L
%L placetoTeX = function (arrow)
%L     local node = arrow.from
%L     return format("\\place(%d,%d)[{%s}]", realx(node.x), realy(node.y),
%L         node.TeX)
%L   end
%L forths["place"] = function ()
%L     storearrow {special=placetoTeX, from=ds[1]}
%L   end




%%%%%
%
% BCC and Frobenius maps in several fibrations
% (only LCCCs at the moment)
%
%%%%%

%D diagram LCCC-BCC
%D 2Dx         100     +30        +25      +30
%D 2D  100   {}d ===============> c,d{}		 
%D 2D          - /\               - ^		 
%D 2D          |  \\   |->        | |\BCC		 
%D 2D          v   \\             v -		 
%D 2D  +20  {}c,d <=\\=========== c,d{}{}		 
%D 2D           /\   \\             /\		 
%D 2D  +10       \\    d ===============> c,d{{}}	 
%D 2D             \\   -              \\   -	 
%D 2D              \\  |       <-|     \\  |\id	 
%D 2D               \\ v                \\ v	 
%D 2D  +20            c,d <============== c,d{{}}{}
%D 2D                                              
%D 2D                                              
%D 2D  +10     a,b,c |----------> a,b		 
%D 2D              -  _|              -		 
%D 2D               \                  \		 
%D 2D                v                  v		 
%D 2D  +35            a,c |--------------> a	 
%D 2D                                              
%D ((  {}d      c,d{}		 # 0   1
%D    {}c,d     c,d{}{}	         # 2   3 
%D           d        c,d{{}}    #   4   5
%D          c,d       c,d{{}}{}  #   6   7
%D    @ 0 @ 1 =>
%D    @ 0 @ 2 |-> @ 1 @ 3 |-> sl_ .plabel= l \natural
%D                @ 1 @ 3 <-| sl^ .plabel= r \mathrm{BCC}
%D            @ 0 @ 3 harrownodes nil 20 nil |->
%D    @ 2 @ 3 <=
%D    @ 0 @ 4 <=  @ 2 @ 6 <=  @ 3 @ 7 <=
%D    @ 0 @ 2 midpoint @ 4 @ 6 midpoint dharrownodes nil 14 nil <-|
%D    @ 4 @ 5 =>  @ 4 @ 6 |-> @ 5 @ 7 |-> .plabel= r \mathrm{id}
%D            @ 4 @ 7 harrownodes nil 20 nil <-|
%D    @ 6 @ 7 <=
%D ))
%D (( a,b,c     a,b		 
%D          a,c     a	 
%D    @ 0 @ 1 |->  @ 0 @ 2 |->  @ 1 @ 3 |->  @ 2 @ 3 |->
%D    @ 0 relplace 15 7 \pbsymbol{7}
%D )) 
%D enddiagram
%D
% $$\diag{LCCC-BCC}$$



% (find-tesefile "NOTES" "%D diagram Frob-functional")

%D diagram Frob-functional
%D 2Dx       100      +30          +35
%D 2D  100   c =================> b,c
%D 2D	     ^             ---->   ^
%D 2D	  \pi|            /        |\pi
%D 2D	     -           -  Frob   -
%D 2D  +20  c,d => b,(c,d) <--| (b,c),d
%D 2D	     -           - |-->    -
%D 2D	 \pi'|            \ nat    |\pi'
%D 2D	     v             ------> v
%D 2D  +20   d <================= d{}
%D 2D
%D 2D  +15  a,b |----------------> a
%D 2D
%D (( c            b,c      # 0    1
%D    c,d b,(c,d) (b,c),d   # 2  3 4
%D      d               d{} # 5    6
%D    @ 0 @ 1 =>
%D    @ 0 @ 3 harrownodes 15 20 nil |-> 
%D    @ 0 @ 2 <-| .plabel= l \pi  @ 1 @ 3 <-| @ 1 @ 4 <-| .plabel= r \pi
%D    @ 2 @ 3 =>
%D    @ 3 @ 4 |-> sl_ .plabel= b \nat  @ 3 @ 4 <-| sl^ .plabel= a \Frob
%D    @ 2 @ 5 |->     .plabel= l \pi'  @ 3 @ 6 |->  @ 4 @ 6 |-> .plabel= r \pi'
%D    @ 5 @ 3 harrownodes 15 20 nil |-> 
%D    @ 5 @ 6 <=
%D ))
%D (( a,b a |->
%D ))
%D enddiagram
%D
% $$\diag{Frob-functional}$$

$$\diag{LCCC-BCC} \qquad \diag{Frob-functional}$$





%%%%%
%
% Equality fibrations: identity, reflexivity, transitivity
% (only transitivity at the moment)
%
%%%%%

%D diagram fibeq-trans-1
%D 2Dx        100     +25             +45        +35
%D 2D  100                   {b'.=b''\;\;\;\;b.=b'}
%D 2D
%D 2D  +18                      {b'.=b''&\,b.=b'}
%D 2D	                               ^ -
%D 2D	                           \nat| |Frob
%D 2D	                               - v
%D 2D  +20            b.=b' ===> b'.=b''&\,b.=b'
%D 2D	                -               -
%D 2D	              id|      |->      |
%D 2D	                v               v
%D 2D  +20          {}b.=b' <======== b.=b''
%D 2D	         /=>                        <=\
%D 2D	        //                            \\
%D 2D	       //                              \\
%D 2D  +20   \top ============================> b=b''
%D 2D
%D 2D  +15           a,b,b' |-----> a,b,b',b''
%D 2D	           ^                         |
%D 2D	          /                           \
%D 2D           |-                             v
%D 2D  +20   a,b |---------------------------> a,b,b''
%D 2D
%D ((        {b'.=b''\;\;\;\;b.=b'}
%D              {b'.=b''&\,b.=b'}	    #     0
%D        b.=b'  b'.=b''&\,b.=b'	    #   1 2
%D      {}b.=b'      b.=b''	            #   3 4
%D    \top                        b=b''     # 5    6
%D #  @ 1 @ 0 |-> .slide=  15pt .plabel= l \pi
%D #  @ 1 @ 0 |-> .slide= -15pt .plabel= r \pi'
%D #  @ 1 @ 3 <-| sl_ .plabel= l \natural
%D #  @ 1 @ 3 |-> sl^ .plabel= r \mathrm{Frob}
%D    @ 2 @ 3 =>
%D    @ 2 @ 4 |-> .plabel= l \id @ 2 @ 5 hadjnodes |-> @ 3 @ 5 |->
%D    @ 4 @ 5 <=    @ 6 @ 4 => @ 4 @ 7 <= @ 5 @ 7 <=   @ 6 @ 7 =>
%D ))
%D ((     a,b,b' a,b,b',b''                 #   0 1
%D    a,b                  a,b,b''          # 2     3
%D    @ 0 @ 1 |-> .plabel= a \delta
%D    @ 2 @ 0 |-> .plabel= a \delta @ 0 @ 3 |-> .plabel= m {b'':=b} @ 1 @ 3 |->
%D    @ 2 @ 3 |-> .plabel= m \delta @ 0 @ 3
%D ))
%D enddiagram
%D
$$\diag{fibeq-trans-1}$$


% (find-tesefile "tscats.metatex" "%D diagram fibeq-pairs-1\n")

\newpage




%%%%%
%
% Equality fibrations: pairs
%
%%%%%

%D diagram fibeq-pairs-1
%D 2Dx         100         +50           +30          +50
%D 2D  100     \top ==================> c_1.=c_2
%D 2D	         -  /\                     -       
%D 2D	         |   \\       |->          |                   
%D 2D	         v    \\                   v                  
%D 2D  +20 (b,c).=(b,c) <======== (b_1,c_1).=(b_1,c_2)
%D 2D	          /\    \\                  /\                
%D 2D	           \\    \\                  \\               
%D 2D  +10          \\   \top{} ==========> (b_1,c_1).=(b_2,c_2){}
%D 2D	             \\    -                   \\     -
%D 2D	              \\   |          <-|       \\    |\id
%D 2D	               \\  v                     \\   v
%D 2D  +20          (b,c).=(b,c){}  <====== (b_1,c_1).=(b_2,c_2){}{}
%D 2D
%D 2D
%D 2D  +15     a,b,c |----------------> a,b_1,c_1,c_2
%D 2D	             -  _|                     -
%D 2D	              \                         \
%D 2D	               v                         v
%D 2D  +30            a,(b,c) |-----------> a,(b_1,c_1),(b_2,c_2)
%D 2D
%D ((     \top                     c_1.=c_2                      # 0   1
%D    (b,c).=(b,c)           (b_1,c_1).=(b_1,c_2)                # 2   3
%D                   \top{}            (b_1,c_1).=(b_2,c_2){}    #   4   5
%D               (b,c).=(b,c){}        (b_1,c_1).=(b_2,c_2){}{}  #   6   7
%D    @ 0 @ 1 =>
%D    @ 0 @ 2 |->  @ 1 @ 3 |->  @ 0 @ 3 harrownodes nil 20 nil |->
%D    @ 2 @ 3 <=
%D    @ 0 @ 4 <=  @ 2 @ 6 <=  @ 3 @ 7 <=
%D    @ 0 @ 2 midpoint @ 4 @ 6 midpoint dharrownodes nil 17 nil <-|
%D    @ 4 @ 5 =>
%D    @ 4 @ 6 |->  @ 5 @ 7 |-> .plabel= r \id
%D    @ 4 @ 7 harrownodes nil 20 nil <-|
%D    @ 6 @ 7 <=
%D ))
%D (( a,b,c       a,b_1,c_1,c_2
%D         a,(b,c)           a,(b_1,c_1),(b_2,c_2)
%D    @ 0 @ 1 |->  @ 0 @ 2 |->  @ 1 @ 3 |->  @ 2 @ 3 |->
%D    @ 0 relplace 23 7 \pbsymbol{7}
%D )) 
%D enddiagram
%D
$$\diag{fibeq-pairs-1}$$

%D diagram fibeq-pairs-2
%D 2Dx         100         +50           +30          +50
%D 2D  100     \top ==================> b_1.=b_2
%D 2D	         -  /\                     -       
%D 2D	         |   \\       |->          |                   
%D 2D	         v    \\                   v                  
%D 2D  +20 (b,c).=(b,c) <======== (b_1,c_1).=(b_2,c_1)
%D 2D	          /\    \\                  /\                
%D 2D	           \\    \\                  \\               
%D 2D  +10          \\   \top{} ==========> (b_1,c_1).=(b_2,c_2){}
%D 2D	             \\    -                   \\     -
%D 2D	              \\   |          <-|       \\    |\id
%D 2D	               \\  v                     \\   v
%D 2D  +20          (b,c).=(b,c){}  <====== (b_1,c_1).=(b_2,c_2){}{}
%D 2D
%D 2D
%D 2D  +15     a,c,b |---------------> a,c_1,b_1,b_2
%D 2D	             -  _|                     -
%D 2D	              \                         \
%D 2D	               v                         v
%D 2D  +30            a,(b,c) |-----------> a,(b_1,c_1),(b_2,c_2)
%D 2D
%D ((     \top                 b_1.=b_2                          # 0   1
%D    (b,c).=(b,c)       (b_1,c_1).=(b_2,c_1)                    # 2   3
%D                  \top{}             (b_1,c_1).=(b_2,c_2){}    #   4   5
%D             (b,c).=(b,c){}          (b_1,c_1).=(b_2,c_2){}{}  #   6   7
%D    @ 0 @ 1 =>
%D    @ 0 @ 2 |->  @ 1 @ 3 |->  @ 0 @ 3 harrownodes nil 20 nil |->
%D    @ 2 @ 3 <=
%D    @ 0 @ 4 <=  @ 2 @ 6 <=  @ 3 @ 7 <=
%D    @ 0 @ 2 midpoint @ 4 @ 6 midpoint dharrownodes nil 17 nil <-|
%D    @ 4 @ 5 =>
%D    @ 4 @ 6 |->  @ 5 @ 7 |-> .plabel= r \id
%D    @ 4 @ 7 harrownodes nil 20 nil <-|
%D    @ 6 @ 7 <=
%D ))
%D ((   a,c,b         a,c_1,b_1,b_2
%D            a,(b,c)               a,(b_1,c_1),(b_2,c_2)
%D    @ 0 @ 1 |->  @ 0 @ 2 |->  @ 1 @ 3 |->  @ 2 @ 3 |->
%D    @ 0 relplace 23 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\diag{fibeq-pairs-2}$$

%D diagram fibeq-pairs-3
%D 2Dx           100                   +60                   +60
%D 2D 100                       b_1.=b_2&c_1.=c_2
%D 2D                       -           -           -
%D 2D                      /            |             \
%D 2D                     v             |              v
%D 2D +15      b_1.=b_2                 |                 c_1.=c_2
%D 2D             -                     |                     -
%D 2D             |                     v                     |
%D 2D +10         | (b_1,c_1).=(b_2,c_1)&(b_2,c_1).=(b_2,c_2) |
%D 2D             |         -           -           -         |
%D 2D             |        /            |            \        |
%D 2D             v       v             |             v       v
%D 2D +15 (b_1,c_1).=(b_2,c_1)         trans         (b_2,c_1).=(b_2,c_2)
%D 2D                                   |
%D 2D                                   |
%D 2D                                   v
%D 2D +15                      (b_1,c_1).=(b_2,c_2)
%D 2D
%D 2D +15                       a,b_1,c_1,b_2,c_2
%D 2D
%D ((              b_1.=b_2&c_1.=c_2               #   0
%D                b_1.=b_2   c_1.=c_2              # 1   2
%D     (b_1,c_1).=(b_2,c_1)&(b_2,c_1).=(b_2,c_2)   #   3
%D    (b_1,c_1).=(b_2,c_1)   (b_2,c_1).=(b_2,c_2)  # 4   5
%D               (b_1,c_1).=(b_2,c_2)              #   6
%D                 a,b_1,c_1,b_2,c_2  place
%D    @ 0 @ 1 |-> .plabel= b \pi  @ 0 @ 2 |-> .plabel= b \pi'
%D    @ 0 @ 3 |->  @ 1 @ 4 |->  @ 2 @ 5 |->
%D    @ 3 @ 4 |-> .plabel= b \pi  @ 3 @ 5 |-> .plabel= b \pi'
%D    @ 3 @ 6 |-> .plabel= m \mathrm{trans}
%D ))
%D enddiagram
%D
$$\diag{fibeq-pairs-3}$$





% (find-eimage0 "~/IMAGES/preslim.png")


%(find-eimage0 "/tmp/screenshots/ss1.png")


\def\smallpb#1#2#3{
  \begin{smallmatrix}
       &     & #1 \mathstrut    \\
       &     & \downarrow       \\
    #2 & \to & #3 \mathstrut    \\
  \end{smallmatrix}
}

%D diagram preslims
%D 2Dx            100          +47        +45         +40              +40
%D 2D 100       {}a =========> aaa ===> aLaLaL <===== a^L <=========== a        
%D 2D             -             -          -           -               -        
%D 2D             |    <->      |    <->   |    <->    |    <->        |        
%D 2D             v             v          v           v               v        
%D 2D +30 (b^R,c^R)|_{d^R} <= bRcRdR <=== bcd ===> (b,c)|_d ===> ((b,c)|_d)^R   
%D 2D
%D (( {}a    aaa .tex= \left(\smallpb{a}{a}{a}\right)
%D        aLaLaL .tex= \left(\smallpb{a^L}{a^L}{a^L}\right)  a^L  a
%D    (b^R,c^R)|_{d^R}
%D    bRcRdR .tex= \left(\smallpb{b^R}{c^R}{d^R}\right)
%D    bcd    .tex= \left(\smallpb{b}{c}{d}\right)        (b,c)|_d  ((b,c)|_d)^R
%D    @ 0 @ 1 =>  @ 1 @ 2 =>  @ 2 @ 3 <=  @ 3 @ 4 <=
%D    @ 0 @ 5 |->  @ 1 @ 6 |->  @ 2 @ 7 |->  @ 3 @ 8 |->  @ 4 @ 9 |->  
%D    @ 0 @ 6 harrownodes nil 20 nil <->
%D    @ 1 @ 7 harrownodes nil 20 nil <->
%D    @ 2 @ 8 harrownodes nil 20 nil <->
%D    @ 3 @ 9 harrownodes nil 20 nil <->
%D    @ 5 @ 6 <=  @ 6 @ 7 <=  @ 7 @ 8 =>  @ 8 @ 9 =>
%D ))
%D enddiagram
%D
$$\diag{preslims}$$

\end{document}




#####
#
# e-scripts (see http://angg.twu.net/)
#
#####

#*
mkdir  /tmp/dn4/
cd     /tmp/dn4/
unzip -a -o $S/ftp/ftp.math.mcgill.ca/pub/barr/diagxy.zip
cp $S/http/www.ctan.org/tex-archive/macros/latex/contrib/proof/proof.sty .
cp ~/dednat4/demodefs.tex .
cp ~/dednat4/eqfibs.metatex .

#*
# (find-node "(kpathsea)Supported file formats")
# (find-node "(kpathsea)Supported file formats" "`TEXINPUTS'; suffix `.tex'")
# (find-node "(web2c)tex invocation" "KPATHSEA_DEBUG")

cd ~/dednat4/
~/dednat4/dednat4.lua eqfibs.metatex  && \
  TEXINPUTS=/tmp/dn4: \
    latex eqfibs.tex && \
    xdvi eqfibs.dvi &

#*




% Local Variables:
% coding: raw-text-unix
% mode:   latex
% End: