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

annotate LEMC.agda @ 285:313140ae5e3d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 10 May 2020 09:25:13 +0900
parents a8f9c8a27e8d
children 5de8905a5a2b
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
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
26 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
27 ---
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
28 record choiced ( X : OD) : Set (suc n) where
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
29 field
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
30 a-choice : OD
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
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
33 open choiced
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
34
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
35 double-neg-eilm : {A : Set (suc n)} → ¬ ¬ A → A -- we don't have this in intutionistic logic
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
36 double-neg-eilm {A} notnot with p∨¬p A -- assuming axiom of choice
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
37 ... | case1 p = p
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
38 ... | case2 ¬p = ⊥-elim ( notnot ¬p )
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
39
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
40
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
41 OD→ZFC : ZFC
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
42 OD→ZFC = record {
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
43 ZFSet = OD
43
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
44 ; _∋_ = _∋_
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
45 ; _≈_ = _==_
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
46 ; ∅ = od∅
28
f36e40d5d2c3 OD continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
47 ; Select = Select
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
48 ; isZFC = isZFC
28
f36e40d5d2c3 OD continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
49 } where
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
50 -- infixr 200 _∈_
96
f239ffc27fd0 Power Set and L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
51 -- infixr 230 _∩_ _∪_
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
52 isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
53 isZFC = record {
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
54 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
55 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
56 } where
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
57 choice-func : (X : OD ) → ¬ ( X == od∅ ) → choiced X
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
58 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
59 ψ : ( ox : Ordinal ) → Set (suc n)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
60 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
61 lemma-ord : ( ox : Ordinal ) → ψ ox
235
846e0926bb89 fix cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
62 lemma-ord ox = TransFinite {ψ} induction ox where
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
63 ∋-p : (A x : OD ) → Dec ( A ∋ x )
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
64 ∋-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
65 ∋-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
66 ∋-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
67 ∀-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
68 → ((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
69 ∀-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
70 ∀-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
71 ∀-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
72 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
73 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
74 lemma not | case1 b = b
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
75 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
76 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
77 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
78 ... | 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
79 ... | no ¬p = lemma where
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
80 lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
81 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
82 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
83 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
84 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
85 lemma = ∀-imply-or lemma1
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
86 have_to_find : choiced X
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
87 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
88 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
89 ¬¬X∋x nn = not record {
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
90 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
91 ; 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
92 }
285
313140ae5e3d clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
93 record Minimal (x : OD) : Set (suc n) where
280
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 279
diff changeset
94 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 279
diff changeset
95 min : OD
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
96 x∋min : x ∋ min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
97 min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
280
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 279
diff changeset
98 open Minimal
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
99 open _∧_
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
100 --
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
101 -- 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
102 --
285
313140ae5e3d clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
103 induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u )
313140ae5e3d clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
104 → (u : OD ) → (u∋x : u ∋ x) → Minimal u
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
105 induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y))
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
106 ... | case1 P =
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
107 record { min = x
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
108 ; x∋min = u∋x
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
109 ; min-empty = P
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
110 }
285
313140ae5e3d clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
111 ... | case2 NP = min2 where
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
112 p : OD
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
113 p = record { def = λ y1 → def x y1 ∧ def u y1 }
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
114 np : ¬ (p == od∅)
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
115 np p∅ = NP (λ y p∋y → ∅< p∋y p∅ )
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
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
118 y1 : OD
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)
285
313140ae5e3d clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
124 Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u
313140ae5e3d clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
125 Min2 x u u∋x = (ε-induction {λ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x )
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
126 cx : {x : OD} → ¬ (x == od∅ ) → choiced x
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
127 cx {x} nx = choice-func x nx
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
128 minimal : (x : OD ) → ¬ (x == od∅ ) → OD
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
129 minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not)))
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
130 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
284
a8f9c8a27e8d minimal from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
131 x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne)))
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
132 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def 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