aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/faq/axioms.eps
blob: 3f3c01c43adccb7ff6e447c912a17077f48788f3 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
%!PS-Adobe-2.0 EPSF-2.0
%%Title: axioms.fig
%%Creator: fig2dev Version 3.2 Patchlevel 4
%%CreationDate: Wed May  5 18:30:03 2004
%%For: herbelin@limoux.polytechnique.fr (Hugo Herbelin)
%%BoundingBox: 0 0 437 372
%%Magnification: 1.0000
%%EndComments
/$F2psDict 200 dict def
$F2psDict begin
$F2psDict /mtrx matrix put
/col-1 {0 setgray} bind def
/col0 {0.000 0.000 0.000 srgb} bind def
/col1 {0.000 0.000 1.000 srgb} bind def
/col2 {0.000 1.000 0.000 srgb} bind def
/col3 {0.000 1.000 1.000 srgb} bind def
/col4 {1.000 0.000 0.000 srgb} bind def
/col5 {1.000 0.000 1.000 srgb} bind def
/col6 {1.000 1.000 0.000 srgb} bind def
/col7 {1.000 1.000 1.000 srgb} bind def
/col8 {0.000 0.000 0.560 srgb} bind def
/col9 {0.000 0.000 0.690 srgb} bind def
/col10 {0.000 0.000 0.820 srgb} bind def
/col11 {0.530 0.810 1.000 srgb} bind def
/col12 {0.000 0.560 0.000 srgb} bind def
/col13 {0.000 0.690 0.000 srgb} bind def
/col14 {0.000 0.820 0.000 srgb} bind def
/col15 {0.000 0.560 0.560 srgb} bind def
/col16 {0.000 0.690 0.690 srgb} bind def
/col17 {0.000 0.820 0.820 srgb} bind def
/col18 {0.560 0.000 0.000 srgb} bind def
/col19 {0.690 0.000 0.000 srgb} bind def
/col20 {0.820 0.000 0.000 srgb} bind def
/col21 {0.560 0.000 0.560 srgb} bind def
/col22 {0.690 0.000 0.690 srgb} bind def
/col23 {0.820 0.000 0.820 srgb} bind def
/col24 {0.500 0.190 0.000 srgb} bind def
/col25 {0.630 0.250 0.000 srgb} bind def
/col26 {0.750 0.380 0.000 srgb} bind def
/col27 {1.000 0.500 0.500 srgb} bind def
/col28 {1.000 0.630 0.630 srgb} bind def
/col29 {1.000 0.750 0.750 srgb} bind def
/col30 {1.000 0.880 0.880 srgb} bind def
/col31 {1.000 0.840 0.000 srgb} bind def

end
save
newpath 0 372 moveto 0 0 lineto 437 0 lineto 437 372 lineto closepath clip newpath
-90.0 435.2 translate
1 -1 scale

/cp {closepath} bind def
/ef {eofill} bind def
/gr {grestore} bind def
/gs {gsave} bind def
/sa {save} bind def
/rs {restore} bind def
/l {lineto} bind def
/m {moveto} bind def
/rm {rmoveto} bind def
/n {newpath} bind def
/s {stroke} bind def
/sh {show} bind def
/slc {setlinecap} bind def
/slj {setlinejoin} bind def
/slw {setlinewidth} bind def
/srgb {setrgbcolor} bind def
/rot {rotate} bind def
/sc {scale} bind def
/sd {setdash} bind def
/ff {findfont} bind def
/sf {setfont} bind def
/scf {scalefont} bind def
/sw {stringwidth} bind def
/tr {translate} bind def
/tnt {dup dup currentrgbcolor
  4 -2 roll dup 1 exch sub 3 -1 roll mul add
  4 -2 roll dup 1 exch sub 3 -1 roll mul add
  4 -2 roll dup 1 exch sub 3 -1 roll mul add srgb}
  bind def
/shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul
  4 -2 roll mul srgb} bind def
/reencdict 12 dict def /ReEncode { reencdict begin
/newcodesandnames exch def /newfontname exch def /basefontname exch def
/basefontdict basefontname findfont def /newfont basefontdict maxlength dict def
basefontdict { exch dup /FID ne { dup /Encoding eq
{ exch dup length array copy newfont 3 1 roll put }
{ exch newfont 3 1 roll put } ifelse } { pop pop } ifelse } forall
newfont /FontName newfontname put newcodesandnames aload pop
128 1 255 { newfont /Encoding get exch /.notdef put } for
newcodesandnames length 2 idiv { newfont /Encoding get 3 1 roll put } repeat
newfontname newfont definefont pop end } def
/isovec [
8#055 /minus 8#200 /grave 8#201 /acute 8#202 /circumflex 8#203 /tilde
8#204 /macron 8#205 /breve 8#206 /dotaccent 8#207 /dieresis
8#210 /ring 8#211 /cedilla 8#212 /hungarumlaut 8#213 /ogonek 8#214 /caron
8#220 /dotlessi 8#230 /oe 8#231 /OE
8#240 /space 8#241 /exclamdown 8#242 /cent 8#243 /sterling
8#244 /currency 8#245 /yen 8#246 /brokenbar 8#247 /section 8#250 /dieresis
8#251 /copyright 8#252 /ordfeminine 8#253 /guillemotleft 8#254 /logicalnot
8#255 /hyphen 8#256 /registered 8#257 /macron 8#260 /degree 8#261 /plusminus
8#262 /twosuperior 8#263 /threesuperior 8#264 /acute 8#265 /mu 8#266 /paragraph
8#267 /periodcentered 8#270 /cedilla 8#271 /onesuperior 8#272 /ordmasculine
8#273 /guillemotright 8#274 /onequarter 8#275 /onehalf
8#276 /threequarters 8#277 /questiondown 8#300 /Agrave 8#301 /Aacute
8#302 /Acircumflex 8#303 /Atilde 8#304 /Adieresis 8#305 /Aring
8#306 /AE 8#307 /Ccedilla 8#310 /Egrave 8#311 /Eacute
8#312 /Ecircumflex 8#313 /Edieresis 8#314 /Igrave 8#315 /Iacute
8#316 /Icircumflex 8#317 /Idieresis 8#320 /Eth 8#321 /Ntilde 8#322 /Ograve
8#323 /Oacute 8#324 /Ocircumflex 8#325 /Otilde 8#326 /Odieresis 8#327 /multiply
8#330 /Oslash 8#331 /Ugrave 8#332 /Uacute 8#333 /Ucircumflex
8#334 /Udieresis 8#335 /Yacute 8#336 /Thorn 8#337 /germandbls 8#340 /agrave
8#341 /aacute 8#342 /acircumflex 8#343 /atilde 8#344 /adieresis 8#345 /aring
8#346 /ae 8#347 /ccedilla 8#350 /egrave 8#351 /eacute
8#352 /ecircumflex 8#353 /edieresis 8#354 /igrave 8#355 /iacute
8#356 /icircumflex 8#357 /idieresis 8#360 /eth 8#361 /ntilde 8#362 /ograve
8#363 /oacute 8#364 /ocircumflex 8#365 /otilde 8#366 /odieresis 8#367 /divide
8#370 /oslash 8#371 /ugrave 8#372 /uacute 8#373 /ucircumflex
8#374 /udieresis 8#375 /yacute 8#376 /thorn 8#377 /ydieresis] def
/Times-Roman /Times-Roman-iso isovec ReEncode
/$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def
/$F2psEnd {$F2psEnteredState restore end} def

$F2psBegin
10 setmiterlimit
0 slj 0 slc
 0.06000 0.06000 sc
%
% Fig objects follow
%
% 
% here starts figure with depth 50
% Arc
7.500 slw
gs  clippath
3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp
eoclip
n 3600.0 6750.0 150.0 90.0 -90.0 arc
gs col0 s gr
 gr

% arrowhead
n 3465 6865 m 3586 6893 l 3492 6812 l 3465 6865 l  cp gs 0.00 setgray ef gr  col0 s
% Arc
gs  clippath
3599 6633 m 3626 6579 l 3492 6512 l 3586 6593 l 3465 6565 l cp
eoclip
n 3600.0 6450.0 150.0 90.0 -90.0 arc
gs col0 s gr
 gr

% arrowhead
n 3465 6565 m 3586 6593 l 3492 6512 l 3465 6565 l  cp gs 0.00 setgray ef gr  col0 s
% Arc
gs  clippath
3626 6020 m 3599 5966 l 3465 6034 l 3586 6007 l 3492 6087 l cp
3599 6333 m 3626 6279 l 3492 6212 l 3586 6293 l 3465 6265 l cp
eoclip
n 3600.0 6150.0 150.0 90.0 -90.0 arc
gs col0 s gr
 gr

% arrowhead
n 3492 6087 m 3586 6007 l 3465 6034 l 3492 6087 l  cp gs 0.00 setgray ef gr  col0 s
% arrowhead
n 3465 6265 m 3586 6293 l 3492 6212 l 3465 6265 l  cp gs 0.00 setgray ef gr  col0 s
% Arc
gs  clippath
3626 6320 m 3599 6266 l 3465 6334 l 3586 6307 l 3492 6387 l cp
3599 6633 m 3626 6579 l 3492 6512 l 3586 6593 l 3465 6565 l cp
eoclip
n 3600.0 6450.0 150.0 90.0 -90.0 arc
gs col0 s gr
 gr

% arrowhead
n 3492 6387 m 3586 6307 l 3465 6334 l 3492 6387 l  cp gs 0.00 setgray ef gr  col0 s
% arrowhead
n 3465 6565 m 3586 6593 l 3492 6512 l 3465 6565 l  cp gs 0.00 setgray ef gr  col0 s
% Arc
gs  clippath
3626 6620 m 3599 6566 l 3465 6634 l 3586 6607 l 3492 6687 l cp
3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp
eoclip
n 3600.0 6750.0 150.0 90.0 -90.0 arc
gs col0 s gr
 gr

% arrowhead
n 3492 6687 m 3586 6607 l 3465 6634 l 3492 6687 l  cp gs 0.00 setgray ef gr  col0 s
% arrowhead
n 3465 6865 m 3586 6893 l 3492 6812 l 3465 6865 l  cp gs 0.00 setgray ef gr  col0 s
% Arc
gs  clippath
3626 6920 m 3599 6866 l 3465 6934 l 3586 6907 l 3492 6987 l cp
3599 7233 m 3626 7179 l 3492 7112 l 3586 7193 l 3465 7165 l cp
eoclip
n 3600.0 7050.0 150.0 90.0 -90.0 arc
gs col0 s gr
 gr

% arrowhead
n 3492 6987 m 3586 6907 l 3465 6934 l 3492 6987 l  cp gs 0.00 setgray ef gr  col0 s
% arrowhead
n 3465 7165 m 3586 7193 l 3492 7112 l 3465 7165 l  cp gs 0.00 setgray ef gr  col0 s
% Arc
gs  clippath
4168 4060 m 4227 4068 l 4247 3919 l 4202 4034 l 4188 3911 l cp
eoclip
n 14032.5 5272.5 9908.2 -159.9 -172.9 arcn
gs col0 s gr
 gr

% arrowhead
n 4188 3911 m 4202 4034 l 4247 3919 l 4188 3911 l  cp gs 0.00 setgray ef gr  col0 s
% Polyline
gs  clippath
4170 5790 m 4230 5790 l 4230 5639 l 4200 5759 l 4170 5639 l cp
eoclip
n 4200 5175 m
 4200 5775 l gs col0 s gr gr

% arrowhead
n 4170 5639 m 4200 5759 l 4230 5639 l 4170 5639 l  cp gs 0.00 setgray ef gr  col0 s
% Polyline
gs  clippath
4553 5749 m 4567 5807 l 4714 5771 l 4591 5771 l 4700 5713 l cp
eoclip
n 7050 5175 m
 4575 5775 l gs col0 s gr gr

% arrowhead
n 4700 5713 m 4591 5771 l 4714 5771 l 4700 5713 l  cp gs 0.00 setgray ef gr  col0 s
% Polyline
gs  clippath
4170 4890 m 4230 4890 l 4230 4739 l 4200 4859 l 4170 4739 l cp
eoclip
n 4200 4275 m
 4200 4875 l gs col0 s gr gr

% arrowhead
n 4170 4739 m 4200 4859 l 4230 4739 l 4170 4739 l  cp gs 0.00 setgray ef gr  col0 s
% Polyline
gs  clippath
7131 4907 m 7147 4850 l 7001 4810 l 7109 4871 l 6985 4868 l cp
eoclip
n 4950 4275 m
 7125 4875 l gs col0 s gr gr

% arrowhead
n 6985 4868 m 7109 4871 l 7001 4810 l 6985 4868 l  cp gs 0.00 setgray ef gr  col0 s
% Polyline
gs  clippath
7167 4057 m 7225 4071 l 7262 3924 l 7204 4034 l 7204 3910 l cp
eoclip
n 7725 1950 m
 7200 4050 l gs col0 s gr gr

% arrowhead
n 7204 3910 m 7204 4034 l 7262 3924 l 7204 3910 l  cp gs 0.00 setgray ef gr  col0 s
% Polyline
n 4350 3075 m
 7350 1950 l gs col0 s gr 
% Polyline
gs  clippath
7170 4890 m 7230 4890 l 7230 4739 l 7200 4859 l 7170 4739 l cp
eoclip
n 7200 4275 m
 7200 4875 l gs col0 s gr gr

% arrowhead
n 7170 4739 m 7200 4859 l 7230 4739 l 7170 4739 l  cp gs 0.00 setgray ef gr  col0 s
% Polyline
n 3075 1875 m
 3975 1875 l gs col0 s gr 
% Polyline
gs  clippath
5520 4065 m 5580 4065 l 5580 3914 l 5550 4034 l 5520 3914 l cp
5580 3660 m 5520 3660 l 5520 3811 l 5550 3691 l 5580 3811 l cp
eoclip
n 5550 3675 m
 5550 4050 l gs col0 s gr gr

% arrowhead
n 5580 3811 m 5550 3691 l 5520 3811 l 5580 3811 l  cp gs 0.00 setgray ef gr  col0 s
% arrowhead
n 5520 3914 m 5550 4034 l 5580 3914 l 5520 3914 l  cp gs 0.00 setgray ef gr  col0 s
% Polyline
n 4575 4050 m
 6450 4050 l gs col0 s gr 
% Polyline
gs  clippath
3495 2265 m 3555 2265 l 3555 2114 l 3525 2234 l 3495 2114 l cp
3555 1860 m 3495 1860 l 3495 2011 l 3525 1891 l 3555 2011 l cp
eoclip
n 3525 1875 m
 3525 2250 l gs col0 s gr gr

% arrowhead
n 3555 2011 m 3525 1891 l 3495 2011 l 3555 2011 l  cp gs 0.00 setgray ef gr  col0 s
% arrowhead
n 3495 2114 m 3525 2234 l 3555 2114 l 3495 2114 l  cp gs 0.00 setgray ef gr  col0 s
% Polyline
gs  clippath
2219 3988 m 2279 3991 l 2285 3840 l 2251 3959 l 2225 3838 l cp
eoclip
n 2325 1875 m
 2250 3975 l gs col0 s gr gr

% arrowhead
n 2225 3838 m 2251 3959 l 2285 3840 l 2225 3838 l  cp gs 0.00 setgray ef gr  col0 s
% Polyline
n 7800 1275 m
 2100 1275 l gs col0 s gr 
/Times-Roman-iso ff 180.00 scf sf
6600 5100 m
gs 1 -1 sc (Proof-irrelevance) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
3675 4200 m
gs 1 -1 sc (Excluded-middle) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
6900 1800 m
gs 1 -1 sc (Predicate extensionality) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
3375 3525 m
gs 1 -1 sc (\(Diaconescu\)) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
4650 3600 m
gs 1 -1 sc (Propositional degeneracy) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
3825 1800 m
gs 1 -1 sc (Relational choice axiom) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
1725 1800 m
gs 1 -1 sc (Description principle) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
2550 2400 m
gs 1 -1 sc (Functional choice axiom) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
3600 5100 m
gs 1 -1 sc (Decidability of equality on $A$) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
4425 4575 m
gs 1 -1 sc (\(needs Prop-impredicativity\)) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
5025 4725 m
gs 1 -1 sc (\(Berardi\)) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
1500 3075 m
gs 1 -1 sc (\(if Set impredicative\)) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
1500 4200 m
gs 1 -1 sc (Not excluded-middle) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
3600 6000 m
gs 1 -1 sc (Axiom K on A) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
3600 7200 m
gs 1 -1 sc (Invariance by substitution of reflexivity proofs for equality on A) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
6150 4200 m
gs 1 -1 sc (Propositional extensionality) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
2100 1200 m
gs 1 -1 sc (The dependency graph of axioms in the Calculus of Inductive Constructions) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
3600 6900 m
gs 1 -1 sc (Injectivity of equality on sigma-types on A) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
3600 6300 m
gs 1 -1 sc (Uniqueness of reflexivity proofs for equality on A) col0 sh gr
/Times-Roman-iso ff 180.00 scf sf
3600 6600 m
gs 1 -1 sc (Uniqueness of equality proofs on A) col0 sh gr
% here ends figure;
$F2psEnd
rs
showpage