Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 277:d9d3654baee1
seperate choice from LEM
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 09 May 2020 09:38:21 +0900 |
parents | 6f10c47e4e7a |
children | 5de8905a5a2b 359402cc6c3d |
comparison
equal
deleted
inserted
replaced
276:6f10c47e4e7a | 277:d9d3654baee1 |
---|---|
50 | 50 |
51 ⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y | 51 ⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y |
52 eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m | 52 eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m |
53 eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m | 53 eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m |
54 | 54 |
55 -- Ordinal in OD ( and ZFSet ) Transitive Set | |
56 Ord : ( a : Ordinal ) → OD | |
57 Ord a = record { def = λ y → y o< a } | |
58 | |
59 od∅ : OD | |
60 od∅ = Ord o∅ | |
61 | |
62 -- next assumptions are our axiom | 55 -- next assumptions are our axiom |
63 -- it defines a subset of OD, which is called HOD, usually defined as | 56 -- it defines a subset of OD, which is called HOD, usually defined as |
64 -- HOD = { x | TC x ⊆ OD } | 57 -- HOD = { x | TC x ⊆ OD } |
65 -- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x | 58 -- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x |
66 | 59 |
67 postulate | 60 record ODAxiom : Set (suc n) where |
68 -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) | 61 -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) |
62 field | |
69 od→ord : OD → Ordinal | 63 od→ord : OD → Ordinal |
70 ord→od : Ordinal → OD | 64 ord→od : Ordinal → OD |
71 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y | 65 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y |
72 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x | 66 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x |
73 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x | 67 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x |
74 ==→o≡ : { x y : OD } → (x == y) → x ≡ y | 68 ==→o≡ : { x y : OD } → (x == y) → x ≡ y |
75 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD | |
76 -- o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x | |
77 -- ord→od x ≡ Ord x results the same | |
78 -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum ) | 69 -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum ) |
79 sup-o : ( OD → Ordinal ) → Ordinal | 70 sup-o : ( OD → Ordinal ) → Ordinal |
80 sup-o< : { ψ : OD → Ordinal } → ∀ {x : OD } → ψ x o< sup-o ψ | 71 sup-o< : { ψ : OD → Ordinal } → ∀ {x : OD } → ψ x o< sup-o ψ |
81 -- contra-position of mimimulity of supermum required in Power Set Axiom | 72 -- contra-position of mimimulity of supermum required in Power Set Axiom which we don't use |
82 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal | 73 -- sup-x : {n : Level } → ( OD → Ordinal ) → Ordinal |
83 -- sup-lb : {n : Level } → { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) | 74 -- sup-lb : {n : Level } → { ψ : OD → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) |
75 | |
76 postulate odAxiom : ODAxiom | |
77 open ODAxiom odAxiom | |
84 | 78 |
85 data One : Set n where | 79 data One : Set n where |
86 OneObj : One | 80 OneObj : One |
87 | 81 |
82 -- Ordinals in OD , the maximum | |
88 Ords : OD | 83 Ords : OD |
89 Ords = record { def = λ x → One } | 84 Ords = record { def = λ x → One } |
90 | 85 |
91 maxod : {x : OD} → od→ord x o< od→ord Ords | 86 maxod : {x : OD} → od→ord x o< od→ord Ords |
92 maxod {x} = c<→o< OneObj | 87 maxod {x} = c<→o< OneObj |
88 | |
89 -- Ordinal in OD ( and ZFSet ) Transitive Set | |
90 Ord : ( a : Ordinal ) → OD | |
91 Ord a = record { def = λ y → y o< a } | |
92 | |
93 od∅ : OD | |
94 od∅ = Ord o∅ | |
95 | |
93 | 96 |
94 o<→c<→OD=Ord : ( {x y : Ordinal } → x o< y → def (ord→od y) x ) → {x : OD } → x ≡ Ord (od→ord x) | 97 o<→c<→OD=Ord : ( {x y : Ordinal } → x o< y → def (ord→od y) x ) → {x : OD } → x ≡ Ord (od→ord x) |
95 o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | 98 o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where |
96 lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y | 99 lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y |
97 lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → def x k ) (sym diso) lt)) | 100 lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → def x k ) (sym diso) lt)) |
254 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } | 257 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } |
255 _∈_ : ( A B : ZFSet ) → Set n | 258 _∈_ : ( A B : ZFSet ) → Set n |
256 A ∈ B = B ∋ A | 259 A ∈ B = B ∋ A |
257 Power : OD → OD | 260 Power : OD → OD |
258 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) | 261 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) |
259 {_} : ZFSet → ZFSet | 262 -- {_} : ZFSet → ZFSet |
260 { x } = ( x , x ) | 263 -- { x } = ( x , x ) |
261 | 264 |
262 data infinite-d : ( x : Ordinal ) → Set n where | 265 data infinite-d : ( x : Ordinal ) → Set n where |
263 iφ : infinite-d o∅ | 266 iφ : infinite-d o∅ |
264 isuc : {x : Ordinal } → infinite-d x → | 267 isuc : {x : Ordinal } → infinite-d x → |
265 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) | 268 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) |