# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1566742411 -32400
# Node ID f97a2e4df451ec56bf20fb13045ce9bcb85fdc9f
# Parent  c10048d696148702f4f7ced9b4bca57250644b96
...

diff -r c10048d69614 -r f97a2e4df451 cardinal.agda
--- a/cardinal.agda	Sun Aug 25 18:44:41 2019 +0900
+++ b/cardinal.agda	Sun Aug 25 23:13:31 2019 +0900
@@ -53,36 +53,29 @@
         od→ord < x , y >
     ∎ )
 
-π1-iso :  { x y : OD } → π1 ( p-cons  x  y  ) ≡ od→ord x
-π1-iso {x} {y} = {!!} where
-   lemma : {ox oy : Ordinal} →  pi1 ( pair ox oy )  ≡ ox
-   lemma = refl
-   lemma2 : {ox oy : Ordinal} →
-      def-subst {ZFProduct} {_}  (pair (od→ord (ord→od ox)) (od→ord (ord→od oy))) refl (trans (cong₂ (λ j k → od→ord < j , k >) oiso oiso) refl) ≡ pair ox oy
-   lemma2 {ox} {oy} = let open ≡-Reasoning in begin
-        def-subst {ZFProduct} {_}  (pair (od→ord (ord→od ox)) (od→ord (ord→od oy))) refl (trans (cong₂ (λ j k → od→ord < j , k >) oiso oiso) refl) 
-      ≡⟨ ? ⟩
-        pair ox oy 
-      ∎
-   lemma1 : {ox oy : Ordinal} → π1 ( p-cons  (ord→od ox)  (ord→od oy) ) ≡ ox
-   lemma1 {ox} {oy} = let open ≡-Reasoning in begin
-         π1 ( p-cons  (ord→od ox)  (ord→od oy) )
-      ≡⟨⟩
-         pi1 (pair (pi1 (def-subst {ZFProduct} {_}  (pair (od→ord (ord→od ox)) (od→ord (ord→od oy))) refl (trans (cong₂ (λ j k → od→ord < j , k >) oiso oiso) refl)))  oy )
-      ≡⟨ cong (λ k → pi1 k) lemma2  ⟩
-         pi1 (pair ox oy )
-      ≡⟨ lemma {ox} {oy} ⟩
-         ox
-      ∎
+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
+
+π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 ) (lemma s t refl ) where
+   lemma : { op oq : Ordinal } → (P : ord-pair op ) → (Q : ord-pair oq ) → op ≡ oq →  P ≅ Q
+   lemma (pair x y ) (pair x' y') eq =  eq-pair {!!} {!!}
+
+Tlemma :  { x y x' y' : Ordinal } → (prod : ord-pair (od→ord < ord→od x , ord→od y >))
+       → (prod' : ord-pair (od→ord < ord→od x' , ord→od y' >)) → x ≡ x' → y ≡ y'  → prod ≅ prod'
+Tlemma prod prod' refl refl = lemma prod prod' refl where
+   lemma : { p q : Ordinal } → (prod : ord-pair p) → (prod1 : ord-pair q) → p ≡ q → prod ≅ prod1
+   lemma (pair x y) (pair x' y') eq = {!!}
 
 p-iso :  { x  : OD } → {p : ZFProduct ∋ x } → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
-p-iso {x} {p} = pi p pc  where
-   pc : ZFProduct ∋ < ord→od (π1 p) , ord→od (π2 p) >
-   pc = p-cons (ord→od (π1 p)) (ord→od (π2 p)) 
-   pi : { prod prod1 : Ordinal } →   ord-pair prod → ord-pair prod1 → {!!}
-   pi (pair p1 p2) (pair q1 q2) = {!!}
+p-iso {x} {p} with p-cons (ord→od (π1 p)) (ord→od (π2 p))
+... | t = {!!}
 
-    
 
 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
 ∋-p A x with p∨¬p ( A ∋ x )