# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1567008292 -32400
# Node ID 9e0125b06e767ac43d96701b77110b42984507a9
# Parent  08428a66167761b128af9565aed8fdaf70669c52
...

diff -r 08428a661677 -r 9e0125b06e76 cardinal.agda
--- a/cardinal.agda	Wed Aug 28 23:52:54 2019 +0900
+++ b/cardinal.agda	Thu Aug 29 01:04:52 2019 +0900
@@ -50,6 +50,9 @@
 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
 
+od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y
+od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq )
+
 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
 eq-prod refl refl = refl
 
@@ -131,27 +134,29 @@
 lemma77 : {ox oy : Ordinal } → ZFProduct ∋ < ord→od (pi1 ( pair ox oy ))  , ord→od (pi2 ( pair ox oy ))  >  ≡ ZFProduct ∋ < ord→od ox , ord→od oy > 
 lemma77  = refl
 
+
+p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
+p-iso {x} p = {!!} where
+
+pair-iso : {op ox oy : Ordinal} (x : ord-pair (od→ord < ord→od ox , ord→od oy >) )  → pi1 x ≡ ox → pi2 x ≡ oy → x ≡ pair ox oy
+pair-iso (pair ox oy) = {!!}
+
 p-iso3 : { ox oy  : Ordinal } →  (p : ZFProduct ∋ < ord→od ox , ord→od oy > ) → p ≡ pair ox oy
-p-iso3 p = {!!} where
-     lemma0 : {ox oy  : Ordinal } → ord-pair (od→ord < ord→od ox , ord→od oy >) ≡ ZFProduct ∋ < ord→od ox , ord→od oy >
-     lemma0 = refl
-     lemma1 : {op ox oy : Ordinal } → op ≡ od→ord < ord→od ox , ord→od oy >  → ord-pair op ≡ ZFProduct ∋ < ord→od ox , ord→od oy >
-     lemma1 refl = refl
-     lemma : {op ox oy : Ordinal } → (p : ord-pair op ) →  od→ord < ord→od ox , ord→od oy > ≡ op → p ≅ pair ox oy
-     lemma {op} {ox} {oy} (pair ox' oy') eq = {!!}
-
+p-iso3 {ox} {oy} p with p-iso p
+... | eq with prod-eq ( ord→== (cong (λ k → od→ord k) eq ) )
+... | record { proj1 = eq1 ; proj2 = eq2 } = lemma eq1 eq2 where
+    lemma : ord→od (pi1 p) ≡ ord→od ox → ord→od (pi2 p) ≡ ord→od oy → p ≡ pair ox oy
+    lemma eq1 eq2 with od≡→≡ eq1 | od≡→≡ eq2
+    ... | eq1' | eq2' = pair-iso {od→ord  < ord→od ox , ord→od oy >} {ox} {oy} p eq1' eq2'
 
 p-iso2 :  { ox oy  : Ordinal } → p-cons (ord→od ox) (ord→od oy) ≡ pair ox oy
-p-iso2 = subst₂ ( λ j k → j ≡ k ) {!!} {!!} refl
+p-iso2  {ox} {oy} = p-iso3 (p-cons (ord→od ox) (ord→od oy))
 
-p-iso1 :  { x y  : OD } → (p : ZFProduct ∋ < x , y > ) → < ord→od (π1 p) , ord→od (π2 p) > ≡  < x , y >
+p-iso1 :  { ox oy  : Ordinal  } → (p : ZFProduct ∋ < ord→od ox , ord→od oy > ) → < ord→od (π1 p) , ord→od (π2 p) > ≡  < ord→od ox , ord→od oy >
 p-iso1 {x} {y} p with p-cons (ord→od (π1 p)) (ord→od (π2 p))
-... | t = {!!}
+... | t with p-iso3 p | p-iso3 t
+... | refl | refl  = refl
     
-
-p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
-p-iso {x} p  = {!!}
-
 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
 ∋-p A x with p∨¬p ( A ∋ x )
 ∋-p A x | case1 t = yes t