summaryrefslogtreecommitdiff
path: root/doc/faq/axioms.fig
diff options
context:
space:
mode:
Diffstat (limited to 'doc/faq/axioms.fig')
-rw-r--r--doc/faq/axioms.fig84
1 files changed, 0 insertions, 84 deletions
diff --git a/doc/faq/axioms.fig b/doc/faq/axioms.fig
deleted file mode 100644
index f0775930..00000000
--- a/doc/faq/axioms.fig
+++ /dev/null
@@ -1,84 +0,0 @@
-#FIG 3.2
-Landscape
-Center
-Inches
-Letter
-100.00
-Single
--2
-1200 2
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 6750.000 3600 6900 3450 6750 3600 6600
- 1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 6450.000 3600 6600 3450 6450 3600 6300
- 1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6150.000 3600 6300 3450 6150 3600 6000
- 1 1 1.00 60.00 120.00
- 1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6450.000 3600 6600 3450 6450 3600 6300
- 1 1 1.00 60.00 120.00
- 1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6750.000 3600 6900 3450 6750 3600 6600
- 1 1 1.00 60.00 120.00
- 1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 7050.000 3600 7200 3450 7050 3600 6900
- 1 1 1.00 60.00 120.00
- 1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 14032.500 5272.500 4725 1875 4425 2850 4200 4050
- 1 1 1.00 60.00 120.00
-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 5175 4200 5775
-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
- 7050 5175 4575 5775
-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 4275 4200 4875
-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
- 4950 4275 7125 4875
-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 1950 7200 4050
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
- 4350 3075 7350 1950
-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
- 7200 4275 7200 4875
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
- 3075 1875 3975 1875
-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
- 5550 3675 5550 4050
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
- 4575 4050 6450 4050
-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
- 3525 1875 3525 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
- 2325 1875 2250 3975
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
- 7800 1275 2100 1275
-4 0 0 50 -1 0 12 0.0000 4 135 1305 6600 5100 Proof-irrelevance\001
-4 0 0 50 -1 0 12 0.0000 4 135 1260 3675 4200 Excluded-middle\001
-4 0 0 50 -1 0 12 0.0000 4 180 1830 6900 1800 Predicate extensionality\001
-4 0 0 50 -1 0 12 0.0000 4 180 1050 3375 3525 (Diaconescu)\001
-4 0 0 50 -1 0 12 0.0000 4 180 1905 4650 3600 Propositional degeneracy\001
-4 0 0 50 -1 0 12 0.0000 4 135 1800 3825 1800 Relational choice axiom\001
-4 0 0 50 -1 0 12 0.0000 4 180 1575 1725 1800 Description principle\001
-4 0 0 50 -1 0 12 0.0000 4 135 1830 2550 2400 Functional choice axiom\001
-4 0 0 50 -1 0 12 0.0000 4 195 2340 3600 5100 Decidability of equality on $A$\001
-4 0 0 50 -1 0 12 0.0000 4 180 2175 4425 4575 (needs Prop-impredicativity)\001
-4 0 0 50 -1 0 12 0.0000 4 180 705 5025 4725 (Berardi)\001
-4 0 0 50 -1 0 12 0.0000 4 180 1620 1500 3075 (if Set impredicative)\001
-4 0 0 50 -1 0 12 0.0000 4 135 1560 1500 4200 Not excluded-middle\001
-4 0 0 50 -1 0 12 0.0000 4 135 1080 3600 6000 Axiom K on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 4800 3600 7200 Invariance by substitution of reflexivity proofs for equality on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 2100 6150 4200 Propositional extensionality\001
-4 0 0 50 -1 0 12 0.0000 4 180 5700 2100 1200 The dependency graph of axioms in the Calculus of Inductive Constructions\001
-4 0 0 50 -1 0 12 0.0000 4 180 3210 3600 6900 Injectivity of equality on sigma-types on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 3735 3600 6300 Uniqueness of reflexivity proofs for equality on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 2670 3600 6600 Uniqueness of equality proofs on A\001