Mercurial > hg > Members > kono > Proof > ZF-in-agda

annotate LEMC.agda @ 334:ba3ebb9a16c6 release

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
HOD
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jul 2020 16:59:13 +0900
parents 12071f79f3cf
children 2a8a51375e49
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
1 open import Level
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
2 open import Ordinals
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
3 open import logic
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
4 open import Relation.Nullary
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
5 module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) where
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
7 open import zf
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
8 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
9 open import Relation.Binary.PropositionalEquality
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
10 open import Data.Nat.Properties
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
11 open import Data.Empty
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
12 open import Relation.Binary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
13 open import Relation.Binary.Core
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
14
213
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
15 open import nat
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
16 import OD
213
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
17
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
18 open inOrdinal O
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
19 open OD O
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
20 open OD.OD
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
21 open OD._==_
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
22 open ODAxiom odAxiom
119
6e264c78e420 infinite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
23
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
24 open import zfc
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
25
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
26 --- With assuption of HOD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
27 ---
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
28 record choiced ( X : HOD) : Set (suc n) where
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
29 field
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
30 a-choice : HOD
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
31 is-in : X ∋ a-choice
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
32
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
33 open HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
34 _=h=_ : (x y : HOD) → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
35 x =h= y = od x == od y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
36
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
37 open choiced
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
38
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
39 OD→ZFC : ZFC
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
40 OD→ZFC = record {
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
41 ZFSet = HOD
43
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
42 ; _∋_ = _∋_
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
43 ; _≈_ = _=h=_
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
44 ; ∅ = od∅
28
f36e40d5d2c3 OD continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
45 ; Select = Select
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
46 ; isZFC = isZFC
28
f36e40d5d2c3 OD continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
47 } where
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
48 -- infixr 200 _∈_
96
f239ffc27fd0 Power Set and L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
49 -- infixr 230 _∩_ _∪_
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
50 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
51 isZFC = record {
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
52 choice-func = λ A {X} not A∋X → a-choice (choice-func X not );
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
53 choice = λ A {X} A∋X not → is-in (choice-func X not)
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
54 } where
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
55 choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced X
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
56 choice-func X not = have_to_find where
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
57 ψ : ( ox : Ordinal ) → Set (suc n)
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
58 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced X
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
59 lemma-ord : ( ox : Ordinal ) → ψ ox
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
60 lemma-ord ox = TransFinite1 {ψ} induction ox where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
61 ∋-p : (A x : HOD ) → Dec ( A ∋ x )
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
62 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
63 ∋-p A x | case1 (lift t) = yes t
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
64 ∋-p A x | case2 t = no (λ x → t (lift x ))
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
65 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) }
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
66 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
67 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
68 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
69 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
70 lemma : ¬ ((x : Ordinal ) → A x) → B
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
71 lemma not with p∨¬p B
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
72 lemma not | case1 b = b
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
73 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
74 induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
75 induction x prev with ∋-p X ( ord→od x)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
76 ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
77 ... | no ¬p = lemma where
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
78 lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced X
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
79 lemma1 y with ∋-p X (ord→od y)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
80 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
81 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
82 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced X
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
83 lemma = ∀-imply-or lemma1
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
84 have_to_find : choiced X
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
85 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
86 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥)
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
87 ¬¬X∋x nn = not record {
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
88 eq→ = λ {x} lt → ⊥-elim (nn x (odef→o< lt) lt)
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
89 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
90 }
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
91 record Minimal (x : HOD) : Set (suc n) where
280
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 279
diff changeset
92 field
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
93 min : HOD
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
94 x∋min : x ∋ min
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
95 min-empty : (y : HOD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
280
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 279
diff changeset
96 open Minimal
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
97 open _∧_
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
98 --
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
99 -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
100 --
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
101 induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
102 → (u : HOD ) → (u∋x : u ∋ x) → Minimal u
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
103 induction {x} prev u u∋x with p∨¬p ((y : HOD) → ¬ (x ∋ y) ∧ (u ∋ y))
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
104 ... | case1 P =
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
105 record { min = x
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
106 ; x∋min = u∋x
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
107 ; min-empty = P
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
108 }
285
313140ae5e3d clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
109 ... | case2 NP = min2 where
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
110 p : HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
111 p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
112 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
113 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
114 np : ¬ (p =h= od∅)
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
115 np p∅ = NP (λ y p∋y → ∅< {p} {_} p∋y p∅ )
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
116 y1choice : choiced p
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
117 y1choice = choice-func p np
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
118 y1 : HOD
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
119 y1 = a-choice y1choice
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
120 y1prop : (x ∋ y1) ∧ (u ∋ y1)
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
121 y1prop = is-in y1choice
285
313140ae5e3d clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
122 min2 : Minimal u
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
123 min2 = prev (proj1 y1prop) u (proj2 y1prop)
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
124 Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
125 Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
126 cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced x
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
127 cx {x} nx = choice-func x nx
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
128 minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
129 minimal x ne = min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne)))
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
130 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
131 x∋minimal x ne = x∋min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne)))
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
132 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) )
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
133 minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
134
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
135
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
136
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
137