# HG changeset patch # User Shinji KONO # Date 1592811811 -32400 # Node ID be6670af87fa32a81179eb4ccf1378b1e6cb8892 # Parent 42f89e5efb00569c5edce3ea795853e91386dc32 maxod try diff -r 42f89e5efb00 -r be6670af87fa OD.agda --- a/OD.agda Mon Jun 15 18:15:48 2020 +0900 +++ b/OD.agda Mon Jun 22 16:43:31 2020 +0900 @@ -70,15 +70,18 @@ record ODAxiom : Set (suc n) where -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) field + maxod : Ordinal od→ord : OD → Ordinal - ord→od : Ordinal → OD + ord→od : (x : Ordinal ) → x o< maxod → OD + o ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl ) - ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) + ⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym (diso {!!})) refl ) + ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt (diso {!!}) refl )) union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) union← X z UX∋z = FExists _ lemma UX∋z where - lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z)) - lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } + lemma : {y : Ordinal} → def X y ∧ def (ord→od y {!!} ) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z)) + lemma {y} xx not = not (ord→od y {!!} ) record { proj1 = subst ( λ k → def X k ) (sym (diso {!!})) (proj1 xx ) ; proj2 = proj2 xx } ψiso : {ψ : OD → Set n} {x y : OD } → ψ x → x ≡ y → ψ y ψiso {ψ} t refl = t @@ -345,13 +353,13 @@ lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where - lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y)))) - → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y))) + lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y {!!} )))) + → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} ))) lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where - lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y))) → (ord→od (od→ord x) == ψ (ord→od y)) - lemma3 {y} eq = subst (λ k → ord→od (od→ord x) == k ) oiso (o≡→== eq ) - lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)) ) - lemma not y not2 = not (ord→od y) (subst (λ k → k == ψ (ord→od y)) oiso ( proj2 not2 )) + lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y {!!} ))) → (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} )) + lemma3 {y} eq = subst (λ k → ord→od (od→ord x) {!!} == k ) oiso (o≡→== eq ) + lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} )) ) + lemma not y not2 = not (ord→od y {!!} ) (subst (λ k → k == ψ (ord→od y {!!} )) oiso ( proj2 not2 )) --- --- Power Set @@ -364,7 +372,7 @@ ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) ∩-≡ {a} {b} inc = record { eq→ = λ {x} x