Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 183:de3d87b7494f
fix zf
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 21 Jul 2019 17:56:12 +0900 |
parents | 9f3c0e0b2bc9 |
children | 65e1b2e415bb |
comparison
equal
deleted
inserted
replaced
182:9f3c0e0b2bc9 | 183:de3d87b7494f |
---|---|
69 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ | 69 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ |
70 -- contra-position of mimimulity of supermum required in Power Set Axiom | 70 -- contra-position of mimimulity of supermum required in Power Set Axiom |
71 -- sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} | 71 -- sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} |
72 -- sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) | 72 -- sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) |
73 -- sup-lb : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → ( ∀ {x : Ordinal {n}} → ψx o< z ) → z o< osuc ( sup-o ψ ) | 73 -- sup-lb : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → ( ∀ {x : Ordinal {n}} → ψx o< z ) → z o< osuc ( sup-o ψ ) |
74 -- mimimul and x∋minimul is a weaker form of Axiom of choice | 74 -- mimimul and x∋minimul is an Axiom of choice |
75 minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} | 75 minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} |
76 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) | 76 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) |
77 x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) ) | 77 x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) ) |
78 -- | |
78 minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) ) | 79 minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) ) |
79 | 80 |
80 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n | 81 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n |
81 _∋_ {n} a x = def a ( od→ord x ) | 82 _∋_ {n} a x = def a ( od→ord x ) |
82 | 83 |
290 ; union← = union← | 291 ; union← = union← |
291 ; empty = empty | 292 ; empty = empty |
292 ; power→ = power→ | 293 ; power→ = power→ |
293 ; power← = power← | 294 ; power← = power← |
294 ; extensionality = extensionality | 295 ; extensionality = extensionality |
295 ; minimul = minimul | 296 ; ε-induction = ε-induction |
296 ; regularity = regularity | |
297 ; infinity∅ = infinity∅ | 297 ; infinity∅ = infinity∅ |
298 ; infinity = infinity | 298 ; infinity = infinity |
299 ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y} | 299 ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y} |
300 ; replacement← = replacement← | 300 ; replacement← = replacement← |
301 ; replacement→ = replacement→ | 301 ; replacement→ = replacement→ |
302 ; choice-func = choice-func | |
303 ; choice = choice | |
302 } where | 304 } where |
303 | 305 |
304 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) | 306 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) |
305 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B) | 307 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B) |
306 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B) | 308 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B) |