Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 419:4af94768e372

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 31 Jul 2020 12:57:59 +0900
parents f6f08d5a4941
children 53422a8ea836
files OPair.agda ordinal.agda
diffstat 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