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

diff -r f97a2e4df451 -r 0bd498de2ef4 cardinal.agda
--- a/cardinal.agda	Sun Aug 25 23:13:31 2019 +0900
+++ b/cardinal.agda	Mon Aug 26 02:07:44 2019 +0900
@@ -30,6 +30,11 @@
 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 }
 
@@ -61,10 +66,33 @@
 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 _ _ = ?
+
+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 = {!!}
+
 π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 {!!} {!!}
+π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'
@@ -72,6 +100,13 @@
    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--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 = {!!}
+   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  = {!!}
+
 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 = {!!}