Regenerate the axiom figure of the FAQ.

The .png was ugly (less than 400px wide) and did not match the content of
the .fig file (e.g. presence of '$'). To improve things a bit, text is now
rendered by latex.

7 files changed, 381 insertions, 247 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index d264ac62a..8495156ca 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -503,19 +503,34 @@ $\forall A \forall x y:A \forall p_1 p_2:x=y, p_1=p_2$
 \item Extensionality of functions: $\forall f g:A\rightarrow B, (\forall x, f(x)=g(x)) \rightarrow f=g$
 \end{itemize}
 
-Here is a summary of the relative strength of these axioms, most
-proofs can be found in directory {\tt Logic} of the standard library.
-The justification of their validity relies on the interpretability in
-set theory.
-
+Figure~\ref{fig:axioms} is a summary of the relative strength of these
+axioms, most proofs can be found in directory {\tt Logic} of the standard
+library. (Statements in boldface are the most ``interesting'' ones for
+Coq.) The justification of their validity relies on the interpretability
+in set theory.
+
+% fig2dev -m 2 -L png axioms.fig axioms.png
+% fig2dev -L pdftex axioms.fig axioms.pdf
+% fig2dev -L pdftex_t -p axioms.pdf axioms.fig axioms.pdf_t
+% fig2dev -L pstex axioms.fig axioms.eps
+% fig2dev -L pstex_t -p axioms.eps axioms.fig axioms.eps_t
+
+\begin{figure}[htbp]
 %HEVEA\imgsrc{axioms.png}
 %BEGIN LATEX
+\begin{center}
 \ifpdf   % si on est en pdflatex
-\includegraphics[width=1.0\textwidth]{axioms.png}
+\scalebox{0.65}{\input{axioms.pdf_t}}
+%\includegraphics[width=1.0\textwidth]{axioms.png}
 \else
-\includegraphics[width=1.0\textwidth]{axioms.eps}
+\scalebox{0.65}{\input{axioms.eps_t}}
+%\includegraphics[width=1.0\textwidth]{axioms.eps}
 \fi
+\end{center}
 %END LATEX
+\caption{The dependency graph of axioms in the Calculus of Inductive Constructions}
+\label{fig:axioms}
+\end{figure}
 
 \Question{What standard axioms are inconsistent with {\Coq}?}
 
diff --git a/doc/faq/axioms.eps b/doc/faq/axioms.eps
index 3f3c01c43..836afc347 100644
--- a/doc/faq/axioms.eps
+++ b/doc/faq/axioms.eps
@@ -1,11 +1,11 @@
-%!PS-Adobe-2.0 EPSF-2.0
+%!PS-Adobe-3.0 EPSF-3.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
+%%Creator: fig2dev Version 3.2 Patchlevel 5e
+%%CreationDate: Sun Jul 26 08:23:54 2015
+%%BoundingBox: 0 0 647 514
+%Magnification: 1.0000
 %%EndComments
+%%BeginProlog
 /$F2psDict 200 dict def
 $F2psDict begin
 $F2psDict /mtrx matrix put
@@ -44,10 +44,6 @@ $F2psDict /mtrx matrix put
 /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
@@ -80,51 +76,25 @@ newpath 0 372 moveto 0 0 lineto 437 0 lineto 437 372 lineto closepath clip newpa
   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
 
+/pageheader {
+save
+newpath 0 514 moveto 0 0 lineto 647 0 lineto 647 514 lineto closepath clip newpath
+-26.1 566.6 translate
+1 -1 scale
 $F2psBegin
 10 setmiterlimit
 0 slj 0 slc
  0.06000 0.06000 sc
+} bind def
+/pagefooter {
+$F2psEnd
+restore
+} bind def
+%%EndProlog
+pageheader
 %
 % Fig objects follow
 %
@@ -132,247 +102,316 @@ $F2psBegin
 % here starts figure with depth 50
 % Arc
 7.500 slw
+0 slc
 gs  clippath
-3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp
+4188 5861 m 4168 6010 l 4227 6018 l 4247 5869 l 4247 5869 l 4202 5984 l 4188 5861 l cp
 eoclip
-n 3600.0 6750.0 150.0 90.0 -90.0 arc
+n 14032.5 7222.5 9908.2 -159.9465 -172.9126 arcn
 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
+0 slj
+n 4188 5861 m 4202 5984 l 4247 5869 l 4188 5861 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
+3465 9040 m 3599 9108 l 3626 9054 l 3492 8987 l 3492 8987 l 3586 9068 l 3465 9040 l cp
 eoclip
-n 3600.0 6450.0 150.0 90.0 -90.0 arc
+n 3600.0 8925.0 150.0 90.0000 -90.0000 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
+n 3465 9040 m 3586 9068 l 3492 8987 l 3465 9040 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
+3465 8740 m 3599 8808 l 3626 8754 l 3492 8687 l 3492 8687 l 3586 8768 l 3465 8740 l cp
 eoclip
-n 3600.0 6150.0 150.0 90.0 -90.0 arc
+n 3600.0 8625.0 150.0 90.0000 -90.0000 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
+n 3465 8740 m 3586 8768 l 3492 8687 l 3465 8740 l  cp gs 0.00 setgray ef gr  col0 s
+% Arc
+gs  clippath
+3492 8262 m 3626 8195 l 3599 8141 l 3465 8209 l 3465 8209 l 3586 8182 l 3492 8262 l cp
+3465 8440 m 3599 8508 l 3626 8454 l 3492 8387 l 3492 8387 l 3586 8468 l 3465 8440 l cp
+eoclip
+n 3600.0 8325.0 150.0 90.0000 -90.0000 arc
+gs col0 s gr
+ gr
+
 % arrowhead
-n 3465 6265 m 3586 6293 l 3492 6212 l 3465 6265 l  cp gs 0.00 setgray ef gr  col0 s
+n 3465 8440 m 3586 8468 l 3492 8387 l 3465 8440 l  cp gs 0.00 setgray ef gr  col0 s
+% arrowhead
+n 3492 8262 m 3586 8182 l 3465 8209 l 3492 8262 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
+3492 8562 m 3626 8495 l 3599 8441 l 3465 8509 l 3465 8509 l 3586 8482 l 3492 8562 l cp
+3465 8740 m 3599 8808 l 3626 8754 l 3492 8687 l 3492 8687 l 3586 8768 l 3465 8740 l cp
 eoclip
-n 3600.0 6450.0 150.0 90.0 -90.0 arc
+n 3600.0 8625.0 150.0 90.0000 -90.0000 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
+n 3465 8740 m 3586 8768 l 3492 8687 l 3465 8740 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
+n 3492 8562 m 3586 8482 l 3465 8509 l 3492 8562 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
+3492 8862 m 3626 8795 l 3599 8741 l 3465 8809 l 3465 8809 l 3586 8782 l 3492 8862 l cp
+3465 9040 m 3599 9108 l 3626 9054 l 3492 8987 l 3492 8987 l 3586 9068 l 3465 9040 l cp
 eoclip
-n 3600.0 6750.0 150.0 90.0 -90.0 arc
+n 3600.0 8925.0 150.0 90.0000 -90.0000 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
+n 3465 9040 m 3586 9068 l 3492 8987 l 3465 9040 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
+n 3492 8862 m 3586 8782 l 3465 8809 l 3492 8862 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
+3492 9162 m 3626 9095 l 3599 9041 l 3465 9109 l 3465 9109 l 3586 9082 l 3492 9162 l cp
+3465 9340 m 3599 9408 l 3626 9354 l 3492 9287 l 3492 9287 l 3586 9368 l 3465 9340 l cp
 eoclip
-n 3600.0 7050.0 150.0 90.0 -90.0 arc
+n 3600.0 9225.0 150.0 90.0000 -90.0000 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
+n 3465 9340 m 3586 9368 l 3492 9287 l 3465 9340 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
+n 3492 9162 m 3586 9082 l 3465 9109 l 3492 9162 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
+3733 7095 m 3805 7227 l 3858 7198 l 3785 7066 l 3785 7066 l 3817 7186 l 3733 7095 l cp
 eoclip
-n 14032.5 5272.5 9908.2 -159.9 -172.9 arcn
+n 6309.5 5767.7 2867.8 -137.3570 150.0374 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
+n 3733 7095 m 3817 7186 l 3785 7066 l 3733 7095 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+gs  clippath
+7204 5860 m 7167 6007 l 7225 6021 l 7262 5874 l 7262 5874 l 7204 5984 l 7204 5860 l cp
+eoclip
+n 7725 3900 m
+ 7200 6000 l gs col0 s gr gr
+
+% arrowhead
+n 7204 5860 m 7204 5984 l 7262 5874 l 7204 5860 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
+7170 6914 m 7170 7065 l 7230 7065 l 7230 6914 l 7230 6914 l 7200 7034 l 7170 6914 l cp
 eoclip
-n 4200 5175 m
- 4200 5775 l gs col0 s gr gr
+n 7200 6225 m
+ 7200 7050 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
+n 7170 6914 m 7200 7034 l 7230 6914 l 7170 6914 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
+5520 5864 m 5520 6015 l 5580 6015 l 5580 5864 l 5580 5864 l 5550 5984 l 5520 5864 l cp
+5580 5761 m 5580 5610 l 5520 5610 l 5520 5761 l 5520 5761 l 5550 5641 l 5580 5761 l cp
 eoclip
-n 7050 5175 m
- 4575 5775 l gs col0 s gr gr
+n 5550 5625 m
+ 5550 6000 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
+n 5580 5761 m 5550 5641 l 5520 5761 l 5580 5761 l  cp gs 0.00 setgray ef gr  col0 s
+% arrowhead
+n 5520 5864 m 5550 5984 l 5580 5864 l 5520 5864 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
+3345 3464 m 3345 3615 l 3405 3615 l 3405 3464 l 3405 3464 l 3375 3584 l 3345 3464 l cp
+3405 3361 m 3405 3210 l 3345 3210 l 3345 3361 l 3345 3361 l 3375 3241 l 3405 3361 l cp
 eoclip
-n 4200 4275 m
- 4200 4875 l gs col0 s gr gr
+n 3375 3225 m
+ 3375 3600 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
+n 3405 3361 m 3375 3241 l 3345 3361 l 3405 3361 l  cp gs 0.00 setgray ef gr  col0 s
+% arrowhead
+n 3345 3464 m 3375 3584 l 3405 3464 l 3345 3464 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
+3344 2114 m 3346 2265 l 3406 2264 l 3404 2113 l 3404 2113 l 3376 2234 l 3344 2114 l cp
 eoclip
-n 4950 4275 m
- 7125 4875 l gs col0 s gr gr
+n 3373 1950 m
+ 3376 2250 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
+n 3344 2114 m 3376 2234 l 3404 2113 l 3344 2114 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
+3345 2864 m 3345 3015 l 3405 3015 l 3405 2864 l 3405 2864 l 3375 2984 l 3345 2864 l cp
+3405 2761 m 3405 2610 l 3345 2610 l 3345 2761 l 3345 2761 l 3375 2641 l 3405 2761 l cp
 eoclip
-n 7725 1950 m
- 7200 4050 l gs col0 s gr gr
+n 3375 2625 m
+ 3375 3000 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
+n 3405 2761 m 3375 2641 l 3345 2761 l 3405 2761 l  cp gs 0.00 setgray ef gr  col0 s
+% arrowhead
+n 3345 2864 m 3375 2984 l 3405 2864 l 3345 2864 l  cp gs 0.00 setgray ef gr  col0 s
 % Polyline
-n 4350 3075 m
- 7350 1950 l gs col0 s gr 
+n 2175 3600 m
+ 3750 3600 l gs col0 s gr 
 % Polyline
 gs  clippath
-7170 4890 m 7230 4890 l 7230 4739 l 7200 4859 l 7170 4739 l cp
+2611 2445 m 2460 2445 l 2460 2505 l 2611 2505 l 2611 2505 l 2491 2475 l 2611 2445 l cp
 eoclip
-n 7200 4275 m
- 7200 4875 l gs col0 s gr gr
+n 3075 2475 m
+ 2475 2475 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
+n 2611 2445 m 2491 2475 l 2611 2505 l 2611 2445 l  cp gs 0.00 setgray ef gr  col0 s
 % Polyline
-n 3075 1875 m
- 3975 1875 l gs col0 s gr 
+gs  clippath
+3345 1289 m 3347 1440 l 3407 1439 l 3405 1288 l 3405 1288 l 3377 1409 l 3345 1289 l cp
+eoclip
+n 3374 1125 m
+ 3377 1425 l gs col0 s gr gr
+
+% arrowhead
+n 3345 1289 m 3377 1409 l 3405 1288 l 3345 1289 l  cp gs 0.00 setgray ef gr  col0 s
 % 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
+1711 945 m 1560 945 l 1560 1005 l 1711 1005 l 1711 1005 l 1591 975 l 1711 945 l cp
 eoclip
-n 5550 3675 m
- 5550 4050 l gs col0 s gr gr
+n 3075 975 m
+ 1575 975 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
+n 1711 945 m 1591 975 l 1711 1005 l 1711 945 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+gs  clippath
+2161 1695 m 2010 1695 l 2010 1755 l 2161 1755 l 2161 1755 l 2041 1725 l 2161 1695 l cp
+eoclip
+n 3075 1725 m
+ 2025 1725 l gs col0 s gr gr
+
 % arrowhead
-n 5520 3914 m 5550 4034 l 5580 3914 l 5520 3914 l  cp gs 0.00 setgray ef gr  col0 s
+n 2161 1695 m 2041 1725 l 2161 1755 l 2161 1695 l  cp gs 0.00 setgray ef gr  col0 s
 % Polyline
-n 4575 4050 m
- 6450 4050 l gs col0 s gr 
+n 8025 5925 m 8250 5925 l 9000 4950 l
+ 9150 4950 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
+8312 4025 m 8275 3878 l 8217 3892 l 8254 4039 l 8254 4039 l 8254 3916 l 8312 4025 l cp
 eoclip
-n 3525 1875 m
- 3525 2250 l gs col0 s gr gr
+n 8625 5400 m
+ 8250 3900 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
+n 8312 4025 m 8254 3916 l 8254 4039 l 8312 4025 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+gs  clippath
+4700 7888 m 4553 7924 l 4567 7982 l 4714 7946 l 4714 7946 l 4591 7946 l 4700 7888 l cp
+eoclip
+n 7050 7350 m
+ 4575 7950 l gs col0 s gr gr
+
 % arrowhead
-n 3495 2114 m 3525 2234 l 3555 2114 l 3495 2114 l  cp gs 0.00 setgray ef gr  col0 s
+n 4700 7888 m 4591 7946 l 4714 7946 l 4700 7888 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
+4170 7814 m 4170 7965 l 4230 7965 l 4230 7814 l 4230 7814 l 4200 7934 l 4170 7814 l cp
 eoclip
-n 2325 1875 m
- 2250 3975 l gs col0 s gr gr
+n 4200 7500 m
+ 4200 7950 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
+n 4170 7814 m 4200 7934 l 4230 7814 l 4170 7814 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
+gs  clippath
+1295 3398 m 1339 3543 l 1397 3526 l 1353 3381 l 1353 3381 l 1359 3505 l 1295 3398 l cp
+1207 2893 m 1163 2748 l 1105 2765 l 1149 2910 l 1149 2910 l 1144 2787 l 1207 2893 l cp
+eoclip
+n 1139 2771 m
+ 1364 3521 l gs col0 s gr gr
+
+% arrowhead
+n 1207 2893 m 1144 2787 l 1149 2910 l 1207 2893 l  cp gs 0.00 setgray ef gr  col0 s
+% arrowhead
+n 1295 3398 m 1359 3505 l 1353 3381 l 1295 3398 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+n 4425 4875 m
+ 7350 3825 l gs col0 s gr 
+% Polyline
+gs  clippath
+1019 1289 m 1021 1440 l 1081 1439 l 1079 1288 l 1079 1288 l 1051 1409 l 1019 1289 l cp
+eoclip
+n 1048 1125 m
+ 1051 1425 l gs col0 s gr gr
+
+% arrowhead
+n 1019 1289 m 1051 1409 l 1079 1288 l 1019 1289 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+gs  clippath
+1020 2114 m 1022 2265 l 1082 2264 l 1080 2113 l 1080 2113 l 1052 2234 l 1020 2114 l cp
+eoclip
+n 1049 1950 m
+ 1052 2250 l gs col0 s gr gr
+
+% arrowhead
+n 1020 2114 m 1052 2234 l 1080 2113 l 1020 2114 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+gs  clippath
+2104 5879 m 2151 6023 l 2208 6005 l 2161 5861 l 2161 5861 l 2170 5985 l 2104 5879 l cp
+eoclip
+n 1500 3900 m
+ 2175 6000 l gs col0 s gr gr
+
+% arrowhead
+n 2104 5879 m 2170 5985 l 2161 5861 l 2104 5879 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+n 4575 6000 m
+ 6450 6000 l gs col0 s gr 
+% Polyline
+gs  clippath
+6900 7063 m 7043 7113 l 7063 7056 l 6920 7006 l 6920 7006 l 7024 7075 l 6900 7063 l cp
+eoclip
+n 4714 6255 m
+ 7039 7080 l gs col0 s gr gr
+
+% arrowhead
+n 6900 7063 m 7024 7075 l 6920 7006 l 6900 7063 l  cp gs 0.00 setgray ef gr  col0 s
+% Polyline
+gs  clippath
+4170 7064 m 4170 7215 l 4230 7215 l 4230 7064 l 4230 7064 l 4200 7184 l 4170 7064 l cp
+eoclip
+n 4200 6225 m
+ 4200 7200 l gs col-1 s gr gr
+
+% arrowhead
+n 4170 7064 m 4200 7184 l 4230 7064 l 4170 7064 l  cp gs 0.00 setgray ef gr  col-1 s
+% Polyline
+2 slj
+n 6450 7050 m 6448 7050 l 6444 7049 l 6437 7048 l 6425 7046 l 6408 7044 l
+ 6385 7040 l 6356 7036 l 6320 7030 l 6279 7024 l 6231 7017 l
+ 6177 7008 l 6118 6999 l 6054 6990 l 5986 6979 l 5915 6969 l
+ 5841 6958 l 5766 6946 l 5690 6935 l 5614 6924 l 5539 6913 l
+ 5464 6902 l 5391 6891 l 5320 6881 l 5252 6871 l 5185 6861 l
+ 5122 6852 l 5061 6843 l 5002 6835 l 4947 6827 l 4894 6820 l
+ 4843 6813 l 4796 6807 l 4750 6801 l 4707 6796 l 4666 6791 l
+ 4627 6786 l 4590 6782 l 4555 6778 l 4521 6774 l 4489 6771 l
+ 4458 6768 l 4429 6765 l 4400 6763 l 4350 6759 l 4303 6755 l
+ 4258 6753 l 4216 6751 l 4176 6751 l 4138 6750 l 4102 6751 l
+ 4068 6752 l 4037 6754 l 4008 6757 l 3980 6760 l 3955 6764 l
+ 3933 6768 l 3912 6773 l 3894 6778 l 3877 6784 l 3863 6790 l
+ 3850 6796 l 3839 6803 l 3829 6810 l 3820 6816 l 3813 6823 l
+ 3806 6830 l 3800 6838 l 3791 6850 l 3783 6863 l 3776 6878 l
+ 3771 6894 l 3766 6912 l 3762 6932 l 3759 6954 l 3756 6977 l
+ 3753 7000 l 3752 7021 l 3751 7036 l 3750 7045 l 3750 7049 l
+
+ 3750 7050 l gs col0 s gr 
 % here ends figure;
-$F2psEnd
-rs
+pagefooter
 showpage
+%%Trailer
+%EOF
diff --git a/doc/faq/axioms.eps_t b/doc/faq/axioms.eps_t
new file mode 100644
index 000000000..38f1a3fed
--- /dev/null
+++ b/doc/faq/axioms.eps_t
@@ -0,0 +1,43 @@
+\begin{picture}(0,0)%
+\includegraphics{axioms.eps}%
+\end{picture}%
+\setlength{\unitlength}{3947sp}%
+%
+\begingroup\makeatletter\ifx\SetFigFont\undefined%
+\gdef\SetFigFont#1#2#3#4#5{%
+  \reset@font\fontsize{#1}{#2pt}%
+  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
+  \selectfont}%
+\fi\endgroup%
+\begin{picture}(10779,8553)(436,-8605)
+\put(3676,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Excluded-middle}}}}
+\put(451,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Operator iota}}}}
+\put(3151,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive indefinite description}}}}
+\put(3151,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}}
+\put(451,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive definite descr.}}}}
+\put(451,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}}
+\put(3826,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Relational choice axiom}}}}
+\put(6901,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Predicate extensionality}}}}
+\put(1276,-4186){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(if Set impredicative)}}}}
+\put(3751,-4411){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Diaconescu)}}}}
+\put(4951,-4711){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional degeneracy}}}}
+\put(6151,-5311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional extensionality}}}}
+\put(4951,-5686){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(needs Prop-impredicativity)}}}}
+\put(6001,-5911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Berardi)}}}}
+\put(1576,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Not excluded-middle}}}}
+\put(3376,-6586){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Decidability of equality on any A}}}}
+\put(3601,-7336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Axiom K on A}}}}
+\put(3601,-7636){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of reflexivity proofs for equality on A}}}}
+\put(3601,-7936){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of equality proofs on A}}}}
+\put(3601,-8536){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Invariance by substitution of reflexivity proofs for equality on A}}}}
+\put(9001,-4336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional extensionality}}}}
+\put(3601,-8236){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Injectivity of equality on Sigma-types on A}}}}
+\put(6451,-6436){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Proof-irrelevance}}}}
+\put(3151,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Operator epsilon}}}}
+\put(3151,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}}
+\put(3151,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}indefinite description}}}}
+\put(3151,-2311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional choice axiom}}}}
+\put(451,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}}
+\put(451,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}definite description}}}}
+\put(451,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Axiom of unique choice}}}}
+\end{picture}%
diff --git a/doc/faq/axioms.fig b/doc/faq/axioms.fig
index 78e448865..963178503 100644
--- a/doc/faq/axioms.fig
+++ b/doc/faq/axioms.fig
@@ -1,4 +1,4 @@
-#FIG 3.2
+#FIG 3.2  Produced by xfig version 3.2.5c
 Landscape
 Center
 Inches
@@ -27,14 +27,6 @@ Single
 	1 1 1.00 60.00 120.00
 5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 6309.515 5767.724 4200 3825 3450 5550 3825 7200
 	1 1 1.00 60.00 120.00
-6 2025 300 7725 525
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 7725 525 2025 525
-4 0 0 50 -1 0 12 0.0000 4 180 5700 2025 450 The dependency graph of axioms in the Calculus of Inductive Constructions\001
--6
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 4200 6225 4200 7200
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
 	 7725 3900 7200 6000
@@ -45,8 +37,6 @@ Single
 	1 1 1.00 60.00 120.00
 	1 1 1.00 60.00 120.00
 	 5550 5625 5550 6000
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 4575 6000 6450 6000
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
 	1 1 1.00 60.00 120.00
 	1 1 1.00 60.00 120.00
@@ -68,12 +58,6 @@ Single
 	 3374 1125 3377 1425
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
-	 1049 1950 1052 2250
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 1048 1125 1051 1425
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
 	 3075 975 1575 975
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
@@ -89,49 +73,59 @@ Single
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
 	 4200 7500 4200 7950
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
+	1 1 1.00 60.00 120.00
+	1 1 1.00 60.00 120.00
+	 1139 2771 1364 3521
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
+	 4425 4875 7350 3825
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
-	 4714 6255 7039 7080
+	 1048 1125 1051 1425
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 1049 1950 1052 2250
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
 	 1500 3900 2175 6000
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
+	 4575 6000 6450 6000
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
+	 4714 6255 7039 7080
+2 1 0 1 -1 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
-	 1139 2771 1364 3521
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 4425 4875 7350 3825
+	 4200 6225 4200 7200
 3 0 0 1 0 7 50 -1 -1 0.000 0 0 0 4
 	 6450 7050 4050 6675 3750 6825 3750 7050
 	 0.000 1.000 1.000 0.000
-4 0 0 50 -1 0 12 0.0000 4 180 1830 6900 3750 Predicate extensionality\001
-4 0 0 50 -1 0 12 0.0000 4 135 1800 3825 3750 Relational choice axiom\001
-4 0 0 50 -1 0 12 0.0000 4 180 2100 6150 6150 Propositional extensionality\001
-4 0 0 50 -1 0 12 0.0000 4 180 1005 450 1050 Operator iota\001
-4 0 0 50 -1 2 12 0.0000 4 135 1020 450 1650 Constructive\001
-4 0 0 50 -1 2 12 0.0000 4 180 1530 450 1875 definite description\001
-4 0 0 50 -1 2 12 0.0000 4 180 2010 9000 5175 Functional extensionality\001
-4 0 0 50 -1 0 12 0.0000 4 180 4740 150 10050 Statements in boldface are the most "interesting" ones for Coq\001
-4 0 0 50 -1 0 12 0.0000 4 180 4800 3600 9375 Invariance by substitution of reflexivity proofs for equality on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 3735 3600 8475 Uniqueness of reflexivity proofs for equality on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 2670 3600 8775 Uniqueness of equality proofs on A\001
-4 0 0 50 -1 0 12 0.0000 4 135 1080 3600 8175 Axiom K on A\001
-4 0 0 50 -1 2 12 0.0000 4 135 1455 6450 7275 Proof-irrelevance\001
-4 0 0 50 -1 2 12 0.0000 4 180 3360 3600 9075 Injectivity of equality on Sigma-types on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 2175 4950 6525 (needs Prop-impredicativity)\001
-4 0 0 50 -1 0 12 0.0000 4 180 705 6000 6750 (Berardi)\001
-4 0 0 50 -1 2 12 0.0000 4 135 1290 3675 6225 Excluded-middle\001
-4 0 0 50 -1 0 12 0.0000 4 180 1905 4950 5550 Propositional degeneracy\001
-4 0 0 50 -1 0 12 0.0000 4 180 1050 3750 5250 (Diaconescu)\001
-4 0 0 50 -1 0 12 0.0000 4 180 2475 3375 7425 Decidability of equality on any A\001
-4 0 0 50 -1 0 12 0.0000 4 180 1620 1275 5025 (if Set impredicative)\001
-4 0 0 50 -1 0 12 0.0000 4 135 1560 1575 6225 Not excluded-middle\001
-4 0 0 50 -1 0 12 0.0000 4 180 1770 450 2625 in propositional context\001
-4 0 0 50 -1 2 12 0.0000 4 135 1020 3150 1650 Constructive\001
-4 0 0 50 -1 2 12 0.0000 4 180 1665 3150 1875 indefinite description\001
-4 0 0 50 -1 0 12 0.0000 4 180 2610 3150 2400 Constructive indefinite description\001
-4 0 0 50 -1 0 12 0.0000 4 180 1770 3150 2625 in propositional context\001
-4 0 0 50 -1 2 12 0.0000 4 135 1935 3150 3150 Functional choice axiom\001
-4 0 0 50 -1 0 12 0.0000 4 135 2100 450 2400 Constructive definite descr.\001
-4 0 0 50 -1 2 12 0.0000 4 180 1845 450 3750 Axiom of unique choice\001
-4 0 0 50 -1 2 12 0.0000 4 180 1365 3150 1050 Operator epsilon\001
+4 0 -1 50 -1 2 12 0.0000 2 135 1440 3675 6225 Excluded-middle\001
+4 0 -1 50 -1 0 12 0.0000 2 180 1065 450 1050 Operator iota\001
+4 0 -1 50 -1 0 12 0.0000 2 180 2850 3150 2400 Constructive indefinite description\001
+4 0 -1 50 -1 0 12 0.0000 2 180 1965 3150 2625 in propositional context\001
+4 0 -1 50 -1 0 12 0.0000 2 135 2235 450 2400 Constructive definite descr.\001
+4 0 -1 50 -1 0 12 0.0000 2 180 1965 450 2625 in propositional context\001
+4 0 -1 50 -1 0 12 0.0000 2 135 1995 3825 3750 Relational choice axiom\001
+4 0 -1 50 -1 0 12 0.0000 2 180 1965 6900 3750 Predicate extensionality\001
+4 0 -1 50 -1 0 12 0.0000 2 180 1710 1275 5025 (if Set impredicative)\001
+4 0 -1 50 -1 0 12 0.0000 2 165 1065 3750 5250 (Diaconescu)\001
+4 0 -1 50 -1 0 12 0.0000 2 180 2070 4950 5550 Propositional degeneracy\001
+4 0 -1 50 -1 0 12 0.0000 2 180 2310 6150 6150 Propositional extensionality\001
+4 0 -1 50 -1 0 12 0.0000 2 180 2325 4950 6525 (needs Prop-impredicativity)\001
+4 0 -1 50 -1 0 12 0.0000 2 165 720 6000 6750 (Berardi)\001
+4 0 -1 50 -1 0 12 0.0000 2 135 1725 1575 6225 Not excluded-middle\001
+4 0 -1 50 -1 0 12 0.0000 2 180 2730 3375 7425 Decidability of equality on any A\001
+4 0 -1 50 -1 0 12 0.0000 2 135 1170 3600 8175 Axiom K on A\001
+4 0 -1 50 -1 0 12 0.0000 2 180 4035 3600 8475 Uniqueness of reflexivity proofs for equality on A\001
+4 0 -1 50 -1 0 12 0.0000 2 180 2865 3600 8775 Uniqueness of equality proofs on A\001
+4 0 -1 50 -1 0 12 0.0000 2 180 5220 3600 9375 Invariance by substitution of reflexivity proofs for equality on A\001
+4 0 -1 50 -1 2 12 0.0000 2 180 2145 9000 5175 Functional extensionality\001
+4 0 -1 50 -1 2 12 0.0000 2 180 3585 3600 9075 Injectivity of equality on Sigma-types on A\001
+4 0 -1 50 -1 2 12 0.0000 2 135 1515 6450 7275 Proof-irrelevance\001
+4 0 -1 50 -1 2 12 0.0000 2 180 1440 3150 1050 Operator epsilon\001
+4 0 -1 50 -1 2 12 0.0000 2 135 1080 3150 1650 Constructive\001
+4 0 -1 50 -1 2 12 0.0000 2 180 1785 3150 1875 indefinite description\001
+4 0 -1 50 -1 2 12 0.0000 2 135 2085 3150 3150 Functional choice axiom\001
+4 0 -1 50 -1 2 12 0.0000 2 135 1080 450 1650 Constructive\001
+4 0 -1 50 -1 2 12 0.0000 2 180 1620 450 1875 definite description\001
+4 0 -1 50 -1 2 12 0.0000 2 180 1980 450 3750 Axiom of unique choice\001
diff --git a/doc/faq/axioms.pdf b/doc/faq/axioms.pdf
new file mode 100644
index 000000000..2ba5bf85b
--- /dev/null
+++ b/doc/faq/axioms.pdf
diff --git a/doc/faq/axioms.pdf_t b/doc/faq/axioms.pdf_t
new file mode 100644
index 000000000..06dc4b280
--- /dev/null
+++ b/doc/faq/axioms.pdf_t
@@ -0,0 +1,43 @@
+\begin{picture}(0,0)%
+\includegraphics{axioms.pdf}%
+\end{picture}%
+\setlength{\unitlength}{3947sp}%
+%
+\begingroup\makeatletter\ifx\SetFigFont\undefined%
+\gdef\SetFigFont#1#2#3#4#5{%
+  \reset@font\fontsize{#1}{#2pt}%
+  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
+  \selectfont}%
+\fi\endgroup%
+\begin{picture}(10779,8553)(436,-8605)
+\put(3676,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Excluded-middle}}}}
+\put(451,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Operator iota}}}}
+\put(3151,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive indefinite description}}}}
+\put(3151,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}}
+\put(451,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive definite descr.}}}}
+\put(451,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}}
+\put(3826,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Relational choice axiom}}}}
+\put(6901,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Predicate extensionality}}}}
+\put(1276,-4186){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(if Set impredicative)}}}}
+\put(3751,-4411){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Diaconescu)}}}}
+\put(4951,-4711){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional degeneracy}}}}
+\put(6151,-5311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional extensionality}}}}
+\put(4951,-5686){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(needs Prop-impredicativity)}}}}
+\put(6001,-5911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Berardi)}}}}
+\put(1576,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Not excluded-middle}}}}
+\put(3376,-6586){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Decidability of equality on any A}}}}
+\put(3601,-7336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Axiom K on A}}}}
+\put(3601,-7636){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of reflexivity proofs for equality on A}}}}
+\put(3601,-7936){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of equality proofs on A}}}}
+\put(3601,-8536){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Invariance by substitution of reflexivity proofs for equality on A}}}}
+\put(9001,-4336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional extensionality}}}}
+\put(3601,-8236){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Injectivity of equality on Sigma-types on A}}}}
+\put(6451,-6436){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Proof-irrelevance}}}}
+\put(3151,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Operator epsilon}}}}
+\put(3151,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}}
+\put(3151,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}indefinite description}}}}
+\put(3151,-2311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional choice axiom}}}}
+\put(451,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}}
+\put(451,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}definite description}}}}
+\put(451,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Axiom of unique choice}}}}
+\end{picture}%
diff --git a/doc/faq/axioms.png b/doc/faq/axioms.png
index 2aee09166..a86eed7f1 100644
--- a/doc/faq/axioms.png
+++ b/doc/faq/axioms.png