Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff cardinal.agda @ 237:521290e85527
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 19 Aug 2019 00:37:35 +0900 |
parents | 650bdad56729 |
children | a8c6239176db |
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