### changeset 419:4af94768e372

...
author Shinji KONO Fri, 31 Jul 2020 12:57:59 +0900 f6f08d5a4941 53422a8ea836 OPair.agda ordinal.agda 2 files changed, 4 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
```--- a/OPair.agda	Fri Jul 31 12:46:45 2020 +0900
+++ b/OPair.agda	Fri Jul 31 12:57:59 2020 +0900
@@ -203,12 +203,13 @@

ZFP⊗ :  {A B : HOD} → ZFP A B ≡ A ⊗ B
ZFP⊗ {A} {B} = ==→o≡ record { eq→ = lemma0 ; eq← = lemma1 } where
+      AxB : HOD
+      AxB =  Replace B (λ b → Replace A (λ a → < a , b > ))
lemma0 :  {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
lemma0 {px} record { proj1 = (pair x y) ; proj2 = p2 } = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) )))
lemma1 :  {x : Ordinal} → odef (A ⊗ B) x → odef (ZFP A B) x
-      lemma1 {x} lt = ⊥-elim (lt (λ u not → proj2 (proj1 not) (λ y p → lemma2 u y p ))) where
-           lemma2 : (u y : Ordinal) → odef B y ∧ (u ≡ od→ord (Replace A (λ a → < a , ord→od y >))) → ⊥
-           lemma2 = {!!}
+      lemma1 {x} lt with union← AxB (ord→od x) (d→∋ (A ⊗ B) lt)
+      ... | t = {!!}

```
```--- a/ordinal.agda	Fri Jul 31 12:46:45 2020 +0900
+++ b/ordinal.agda	Fri Jul 31 12:57:59 2020 +0900
@@ -244,7 +244,6 @@
lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where
lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
lemma3   (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n
-
open Oprev
Oprev-p  : (x : Ordinal) → Dec ( Oprev (Ordinal {suc n})  osuc x )
Oprev-p  (ordinal lv (Φ lv)) = no (λ not → lemma (oprev not) (oprev=x not) ) where```