\defdiag{ccwu-pb}{    % (find-fline "ee.tex" 37)
  \morphism(675,0)/|->/<-450,-375>[{1I}`{\{1I\}};{}]
  \morphism(675,0)/<-|/<0,-375>[{1I}`{I};{}]
  \morphism(900,-375)/|->/<-450,-375>[{X}`{\{X\}};{}]
  \morphism(900,-375)/|->/<0,-375>[{X}`{pX};{}]
  \morphism(0,-1125)/<-|/<0,-375>[{1I}`{I};{}]
  \morphism(450,-1125)/<-|/<0,-375>[{1\{Y\}}`{\{Y\}};{}]
  \morphism(1350,-1125)/|->/<-450,-375>[{Y}`{\{Y\}};{}]
  \morphism(1350,-1125)/|->/<0,-375>[{Y}`{pY};{}]
  \morphism(225,-375)|b|/{@{->}@<-2.5pt>}/<450,0>[{\{1I\}}`{I};{\pi_{1I}}]
  \morphism(225,-375)|a|/{@{<-}@<2.5pt>}/<450,0>[{\{1I\}}`{I};{\eta_I}]
  \morphism(225,-375)|l|/->/<225,-375>[{\{1I\}}`{\{X\}};{\{g\}}]
  \morphism(675,-375)|m|/->/<-225,-375>[{I}`{\{X\}};{g^\vee}]
  \morphism(675,0)|a|/->/<225,-375>[{1I}`{X};{g}]
  \morphism(675,-375)|m|/->/<225,-375>[{I}`{pX};{u}]
  \morphism(450,-750)|b|/->/<450,0>[{\{X\}}`{pX};{\pi_X}]
  \morphism(900,-375)/{@{->}^(0.33){f}}/<450,-750>[{X}`{Y};]
  \morphism(450,-750)/{@{->}^(0.33){\{f\}}}/<450,-750>[{\{X\}}`{\{Y\}};]
  \morphism(900,-750)/{@{->}^(0.33){pf}}/<450,-750>[{pX}`{pY};]
  \morphism(0,-1125)|b|/->/<450,0>[{1I}`{1\{Y\}};{1v}]
  \morphism(450,-1125)/{@{->}_(0.5){\ee_Y}}/<900,0>[{1\{Y\}}`{Y};]
  \morphism(0,-1500)|b|/->/<450,0>[{I}`{\{Y\}};{v}]
  \morphism(450,-1500)|b|/->/<450,0>[{\{Y\}}`{\{Y\}};{\id}]
  \morphism(900,-1500)|b|/->/<450,0>[{\{Y\}}`{pY};{\pi_Y}]
}
\defdiag{ccwu-pb-dnc}{    % (find-fline "ee.tex" 81)
  \morphism(675,0)/<=/<0,-375>[{\dncdisplay[i|*]}`{i};{}]
  \morphism(675,0)/=>/<-450,-375>[{\dncdisplay[i|*]}`{i,*};{}]
  \morphism(900,-375)/=>/<-450,-375>[{\dncdisplay[a|b]}`{a,b};{}]
  \morphism(900,-375)/=>/<0,-375>[{\dncdisplay[a|b]}`{a};{}]
  \morphism(0,-1125)/<=/<0,-375>[{\dncdisplay[i|*]}`{i};{}]
  \morphism(450,-1125)/<=/<0,-375>[{\dncdisplay[c,d|*]}`{c,d};{}]
  \morphism(1350,-1125)/=>/<-450,-375>[{\dncdisplay[c|d]}`{c,d};{}]
  \morphism(1350,-1125)/=>/<0,-375>[{\dncdisplay[c|d]}`{c};{}]
  \morphism(675,0)/|->/<225,-375>[{\dncdisplay[i|*]}`{\dncdisplay[a|b]};{}]
  \morphism(225,-375)/<->/<450,0>[{i,*}`{i};{}]
  \morphism(225,-375)/|->/<225,-375>[{i,*}`{a,b};{}]
  \morphism(675,-375)/|->/<-225,-375>[{i}`{a,b};{}]
  \morphism(675,-375)/|->/<225,-375>[{i}`{a};{}]
  \morphism(900,-375)|a|/|->/<450,-750>[{\dncdisplay[a|b]}`{\dncdisplay[c|d]};{\Box}]
  \morphism(450,-750)/|->/<450,0>[{a,b}`{a};{}]
  \morphism(450,-750)/|->/<450,-750>[{a,b}`{c,d};{}]
  \morphism(900,-750)/|->/<450,-750>[{a}`{c};{}]
  \morphism(0,-1125)/|->/<450,0>[{\dncdisplay[i|*]}`{\dncdisplay[c,d|*]};{}]
  \morphism(450,-1125)/|->/<900,0>[{\dncdisplay[c,d|*]}`{\dncdisplay[c|d]};{}]
  \morphism(0,-1500)/|->/<450,0>[{i}`{c,d};{}]
  \morphism(450,-1500)/|->/<450,0>[{c,d}`{c,d};{}]
  \morphism(900,-1500)/|->/<450,0>[{c,d}`{c};{}]
}
\defdiag{T:F->G}{    % (find-fline "ee.tex" 124)
  \morphism(300,0)/|->/<-300,-375>[{A}`{FA};{}]
  \morphism(300,0)/|->/<300,-375>[{A}`{GA};{}]
  \morphism(0,-375)|b|/->/<600,0>[{FA}`{GA};{TA}]
  \morphism(300,0)/|->/<0,-375>[{A}`{\phantom{O}};{}]
}
\defdiag{harrowdemo}{    % (find-fline "ee.tex" 149)
  \morphism(0,0)/|->/<600,0>[{A}`{FA};{}]
  \morphism(0,0)|l|/->/<0,-450>[{A}`{B};{f}]
  \morphism(600,0)|r|/->/<0,-450>[{FA}`{FB};{Ff}]
  \morphism(0,-450)/|->/<600,0>[{B}`{FB};{}]
  \morphism(150,-225)/|->/<300,0>[{\phantom{O}}`{\phantom{O}};{}]
}
\defdiag{a-presheaf-that-is-not-a-sheaf}{    % (find-fline "ee.tex" 189)
  \morphism(225,0)/->/<-225,-300>[{P(X)}`{P(U)};{}]
  \morphism(225,0)/->/<225,-300>[{P(X)}`{P(V)};{}]
  \morphism(0,-300)/->/<225,-300>[{P(U)}`{P(W)};{}]
  \morphism(450,-300)/->/<-225,-300>[{P(V)}`{P(W)};{}]
  \morphism(225,-600)/->/<0,-300>[{P(W)}`{P(\emp)};{}]
  \place(1125,0)[{\{p_X,p'_X\}}]
  \morphism(1035,0)/->/<-135,-300>[{\ph{p_X}}`{\{p_U\}};{}]
  \morphism(1215,0)/->/<-315,-300>[{\ph{p'_X}}`{\{p_U\}};{}]
  \morphism(1035,0)/->/<225,-300>[{\ph{p_X}}`{\ph{p_V}};{}]
  \morphism(1215,0)/->/<45,-300>[{\ph{p'_X}}`{\ph{p_V}};{}]
  \place(1350,-300)[{\{p_V,p'_V\}}]
  \morphism(900,-300)/->/<225,-300>[{\{p_U\}}`{\{p_W\}};{}]
  \morphism(1260,-300)/->/<-135,-300>[{\ph{p_V}}`{\{p_W\}};{}]
  \morphism(1440,-300)/->/<-315,-300>[{\ph{p'_V}}`{\{p_W\}};{}]
  \morphism(1125,-600)/->/<0,-300>[{\{p_W\}}`{\{p_\emp\}};{}]
}
\defdiag{colors-pushing}{    % (find-fline "ee.tex" 255)
  \colorpush 110\morphism(225,0)/<->/<-225,-375>[{{\color{red}\text{red}}}`{{\color{green}\text{green}}};{}] \colorpop
  \colorpush 101\morphism(225,0)/<->/<225,-375>[{{\color{red}\text{red}}}`{{\color{blue}\text{blue}}};{}] \colorpop
  \colorpush 011\morphism(0,-375)/<->/<450,0>[{{\color{green}\text{green}}}`{{\color{blue}\text{blue}}};{}] \colorpop
}
\defded{betared-imp-1}{    % (find-fline "ee.tex" 319)
 \infer[{{⊃\E}}]{ \mathstrut (�x:A.M)N:B }{
  \mathstrut N:A &
  \infer[{{⊃\I};1}]{ \mathstrut (�x:A.M):A\to B }{
   \infer*{ \mathstrut M:B }{
    \mathstrut [x:A]^1 &
    \mathstrut \GG } } } }

\defded{betared-imp-2}{    % (find-fline "ee.tex" 319)
 \infer*{ \mathstrut M[x:=N]:B }{
  \mathstrut N:A &
  \mathstrut \GG } }

\defded{betared-and1-1}{    % (find-fline "ee.tex" 327)
 \infer[{{∧\E}_1}]{ \mathstrut \fst\ang{M,N}:A×B }{
  \infer[{{∧\I}}]{ \mathstrut \ang{M,N}:A×B }{
   \mathstrut M:A &
   \mathstrut N:B } } }

\defded{betared-and1-2}{    % (find-fline "ee.tex" 327)
 \mathstrut M:A }

\defded{betared-or-1}{    % (find-fline "ee.tex" 335)
 \infer[{∨\E}]{ \mathstrut \caseofinlinr{\inl(M)}{x}{N}{y}{P} }{
  \infer[{∨\I}]{ \mathstrut \inl(M):A+B }{
   \mathstrut M:A } &
  \infer*{ \mathstrut N:C }{
   \mathstrut [x:A]^1 &
   \mathstrut \GG } &
  \infer*{ \mathstrut P:C }{
   \mathstrut [y:B]^1 &
   \mathstrut \DD } } }

\defded{betared-or-2}{    % (find-fline "ee.tex" 335)
 \infer*{ \mathstrut N[x:=M]:C }{
  \mathstrut M:A &
  \mathstrut \GG } }

\defded{betared-box-1}{    % (find-fline "ee.tex" 345)
 \infer[{\Box \E}]{ \mathstrut \unboxp{\boxwithfor{N}{\vec M}{\vec x}:\Box B} }{
  \infer[{\Box \I;1}]{ \mathstrut \boxwithfor{N}{\vec M}{\vec x}:\Box B }{
   \infer*{ \mathstrut \vec M:\Box A }{
    \mathstrut \GG } &
   \infer*{ \mathstrut N:B }{
    \mathstrut [\vec x:\Box \vec A]^1 } } } }

\defded{betared-box-2}{    % (find-fline "ee.tex" 345)
 \infer*{ \mathstrut N[\vec x:=\vec M]:B }{
  \infer*{ \mathstrut \vec M:\Box \vec A }{
   \mathstrut \GG } } }

\defded{betared-poss-1}{    % (find-fline "ee.tex" 355)
 \infer[{\poss \E;1}]{ \mathstrut P[\vec x:=\vec M,\poss y:=\poss N]:\poss C }{
  \infer*{ \mathstrut \vec M:\Box A }{
   \mathstrut \GG } &
  \infer[{\poss \I}]{ \mathstrut \poss N:\poss B }{
   \infer*{ \mathstrut N:B }{
    \mathstrut \DD } } &
  \infer*{ \mathstrut P:\poss C }{
   \mathstrut [\vec x:\Box \vec A\;y:B]^1 } } }

\defded{betared-poss-2}{    % (find-fline "ee.tex" 355)
 \infer*{ \mathstrut P[\vec x:=\vec M,y:=N]:\poss C }{
  \infer*{ \mathstrut \vec M:\Box A }{
   \mathstrut \GG } &
  \infer*{ \mathstrut N:B }{
   \mathstrut \DD } } }