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

comparison OD.agda @ 183:de3d87b7494f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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)