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

comparison OD.agda @ 216:5b9b6ef971dd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cardinal start
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 04 Aug 2019 18:09:00 +0900
parents f15eaa7c5932
children d5668179ee69
comparison
equal deleted inserted replaced
215:f15eaa7c5932 216:5b9b6ef971dd
257 subset-lemma : {n : Level} → {A x y : OD {suc n} } → ( x ∋ y → ZFSubset A x ∋ y ) ⇔ ( _⊆_ x A {y} ) 257 subset-lemma : {n : Level} → {A x y : OD {suc n} } → ( x ∋ y → ZFSubset A x ∋ y ) ⇔ ( _⊆_ x A {y} )
258 subset-lemma {n} {A} {x} {y} = record { 258 subset-lemma {n} {A} {x} {y} = record {
259 proj1 = λ z lt → proj1 (z lt) 259 proj1 = λ z lt → proj1 (z lt)
260 ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt } 260 ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
261 } 261 }
262
263 262
264 -- Constructible Set on α 263 -- Constructible Set on α
265 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x } 264 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x }
266 -- L (Φ 0) = Φ 265 -- L (Φ 0) = Φ
267 -- L (OSuc lv n) = { Def ( L n ) } 266 -- L (OSuc lv n) = { Def ( L n ) }
622 ¬¬X∋x nn = not record { 621 ¬¬X∋x nn = not record {
623 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) 622 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
624 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) 623 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
625 } 624 }
626 625
626 ------------
627 --
628 -- Onto map
629 -- def X x -> xmap
630 -- X ---------------------------> Y
631 -- ymap <- def Y y
632 --
633 record Onto {n : Level } (X Y : OD {suc n}) : Set (suc (suc n)) where
634 field
635 xmap : (x : Ordinal {suc n}) → Ordinal {suc n}
636 ymap : (y : Ordinal {suc n}) → Ordinal {suc n}
637 xmap-on-Y : (x : Ordinal {suc n} ) → def X x → def Y (xmap x)
638 ymap-on-X : (y : Ordinal {suc n} ) → def Y y → def X (ymap y)
639 onto-iso : (y : Ordinal {suc n} ) → def Y y → xmap ( ymap y ) ≡ y
640
641 record Cardinal {n : Level } (X : OD {suc n}) : Set (suc (suc n)) where
642 field
643 cardinal : Ordinal {suc n}
644 conto : Onto (Ord cardinal) X
645 cmax : ( y : Ordinal {suc n} ) → cardinal o< y → ¬ Onto (Ord y) X
646
647 cardinal : {n : Level } (X : OD {suc n}) → Cardinal X
648 cardinal {n} X = record {
649 cardinal = sup-o ( λ x → cardinal-p x )
650 ; conto = {!!}
651 ; cmax = {!!}
652 } where
653 cardinal-p : (x : Ordinal {suc n}) → Ordinal {suc n}
654 cardinal-p x with p∨¬p ( Onto (Ord x) X )
655 cardinal-p x | case1 True = x
656 cardinal-p x | case2 False = o∅