|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
# Many diagrams using diaglib.014.
# Edrx 2000apr24.
# (find-angg "LATEX/diaglib.014")
# (find-angg ".emacs")
# (set (make-local-variable 'ee-temp-bounded-function) 'eediag-bounded)
# (find-e20node "Locals")
(query-replace-regexp "^\\(epsfile \\([!-~]*\\)\n\\)" "# «\\2»\n\\1")
# New stuff to make this run with recent versions of eev, 2005mar08:
# (find-es "tcl" "newdiaglib")
(defun eediag (s e) (interactive "r")
(ee-write s e
"cd ~/LATEX; cat > $EEVTMPDIR/ee.diag <<'--%%--'\nsource diaglib.014\n"
"\n--%%--\nwish $EEVTMPDIR/ee.diag &\n"))
(eeb-define 'eediag-bounded 'eediag "----------\n" "\n#----------" t t)
Diagramas da minha tese de mestrado:
# «.variac» (to "variac")
# «.categs0» (to "categs0")
# «.assuntos» (to "assuntos")
# «.diamond1» (to "diamond1")
# «.diamond2» (to "diamond2")
# «.diamond3» (to "diamond3")
# «.construnat1» (to "construnat1")
# «.naoplanar» (to "naoplanar")
# «.planar» (to "planar")
# «.sombra1» (to "sombra1")
# «.sombra2» (to "sombra2")
# «.functor0» (to "functor0")
# «.functor1» (to "functor1")
# «.functor2» (to "functor2")
# «.tn1» (to "tn1")
# «.godement» (to "godement")
# «.adj-excoer» (to "adj-excoer")
# «.prod1» (to "prod1")
# «.prod2» (to "prod2")
# «.adj-sqrab» (to "adj-sqrab")
# «.adj-sqrabc» (to "adj-sqrabc")
# «.adj-sqrbcd» (to "adj-sqrbcd")
# «.adj-sqrexs» (to "adj-sqrexs")
# «.adj-bij» (to "adj-bij")
# «.adj-func1» (to "adj-func1")
# «.adj-Rid» (to "adj-Rid")
# «.adj-Rcomp» (to "adj-Rcomp")
# «.adj-demabc» (to "adj-demabc")
# «.adj-dembcd» (to "adj-dembcd")
# «.adj-big2» (to "adj-big2")
# «.adj-pipa» (to "adj-pipa")
# «.adj-2iso» (to "adj-2iso")
# «.prod3» (to "prod3")
# «.pblim» (to "pblim")
# «.eqlim» (to "eqlim")
# «.exlimit» (to "exlimit")
# «.2pbs» (to "2pbs")
# «.trads» (to "trads")
# «.Tab2ab» (to "Tab2ab")
# «.adj-sqrlog» (to "adj-sqrlog")
# «.classif-pb» (to "classif-pb")
# «.classif-ax» (to "classif-ax")
# «.manifold» (to "manifold")
# «.fibrados» (to "fibrados")
# «.fib-TM» (to "fib-TM")
Itatiaia:
# «.itat1» (to "itat1")
# «.cnatabcd» (to "cnatabcd")
# «.adj-sqrab» (to "adj-sqrab")
# «.itatiadjs» (to "itatiadjs")
# «.adj-qrrab» (to "adj-qrrab")
# «.adj-uid» (to "adj-uid")
# «.adj-mkite» (to "adj-mkite")
# «.adj-lkite» (to "adj-lkite")
# «.monad1» (to "monad1")
# «.monadel1» (to "monadel1")
# «.monadel2» (to "monadel2")
# «.monadel3» (to "monadel3")
# «.monadel4» (to "monadel4")
# «.monadel5» (to "monadel5")
# «.monadalg1» (to "monadalg1")
# «.monadalgm1» (to "monadalgm1")
# «.monadRL1» (to "monadRL1")
# «.monade1» (to "monade1")
# «.monadedem1» (to "monadedem1")
# «.monadq1» (to "monadq1")
# «.adjid-bcL» (to "adjid-bcL")
# «.adjid-bRc» (to "adjid-bRc")
# «.kleisli1old» (to "kleisli1old")
# «.kleisli1» (to "kleisli1")
# «.kleisli2» (to "kleisli2")
# «.kleisli2old» (to "kleisli2old")
# «.kleisli3» (to "kleisli3")
# «.kleisliadj0» (to "kleisliadj0")
Outros:
# «.fibrados2» (to "fibrados2")
# «.iimplica» (to "iimplica")
# «.iforall» (to "iforall")
# «.classq» (to "classq")
# «.condpowt» (to "condpowt")
# «.adjspreslims» (to "adjspreslims")
# «.linux-topics» (to "linux-topics")
# «.clasubT1» (to "clasubT1")
# «.clasubT2» (to "clasubT2")
# «.pbfg» (to "pbfg")
# «.boolpbs» (to "boolpbs")
# «.heytprod» (to "heytprod")
# «.clasubtt» (to "clasubtt")
# «.funandQ» (to "funandQ")
# «.funandQadj» (to "funandQadj")
# «.funQto» (to "funQto")
# «.histmat1» (to "histmat1")
# «.histmat2» (to "histmat2")
# «.netbasics» (to "netbasics")
# «.escripts» (to "escripts")
# «.adj-as-nt» (to "adj-as-nt")
# «.kan1» (to "kan1")
# «.adj-conv» (to "adj-conv")
# «.cat-nts» (to "cat-nts")
# «.adj-demabc-new» (to "adj-demabc-new")
# «.limSetC» (to "limSetC")
# «.monadresls» (to "monadresls")
# «.abcd» (to "abcd")
# «.idcond» (to "idcond")
# «.preslim» (to "preslim")
# «.dncforg» (to "dncforg")
# «.diagxy1» (to "diagxy1")
# «.phil1» (to "phil1")
#-------------------------------
#
# Cap. 1: Introdução
#
#----
# Problema variacional
# «variac» (to ".variac")
epsfile variac
# 5
# y j-->L
# ^ 3 ^ ^
# \->|4 /-->I
# s-->\ | /6 7
# 1 2 x
#
freetext s s 80 120
freetext x x 140 140 y y 100 100 j j 140 100 L L 180 100
freetext I I 200 120
auxiliary _xy * 120 120
auxiliary _xj * 140 120
auxiliary _xL * 160 120
morf s _xy e w
morf x y nw se
morf _xy _xj e w
morf x j n s
morf j L e w
morf x L ne sw
morf _xL I e w
#-------------------------------
# Primeira motivação para categorias
# «categs0» (to ".categs0")
epsfile categs0
freetext c c 140 96
freetext a a 100 140 a^b a^b 140 140 b b 180 140
freetext f f 115 111 g g 166 109
morf a^b a w e
morf a^b b e w
morf c a sw ne
morf c b se nw
morf c a^b s n
#-------------------------------
# lambda----Set-----NSA/SSA
# | _//| \ |
# | _/ / | \ |
# | / | | \ |
# DN------3ªI-----Topoi
# | \ | | \/ |
# | \/ | /\ |
# | /\ | / \ |
# Categs---Lógica---Intuic
#
# e mais: DN-NSA/SSA, DN-Intuic.
# «assuntos» (to ".assuntos")
epsfile assuntos
freetext lambda lambda 100 100
freetext DN DN 100 140
freetext Categs Categs 100 180
freetext Set Set 160 100
freetext I3 3a.I 160 140
freetext Logica Logica 160 180
freetext NSA NSA/SSA 220 100
freetext Topoi Topoi 220 140
freetext Intuic Intuic 220 180
linha lambda DN s n
linha lambda Set e w
linha DN Categs s n
linha DN Set nne sw
linha DN I3 e w
linha DN Logica sse nnw
linha DN NSA ne sw
linha DN Intuic se nw
linha Categs Set nne ssw
linha Categs Logica e w
linha Set I3 s n
linha Set NSA e w
linha Set Topoi se nnw
linha I3 Logica s n
linha I3 Topoi e w
linha I3 Intuic se nnw
linha Logica Topoi nne ssw
linha Logica Intuic e w
linha NSA Topoi s n
linha Topoi Categs sw ne
linha Topoi Intuic s n
#-------------------------------
#
# Cap. 2: Um pouco de ð-cálculo
#
#----
# (\x.+xx)((\y.-y2)5)
# +((\y.-y2)5)((\y.-y2)5)
# +((\y.-y2)5)((\z.-z2)5)
# (\x.+xx)(-52)
# +((\y.-y2)5)(-52)
# (-52)((\z.-z2)5)
# +(-52)(-52)
# «diamond1» (to ".diamond1")
epsfile diamond1
freetext a1 {(\x.+xx)((\y.-y2)5)} 195 63
freetext a2 {+((\y.-y2)5)((\y.-y2)5)} 157 88
freetext a3 {+((\y.-y2)5)((\z.-z2)5)} 155 113
freetext a4 {(\x.+xx)(-52)} 277 115
freetext a5 {+((\y.-y2)5)(-52)} 196 140
freetext a6 {+(-52)((\z.-z2)5)} 131 164
freetext a7 {+(-52)(-52)} 203 191
metaarrow' a1 ssw n a2
metaarrow' a1 sse n a4
metaarrow' a2 s n a3
metaarrow' a3 sse n a5
metaarrow' a3 ssw n a6
metaarrow' a4 s nne a7
metaarrow' a5 s n a7
metaarrow' a6 sse nnw a7
#-------------------------------
# «diamond2» (to ".diamond2")
epsfile diamond2
freetext A A 100 100
freetext B B 70 130 C C 130 130
freetext D D 100 160
morf A B sw ne
morf A C se nw
thin B D se nw
thin C D sw ne
#-------------------------------
# «diamond3» (to ".diamond3")
epsfile diamond3
freetext B B 100 100 D D 160 100
freetext A A 70 130 C C 130 130 E E 190 130 G G 250 130
freetext H H 100 160 I I 160 160 F F 220 160
freetext J J 130 190 K K 190 190
freetext L L 160 220
samedirs sw ne morf B A D C G F
samedirs se nw morf B C D E E F
samedirs se nw thin A H H J J L C I I K
samedirs sw ne thin C H E I I J F K K L
#-------------------------------
#
# Cap. 4: Categorias
#
#-----
# Primeiro lero sobre construções naturais
#
# a->b
# \ |
# v vv
# c->a'
# «construnat1» (to ".construnat1")
epsfile construnat1
freetext a a 100 100 b b 150 100
freetext c c 100 140 a' a' 150 140
morf a b e w
metaarrow' a sw nw c :f:
metaarrow' a s n c :g:
morf a a' se nw b a' s n
morf c a' e w
freetext f f 90 120
freetext g g 106 120
freetext id id 131 114
#-------------------------------
# Exemplo de um diagrama que nao é planar e
# tem problemas com fontes e poços.
#
# a<-b->c
# ^ |\^|
# | v/vv
# d->e->f
# ^ /
# |v
# g
# «naoplanar» (to ".naoplanar")
epsfile naoplanar
freetext a a 100 100 b b 140 100 c c 180 100
freetext d d 100 140 e e 140 140 f f 180 140
freetext g g 120 172
morf b a w e b c e w
morf d a n s b e s n b f se nw e c ne sw c f s n
morf d e e w e f e w
morf g d nw se e g sw ne
#-------------------------------
# Exemplo pro teorema do diagrama planar
#
# a->b->c
# \ | |
# vv v
# d->e
# \ |
# vv
# f
# «planar» (to ".planar")
epsfile planar
freetext a a 100 100 b b 140 100 c c 180 100
freetext d d 140 140 e e 180 140
freetext f f 180 180
morf a b e w b c e w
morf a d se nw b d s n c e s n
morf d e e w
morf d f se nw e f s n
#-------------------------------
# Lema da sombra
#
# _____
# _______/ \
# / /\ \
# / / \ \
# / f1 / g1 v h1 v
# a=====>b=====>c=====>d
# f2 g2 h2
# «sombra1» (to ".sombra1")
epsfile sombra1
freetext a a 100 100 b b 140 100 c c 180 100 d d 220 100
freetext f1 f1 120 90 f2 f2 120 116
freetext g1 g1 160 90 g2 g2 160 116
freetext h1 h1 200 90 h2 h2 200 116
metaarrow' a e w b :f1:
metaarrow' a se sw b :f2:
metaarrow' b e w c :g1:
metaarrow' b se sw c :g2:
metaarrow' c e w d :h1:
metaarrow' c se sw d :h2:
auxiliary /1 /1 115 75 /2 /2 165 75
auxiliary /3 /3 155 75 /4 /4 205 75
metaarrow a->c {[^ ne a] [^ n /1] [^ n /2] [^ nw c]}
metaarrow b->d {[^ ne b] [^ n /3] [^ n /4] [^ nw d]}
#-------------------------------
# Aplicação do lema da sombra
#
# _____
# _______/ \
# / /\ \
# / / \ \
# / f1 / g v h1 v
# b'====>a----->b=====>a'
# f2 h2
# «sombra2» (to ".sombra2")
epsfile sombra2
freetext b' b' 100 100 a a 140 100 b b 180 100 a' a' 220 100
freetext f1 f1 120 90 f2 f2 120 116
freetext g g 160 90
freetext h1 h1 200 90 h2 h2 200 116
freetext id1 id 140 58 id2 id 180 58
metaarrow' b' e w a :f1:
metaarrow' b' se sw a :f2:
metaarrow' a e w b :g:
metaarrow' b e w a' :h1:
metaarrow' b se sw a' :h2:
auxiliary /1 /1 115 75 /2 /2 165 75
auxiliary /3 /3 155 75 /4 /4 205 75
metaarrow b'->b {[^ ne b'] [^ n /1] [^ n /2] [^ nw b]}
metaarrow a->a' {[^ ne a] [^ n /3] [^ n /4] [^ nw a']}
#-------------------------------
# A condição que o funtor obedece
#
# >b-
# / \
# a---->c
# bF
# / \
# aF--->cF
#
# «functor0» (to ".functor0")
epsfile functor0
freetext a1 a 100 140 b1 b 140 120 c1 c 180 140
freetext a2 aF 100 175 b2 bF 140 155 c2 cF 180 175
morf a1 b1 ne w b1 c1 e nw a1 c1 e w
morf a2 b2 ne w b2 c2 e nw a2 c2 e w
R a1 a2 s n
R b1 b2 s n
R c1 c2 s n
setdragxy a1 a2
setdragxy b1 b2
setdragxy c1 c2
setdragxy a2 b2 c2
#-------------------------------
# Teoreminha de coerência para funtores: antes
#
# a
# |\
# v v
# b->c
# | |
# v v
# d->e
# «functor1» (to ".functor1")
epsfile functor1
freetext a1 a 118 101 b1 b 100 140 c1 c 140 140
freetext d1 d 100 180 e1 e 140 180
morf a1 b1 sw ne a1 c1 se nw b1 c1 e w
morf b1 d1 s n c1 e1 s n d1 e1 e w
#-------------------------------
# Teoreminha de coerência para funtores: depois
#
# a aF
# |\ | \
# v v v v
# b->c bF->cF
# | | | |
# v v v v
# d->e dF->eF
# «functor2» (to ".functor2")
epsfile functor2
freetext a1 a 118 101 b1 b 100 140 c1 c 140 140
freetext d1 d 100 180 e1 e 140 180
morf a1 b1 sw ne a1 c1 se nw b1 c1 e w
morf b1 d1 s n c1 e1 s n d1 e1 e w
freetext a2 aF 140 113 b2 bF 122 152 c2 cF 162 152
freetext d2 dF 122 192 e2 eF 162 192
morf a2 b2 sw n a2 c2 se n b2 c2 e w
morf b2 d2 s n c2 e2 s n d2 e2 e w
setdragxy a1 a2
setdragxy b1 b2
setdragxy c1 c2
setdragxy d1 d2
setdragxy e1 e2
setdragxy a2 b2 c2 d2 e2
#-------------------------------
# Transformações naturais
#
# a---->b
# | | | |
# | v | v
# | aG--|>bG
# | ^ | ^
# v/ v/
# aF--->bF
#
# «tn1» (to ".tn1")
epsfile tn1
freetext a a 100 100 b b 142 104
freetext aF aF 95 150
freetext aG aG 120 127
setdragxy a b
setdragxy aF aG
deltatext a b aF bF bF {aF} aG bG bG {aG}
samedirs e w morf a b aF bF aG bG
samedirs ne sw morf aF aG bF bG
samedirs s n R a aF b bF
samedirs se nww L a aG b bG
#-------------------------------
# Transformações naturais: produto de Godement
#
# O desenho em ascii é tão horrível que eu troquei
# por um bloco de caracteres aleatórios.
#
# 4G>PH=(f%d-@S[Wcf7p>Bup"dA^Gq|BH
# W\.yON+oXZy1FewzLjP+jom6Hr:YX+m)
# O>zYGbtA#$3oaJ3uOLHQ%#TcRjuN'E-y
# 4H+P+;QMXpCpP6oSRQ]'~[>aa5a-A)w~
# lOBe@1JP>L8ln1[u%hSD9=cN>t&a:%*@
# 2\aI\oGj$rxCFs\+@Wi->?\L`&j?P_u(
# %NKlE=NcI[o9kQ7?RtB'IR>'nTw>SurJ
# v9=,i3#fzoa;Fp/iR4W}b:;j^hrz]:q`
# *h2ei_fGt0Q:G0Eg(Y&g#QC2q]=\ys%+
# j>D!5J[>@pa-o@;[e`f;+ifsvc7k@Bw-
# spLHcm|)4bppQlKkp]oWO)pT/%~yVw93
# 2l@Nb\GM6&|K&TrgZ6w`Q-Nzc<3]1B2m
#
#icone '' 'every 1 to 12 do {every 1 to 32 do writes(char(?94 + 32)); write()}'
# «godement» (to ".godement")
epsfile godement
freetext a a 99 73
freetext b b 234 73
freetext aF aF 82 142
freetext aG aG 119 115
freetext aFH aFH 63 195
freetext aFK aFK 112 212
setdragxy a b
setdragxy aF aG
setdragxy aFH aFK
deltatext aF aG aFH aGH aGH {aG} aFK aGK aGK {aFK}
deltatext a b aF bF bF {aF} aG bG bG {aG}
deltatext a b aFH bFH bFH {aFH aFK} aGH bGH bGH {aG}
deltatext a b aFK bFK bFK {aFK} aGK bGK bGK {aFK}
samedirs e w morf a b aF bF aG bG aFH bFH aFK bFK aGH bGH aGK bGK
samedirs ne sw morf aF aG bF bG aFH aGH bFH bGH aFK aGK bFK bGK
samedirs see nw morf aFH aFK aGH aGK bFH bFK bGH bGK
samedirs s n R a aF b bF
samedirs se n L a aG b bG
samedirs ssw n R aF aFH aG aGH bF bFH bG bGH
samedirs sse n L aF aFK aG aGK bF bFK bG bGK
#-------------------------------
# Teoreminha de coerencia para adjuncoes (exemplo)
#
# a-->b-->c
# | | | aR->bR->cR
# v v v | | |
# d-->eL->fL v v v
# | | | dR->e-->f
# v v v | | |
# gL->hL->iL v v v
# g-->h-->i
# «adj-excoer» (to ".adj-excoer")
epsfile adj-excoer
freetext a a 100 100 b b 150 100
freetext d d 100 150
freetext aR aR 133 126
deltatext a d d g gL {}
deltatext a b b c c {} d e eL {b} e f fL {b} g h hL {b} h i iL {}
deltatext a aR b bR bR {aR} c cR cR {aR} d dR dR {aR} e eR e {aR}
deltatext a aR f fR f {aR} g gR g {aR} h hR h {aR} i iR i {aR}
samedirs e w morf a b b c d e e f g h h i
samedirs e w morf aR bR bR cR dR eR eR fR gR hR hR iR
samedirs s n morf a d d g b e e h c f f i
samedirs s n morf aR dR dR gR bR eR eR hR cR fR fR iR
samedirs se nw R a aR b bR c cR d dR
samedirs nw se L eR e fR f gR g hR h iR i
#-------------------------------
# Produtos 1
#
# x--->p
# |\ /|
# | \/ |
# | /\ |
# vv vv
# a b
# «prod1» (to ".prod1")
epsfile prod1
freetext x x 100 100 p p 155 100
freetext a a 115 145 b b 140 145
morf x p e w x a s nnw x b se nnw p a sw nne p b s nne
#-------------------------------
# Produtos 2
#
# /---->q
# x--->p=|
# |\ /|/|
# | \/ / /
# | /\/|/
# vv /vvv
# a < b
# «prod2» (to ".prod2")
epsfile prod2
freetext x x 97 95
freetext p p 142 108 q q 169 94
freetext a a 131 149 b b 149 149
morf x p see w x q e w
bij p q e sww
morf x a s nnw x b se nnw
morf p a sw n p b s n
morf q a sw nne q b s nne
#-------------------------------
#
# Cap. 4.8: Adjunções
#
#-----
# Adjunções: a bijeção num quadradinho.
#
# a====>aR
# | |
# | <-> |
# v v
# bL<b
#
# «adj-sqrab» (to ".adj-sqrab")
epsfile adj-sqrab
vtorre 100 100 a a bL bL
vtorre 140 100 aR aR b b
R' a aR
L' b bL
auxiliary _1 * 105 120
auxiliary _2 * 135 120
bij _1 _2 e w
#-------------------------------
# Adjunções: a condição de naturalidade sobre abc (quadrada).
#
# a====>aR
# | |
# | |
# v v
# b====>bR
# | |
# | |
# v v
# cL<c
#
# «adj-sqrabc» (to ".adj-sqrabc")
epsfile adj-sqrabc
vtorre 100 100 a a b b cL cL
vtorre 140 100 aR aR bR bR c c
R' a aR b bR
L' c cL
#-------------------------------
# Adjunções: a condição de naturalidade sobre bcd (quadrada).
#
# b====>bR
# | |
# | |
# v v
# cL<c
# | |
# | |
# v v
# dL<d
#
# «adj-sqrbcd» (to ".adj-sqrbcd")
epsfile adj-sqrbcd
vtorre 100 100 b b cL cL dL dL
vtorre 140 100 bR bR c c d d
R' b bR
L' c cL d dL
#-------------------------------
# Adjunções: as duas mais interessantes
#
# x===>x[] a===>a^b
# | | | |
# | <-> | | <-> |
# v v v v
# mL<m b>c<c
#
# «adj-sqrexs» (to ".adj-sqrexs")
epsfile adj-sqrexs
quadrado-adj 100 100 a2 a a^b a^b b>c b>c c c
quadrado-adj 200 100 x x xR {x[ ]} mL mL m m
#-------------------------------
# Adjunções: bijeção
#
# aR---->b
#
#
# v v
# aRL--->bL
# ^ ^
# \ /
# a
# «adj-bij» (to ".adj-bij")
epsfile adj-bij
reflec 100 100 aR aR aRL aRL a a
reflec 140 100 b b bL bL
hmorf aR b aRL bL
morf a bL ne s
#-------------------------------
# Adjunções: funtor 1
#
# aR---->bR
#
#
# v v
# aRL-->bRL
# ^ ^ ^
# \ / \
# a---->b
# «adj-func1» (to ".adj-func1")
epsfile adj-func1
reflec 100 100 aR aR aRL aRL a a
reflec 140 100 bR bR bRL bRL b b
hmorf aR bR aRL bRL a b
morf a bRL ne s
#-------------------------------
# Adjunções: o funtor R aplicado à identidade.
#
# id
# aR---->aR
#
#
# v id v
# aRL-->aRL
# ^ ^ ^
# \ / id\
# a---->a
#
# «adj-Rid» (to ".adj-Rid")
epsfile adj-Rid
reflec 100 100 aR aR aRL aRL a a
reflec 140 100 bR aR bRL aRL b a
hmorf aR bR aRL bRL a b
morf a bRL ne s
R a aR n se
R b bR n se
freetext id1 id 119 91
freetext id2 id 123 131
freetext id3 id 142 163
#-------------------------------
# Adjunções: o funtor R e a composição.
#
#
# aR---->bR--->cR
#
#
# v v v
# aRL-->bRL-->cRL
# ^ ^ ^ ^ ^
# \ / \ / \
# a---->b---->c
#
# «adj-Rcomp» (to ".adj-Rcomp")
epsfile adj-Rcomp
reflec 100 100 aR aR aRL aRL a a
reflec 140 100 bR bR bRL bRL b b
reflec 180 100 cR cR cRL cRL c c
hmorf aR bR aRL bRL a b
hmorf bR cR bRL cRL b c
morf a bRL ne s
morf b cRL ne s
R a aR n se
R b bR n se
R c cR n se
#-------------------------------
# Adjunções: a condição de naturalidade sobre abc (demonstração).
#
# aR---->bR--->c
#
#
# v v v
# aRL-->bRL--->cL
# ^ ^ ^ ^
# \ / \ /
# a---->b
#
#
# «adj-demabc» (to ".adj-demabc")
epsfile adj-demabc
reflec 100 100 aR aR aRL aRL a a
reflec 140 100 bR bR bRL bRL b b
reflec 180 100 c c cL cL
hmorf aR bR aRL bRL a b
hmorf bR c bRL cL
morf a bRL ne s
morf b cL ne s
R a aR n se
R b bR n se
#-------------------------------
# Adjunções: a condição de naturalidade sobre bcd (demonstração).
#
# bR---->c---->d
#
#
# v v v
# bRL--->cL--->dL
# ^ ^
# \ /
# b
#
#
# «adj-dembcd» (to ".adj-dembcd")
epsfile adj-dembcd
reflec 100 100 bR bR bRL bRL b b
reflec 140 100 c c cL cL
reflec 180 100 d d dL dL
hmorf bR c bRL cL
hmorf c d cL dL
morf b cL ne s
R b bR n se
#-------------------------------
# Adjunções: uma coisa grande entre os nossos dois funtores lógicos.
#
# b>c'<-----b>c<-----a<----a'
#
#
# v v v v
# b&(b>c')<--b&(b>c)<--b&a<--b&a'
# \ / \ /
# \ / \ /
# v v v v
# c'<-------c
# «adj-big2» (to ".adj-big2")
epsfile adj-big2
freetext bc' b>c' 100 100 bc b>c 165 100
freetext bbc' b^(b>c') 100 150
freetext c' c' 144 180
deltatext bc' bc bc a a {} a a' a' {}
deltatext bc' bc bbc' bbc b^(b>c) {} bbc ba b^a {} ba a'b b^a' {}
deltatext bc' bc c' c c {}
samedirs w e morf a' a a bc bc bc' a'b ba ba bbc bbc bbc' c c'
samedirs s n R bc' bbc' bc bbc a ba a' a'b
morf bbc c' s ne
morf ba c s ne
morf bbc' c' s nw
morf bbc c s nw
L c' bc' n se
L c bc n se
#-------------------------------
# Adjunções: demonstração de que duas adjuntas são isomorfas.
#
# aR--->aR'--->aR
#
#
# v v v
# aRL->aR'L-->aRL
# ^ ^ ^
# \ | /
# ---a---
# «adj-pipa» (to ".adj-pipa")
epsfile adj-pipa
freetext aR aR 100 100 aR' aR' 140 100
freetext aRL aRL 100 140
freetext a a 140 170
deltatext aR aR' aR' aR2 aR {} aRL aR'L aR'L {} aR'L aRL2 aRL {}
samedirs e w morf aR aR' aR' aR2 aRL aR'L aR'L aRL2
samedirs s n L aR aRL aR' aR'L aR2 aRL2
morf a aRL nw sse a aR'L n s a aRL2 ne ssw
#-------------------------------
# Adjunções: TN entre duas adjuntas pro mesmo funtor.
#
# aR--->bR
# \ \
# aR'-->bR'
# v v
# aRL->bRL
# ^\ v ^ \v
# | aR'L->bR'L
# \ ^ \ ^
# a---->b
#
# «adj-2iso» (to ".adj-2iso")
epsfile adj-2iso
freetext aR aR 100 100 bR bR 160 100 aR' aR' 130 120 aRL aRL 100 140
freetext a a 115 185
deltatext aR aRL aR' aR'L aR'L {}
deltatext aR bR aR' bR' bR' {} aRL bRL bRL {} aR'L bR'L bR'L {} a b b {}
samedirs e w morf aR bR aR' bR' aRL bRL aR'L bR'L a b
samedirs sse nnw morf aR aR' bR bR' aRL aR'L bRL bR'L
samedirs s n L aR aRL bR bRL aR' aR'L bR' bR'L
samedirs nw s morf a aRL b bRL
samedirs ne s morf a aR'L b bR'L
#-------------------------------
#
# Sec. 4.10: Limites
#
#----
# Produto de três caras
# «prod3» (to ".prod3")
epsfile prod3
freetext x x 100 100 Plong (a,b,c) 160 100
freetext a a 115 150 b b 130 150 c c 145 150
auxiliary P P 160 100
morf x Plong e w
morf x a s nnw x b sse nnw x c se nnw
morf P a sw nne P b ssw nne P c s nne
#-------------------------------
# Pullback
# «pblim» (to ".pblim")
epsfile pblim
freetext a a 120 140
freetext b b 140 115
freetext c c 140 140
freetext x x 35 55
freetext Plong (a,b)|c 108 55
auxiliary P P 108 55
setdragxy Plong P
morf x Plong e w a c e w b c s n
morf x a s nw x c sse nw x b se nw
morf P a s nnw P c sse nnw P b se nnw
#-------------------------------
# Equalizador
# «eqlim» (to ".eqlim")
epsfile eqlim
freetext x x 80 100 E a|f=g 140 100
freetext a a 140 160 b b 172 160
freetext f f 151 152 g g 155 174
morf x E e w
morf x a se nw x b see nw
morf E a s n E b sse nnw
metaarrow' a e w b :f:
metaarrow' a se sw b :g:
#-------------------------------
# Um limite grandão, versão nova.
# «exlimit» (to ".exlimit")
epsfile exlimit
freetext a a 105 165
freetext b b 136 173
freetext c c 168 155
freetext d d 196 154
freetext L L 169 67
freetext x x 90 67
freetext f f 121 163
freetext g g 152 151
freetext h h 158 175
freetext k k 180 148
metaarrow' a e w b
metaarrow' c w ne b :f:
metaarrow' c sw e b :g:
metaarrow' c e w d
morf x L e w
morf L a sw ne L b sw n L c s n L d se n
morf x a sw n x b s nw x c se nw x d se nw
#-------------------------------
# Dois pullbacks colados.
# «2pbs» (to ".2pbs")
epsfile 2pbs
freetext x x 59 82 a' a' 87 82
freetext a a 100 100 b b 140 100 c c 180 100
freetext d d 100 140 e e 140 140 f f 180 140
samedirs e w morf a b b c d e e f
samedirs s n morf a d b e c f
morf a' c e nw a' d s nw x a see w x a' e w
#-------------------------------
#
# Cap. 5: O teorema da dedução
#
#----
# DN<--->DN+T
# .. ^
# ../.
# / ..
# / v
# CCC<-->CCC+T
# «trads» (to ".trads")
epsfile trads
freetext DN DN 100 100
freetext DN+T DN+T 160 100
freetext CCC CCC 100 160
freetext CCC+T CCC+T 160 160
morf DN DN+T e w DN+T DN sw se
morf CCC CCC+T e w CCC+T CCC sw se
# (find-fline "gray50.bmp")
set ArrowOptions(dim) \
[concat $ArrowOptions(m) -stipple @gray50.bmp]
morf CCC DN+T nne ssw
metaarrow' DN sse nnw CCC+T {} dim
#-------------------------------
# Explicações sobre o isomorfismo entre §->(a->b) e a->b.
# b>c<---T T==>T^b<->b
# | |
# | |
# v v v v
# b^(b>c)<--T^b<->b b>c<==c
# \ /
# v v
# c
#
# a1a2 b1b2b5
# a3a4a5 b3b4
# a6
# «Tab2ab» (to ".Tab2ab")
epsfile Tab2ab
reflec' 100 100 a1 b>c a3 b^(b>c) a6 c
reflec' 170 100 a2 T a4 T^b
hmorf' a2 a1 a4 a3
morf a4 a6 ssw ne
L a6 a1 n se
freetext a5 b 210 150
bij a4 a5 e w
freetext b1 T 260 100 b2 T^b 310 100 b5 b 350 100
freetext b3 b>c 260 150 b4 c 310 150
morf b1 b3 s n b2 b4 s n
bij b2 b5 e w
R b1 b2 e w
L b4 b3 w e
setdragxy a1 a2 a3 a4 a5 a6
setdragxy b1 b2 b3 b4 b5
#-------------------------------
#
# Cap. 6: A álgebra dos valores de verdade
#
#----
# Adjunções: /\ e -> como adjuntas
#
# A===>A^B
# | |
# | <-> |
# v v
# B>C<B
#
# «adj-sqrlog» (to ".adj-sqrlog")
epsfile adj-sqrlog
vtorre 100 100 A A B>C B>C
vtorre 140 100 A^B A^B B B
R' A A^B
L' B B>C
auxiliary _1 * 105 120
auxiliary _2 * 135 120
bij _1 _2 e w
#-------------------------------
#
# Cap. 8: Topoi
#
#----
# Subobjetos e seus pullbacks amigos:
#
# a|T------\
# |\ v
# (a,T)|t-->T (a,T)|t-->T a|T---->T
# | | | | | | |
# | | | | | | |
# | | \ | | | |
# v v vv v v v
# a----->t a----->t a----->t
#
# «classif-pb» (to ".classif-pb")
epsfile classif-pb
quadrado 100 100 a1 (a,T)|t a2 T a3 a a4 t
quadrado 190 100 b1 (a,T)|t b2 T b3 a b4 t
quadrado 260 100 c1 a|T c2 T c3 a c4 t
freetext b0 a|T 152 75
bij b0 b1 se nnw
morf b0 b2 e nw
morf b0 b3 s nw
#-------------------------------
# Axioma do classificador.
# a'-->T
# | |
# |- |
# v v v
# a--->t
# «classif-ax» (to ".classif-ax")
epsfile classif-ax
quadrado 100 100 a' a' T T a a t t
auxiliary * * 124 113
metaarrow claxiom {[^+ [^ sw *] -15 0 -5 0 0 5 0 15]} thin
# (find-fline "diaglib.013" "metaarrow")
#-------------------------------
#
# Cap. ?: Onde nós gostaríamos de chegar
#
#----
# Variedades
#
# f
# ^
# /
# t->m--------->m'
# ^ ^ ^ ^
# / \ / \
# v v v v
# u v u' v'
#
# «manifold» (to ".manifold")
epsfile manifold
freetext t t 107 111
freetext f f 152 100
freetext m m 135 125 m' m' 190 125
freetext u u 120 160 u' u' 175 160
freetext v v 150 160 v' v' 205 160
morf t m e w m m' e w m f ne sw
gbij u m n ssw
gbij v m n sse
gbij u' m' n ssw
gbij v' m' n sse
#-------------------------------
# m<---p
# ^ ^
# : : m<---p
# v v ^ ^
# ui<-ui,gi : :
# v v
# ui<-ui,gi
#
# «fibrados» (to ".fibrados")
epsfile fibrados
fibrado 100 100 m m p p ui ui ui,gi ui,gi
fibrado 164 124 n n q q vj vj vj,hj vj,hj
morf m n see w
morf p q e nww
gmorf ui vj see w
gmorf ui,gi vj,hj e nnw
#-------------------------------
# m<---Tm
# ^ ^
# : : n<---Tn
# v v ^ ^
# u<-u,u_t : :
# v v
# v<-v,v_t
#
# «fib-TM» (to ".fib-TM")
epsfile fib-TM
fibrado 100 100 p p Tp Tp u u u,u_t u,u_t
fibrado 164 124 q q Tq Tq v v v,v_t v,v_t
morf p q see w
morf Tp Tq e nww
gmorf u v see w
gmorf u,u_t v,v_t e nnw
#----
# Maio/99: notas de Itatiaia
#-------------------------------
# Primeira adjunção
#
# a===>a^b
# | |
# | <-> |
# v v
# b>c<c
#
# «itat1» (to ".itat1")
epsfile itat1
quadrado-adj 100 100 a2 a a^b a^b b>c b>c c c
#-------------------------------
# Primeiro diagrama para construções naturais
#
# f g h
# a---->b---->c---->d
#
# «cnatabcd» (to ".cnatabcd")
epsfile cnatabcd
freetext a a 100 100 b b 140 100 c c 180 100 d d 220 100
freetext f f 120 90 g g 160 90 h h 200 90
samedirs e w morf a b b c c d
#-------------------------------
# Adjunções: a bijeção num quadradinho.
#
#
# «adj-sqrab» (to ".adj-sqrab")
epsfile adj-sqrab
vtorre 100 100 a a bL bL
vtorre 140 100 aR aR b b
R' a aR
L' b bL
auxiliary _1 * 105 120
auxiliary _2 * 135 120
bij _1 _2 e w
#-------------------------------
# Adjunções: muitas (Ititaia).
#
# a====>aR a===>a^b
# | | | |
# | | | <-> | 4
# v v v v
# b====>bR b====>bR b====>bR b>c<c
# | | | | | |
# | <-> | | <-> | | <-> |
# v v v v v v x===>x[]
# cL<c cL<c cL<c | |
# | | | <-> | 5
# | | v v
# v v mL<m
# 1 2 dL<d
#
# 3
# «itatiadjs» (to ".itatiadjs")
epsfile itatiadjs
quadrado-adj 100 100 b1 b bR1 bR cL1 cL c1 c
quadrado-adj 170 100 b2 b bR2 bR cL2 cL c2 c
quadrado-adj 240 100 b3 b bR3 bR cL3 cL c3 c
freetext a2 a 170 60 aR2 aR 210 60
setdragxy a2 aR2 b2 bR2 cL2 c2 1_b2c2 2_b2c2
freetext dL3 dL 240 180 d3 d 280 180
setdragxy b3 bR3 cL3 c3 dL3 d3 1_b3c3 2_b3c3
samedirs s n morf a2 b2 aR2 bR2 cL3 dL3 c3 d3
R' a2 aR2
L' d3 dL3
quadrado-adj 310 60 x x xR {x[ ]} mL mL m m
quadrado-adj 310 140 a4 a ab a^b bc b>c c4 c
#-------------------------------
# Adjunções: quadrado e retangulos, usando "a"s, "b"s e plics
#
# a'==>a'R
# | |
# | |
# v v
# a====>aR a====>aR a====>aR
# | | | | | |
# | <-> | | <-> | | <-> |
# v v v v v v
# bL<b bL<b bL<b
# | |
# | |
# v v
# 1 2 b'L<b'
#
# 3
# «adj-qrrab» (to ".adj-qrrab")
epsfile adj-qrrab
quadrado-adj 100 100 b1 a bR1 aR cL1 bL c1 b
quadrado-adj 170 100 b2 a bR2 aR cL2 bL c2 b
quadrado-adj 240 100 b3 a bR3 aR cL3 bL c3 b
freetext a2 a' 170 60 aR2 a'R 210 60
setdragxy a2 aR2 b2 bR2 cL2 c2 1_b2c2 2_b2c2
freetext dL3 b'L 240 180 d3 b' 280 180
setdragxy b3 bR3 cL3 c3 dL3 d3 1_b3c3 2_b3c3
samedirs s n morf a2 b2 aR2 bR2 cL3 dL3 c3 d3
R' a2 aR2
L' d3 dL3
#-------------------------------
# id
# aR--->aR
#
#
# v id v
# aRL-->aRL
# ^ ^
# \ /
# a
#
# «adj-uid» (to ".adj-uid")
epsfile adj-uid
kite 100 100 a a aR1 aR aRL1 aRL aR2 aR aRL2 aRL
freetext idR id 120 90 idRL id 120 130
#-------------------------------
# x[]--->m
#
#
# v v
# x[]L--->mL
# ^ ^
# \ /
# x
#
# «adj-mkite» (to ".adj-mkite")
epsfile adj-mkite
kite 100 100 a x aR {x[ ]} aRL {x[ ]L} b m bL mL
#-------------------------------
# b>c<-----a
#
#
# v v
# (b>c)&b<--a&b
# \ /
# \ /
# v v
# c
# «adj-lkite» (to ".adj-lkite")
epsfile adj-lkite
freetext bc b>c 100 100 a a 155 100 bbc (b>c)^b 100 140 c c 125 170
deltatext bc bbc a ba a^b {}
samedirs s n R bc bbc a ba
morf a bc w e ba bbc w e bbc c s nw ba c s ne
#-------------------------------
#epsfile adj-uid
# OLD - use the other adj-uid diag instead
# u
# bLR--->b
#
#
# v v
# bLRL--->bL
# ^ ^
# cou\ / id
# bL
reflec 100 100 bLR bLR bLRL bLRL bL0 bL
reflec 140 100 b b bL bL
hmorf bLR b bLRL bL
morf bL0 bL ne s
freetext cou cou 123 91 u u 97 159 id id 145 159
#-------------------------------
# Mônadas
#
# eT mT
# aT===>aTT<===aTTT
# | e / m
# id| /m
# | /
# v v
# aT'
#
# «monad1» (to ".monad1")
epsfile monad1
freetext aT aT 100 100 aTT aTT 145 100 aTTT aTTT 195 100
freetext aT' aT' 100 145
freetext eT eT 119 89 mT mT 171 88
freetext e e 117 111 m m 169 111
freetext id id 92 122 m' m 134 127
metaarrow' aT nee nww aTT :up:
metaarrow' aTTT nww nee aTT :up:
morf aT aTT see sww aTTT aTT sww see aT aT' s n aTT aT' ssw ne
#-------------------------------
# Mônadas: a categoria de Eilenbeg-Moore (1)
#
# a-->aT-->aTT
# \ | |
# id\f| ==> |fT
# vv v
# a--->aT
# «monadel1» (to ".monadel1")
epsfile monadel1
freetext a0 a 100 100 aT aT 140 100 aTT aTT 180 100
freetext a a' 140 140 aT' aT' 180 140
freetext id id 114 128 f f 134 118 fT fT 190 120
freetext *0 0 145 120 *1 1 175 120
aux *0 *1
morf a0 aT e w aT aTT e w
morf a0 a se nw aT a s n aTT aT' s n
morf a aT' e w
T *0 *1 e w
#-------------------------------
# Mônadas: a categoria de Eilenbeg-Moore (2)
#
# a<---aT
# | |
# | ==> |
# v v
# b<---bT
# «monadel2» (to ".monadel2")
epsfile monadel2
freetext a a 100 100 aT aT 140 100
freetext b b 100 140 bT bT 140 140
freetext *0 0 105 120 *1 1 135 120
aux *0 *1
morf aT a w e
morf a b s n aT bT s n
morf bT b w e
T *0 *1 e w
#-------------------------------
# Mônadas: a categoria de Eilenbeg-Moore (3)
#
# a'==>a'T<--a'T
# | | |
# | | ==> |
# v v v
# a====>aT<--aTT
# | | |
# | <-> | ==> |
# v v v
# b<====b<---bT
# | | |
# | | ==> |
# v v v
# b'<===b'<--b'T
# «monadel3» (to ".monadel3")
epsfile monadel3
freetext a0' a' 100 100 a1' a'T 140 100 a2' a'T 180 100
freetext a0 a 100 140 a1 aT 140 140 a2 aTT 180 140
freetext b0 b 100 180 b1 b 140 180 b2 bT 180 180
freetext b0' b' 100 220 b1' b' 140 220 b2' b'T 180 220
freetext *0 * 145 120 *1 * 175 120
freetext *2 * 145 160 *3 * 175 160
freetext *4 * 145 200 *5 * 175 200
freetext *6 * 105 160 *7 * 135 160
aux *0 *1 *2 *3 *4 *5 *6 *7
samedirs w e morf a2' a1' a2 a1 b2 b1 b2' b1'
samedirs s n morf a0' a0 a1' a1 a2' a2 a0 b0 a1 b1 a2 b2 b0 b0' b1 b1' b2 b2'
samedirs e w R a0' a1' a0 a1
samedirs w e L b1 b0 b1' b0'
samedirs e w T *0 *1 *2 *3 *4 *5
bij *6 *7 e w
#-------------------------------
# Mônadas: a categoria de Eilenbeg-Moore (4)
#
# b====>bT<--bTT
# | | |
# | <-> | ==> |
# v v v
# b<====b<---bT
# «monadel4» (to ".monadel4")
epsfile monadel4
freetext a0 b 100 100 a1 bT 140 100 a2 bTT 180 100
freetext b0 b 100 140 b1 b 140 140 b2 bT 180 140
freetext *0 * 105 120 *1 * 135 120
freetext *2 * 145 120 *3 * 175 120
aux *0 *1 *2 *3
freetext f f 146 113 f1 f 160 149 fT fT 189 119
freetext m m 162 91 id id 91 118
R a0 a1 e w
morf a2 a1 w e a0 b0 s n a1 b1 s n a2 b2 s n b2 b1 w e
L b1 b0 w e
bij *0 *1 e w
T *2 *3 e w
#-------------------------------
# Mônadas: a categoria de Eilenbeg-Moore (5)
#
# a====>aT<--aTT
# | | |
# | <-> | ==> |
# v v v
# aT<===aT<--aTT
# «monadel5» (to ".monadel5")
epsfile monadel5
freetext a0 a 100 100 a1 aT 140 100 a2 aTT 180 100
freetext b0 aT 100 140 b1 aT 140 140 b2 aTT 180 140
freetext *0 * 105 120 *1 * 135 120
freetext *2 * 145 120 *3 * 175 120
aux *0 *1 *2 *3
freetext m1 m 159 91
freetext m2 m 160 149
freetext m3 e 91 121
R a0 a1 e w
morf a2 a1 w e a0 b0 s n a1 b1 s n a2 b2 s n b2 b1 w e
L b1 b0 w e
bij *0 *1 e w
T *2 *3 e w
#-------------------------------
# Mônadas: álgebras
#
# e pT
# a--->aT<===aTT
# | / m
# id| /p
# | /
# v v
# a'
#
# «monadalg1» (to ".monadalg1")
epsfile monadalg1
freetext a a 100 100 aT aT 145 100 aTT aTT 195 100
freetext a' a' 100 145
freetext e e 121 92 pT pT 171 88
freetext m m 169 111
freetext id id 92 122 p p 131 126
metaarrow' aTT nww nee aT :up:
morf a aT e w aTT aT sww see a a' s n aT a' ssw ne
#-------------------------------
# Mônadas: morfismos de álgebras
#
# p
# c<--cT
# | |
# f| |fT
# v q v
# d<--dT
#
# «monadalgm1» (to ".monadalgm1")
epsfile monadalgm1
freetext c c 100 100 cT cT 140 100
freetext d d 100 140 dT dT 140 140
freetext p p 120 90 f f 92 120 fT fT 150 120 q q 120 131
morf cT c w e c d s n cT dT s n dT d w e
#-------------------------------
# Mônadas: os dois funtores da adjunção
#
# m
# a>aT<--aTT
# | | |
# f| |fT |fTT
# v v v
# b>bT<--bTT
# m
#
# p
# c<===c<---cT
# | | |
# g| |g |gT
# v v v
# d<===d<---dT
# q
#
# «monadRL1» (to ".monadRL1")
epsfile monadRL1
freetext a a 100 100 aT aT 140 100 aTT aTT 180 100
freetext b b 100 140 bT bT 140 140 bTT bTT 180 140
freetext c c 100 180 c' c 140 180 cT cT 180 180
freetext d d 100 220 d' d 140 220 dT dT 180 220
freetext f f 91 120 fT fT 150 120 fTT fTT 192 120
freetext m m 160 90 m' m 160 150
morf aTT aT w e a b s n aT bT s n aTT bTT s n bTT bT w e
R' a aT
R' b bT
freetext g g 91 200 g' g 148 200 gT gT 191 200
freetext p p 160 170 q q 160 229
morf cT c' w e c d s n c' d' s n cT dT s n dT d' w e
L' c' c
L' d' d
#-------------------------------
# Mônadas: o "eigen" como unidade
#
# m
# b>bT<--bTT
# | | |
# e| |id |id
# v v m v
# bT<==bT<--bTT
# | | |
# g| |g |gT
# v v v
# c<===c<---cT
# q
#
# «monade1» (to ".monade1")
epsfile monade1
freetext x1 b 100 100 x2 bT 140 100 x3 bTT 180 100
freetext x4 bT 100 140 x5 bT 140 140 x6 bTT 180 140
freetext x7 c 100 180 x8 c 140 180 x9 cT 180 180
R' x1 x2
L' x5 x4
L' x8 x7
samedirs w e morf x3 x2 x6 x5 x9 x8
samedirs s n morf x1 x4 x2 x5 x3 x6 x4 x7 x5 x8 x6 x9
freetext m1 m 160 92 e e 92 120 id1 id 149 120 id2 id 189 120
freetext m2 m 160 132 g1 g 92 160 g2 g 147 160 gT gT 190 160
freetext q q 160 187
#-------------------------------
# Mônadas: o "eigen" como unidade (demonstração, estranha)
#
# e
# b--->bT'
# / | / | \
# / e|>|eT \
# | vv v |
# f| bT<-bTT |fT
# | | | |
# \ g|>|gT /
# v v v v
# c<---cT
# q
#
# «monadedem1» (to ".monadedem1")
epsfile monadedem1
freetext b b 100 100 bT' bT' 140 100
freetext bT bT 100 140 bTT bTT 140 140
freetext c c 100 180 cT cT 140 180
freetext e e 93 122 eT eT 149 122
freetext g g 93 158 gT gT 149 158
freetext f f 65 140 fT fT 180 140
freetext e' e 120 92 m m 122 146 q q 122 187
morf b bT' e w b bT s n bT' bT sw ne bT' bTT s n
morf bTT bT w e bT c s n bTT cT s n cT c w e
auxiliary e1 * 105 120 e2 * 135 120
auxiliary g1 * 105 160 g2 * 135 160
R' e1 e2
R' g1 g2
auxiliary f' * 47 140 fT' * 193 140
metaarrow b->c {[^ w b] [^ c f'] [^ w c]}
metaarrow bT'->cT {[^ e bT'] [^ c fT'] [^ e cT]}
#-------------------------------
# Mônadas: o zeta (i.e., q) como counidade
#
# m
# a>aT<--aTT
# | | |
# f| |fT |fTT
# v v m v
# b>bT<--bTT
# | | |
#id| |q |qT
# v v q v
# b<===b<----bT
#
# «monadq1» (to ".monadq1")
epsfile monadq1
freetext x1 a 100 100 x2 aT 140 100 x3 aTT 180 100
freetext x4 b 100 140 x5 bT 140 140 x6 bTT 180 140
freetext x7 b 100 180 x8 b 140 180 x9 bT 180 180
R' x1 x2
R' x4 x5
L' x8 x7
samedirs w e morf x3 x2 x6 x5 x9 x8
samedirs s n morf x1 x4 x2 x5 x3 x6 x4 x7 x5 x8 x6 x9
freetext m1 m 160 92 e e 92 120 id1 id 149 120 id2 id 189 120
freetext m2 m 160 132 g1 g 92 160 g2 g 147 160 gT gT 190 160
freetext q q 160 187
# (incompleto, né?)
#-------------------------------
# Adjunções: operações com unidades e counidades (b->cL => b'->cL')
#
# b'
# <|
# b>bR |
# | | => v
# | | bRL
# | v |
# | cLR |
# v > | |
# cL | |
# <==v v
# c==>cL'
#
# «adjid-bcL» (to ".adjid-bcL")
epsfile adjid-bcL
freetext b b 100 100 cL cL 100 160
freetext bR bR 140 100 cLR cLR 140 140 c c 140 180
freetext b' b' 180 80 bRL bRL 180 120 cL' cL' 180 180
samedirs s n morf b cL bR cLR cLR c b' bRL bRL cL'
R b bR e w; R cL cLR nee sww; R b' bR sww nee
L c cL nww see; L bR bRL see nww; L c cL' e w
#-------------------------------
# Adjunções: operações com unidades e counidades (b->cL => b'->cL')
#
# bR'<b
# | |>
# | | bR
# | v <==|
# | bRL |
# v | |
# cLR | |
# | <v v
# | cL<==c
# v ==>
# c'
#
# «adjid-bRc» (to ".adjid-bRc")
epsfile adjid-bRc
freetext bR' bR' 100 100 cLR cLR 100 160 c' c' 100 200
freetext b b 140 100 bRL bRL 140 140 cL cL 140 180
freetext bR bR 180 120 c c 180 180
samedirs s n morf bR' cLR cLR c' b bRL bRL cL bR c
R b bR' w e; R cL cLR nww see; R b bR see nww
L c' cL nee sww; L bR bRL sww nee; L c cL w e
#-------------------------------
# Kleisli 1 (antigo, obsoleto)
#
# b
# |>
# e| b bT
# v <== \ \
# bT \g \gT
# | v v
# gL| c cT<-cTT
# v <== m
# cT
#
# «kleisli1old» (to ".kleisli1old")
epsfile kleisli1old
freetext b' b 100 80 bT' bT 100 120 cT' cT 100 160
freetext b b 140 100 bT bT 175 100
freetext c c 140 140 cT cT 175 140 cTT cTT 216 140
freetext e e 92 100 gL gL 90 140 g g 162 115 gT gT 206 116 m m 196 147
morf b' bT' s n bT' cT' s n b cT se nw bT cTT se nw cTT cT w e
R b' b see nww
L b bT' sww nee
L c cT' sww nee
#-------------------------------
# Kleisli 1
#
# a
# \
# v
# b bT
# \ \
# v v
# c cT<-cTT
# \ \ \
# v v v
# d dT<-dTT<-dTTT
#
# «kleisli1» (to ".kleisli1")
epsfile kleisli1
kleislirow 100 100 a
kleislirow 100 140 b bT
kleislirow 100 180 c cT cTT
kleislirow 100 220 d dT dTT dTTT
samedirs se nw morf a bT b cT c dT
samedirs w e morf cTT cT dTT dT
samedirs se nnw morf bT cTT cT dTT cTT dTTT
samedirs w e morf dTTT dTT
setdragxy bT cT dT cTT dTT dTTT
setdragxy cTT dTT dTTT
#-------------------------------
# Kleisli 2
#
# a
# \
# \
# v
# b-->bT
# \ \
# v v
# cT'->cTT'
# | / \
# v v \
# c-->cT \
# \ \ \
# v v v
# dT'->dTT'<-dTTT'
# | / /
# v v v
# d-->dT<--dTT
#
# «kleisli2» (to ".kleisli2")
epsfile kleisli2
kleislirow 100 100 a
kleislirow 100 140 b bT
kleislirow 100 180 {} cT' cTT'
kleislirow 100 205 c cT
kleislirow 100 245 {} dT' dTT' dTTT'
kleislirow 100 270 d dT dTT
samedirs se nw morf a bT b cT' c dT'
samedirs e w morf b bT cT' cTT' c cT dT' dTT' d dT
thin bT cTT' se nnw cTT' dTTT' s n cT dTT' se nnw
samedirs s n morf cT' cT dT' dT
samedirs sw ne morf cTT' cT dTT' dT
samedirs w e morf dTTT' dTT' dTT dT
thin dTTT' dTT ssw nee
#-------------------------------
# Kleisli 2old
#
# a
# |\
# v v
# b->bT
# |\ \
# v v v
# c->cT<-cTT
# |\ \ \
# v v v v
# d->dT<-dTT<-dTTT
#
# «kleisli2old» (to ".kleisli2old")
epsfile kleisli2old
kleislirow 100 100 a
kleislirow 100 140 b bT
kleislirow 100 180 c cT cTT
kleislirow 100 220 d dT dTT dTTT
samedirs se nw morf a bT b cT c dT
samedirs w e morf cTT cT dTT dT
samedirs se nnw thin bT cTT cT dTT cTT dTTT
samedirs w e thin dTTT dTT
# samedirs s n morf a b b c c d
samedirs e w morf b bT c cT d dT
#-------------------------------
# Kleisli 3
#
# b->bT
# \ \
# v v
# cT'>cTT
# | /
# vv
# cT
#
# «kleisli3» (to ".kleisli3")
epsfile kleisli3
kleislirow 100 100 b bT
kleislirow 100 140 "" cT' cTT
kleislirow 100 170 "" cT
morf b bT e w b cT' se nw cT' cTT e w cT' cT s n cTT cT ssw ne
thin bT cTT se nnw
#-------------------------------
# Kleisli: os dois funtores
#
# a>a
# | |\
# f| |f\fK
# v v ev
# b>b-->bT
# | \
# | \
# v v
# cT<==c cT
# | \ \
# gL| \g \gT
# v v v
# dT<==d dT<--dTT
# m
#
# «kleisliadj0» (to ".kleisliadj0")
epsfile kleisliadj0
proc krow {x y tag txt args} {
freetext $tag $txt $x $y
eval kleislirow [expr $x + 40] $y $args
}
krow 100 100 a0 a a
krow 100 140 b0 b b bT
krow 100 180 c0 cT c cT
krow 100 220 d0 dT d dT dTT
freetext f0 f 94 121 f f 144 121 fK fK 165 115 e e 152 133
freetext gL gL 90 200 g g 164 193 gT gT 209 191 m m 197 227
samedirs s n morf a0 b0 a b b0 c0 c0 d0
samedirs se nw morf a bT b cT c dT
morf b bT e w cT dTT se nnw dTT dT w e
R' a0 a
R' b0 b
L' c c0
L' d d0
#-------------------------------
# Fim das notas de Itatiaia (acho)
#-------------------------------
# p f y_k
#
# m m,f_i m,y_ik
#
# x_j x_j,f_i x_j,y_ik
# «fibrados2» (to ".fibrados2")
epsfile fibrados2
freetext p p 107 100
freetext f f 140 100
freetext y y_k 200 100
freetext m m 100 140
freetext mf m,f_i 140 140
freetext my m,y_ik 200 140
freetext x x_j 100 188
freetext xf x_j,f_i 140 188
freetext xy x_j,y_ik 200 188
gbij p mf se nw f y e w m x s n
gbij mf my e w mf xf s n my xy s n xf xy e w
#-------------------------------
# A internalização do "implica" num topos.
#
# T->t|P T->t|Q
# ----------------
# a->t|P a->t|Q T->t|P,t|Q
# -------------- --------------
# a->t|P,t|Q t|P,t|Q->t|P^Q
# ----------------------------
# a->t|P^Q a->t|P
# --------------------------
# a|P->Q->a
# ----------
# a->t|P->Q
# «iimplica» (to ".iimplica")
epsfile iimplica
freetext a a 157 108
freetext T T 152 147
freetext t|P t.P 109 182
freetext t|Q t.Q 218 182
freetext t|P,t|Q t.P,t.Q 165 182
freetext t|P^Q t.P^Q 203 220
freetext a|P->Q a|P->Q 157 72
freetext t|P->Q t.P->Q 212 108
morf a t|P sw n
morf a t|Q se n
morf a t|P,t|Q s n
gmorf t|P,t|Q t|P w e
gmorf t|P,t|Q t|Q e w
morf T t|P sw ne
morf T t|Q se nw
morf T t|P,t|Q s nnw
morf t|P,t|Q t|P^Q s nnw
morf a t|P^Q sse n
morf a|P->Q a s n
morf a t|P->Q e w
#-------------------------------
# A internalização do "para todo".
# «iforall» (to ".iforall")
epsfile iforall
freetext a|VbP a|VbP 102 96
freetext t.VbP t.VbP 148 128
freetext a a 103 141
freetext a,b a,b 167 145
freetext T T 192 177
freetext b b 182 181
freetext b->t.T (b->t).T 118 208
freetext t.T t.T 179 212
freetext b->t.P (b->t).P 101 227
freetext t.P t.P 159 231
morf a|VbP a s n
morf a t.VbP ne w
R a a,b e w
L t.T b->t.T w e
L t.P b->t.P w e
morf a b->t.T sse n
morf a b->t.P s nnw
morf a,b T se nw
morf T t.T ssw n
morf a,b t.T s nnw
morf a,b b sse nw
morf b t.P ssw nne
morf a,b t.P ssw n
#-------------------------------
# O axioma do classificador, escrito com montes de quantificadores.
#
# ý b'-->§
#
# ý | pb |
# v v
# ý b--->t
# Ý!
# «classq» (to ".classq")
epsfile classq
freetext b' b' 100 100 T T 140 100 b b 100 140 t t 140 140
freetext V1 V 83 99 V2 V 85 120 V3 V 84 142 E! E! 119 154
freetext pb pb 116 113
morf b' T e w b' b s n T t s n b t e w
#-------------------------------
# A condição sobre os power objects, que vai implicar na existência de
# todas as exponenciais.
#
# ý
# ý a b,a--__
# | | ->
# Ý! | ===> | t
# | | >
# v v /Î
# b->t b,(b->t)
# «condpowt» (to ".condpowt")
epsfile condpowt
freetext a a 100 100 b,a b,a 152 100 b->t b->t 100 140
freetext bbt b,(b->t) 152 140 t t 185 120
freetext V1 V 87 99 V2 V 173 97 E! E! 86 118 e e 183 138
auxiliary *1 * 105 120 *2 * 147 120
morf a b->t s n b,a bbt s n bbt t nne sw b,a t see nw
R *1 *2 e w
#-------------------------------
# Functors with (left? right?) adjoints preserve limits.
#
# x > xR
# /| /||
# v |\ v | \
# (a,b)|cL : | <= (a,b)|c : |
# |\\ v |\ v
# | \->bL <== |\->b
# || \ | |:\ |
# vv vv <== vv vv
# aL-->cL <== a-->c
# «adjspreslims» (to ".adjspreslims")
epsfile adjspreslims
freetext x x 96 85 xR xR 199 85
freetext abcL limL 75 120
freetext aL aL 120 142
freetext bL bL 90 168
freetext cL cL 118 171
freetext *0 * 129 87 *1 * 164 87
freetext *2 * 120 122
freetext *4 * 141 142
freetext *6 * 141 175
freetext *8 * 127 167
deltatext x xR abcL abc lim {} bL b b {} aL a a {} cL c c {}
setdragxy x xR
deltatext *0 *1 *2 *3 * {} *4 *5 * {} *6 *7 * {} *8 *9 * {}
setdragxy *0 *1
aux *0 *1 *2 *3 *4 *5 *6 *7 *8 *9
R *0 *1 e w
samedirs w e L *3 *2 *5 *4 *7 *6 *9 *8
morf x abcL sw nne x aL se n x bL s n x cL sse nw
morf xR abc sw nne xR a se n xR b s n xR c sse nw
morf abcL aL e nww abcL bL sse nnw abcL cL se nww
morf abc a e nww abc b sse nnw abc c se nww
morf aL cL s n bL cL e w a c s n b c e w
#-------------------------------
# «linux-topics» (to ".linux-topics")
epsfile linux-topics
freetext TeX TeX 220 139
freetext agrep agrep 144 222
freetext console console 149 125
freetext emacs emacs 169 182
freetext escripts escripts 220 192
freetext expect expect 343 188
freetext expectD {expect -D} 286 161
freetext gdb gdb 266 221
freetext glimpse glimpse 137 240
freetext glyphs glyphs 198 111
freetext less less 146 150
freetext makeg {make -g} 214 221
freetext man man 200 167
freetext pdsc pdsc 186 250
freetext perl perl 107 267
freetext perldb perldb 281 191
freetext postscript postscript 407 160
freetext psne psne 192 284
freetext regexps regexps 97 189
freetext sed sed 54 162
freetext tags tags 160 200
freetext tcl tcl 336 161
freetext tclb {tcl book} 373 134
freetext tclt {tcl tutorial} 346 109
freetext tk tk 315 132
freetext zsh zsh 229 257
proc star {center args} {
foreach {tag2 d1 d2} $args {linha $center $tag2 $d1 $d2}
}
linha TeX escripts s n
linha TeX glyphs n s
linha agrep glimpse s n
linha agrep makeg e w
linha agrep pdsc e w
linha agrep regexps nnw sse
linha console glyphs ne sw
linha console less s n
linha emacs escripts see nww
linha emacs regexps w e
linha emacs tags s n
linha escripts gdb se nw
linha escripts makeg s n
linha escripts man nnw s
linha escripts tags w e
linha expect expectD nw se
linha expect tcl n s
linha expectD gdb ssw nne
linha expectD tcl e w
linha gdb perldb n s
linha less man e w
linha less regexps sw nne
linha makeg gdb e w
linha makeg zsh s n
linha pdsc zsh e w
linha perl pdsc e w
linha perl psne e w
linha perl regexps n s
linha postscript tclb nnw sse
linha psne zsh e w
linha regexps sed nnw sse
linha tcl tclb ne sw
linha tcl tclt n s
linha tcl tk nw se
linha tclt tk ssw ne
linha emacs glyphs n ssw
linha expectD perldb s n
linha tclb tk w e
#-------------------------------
#-------------------------------
# Diagrama do classificador pros subobjs do T
#
# !
# Ý! T|P--->T
#
# !| | T
# | |
# v P v
# T---->t
# fa
# «clasubT1» (to ".clasubT1")
epsfile clasubT1
freetext TP T|P 100 100 TR T 140 100
freetext TD T 100 140 t t 140 140
freetext ex! ex! 74 100 bang1 ! 120 92 bang2 ! 87 117
freetext Tarr T 150 120 P P 123 131 fa fa 121 150
morf TP TR e w TP TD s n TR t s n TD t e w
#-------------------------------
# idem, mas em notação usual
#
# S--->1
#
# | |T
# | |
# v v
# 1--->Om
# fa f
# «clasubT2» (to ".clasubT2")
epsfile clasubT2
freetext TP S 100 100 TR 1 140 100
freetext TD 1 100 140 t Om 140 140
freetext Tarr T 150 120
freetext fa {fa f} 118 132
morf TP TR e w TP TD s n TR t s n TD t e w
#-------------------------------
# (a,b)|c--->b
#
# | |g
# | |
# v f v
# a------>c
# «pbfg» (to ".pbfg")
epsfile pbfg
freetext abc (a,b)|c 100 100 b b 140 100
freetext a a 100 140 c c 140 140
freetext f f 119 130
freetext g g 148 119
morf abc b e w abc a s n b c s n a c e w
#-------------------------------
# {}--->{T} {T}--->{T}
# | | | |
# | | | |
# | | | |
# v v v v
# {T}-->{F,T} {T}-->{F,T}
# «boolpbs» (to ".boolpbs")
epsfile boolpbs
freetext a1 {{ }} 100 100 b1 {{T}} 140 100
freetext c1 {{T}} 100 140 d1 {{F,T}} 140 140
freetext a2 {{T}} 180 100 b2 {{T}} 220 100
freetext c2 {{T}} 180 140 d2 {{F,T}} 220 140
freetext e1 1 113 161
freetext f1 2 134 152
freetext e2 3 200 161
freetext f2 4 226 152
aux e1 f1 e2 f2
morf a1 b1 e w a1 c1 s n b1 d1 s n
morf a2 b2 e w a2 c2 s n b2 d2 s n
metaarrow arr1 {[^ e c1] [^ c e1] [^ n f1]}
metaarrow arr2 {[^ e c2] [^ c e2] [^ n f2]}
#-------------------------------
# T|A
# / | \
# ý / | \ý
# / | \
# / |ex! \
# v v v
# T|P<---T|P&Q--->T|Q
# «heytprod» (to ".heytprod")
epsfile heytprod
freetext x T|A 140 100
freetext a T|P 90 140
freetext ab T|P&Q 140 140
freetext b T|Q 190 140
freetext fa1 fa 105 114
freetext fa2 fa 177 116
freetext ex ex! 152 126
morf x a sw ne x ab s n x b se nw
morf ab a w e ab b e w
#-------------------------------
# Diagrama do classificador pros subobjs do T
#
# T|P&Q-->T
#
# !| |T
# | |
# v P&Q v
# T---->t_P&Q
#
# «clasubtt» (to ".clasubtt")
epsfile clasubtt
freetext a T|P&Q 100 100
freetext b T 162 100
freetext c T 100 140
freetext d t_P&Q 162 140
freetext bang1 ! 90 121
freetext T T 169 120
freetext arr P&Q 127 130
morf a b e w a c s n b d s n c d e w
#-------------------------------
# «funandQ» (to ".funandQ")
epsfile funandQ
freetext a T|A 100 100 b T|A&Q 157 100
freetext c T|B 100 140 d T|B&Q 157 140
morf a c s n b d s n
R a b e w c d e w
#-------------------------------
# «funandQadj» (to ".funandQadj")
epsfile funandQadj
freetext a T|P 100 100 b T|P&Q 157 100
freetext c T|Q->R 100 140 d T|R 157 140
freetext *1 * 105 120 *2 * 152 120
aux *1 *2
morf a c s n b d s n
bij *1 *2 e w
R a b e w
L d c w e
#-------------------------------
# «funQto» (to ".funQto")
epsfile funQto
freetext a T|Q->A 100 100 b T|A 157 100
freetext c T|Q->B 100 140 d T|B 157 140
morf a c s n b d s n
L b a w e d c w e
#-------------------------------
# (eeman "3tk canvas" "ARC ITEMS")
# (find-angg "LATEX/diaglib.014" "code arrays")
# Beckmann p. 93
# «histmat1» (to ".histmat1")
epsfile histmat1
freetext Oc O 200 200
freetext O O 200 206
freetext b1 b 179 184
freetext b2 b 170 194
freetext b3 b/2 279 189
freetext r1 r 137 207
freetext r2 r 164 148
freetext A A 96 200
freetext B B 132 116
freetext C C 104 156
freetext SC SC 237 178
freetext R R 300 200
aux R Oc
blackify
oncreate .c create arc 100 100 300 300 \
-start 0 -extent 180 -width 1
thinlinha A B e se A C e see B C se see B Oc se c C Oc see c C R see c
#-------------------------------
# «histmat2» (to ".histmat2")
epsfile histmat2
oncreate .c create oval 100 100 310 310 -width 1
# oncreate .c create arc 100 100 310 310 -width 1 \
# -start 0 -extent 180 -style arc
# oncreate .c create arc 100 100 310 310 -width 1 \
# -start 180 -extent 180 -style arc
proc line {x1 y1 x2 y2} {
oncreate .c create line $x1 $y1 $x2 $y2 -width 1
}
set w0 100
set w1 170
set w2 240
set w3 310
foreach p [list $w0 $w1 $w2 $w3] {
line $p $w0 $p $w3
line $w0 $p $w3 $p
}
line $w0 $w1 $w1 $w0
line $w0 $w2 $w1 $w3
line $w3 $w1 $w2 $w0
line $w3 $w2 $w2 $w3
#-------------------------------
# «netbasics» (to ".netbasics")
epsfile netbasics
freetext sockets sockets 169 53
freetext HTTP HTTP 76 77
freetext apache apache 78 97
freetext CGIs CGIs 77 109
freetext TL {transport layer} 260 72
freetext ping ping 233 108
freetext ifconfig ifconfig 234 122
freetext route route 233 133
freetext ethernet ethernet 349 72
freetext PPP PPP 349 87
freetext PLIP PLIP 348 99
freetext inetd inetd 148 84
freetext lsof lsof 148 95
freetext DNS DNS 280 113
freetext NIS NIS 310 100
freetext tcpd tcpd 135 120
freetext logs logs 134 131
freetext PAM PAM 182 124
freetext ARP ARP 403 79
#-------------------------------
# «escripts» (to ".escripts")
epsfile escripts
freetext _21 21 241 80
freetext anatocc anatocc 130 232
freetext angg angg 536 350
freetext anggsmil anggsmil 540 364
freetext bis bis 583 160
freetext bsd bsd 354 429
freetext cartas cartas 556 101
freetext cfengine cfengine 358 442
freetext clock clock 191 265
freetext console console 189 254
freetext contas contas 567 77
freetext coq coq 208 423
freetext corresp corresp 569 66
freetext crim crim 261 74
freetext debian-net debian-net 115 295
freetext debian debian 65 249
freetext debian.old debian.old 68 273
freetext debian0 debian0 63 261
freetext debiandev debiandev 59 225
freetext dos dos 238 67
freetext dpkg dpkg 66 236
freetext dual dual 540 324
freetext emacs emacs 369 502
freetext escripts escripts 404 491
freetext ethernet ethernet 496 322
freetext expect expect 109 170
freetext fl fl 231 424
freetext floppy floppy 55 308
freetext forth forth 215 79
freetext fortho fortho 237 92
freetext games games 296 99
freetext gdb gdb 131 220
freetext general general 534 416
freetext gimp gimp 295 111
freetext greenmatrix greenmatrix 559 114
freetext hardware hardware 52 322
freetext hsforth hsforth 233 56
freetext html html 150 146
freetext http http 154 158
freetext hw-cdrw hw-cdrw 429 74
freetext hw-eth hw-eth 494 309
freetext hw-parport hw-parport 64 344
freetext hw-sound hw-sound 343 239
freetext icon icon 181 376
freetext icq icq 443 414
freetext init init 185 242
freetext k22 k22 181 220
freetext kernel kernel 184 231
freetext latest latest 85 67
freetext localnet localnet 544 336
freetext locz locz 576 136
freetext lynx lynx 178 125
freetext mail mail 197 183
freetext maple maple 243 468
freetext math math 209 467
freetext mini mini 521 193
freetext mktclapp mktclapp 92 202
freetext modelcheck modelcheck 219 437
freetext modem modem 57 356
freetext mouse mouse 67 367
freetext mp3 mp3 350 260
freetext music music 347 249
freetext mysql mysql 133 440
freetext net net 507 333
freetext netbasics netbasics 548 312
freetext netscape netscape 206 136
freetext news news 195 156
freetext nonfree nonfree 571 53
freetext oldpage oldpage 584 202
freetext page page 584 215
freetext pam pam 540 300
freetext perl perl 151 180
freetext perl1 perl1 151 193
freetext potato potato 410 53
freetext potatocds potatocds 428 63
freetext print print 313 148
freetext ps ps 299 162
freetext python python 225 388
freetext raven10 raven10 573 126
freetext raven10b raven10b 580 147
freetext redhat redhat 520 441
freetext rest rest 518 429
freetext scheme scheme 165 402
freetext secret secret 556 90
freetext slink slink 520 451
freetext snarf snarf 138 109
freetext sql sql 133 428
freetext tcl tcl 112 159
freetext tese tese 305 133
freetext tex tex 278 136
freetext tex.old tex.old 277 150
freetext todo todo 586 187
freetext transp transp 587 173
freetext wget wget 148 122
freetext wiki wiki 109 183
freetext x x 248 115
freetext yard yard 521 204
freetext zsh zsh 118 122
#-------------------------------
# «adj-as-nt» (to ".adj-as-nt")
epsfile adj-as-nt
freetext a0 a 101 101
freetext a0' a' 138 140
freetext b0 b 100 124
deltatext a0 a0' b0 b0' b' {}
freetext a a 67 165
freetext aR aR 159 165
deltatext a0 a0' a a' a' {} aR a'R a'R {}
deltatext a0 b0 a bL bL {} aR b b {} a' b'L b'L {} a'R b' b' {}
morf b0 b0' se nw bL b'L sse nnw b b' se nw
morf a0' a0 nw se a' a nw se a'R aR nnw sse
morf a0 b0 s n a bL s n aR b s n
morf a0' b0' s n a' b'L s n a'R b' s n
set ArrowOptions(M) {-arrow last -width 2 -arrowshape {8 8 3} \
-stipple @gray50.bmp}
proc M {args} { doarrows M $args }
freetext * ** 67 177
deltatext a0 a0' * *' ** {}
deltatext a aR * *R ** {} *' *'R ** {}
aux * *' *R *'R
M * *R e w *' *'R e w
#-------------------------------
# «kan1» (to ".kan1")
epsfile kan1
freetext a a 100 100
freetext b b 160 100
freetext c c 100 160
freetext F F 128 89
freetext G G 91 133
freetext K K 121 124
freetext H H 137 145
R a b e w a c s n
metaarrow' b sw ne c :K: R
metaarrow' b sse e c :H: R
#-------------------------------
# «adj-conv» (to ".adj-conv")
# The usual convention for R and L in adjunction diagrams
epsfile adj-conv
# a===>aL
# | |
# | <-> |
# v v
# bR<b
#
quadrado-adj 100 100 a a aL aL bR bR b b
#-------------------------------
# A category where the objects are natural transformations
#
# ========>aF'
# // |
# // v
# // ==>aF==>aFH
# // // | |
# a'==>a | |
# \\ \\ v v
# \\ ==>aG==>aGH
# \\ |
# \\ v
# ========>aG'
#
# «cat-nts» (to ".cat-nts")
epsfile cat-nts
foreach {v0 v1 v2 v3} {100 140 180 220} {}
foreach {v0 v1 v2 v3} {115 145 175 205} {}
freetext aF' a''F'' 220 $v0
freetext aF a'F' 180 $v1 aFH a'F'H 220 $v1
freetext a' a'' 100 160 a a' 140 160
freetext aG a'G' 180 $v2 aGH a'G'H 220 $v2
freetext aG' a''G'' 220 $v3
L a' aF' ne w
L a aF ne w aF aFH e w
L a' a e w
L a aG se w aG aGH e w
L a' aG' se w
samedirs s n morf aF aG aF' aFH aFH aGH aGH aG'
#-------------------------------
# Adjunções: a condição de naturalidade sobre abc (demonstração).
# Nessa versão L e R seguem a notação "oficial".
#
# aL---->bL--->c
#
#
# v v v
# aLR-->bLR--->cR
# ^ ^ ^ ^
# \ / \ /
# a---->b
#
#
# «adj-demabc-new» (to ".adj-demabc-new")
epsfile adj-demabc-new
reflec 100 100 aL aL aLR aLR a a
reflec 140 100 bL bL bLR bLR b b
reflec 180 100 c c cR cR
hmorf aL bL aLR bLR a b
hmorf bL c bLR cR
morf a bLR ne s
morf b cR ne s
R a aL n se
R b bL n se
#-------------------------------
# Limits in a functor category can be taken pointwise (example)
#
# x1
# | \
# | x2
# v | x1
# x1--->x1 | <===== \
# \ \v x2
# x2--->x2
# | |
# | |
# v v
# a13
# | \
# | a23
# v | (a13,a14)|a15
# a14--->a15 | => \
# \ \ v (a23,a24)|a25
# a24--->a25
# «limSetC» (to ".limSetC")
epsfile limSetC
freetext x13 x1 161 67
freetext x23 x2 193 97
freetext x14 x1 106 116
freetext x15 x1 160 115
freetext a13 a13 168 214
freetext x1 x1 296 101
freetext x2 x2 329 133
freetext a1 (a13,a14)|a15 306 244
freetext a2 (a23,a24)|a25 329 279
freetext _1 1 281 122
freetext _2 2 203 122
freetext _3 3 213 265
freetext _4 4 268 265
freetext _5 5 159 159
freetext _6 6 159 204
freetext _7 7 311 142
freetext _8 8 311 225
deltatext x13 x14 a13 a14 a14 {a13}
deltatext x13 x15 a13 a15 a15 {a13}
deltatext x13 x23 x14 x24 x2 {x14} x15 x25 x2 {x15}
deltatext x13 x23 a13 a23 a23 {} a14 a24 a24 {} a15 a25 a25 {}
setdragxy x13 x23 x14 x15
# setdragxy x14 x15
samedirs s n morf x13 x15 x23 x25 a13 a15 a23 a25
samedirs e w morf x14 x15 x24 x25 a14 a15 a24 a25
samedirs se nw morf x13 x23 x14 x24 x15 x25
samedirs se nnw morf a13 a23 a14 a24 a15 a25
morf x1 x2 se nw
morf a1 a2 s n
aux _1 _2 _3 _4 _5 _6 _7 _8
L _1 _2 w e
R _3 _4 e w
morf _5 _6 s n _7 _8 s n
#-------------------------------
# «monadresls» (to ".monadresls")
#
# Kleisli é inicial e Eilenberg-Moore é terminal na categoria das
# resoluções de uma mônada
epsfile monadresls
freetext aK aK 116 93
freetext aL aL 78 118
freetext aE (aTT->aT)E 161 143
freetext a a 207 117
freetext bK bK 117 176
freetext bL bL 79 204
freetext bE (bTT->bT)E 161 229
freetext b bT 207 204
samedirs s n morf aK bK aL bL aE bE a b
L a aK nw e
R bK b e nw
L a aL w e
R bL b e w
L a aE sw nne
R bE b nne sw
samedirs sw ne T aK aL bK bL
samedirs se nw T aL aE bL bE
#-------------------------------
#-------------------------------
#
# Cap. 4: Categorias
#
#-----
# O diagrama comutativo mais bobo
#
# a->b
# | |
# v v
# c->d
# «abcd» (to ".abcd")
epsfile abcd
freetext a a 100 100 b b 140 100
freetext c c 100 140 d d 140 140
morf a b e w
morf c d e w
morf a c s n
morf b d s n
#-------------------------------
# Primeiro lero sobre construções naturais
#
# a-->a
#
# v v v
# aF->aF
# «idcond» (to ".idcond")
epsfile idcond
freetext a a 100 100 b a 140 100
freetext c aF 100 140 d aF 140 140
freetext _1 _1 120 100 _2 _2 120 140
aux _1 _2
morf a b e w
morf c d e w
R a c s n
R b d s n
R _1 _2 s n
#-------------------------------
# c=>a^F a^F
# | |
# | |
# c=>a | <== a |
# | | | |
# | v <-> | v
# | c=>b_c^F | (lim_c b_c)^F
# v v
# c=>b_c ==> lim_c b_c
# «preslim» (to ".preslim")
epsfile preslim
freetext ca c=>a 100 100 a a 160 100
freetext cb c=>b_c 100 160 lb {lim_c b_c} 160 160
freetext caF c=>aF 130 70 aF aF 190 70
freetext cbF c=>b_c^F 130 130 lbF {(lim_c b_c)^F} 190 130
#-------------------------------
# cat theory
#
# ðC^+ term RW SC tree RW ND tree
#
# ðC^+ term SW SC tree SW ND tree
#
# RW sequent RW term
#
# SW sequent SW term
# «dncforg» (to ".dncforg")
epsfile dncforg
freetext SWSC {SW SC tree} 204 101
freetext RWSC {RW SC tree} 154 73
freetext SWND {SW ND tree} 304 101
freetext SWs {SW sequent} 204 159
freetext SWLt {\C+ term} 96 101
freetext catt {cat theory} 47 35
deltatext SWSC RWSC SWLt RWLt {\C+ term} {}
deltatext SWSC RWSC SWND RWND {RW ND tree} {} SWs RWs {RW sequent} {}
deltatext SWSC SWs SWND SWterm {SW term} {} RWND RWterm {RW term} {}
samedirs s n morf SWSC SWs RWSC RWs SWND SWterm RWND RWterm
samedirs e w morf RWSC RWND SWSC SWND RWs RWterm SWs SWterm
samedirs sse nnw morf RWSC SWSC RWND SWND RWs SWs RWterm SWterm
samedirs sse nnw gmorf RWLt SWLt
samedirs w e morf SWSC SWLt RWSC RWLt
gmorf catt RWLt s n
#-------------------------------
# «diagxy1» (to ".diagxy1")
# (find-angg "LATEX/diaglib.014" "diagxy_hacks")
dxybuttons
dxytext tag1 {oSet} {\o\Set} 100 100
dxytext tag2 {oC} {\o\C} 110 110
dxymorf tag1 tag2 {f_\cdot} /|->/
#-------------------------------
# (find-angg "LATEX/diaglib.014" "diagxy_hacks")
# (find-diagxyfile "diaxydoc.tex" "as well as curved arrows")
# (find-diagxypage 14)
# «phil1» (to ".phil1")
dxybuttons
set dxyscale 20
dxytext aT1 aT {a^T} 100 100
dxytext aT2 aT {a^T} 130 100
dxytext bT bT {b^T} 160 100
dxytext a'T1 a'T {{a'}^T} 100 130
dxytext a'T2 a'T {{a'}^T} 130 130
dxytext b'T b'T {{b'}^T} 160 130
dxymorf aT1 bT {m_{AB}(gĒa)} {/{@{|->}@/^3em/}/}
dxymorf aT1 aT2 {m_{AA}(1_A)} /|->/
dxymorf aT2 bT {T(gĒa)} /|->/
dxymorf aT1 a'T1 {T(a)} /|->/
dxymorf aT1 a'T2 {m{AA'}} /|->/
dxymorf aT2 a'T2 {m{AA'}} |r|/|->/
dxymorf bT b'T {T(b)} |r|/|->/
dxymorf a'T1 a'T2 {m_{A'A'}(1_{A'})} /|->/
dxymorf a'T2 b'T {T(bĒg)} /|->/
dxymorf a'T1 b'T {m_{A'B'}(bĒg)} {/{@{|->}@/_3em/}/}
#-------------------------------
# (defun find-3tkman (page &rest rest) (apply 'find-man (concat "n " page) rest))
# (defun find-3tclman (page &rest rest) (apply 'find-man (concat "n " page) rest))
# (find-fline "~/tmp/ee.diag")
# (find-angg "LATEX/diaglib.014" "text_objects")
# button .buttons3.run -text {run sel} -command {eval [.t get sel.first sel.last]}
# pack .buttons3.run .buttons3.bDxyD .buttons3.beDxyD -side left
# (find-angg "LATEX/diaglib.014" "basic_window")
# (find-es "tcl-cipsga" "mywish")
# (find-3tkman "text")
# (find-3tkman "text" "keyboard")
# (find-3tkman "bind")
text .t -height 10
pack .t -after .buttons3
bind .t <Alt-e> {eval [.t get sel.first sel.last]}
# (find-3tkman "text")
# (find-angg "LATEX/diaglib.014")
# (find-3tkman "pack" "-in other")
# (find-3tkman "pack" "GEOMETRY PROPAGATION")
# puts [pack slaves .]
# puts ".c: [pack info .c]"
# puts ".buttons: [pack info .buttons]"
# puts ".buttons2: [pack info .buttons2]"
# puts ".buttons3: [pack info .buttons3]"
(global-set-key [f3] 'eediag-bounded)
(global-set-key [f3] 'eelatex-bounded)
# (find-es "tcl" "newdiaglib")
# (find-fline "~/.emacs" "014")
(defun eediag-bounded () (interactive)
(write-ee-bounded
"----------\n" "\n#----------"
"cd ~/LATEX; cat > tmpdiag <<'--%%--'\nsource diaglib.014\n"
"\n--%%--\nwish tmpdiag &\n"))
(global-set-key [f3] 'eediag-bounded)
exit
~/TK/emacs.eew
# (find-vldifile "tcl8.0-dev.list")
# (find-fline "/usr/doc/expect5.24/examples/")
# foreach {tag0 txt0 tag1 txt1 tag2 txt2 tag3 txt3} $args {}
# if {$tag0 != "" && $tag1 != ""}
# (find-etag "describe-key")
# (describe-key "f3")
ee-temp-bounded-function
(insert (pp (symbol-function 'ee-bounded)))
# ee-temp-bounded-function
# (insert (pp (symbol-function 'ee-bounded)))
# (insert (pp (symbol-function (key-binding [f3]))))
# (insert (pp (symbol-function ee-temp-bounded-function)))
# (find-fline "~/eev.el" "defvar ee-temp-bounded-function")
# Local Variables:
# coding: no-conversion
# ee-temp-bounded-function: eediag-bounded
# ee-anchor-format: "«%s»"
# ee-charset-indicator: "Ñ"
# End: