# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1566142655 -32400
# Node ID 521290e855274cc3c78982b65bdf108a115f91ab
# Parent  650bdad5672926d79698755cf9e45473832f7b3b
...

diff -r 650bdad56729 -r 521290e85527 cardinal.agda
--- a/cardinal.agda	Fri Aug 16 15:53:29 2019 +0900
+++ b/cardinal.agda	Mon Aug 19 00:37:35 2019 +0900
@@ -27,6 +27,33 @@
 <_,_> : (x y : OD) → OD
 < x , y > = (x , x ) , (x , y )
 
+Ord< : {x y : Ordinal } → x o< y  → od→ord (Ord x) o< od→ord (Ord y)  -- x o< y = Ord y ∋ x → ox o< od→ord (Ord y) 
+Ord< {x} {y} lt with trio< (od→ord (Ord x)) (od→ord (Ord y))
+Ord< {x} {y} lt | tri< a ¬b ¬c =  a        
+Ord< {x} {y} lt | tri≈ ¬a b ¬c =  ⊥-elim ( o<¬≡ refl (def-subst {Ord y} {x} {Ord x} {x} lt   -- Ord x ∋ x
+    (subst₂ (λ j k → j ≡ k) oiso oiso (cong (λ k → ord→od k )(sym b)) )refl ))               -- Ord x ≡ Ord y
+Ord< {x} {y} lt | tri> ¬a ¬b c =  ? where
+     lemma : ¬ ( Ord x ∋ ord→od x )
+     lemma lt = ⊥-elim ( o<¬≡ refl ( def-subst {_} {_} {Ord x} {x} lt refl diso )) 
+     lemma1 : od→ord (Ord y) o< od→ord (Ord x) → x o< od→ord (Ord x )
+     lemma1 lt1 = ordtrans ( o<-subst (c<→o< lt ) diso refl ) {!!} 
+
+---   Ord (osuc ox) ∋ x
+---   ox o< od→ord (Ord (osuc ox)) 
+---   osuc ox  ≡ od→ord (Ord (osuc ox)) 
+
+opair : {x y : OD} → ( < x , y > ∋ x ) ∧ ( < x , y > ∋ y )
+opair {x} {y} = record { proj1 = lemma ; proj2 = {!!} } where
+   ox = (od→ord x)
+   oy = (od→ord y)
+   -- < x , y > ∋ x  --  od→ord (Ord (omax ox ox ))
+   lemma : ox o< (omax (od→ord (x , x)) (od→ord (x , y)))
+   lemma with trio< ox oy
+   lemma | tri< a ¬b ¬c with omax< ox oy a | omxx ox
+   ... | eq | eq1 = {!!}
+   lemma | tri≈ ¬a b ¬c = {!!}
+   lemma | tri> ¬a ¬b c = {!!}
+
 record SetProduct ( A B : OD )  : Set n where
    field
       π1 : Ordinal