changeset 310:73a2a8ec9603

...
author Shinji KONO Tue, 30 Jun 2020 08:55:12 +0900 d4802179a66f bf01e924e62e OD.agda 1 files changed, 7 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Tue Jun 30 00:17:05 2020 +0900
+++ b/OD.agda	Tue Jun 30 08:55:12 2020 +0900
@@ -220,7 +220,7 @@

OPwr :  (A :  HOD ) → HOD
-OPwr  A = Ord ( sup-o A {!!} ) --  ( λ x → od→ord ( ZFSubset A x) ) )
+OPwr  A = Ord ( sup-o A ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )

-- _⊆_ :  ( A B : HOD   ) → ∀{ x : HOD  } →  Set n
-- _⊆_ A B {x} = A ∋ x →  B ∋ x
@@ -270,8 +270,8 @@
ZFSet = HOD             -- is less than Ords because of maxod
Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD
Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
-    Replace : HOD  → (HOD  → HOD  ) → HOD
-    Replace X ψ = record { od = record { def = λ x → (x o< sup-o X {!!} ) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x))
+    Replace : HOD  → (HOD  → HOD) → HOD
+    Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋x → od→ord (ψ (ord→od x)))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x))
_∩_ : ( A B : ZFSet  ) → ZFSet
A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }  ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
Union : HOD  → HOD
@@ -401,7 +401,7 @@
lemma1 :  {a : Ordinal } { t : HOD }
→ (eq : ZFSubset (Ord a) t =h= t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
lemma1  {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
-              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord a) {!!} --  (λ x → od→ord (ZFSubset (Ord a) x))
+              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord a) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x)))
lemma = {!!} -- sup-o<

--
@@ -425,7 +425,7 @@
lemma5 {y} eq not = (lemma3 (ord→od y) eq) not

power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where
+         power← A t t→A = record { proj1 = {!!} ; proj2 = lemma2 } where
a = od→ord A
lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x
lemma0 {x} t∋x = c<→o< (t→A t∋x)
@@ -439,8 +439,8 @@
≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
t
∎
-              lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) {!!} -- (λ x → od→ord (A ∩ x))
-              lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  {!!}) --  (λ x → od→ord (A ∩ x)))
+              lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
+              lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  (λ x lt → od→ord (A ∩ (ord→od x))))
lemma4 {!!} -- (sup-o<  {λ x → od→ord (A ∩ x)}  )
lemma2 :  odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where```