# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# 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<nextA : {A x : HOD} → A ∋ x →  od→ord x o< next (odmax A)
 x<nextA {A} {x} A∋x = ordtrans (c<→o< {x} {A} A∋x) ho<
 
@@ -201,21 +197,10 @@
        lemma p lt | pair x y | tri> ¬a ¬b c = ordtrans (ω-opair  (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y))))))
            (A<Bnext c (subst (λ k → odef B k ) (sym diso) (proj2 (proj2 lt (pair x y)))))) (omax-x _ _ ) 
 
-ZFP⊗ :  {A B : HOD} → ZFP A B ≡ A ⊗ B
-ZFP⊗ {A} {B} = ==→o≡ record { eq→ = lemma0 ; eq← = lemma1 } where
-      AxB : HOD
-      AxB =  Replace B (λ b → Replace A (λ a → < a , b > )) 
-      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<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz
         omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz
 
+        nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny)
+        nn<omax {x} {nx} {ny} xnx xny with trio< nx ny
+        nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny
+        nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny
+        nn<omax {x} {nx} {ny} xnx xny | tri> ¬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) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) }
+
+Func∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
+    → def Func (od→ord  (Replace A (λ x → < x , f x > )))
 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 }