# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1566754454 -32400
# Node ID f0f9aede682f5d4651a244bf49248869d05f0dad
# Parent  0bd498de2ef4fdcebb1ca275f0fd3ce9c28bcea2
new assumption

diff -r 0bd498de2ef4 -r f0f9aede682f cardinal.agda
--- a/cardinal.agda	Mon Aug 26 02:07:44 2019 +0900
+++ b/cardinal.agda	Mon Aug 26 02:34:14 2019 +0900
@@ -30,11 +30,6 @@
 data ord-pair : (p : Ordinal) → Set n where
    pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
 
-lemma33 : { p q : Ordinal } → p ≡ q → ord-pair p ≡ ord-pair q
-lemma33 refl = refl
-
-
-
 ZFProduct : OD
 ZFProduct = record { def = λ x → ord-pair x }
 
@@ -66,44 +61,21 @@
 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
 eq-prod refl refl = refl
 
-prod<x : { x y y' : OD } → od→ord y o< od→ord y' → od→ord (< x , y > ) o< od→ord (< x , y' > )
-prod<x {x} {y} {y'} y<y' with trio< (od→ord x) (od→ord y)
-prod<x {x} {y} {y'} y<y' | tri≈ ¬a refl ¬c = ? where
-   lemma : ?
-   lemma = ?
-prod<x {x} {y} {y'} y<y' | tri< a ¬b ¬c = {!!}
-prod<x {x} {y} {y'} y<y' | tri> ¬a ¬b c = {!!}
-
-eq-prod' : { x y y' : OD } → < x , y > ≡ < x , y' > → y ≡ y' 
-eq-prod' {x} {y} {y'} eq with trio< (od→ord y) (od→ord y')
-eq-prod' {x} {y} {y'} eq | tri≈ ¬a b ¬c = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) b )
-eq-prod' {x} {y} {y'} eq | tri< a ¬b ¬c = {!!}
-eq-prod' {x} {y} {y'} eq | tri> ¬a ¬b c = {!!}
-
--- def-eq :  { P Q p q : OD } →  P ≡ Q → p ≡ q → (pt : P ∋ p ) → (qt : Q ∋ q ) → pt ≅ qt
--- def-eq refl refl _ _ = ?
+postulate
+   def-eq :  { P Q p q : OD } →  P ≡ Q → p ≡ q → (pt : P ∋ p ) → (qt : Q ∋ q ) → pt ≅ qt
 
 lemma34 : { p q : Ordinal } → (x :  ord-pair p ) → (y :  ord-pair q ) → p ≡ q → x ≅ y
-lemma34 {p} (pair x0 x1) (pair y0 y1) eq = {!!}
-
-prod-eq :  { p q : OD } →  p ≡ q → (pt : ZFProduct ∋ p ) → (qt : ZFProduct ∋ q ) → pt ≅ qt
-prod-eq refl s t = {!!} where
-  lemma : {P : Ordinal } → ( pt qt : ord-pair P ) → pt ≅ qt
-  lemma = {!!}
+lemma34 {p} {q} x y eq = {!!} 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 {!!} {!!} {!!}
 
 π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 ) (prod-eq  refl s t ) 
-
-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 = {!!}
+π1-cong {p} {q} refl s t = HE.cong (λ k → pi1 k ) (def-eq {ZFProduct} {ZFProduct} refl refl s t ) 
 
 π1--iso :  { x y : OD } → (p : ZFProduct ∋ < x , y > )  →  π1 p ≡ od→ord x
 π1--iso {x} {y} p  = {!!} 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 = {!!}
+   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 (pair ox' oy') eq  = {!!}