# Um estoque de desenhos pro diaglib.013, e umas rotinas pro emacs.
# 98oct09

# (find-fline "~/TK/diaglib.013")
# (find-fline "~/TK/basiclib.013")

(setq ee-file "~/bin/emacs.ee")
(setq tcl-indent-level 2)

(defun se-to-string (s e &optional P)
  (cond (P (buffer-substring (marker-position (get-register ?b))
			     (marker-position (get-register ?e))))
	((numberp s) (buffer-substring s e))
	((stringp s) s)))
;
(defun write-ee-string (str)
  (write-region str nil ee-file))	; a standard kludge
(defun write-ee (s e pre post &optional P)
  (write-ee-string (concat pre (se-to-string s e) post)))

(defun eediag (s e P) (interactive "r\nP")
  (write-ee s e "cat > ~/TK/temp <<'--%%--'\nsource ~/TK/diaglib.013\n"
	    "\n--%%--\nwish ~/TK/temp &\n" P))


; (find-enode "Query Replace")
; (find-etag "query-replace-regexp")
(defun dr () (interactive)
  (query-replace-regexp "X(\\(.*\\)) \\(.*\\)\nY(\\(.*\\) \\(.*\\)\n"
			"freetext \\1 \\1 \\2 \\4\n"))
(defun dr2 () (interactive) (query-replace-regexp "\nfreetext " "   "))



(global-set-key [f3] 'eediag-bounded)







#-------------------------------
#
# Cap. 1: Introdu‡Æo
#
#----

# Problema variacional
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
auxiliar _xy * 120 120
auxiliar _xj * 140 120
auxiliar _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

set psfile ~/LATEX/categs0.eps

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.

set psfile ~/LATEX/assuntos.eps

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)

set psfile ~/LATEX/diamond1.eps

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

#-------------------------------

set psfile ~/LATEX/diamond2.eps

freetext      A A 100 100
freetext B B 70 130   C C 130 130
freetext      D D 100 160

metaarrow' A sw ne B
metaarrow' A se nw C
thinse B D
thinsw C D

#-------------------------------

set psfile ~/LATEX/diamond3.eps

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

metaarrow' B sw ne A
metaarrow' B se nw C
metaarrow' D sw ne C
metaarrow' D se nw E
metaarrow' E se nw F
metaarrow' G sw ne F
thinse A H
thinse H J
thinse J L
thinse C I
thinse I K

thinsw C H
thinsw E I
thinsw I J
thinsw F K
thinsw K L








#-------------------------------
#
# Cap. 4: Categorias
#
#-----

# Primeiro lero sobre constru‡äes naturais
#
# a->b
# º\ |
# v vv
# c->a'

set psfile ~/LATEX/construnat1.eps

freetext a a 100 100   b  b  150 100
freetext c c 100 140   a' a' 150 140
morfs a b e w
metaarrow' a sw nw c :f:
metaarrow' a  s  n c :g:
morfs a a' se nw   b a' s n
morfs 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

set psfile ~/LATEX/naoplanar.eps

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
morfs   b a w e   b c e w
morfs   d a n s   b e s n   b f se nw   e c ne sw   c f s n
morfs   d e e w   e f e w
morfs   g d nw se   e g sw ne

#-------------------------------

# Exemplo pro teorema do diagrama planar
#
# a->b->c
#  \ |  |
#   vv  v
#    d->e
#     \ |
#      vv
#   	f

set psfile ~/LATEX/planar.eps

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
morfs   a b e w   b c e w
morfs   a d se nw   b d s n   c e s n
morfs   d e e w
morfs   d f se nw   e f s n

#-------------------------------

# Lema da sombra
#
#              _____
#      _______/     \
#     /      /\      \
#    /      /  \      \
#   / f1   / g1 v   h1 v
#  a=====>b=====>c=====>d
#     f2     g2     h2

set psfile ~/LATEX/sombra1.eps

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:

auxiliar /1 /1 115 75   /2 /2 165 75
auxiliar /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

set psfile ~/LATEX/sombra2.eps

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:

auxiliar /1 /1 115 75   /2 /2 165 75
auxiliar /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
#

set psfile ~/LATEX/functor0.eps

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
morfs   a1 b1 ne w   b1 c1 e nw   a1 c1 e w
morfs   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

setdragvars a1 {X(a1) X(a2)} {Y(a1) Y(a2)}
setdragvars b1 {X(b1) X(b2)} {Y(b1) Y(b2)}
setdragvars c1 {X(c1) X(c2)} {Y(c1) Y(c2)}

setdragvars a2 {X(a2) X(b2) X(c2)} {Y(a2) Y(b2) Y(c2)}

#-------------------------------

# Teoreminha de coerˆncia para funtores: antes
#
# a
# |\
# v v
# b->c
# |  |
# v  v
# d->e

set psfile ~/LATEX/functor1.eps

freetext a1 a 118 101   b1 b 100 140   c1 c 140 140
freetext d1 d 100 180   e1 e 140 180
morfs   a1 b1 sw ne   a1 c1 se nw   b1 c1 e w
morfs   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

set psfile ~/LATEX/functor2.eps

freetext a1 a 118 101   b1 b 100 140   c1 c 140 140
freetext d1 d 100 180   e1 e 140 180
morfs   a1 b1 sw ne   a1 c1 se nw   b1 c1 e w
morfs   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
morfs   a2 b2 sw n   a2 c2 se n   b2 c2 e w
morfs   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
#

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()}'

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

#-------------------------------

# Produtos 1
#
# x--->p
# |\  /|
# | \/ |
# | /\ |
# vv  vv
# a    b

epsfile prod1

freetext x x 100 100   p p 155 100
freetext a a 115 145   b b 140 145

morfs 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

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

morfs  x p see w      x q e w
bij    p q e sww

morfs  x a s nnw    x b se nnw
morfs  p a sw n     p b s n
morfs  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
#
set psfile ~/LATEX/adj-sqrab.eps

vtorre 100 100  a a   bL bL
vtorre 140 100  aR aR   b b
R' a aR
L' b bL

auxiliar _1 * 105 120
auxiliar _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
#
set psfile ~/LATEX/adj-sqrabc.eps

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
#
set psfile ~/LATEX/adj-sqrbcd.eps

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
#
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

set psfile ~/LATEX/adj-bij.eps

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

set psfile ~/LATEX/adj-func1.eps

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
#

set psfile ~/LATEX/adj-Rid.eps

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
#

set psfile ~/LATEX/adj-Rcomp.eps

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
#
#
set psfile ~/LATEX/adj-demabc.eps

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
#
#
set psfile ~/LATEX/adj-dembcd.eps

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

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---

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
morfs 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
#
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

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
auxiliar P P 160 100
morf x Plong e w
morfs x a s nnw   x b sse nnw   x c se nnw
morfs P a sw nne   P b ssw nne   P c s nne

#-------------------------------

# Pullback

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
auxiliar P P 108 55
setdragxy Plong P

morfs x Plong e w   a c e w   b c s n
morfs x a s nw   x c sse nw  x b se nw
morfs P a s nnw   P c sse nnw  P b se nnw

#-------------------------------

# Equalizador

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
morfs x E e w
morfs x a se nw   x b see nw
morfs 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.

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

morfs x L e  w
morfs L a sw ne   L b sw n   L c s  n   L d se n
morfs x a sw n    x b s  nw  x c se nw  x d se nw

#-------------------------------

# Dois pullbacks colados.

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
morfs 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

set psfile ~/LATEX/trads.eps

freetext DN    DN    100 100
freetext DN+T  DN+T  160 100
freetext CCC   CCC   100 160
freetext CCC+T CCC+T 160 160

morfs DN  DN+T  e w   DN+T  DN  sw se
morfs CCC CCC+T e w   CCC+T CCC sw se

# (find-fline "~/TK/gray50.bmp")
set ArrowOptions(dim) \
  [concat $ArrowOptions(m) -stipple @~/TK/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

set psfile ~/LATEX/Tab2ab.eps

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
morfs b1 b3 s n   b2 b4 s n
bij b2 b5 e w
R b1 b2 e w
L b4 b3 w e

setdragvars a1 {X(a1) X(a2) X(a3) X(a4) X(a5) X(a6)} \
	       {Y(a1) Y(a2) Y(a3) Y(a4) Y(a5) Y(a6)}
setdragvars b1 {X(b1) X(b2) X(b3) X(b4) X(b5)} \
	       {Y(b1) Y(b2) Y(b3) Y(b4) Y(b5)}

#-------------------------------
#
# Cap. 6: A  lgebra dos valores de verdade
#
#----

# Adjun‡äes: /\ e -> como adjuntas
#
#  A===>A^B
#  |     |
#  | <-> |
#  v     v
# B>C<ÍÍÍB
#
set psfile ~/LATEX/adj-sqrlog.eps

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

auxiliar _1 * 105 120
auxiliar _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
#

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

epsfile classif-ax

quadrado 100 100   a' a'   T T   a a   t t
auxiliar * *  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'
#
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

morfs 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
#
set psfile ~/LATEX/fibrados.eps

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
#
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
#
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
#
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.
#
#
set psfile ~/LATEX/adj-sqrab.eps

vtorre 100 100  a a   bL bL
vtorre 140 100  aR aR   b b
R' a aR
L' b bL

auxiliar _1 * 105 120
auxiliar _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
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   a^b a^b   b>c b>c   c4 c

#-------------------------------

#       id
#    aR--->aR
#    º     º
#    º     º
#    v id  v
#   aRL-->aRL
#     ^   ^
#      \ /
#       a
#
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
#
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

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
morfs a bc w e  ba bbc w e   bbc c s nw   ba c s ne

#-------------------------------

epsfile adj-uid (old)

#       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'
#
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:

morfs aT aTT see sww   aTTT aTT sww see   aT aT' s n   aTT aT' ssw ne

#-------------------------------

# M“nadas:  lgebras
#
#     e      pT
#   a--->aT<===aTT
#   |    /   m
# id|   /p
#   |  /
#   v v
#   a'
#
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:

morfs 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
#
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

morfs 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
#
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
morfs 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
morfs 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
#
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
#
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

morfs b bT' e w   b bT s n   bT' bT sw ne   bT' bTT s n
morfs bTT bT w e   bT c s n   bTT cT s n   cT c w e

auxiliar e1 * 105 120   e2 * 135 120
auxiliar g1 * 105 160   g2 * 135 160
R' e1 e2
R' g1 g2

auxiliar 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
#
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'
#
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'
#
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
#
epsfile kleisli1

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

morfs 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
#
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 thinmorf   bT cTT   cT dTT   cTT dTTT
samedirs w e thinmorf 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
#
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
thinmorf 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
thinmorf 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
#
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 thinmorf   bT cTT   cT dTT   cTT dTTT
samedirs w e thinmorf 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
#
epsfile kleisli3

kleislirow 100 100 b bT
kleislirow 100 140 "" cT' cTT
kleislirow 100 170 "" cT

morfs b bT e w   b cT' se nw   cT' cTT e w   cT' cT s n   cTT cT ssw ne
thinmorf 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
#
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
morfs b bT e w   cT dTT se nnw   dTT dT w e

R' a0 a
R' b0 b
L' c c0
L' d d0

#-------------------------------

#  p      f       y_k
#
#  m    m,f_i    m,y_ik
#
# x_j  x_j,f_i  x_j,y_ik

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
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".

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
#     í!

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

morfs 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)

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

auxiliar *1 * 105 120   *2 * 147 120

morfs a b->t s n   b,a bbt s n   bbt t nne sw   b,a t see nw
R *1 *2 e w

#-------------------------------

set 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


#-------------------------------



linha TeX glyphs n s
linha TeX escripts s n
linha agrep glimpse s n
linha agrep regexps nnw sse
linha agrep tags e w
linha agrep pdsc e w
linha regexps sed nnw sse
linha regexps 



#-------------------------------


# (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 != ""}