### changeset 237:521290e85527

...
author Shinji KONO Mon, 19 Aug 2019 00:37:35 +0900 650bdad56729 a8c6239176db cardinal.agda 1 files changed, 27 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
```--- 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```