# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1566991955 -32400
# Node ID 2ecda48298e319ea011f9ec0cb2aae6ae742dcbb
# Parent  9fd85b954477a124626527f80004d95300b2d728
...

diff -r 9fd85b954477 -r 2ecda48298e3 cardinal.agda
--- a/cardinal.agda	Tue Aug 27 14:13:27 2019 +0900
+++ b/cardinal.agda	Wed Aug 28 20:32:35 2019 +0900
@@ -27,39 +27,8 @@
 <_,_> : (x y : OD) → OD
 < x , y > = (x , x ) , (x , y )
 
-data ord-pair : (p : Ordinal) → Set n where
-   pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
-
-ZFProduct : OD
-ZFProduct = record { def = λ x → ord-pair x }
-
-pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
-pi1 ( pair x y ) = x
-
-π1 : { p : OD } → ZFProduct ∋ p → Ordinal
-π1 lt = pi1 lt 
-
-pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
-pi2 ( pair x y ) = y
-
-π2 : { p : OD } → ZFProduct ∋ p → Ordinal
-π2 lt = pi2 lt 
-
-p-cons :  ( x y  : OD ) → ZFProduct ∋ < x , y >
-p-cons x y =  def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
-    let open ≡-Reasoning in begin
-        od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
-    ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
-        od→ord < x , y >
-    ∎ )
-
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
-eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
-eq-pair refl refl = HE.refl
-
-eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
-eq-prod refl refl = refl
 
 open _==_
 
@@ -81,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 )
 
+eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
+eq-prod refl refl = refl
+
 prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
 prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
     lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y
@@ -116,56 +88,53 @@
     ... | refl with lemma4 eq -- with (x,y)≡(x,y')
     ... | eq1 = lemma4 (ord→== (cong (λ  k → od→ord k )  eq1 ))
 
-postulate
-   def-eq :  { P Q p q : OD } →  P ≡ Q → p ≡ q → (pt : P ∋ p ) → (qt : Q ∋ q ) → pt ≅ qt
-
-∈-to-ord : {p : Ordinal } → ( ZFProduct ∋  ord→od p ) → ord-pair p
-∈-to-ord {p} lt = def-subst {ZFProduct} {(od→ord (ord→od p))} {_} {_} lt refl diso
+data ord-pair : (p : Ordinal) → Set n where
+   pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
 
-ord-to-∈ : {p : Ordinal } → ord-pair p → ZFProduct ∋  ord→od p 
-ord-to-∈ {p} lt = def-subst {_} {_} {ZFProduct} {(od→ord (ord→od p))} lt refl (sym diso)
+ZFProduct : OD
+ZFProduct = record { def = λ x → ord-pair x }
 
-lemma333 : { A a  : OD } → { x : A ∋ a } → def-subst {A} {od→ord a} (def-subst {A} {od→ord a} x refl refl ) refl refl ≡ x
-lemma333 = refl
+eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
+eq-pair refl refl = HE.refl
 
-lemma334 : { A B  : OD } → {a b : Ordinal} → { x : A ∋ ord→od a } → { y : B ∋ ord→od b } → (f1 : A ≡ B) → (f2 : a ≡ b)
-   → def-subst {B} {od→ord (ord→od b)} (def-subst {A} { od→ord (ord→od a)} x f1 (cong (λ k → od→ord (ord→od k)) f2 )) refl refl ≅ x
-lemma334 {A} {A} {a} {a} {x} {y} refl refl with def-eq {A} {A} {ord→od a} {ord→od a} refl refl x y
-... | HE.refl = HE.refl
+pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi1 ( pair x y) = x
+
+π1 : { p : OD } → ZFProduct ∋ p → Ordinal
+π1 lt = pi1 lt 
 
-lemma335 : { A B C : OD } → {a b c : Ordinal} → { x : A ∋ ord→od a } → { y : C ∋ ord→od c } → (f1 : A ≡ B) → (f2 : a ≡ b) → (g1 : B ≡ C) → (g2 : b ≡ c)
-   → def-subst {B} {od→ord (ord→od b)} (def-subst {A} { od→ord (ord→od a)} x f1 (cong (λ k → od→ord (ord→od k)) f2 )) g1 (cong (λ k → od→ord (ord→od k)) g2 )
-      ≅ def-subst {A} { od→ord (ord→od a)} {C } { od→ord (ord→od c)} x (trans f1 g1)
-          (trans (cong (λ k → od→ord (ord→od k)) f2 ) (cong (λ k → od→ord (ord→od k)) g2 ))
-lemma335 {A} {A} {A} {a} {a} {a} {x} {y} refl refl refl refl with def-eq {A} {A} {ord→od a} {ord→od a} refl refl x y
-... | HE.refl = HE.refl
+pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi2 ( pair x y ) = y
+
+π2 : { p : OD } → ZFProduct ∋ p → Ordinal
+π2 lt = pi2 lt 
 
-∈-to-ord-oiso : { p : Ordinal } → { x : ord-pair p } → ∈-to-ord (ord-to-∈ x) ≡ x
-∈-to-ord-oiso {p} {x} = {!!} where
-   lemma : def-subst {_} {_} {ZFProduct} {{!!}} (def-subst {_} {_} {ZFProduct} {{!!}} x refl (sym diso)) refl diso ≡ x
-   lemma = {!!}
+p-cons :  ( x y  : OD ) → ZFProduct ∋ < x , y >
+p-cons x y =  def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
+    let open ≡-Reasoning in begin
+        od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
+    ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
+        od→ord < x , y >
+    ∎ )
 
-lemma34 : { p q : Ordinal } → (x :  ord-pair p ) → (y :  ord-pair q ) → p ≡ q → x ≅ y
-lemma34 {p} {q} x y refl = subst₂ (λ j k → j ≅ k) ∈-to-ord-oiso ∈-to-ord-oiso (HE.cong (λ k → ∈-to-ord k) lemma1 ) where
-   lemma : (pt : ZFProduct ∋ ord→od p ) → (qt : ZFProduct ∋ ord→od q ) → p ≡ q → pt ≅ qt
-   lemma pt qt eq = def-eq {ZFProduct} {ZFProduct} refl (cong (λ k → ord→od k) eq) pt qt
-   lemma1 : (ord-to-∈ x) ≅ (ord-to-∈ y )
-   lemma1 = lemma (ord-to-∈ x) (ord-to-∈ y ) refl
 
-π1-cong :  { p q : OD } →  p ≡ q → (pt : ZFProduct ∋ p ) → (qt : ZFProduct ∋ q ) → π1 pt ≅ π1 qt
-π1-cong {p} {q} refl s t = HE.cong (λ k → pi1 k ) (def-eq {ZFProduct} {ZFProduct} refl refl s t ) 
+p-iso-1 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≡ od→ord x
+p-iso-1 {x} {y} p  = lemma1 {od→ord < x , y >} {od→ord x} {od→ord y} p (cong₂ (λ j k → ord-pair (od→ord < j , k >)) (sym oiso) (sym oiso) ) where
+    lemma1 : {op ox oy : Ordinal } → ( p : ord-pair op ) → ord-pair op ≡ ord-pair (od→ord ( < ord→od ox , ord→od oy > )) → pi1 p ≡ ox
+    lemma1 (pair ox oy) eq = {!!}
+    lemma2 : {op ox oy : Ordinal } →  ord-pair op ≡ ord-pair (od→ord ( < ord→od ox , ord→od oy > ))
+    lemma2 = {!!}
+    lemma0 : {op ox oy : Ordinal } → ( p : ord-pair (od→ord ( < ord→od ox , ord→od oy > )))  → pi1 p ≡ ox
+    lemma0 = {!!}
+    lemma3 : {ox oy : Ordinal } ( p : ord-pair (od→ord ( < ord→od ox , ord→od oy > )) ) →   pi1 p  ≡ ox
+    lemma3 {ox} {oy} p = {!!}
+    lemma4 : {ox oy : Ordinal }   →  ord-pair (od→ord < ord→od ox , ord→od oy > ) ≡ ZFProduct ∋ < ord→od ox , ord→od oy >
+    lemma4  = refl
+    lemma : {p : OD }  →  ord-pair (od→ord p) ≡ ZFProduct ∋ p
+    lemma  = refl
 
-π1--iso :  { x y : OD } → (p : ZFProduct ∋ < x , y > )  →  π1 p ≅  od→ord x
-π1--iso {x} {y} p  = lemma (od→ord x) (od→ord y) {!!} {!!} refl where
-   lemma1 : ( ox oy op : Ordinal ) → (p : ord-pair op) → op ≡  od→ord ( < ord→od ox , ord→od oy >)  → p ≅ pair ox oy
-   lemma1 ox oy op (pair x' y')  eq = lemma34 {!!} {!!} {!!}
-   lemma : ( ox oy op : Ordinal ) → (p : ord-pair op ) → op ≡ od→ord ( < ord→od ox , ord→od oy > )  → pi1 p ≅ ox
-   lemma ox oy op p eq  = {!!} -- HE.cong (λ k → pi1 k ) (lemma1 ox oy op p eq  )
-
-p-iso :  { x  : OD } → {p : ZFProduct ∋ x } → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
-p-iso {x} {p} with p-cons (ord→od (π1 p)) (ord→od (π2 p))
-... | t = {!!}
-
+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 )