Warning: this is an htmlized version!
The original is across this link,
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: