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