# HG changeset patch # User Shinji KONO # Date 1596184945 -32400 # Node ID 53422a8ea836cfa9056fa2c0f3969e7e76c060b0 # Parent 4af94768e3725c8bf4850f30dd7f7fc0fc7d0394 bijection diff -r 4af94768e372 -r 53422a8ea836 OPair.agda --- a/OPair.agda Fri Jul 31 12:57:59 2020 +0900 +++ b/OPair.agda Fri Jul 31 17:42:25 2020 +0900 @@ -166,10 +166,6 @@ lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (od→ord < a , b >) lemma2 = replacement← A a A∋a --- axiom of choice required --- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (od→ord x) --- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (od→ord k )) {!!} op-cons - x ¬a ¬b c = ordtrans (ω-opair (x )) - lemma0 : {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x - lemma0 {px} record { proj1 = (pair x y) ; proj2 = p2 } = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) ))) - lemma1 : {x : Ordinal} → odef (A ⊗ B) x → odef (ZFP A B) x - lemma1 {x} lt with union← AxB (ord→od x) (d→∋ (A ⊗ B) lt) - ... | t = {!!} +ZFP⊆⊗ : {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x +ZFP⊆⊗ {A} {B} {px} record { proj1 = (pair x y) ; proj2 = p2 } = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) ))) - - - +-- axiom of choice required +-- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (od→ord x) +-- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (od→ord k )) {!!} op-cons - - - - diff -r 4af94768e372 -r 53422a8ea836 Ordinals.agda --- a/Ordinals.agda Fri Jul 31 12:57:59 2020 +0900 +++ b/Ordinals.agda Fri Jul 31 17:42:25 2020 +0900 @@ -313,6 +313,12 @@ omax ¬a ¬b c = osuc ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx + record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where field os→ : (x : Ordinal) → x o< maxordinal → Ordinal diff -r 4af94768e372 -r 53422a8ea836 cardinal.agda --- a/cardinal.agda Fri Jul 31 12:57:59 2020 +0900 +++ b/cardinal.agda Fri Jul 31 17:42:25 2020 +0900 @@ -26,37 +26,51 @@ open Bool open _==_ +open HOD + -- _⊗_ : (A B : HOD) → HOD -- A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) )) -Func : ( A B : HOD ) → OD -Func A B = record { def = λ x → (odef (Power (A ⊗ B)) x) +Func : OD +Func = record { def = λ x → def ZFProduct x ∧ ( (a b c : Ordinal) → odef (ord→od x) (od→ord < ord→od a , ord→od b >) ∧ odef (ord→od x) (od→ord < ord→od a , ord→od c >) → b ≡ c ) } -Func∋f : {A B x : HOD} → ( f : (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y ))) → (lt : A ∋ x ) → def (Func A B ) (od→ord < x , proj1 (f x lt) > ) +FuncP : ( A B : HOD ) → HOD +FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x + ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) } + ; odmax = odmax (ZFP A B) ; ))) Func∋f = {!!} -Func→f : {A B f x : HOD} → def ( Func A B) (od→ord f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y )) +FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x ) + → odef (FuncP A B) (od→ord (Replace A (λ x → < x , f x > ))) +FuncP∋f = {!!} + +Func→f : {A B f x : HOD} → def Func (od→ord f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y )) Func→f = {!!} -Func₁ : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!} +Func₁ : {A B f : HOD} → def Func (od→ord f) → {!!} Func₁ = {!!} -Cod : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!} +Cod : {A B f : HOD} → def Func (od→ord f) → {!!} Cod = {!!} -1-1 : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!} +1-1 : {A B f : HOD} → def Func (od→ord f) → {!!} 1-1 = {!!} -onto : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!} +onto : {A B f : HOD} → def Func (od→ord f) → {!!} onto = {!!} record Bijection (A B : Ordinal ) : Set n where field - bfun : Ordinal - bfun-isfun : def (Func (ord→od A) (ord→od B)) bfun - bfun-is1-1 : {!!} - bfun-isonto : {!!} + fun→ : Ordinal → Ordinal + fun← : Ordinal → Ordinal + fun→inA : (x : Ordinal) → odef (ord→od A) ( fun→ x ) + fun←inB : (x : Ordinal) → odef (ord→od B) ( fun← x ) + fiso→ : (x : Ordinal ) → odef (ord→od A) x → fun→ ( fun← x ) ≡ x + fiso← : (x : Ordinal ) → odef (ord→od B) x → fun← ( fun→ x ) ≡ x Card : OD Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }