\documentclass{book}
\usepackage{amsmath}
\usepackage{proof.edrx}
\usepackage{bussproofs}
\input diagxy
  \xyoption{curve}
  % \xyoption{tips}
  \def\diagxyto{\ifnextchar/{\toop}{\toop/>/}}
  \def\mon{\diagxyto/ >->/}
  \def\epi{\diagxyto/->>/}
  \def\toleft{\diagxyto/<-/}
  \def\monleft{\diagxyto/<-< /}
  \def\epileft{\diagxyto/<<-/}
  \def\to{\rightarrow}
\begin{document}

\pagestyle{empty}

\def\defded#1#2{\expandafter\def\csname ded-#1\endcsname{#2}}
\def\ded#1{\csname ded-#1\endcsname}


\def\defdiag#1#2{\expandafter\def\csname diag-#1\endcsname{#2}}
\def\diag#1{\bfig\csname diag-#1\endcsname\efig}

\def\O{\mathbf{O}}
\def\op{{\operatorname{op}}}
\newcommand\E{\mathbf{E}}
\newcommand\Set{\mathbf{Set}}
\newcommand\funto{\Rightarrow}
\newcommand\tnto{\ton{\bullet}}
\newcommand\ton[1]{\overset{#1}{\to}}
\catcode`Î=13 \defÎ{\in}
\input example.dnt

%:*<->*\bij *
%:*|->*\mapsto *
%:*->*\to *
%:*-.>*\tnto *
%:*=>*\funto *
%:*/\*\land *
%:
%:  [a]^1  b             [P]^1  Q
%:  --------             --------
%:    (a,b)   (a,b)->c     P/\Q    P/\Q->R
%:    ----------------     ---------------
%:           c                   R
%:         ----1               ----1
%:         a->c                P->R
%:
%:         ^tree1              ^tree2
%:
$$\ded{tree1} \qquad \ded{tree2}$$

%:
%:           [(rÎD)^\op]^2  [dÎD]^1               [\O[r]^\op]^2  [\O[d]]^1
%:           ----------------------               ------------------------
%:                D(r,d)Î\Set                           \E[r->d]
%:                ==============1                      =========1
%:                D(r,-):D->\Set                       d=>(r->d)
%:                -------------                        -------------
%:  h:s->r        D(r,-)Î\Set^D          s->r          \O[d=>(r->d)]
%:  ------------  --------------------2  ------------  ------------------2
%:  (h:s->r)^\op  D(-,-):D^\op->\Set^D   r^\op->s^\op  r^\op=>(d=>(r->d))
%:  --------------------------------     --------------------------------
%:        D(h,-):D(r,-)-.>D(s,-)               d-.>((r->d)->(s->d))
%:
%:        ^CWM.D(h,-)1                         ^CWM.D(h,-)2
%:
$$\ded{CWM.D(h,-)2} \qquad \ded{CWM.D(h,-)1}$$

%:
%:     t->x,y
%:     =======
%:  t   t->x               x,y  x,y->f  x,y  x,y->f
%:  --------IFT            -----------  ===========IFT
%:    x->t        t->x,y       f          f->(x->y)
%:    ==================       ====================
%:          x->y                      x->y
%:
%:          ^Immersions-short         ^Implicit-short
%:
$$\ded{Immersions-short} \qquad \ded{Implicit-short}$$

%L require("diagxy.lua")
%D diagram miniadj
%D 2Dx     100   120
%D 2D 100 a^L <= a
%D 2D      -     -
%D 2D      | <-> |
%D 2D      v     v
%D 2D 120  b => b^R
%D a (( a^L => drop b |-> drop b^R => )) b^R |->
%D enddiagram

% (eev "cd ~/dednat/; make clean; make example.dnt")
% (eev "cd ~/dednat/; make clean; make example.dvi && rexdvi example.dvi")
% (find-fline "~/dednat/example.dnt" "miniadj")
% (find-fline "~/dednat/Makefile")
$$\diag{miniadj}$$

\end{document}

# Local Variables:
# coding:                   no-conversion
# ee-anchor-format:         "«%s»"
# ee-charset-indicator:     "Ñ"
# End: