### changeset 318:9e0c97ab3a4a

Replace max
author Shinji KONO Fri, 03 Jul 2020 18:49:05 +0900 57df07b63cae eef432aa8dfb OD.agda 1 files changed, 16 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Fri Jul 03 18:29:51 2020 +0900
+++ b/OD.agda	Fri Jul 03 18:49:05 2020 +0900
@@ -209,8 +209,8 @@
-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)

-in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → HOD
-in-codomain  X ψ = record { od = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  } ; odmax = {!!} ; <odmax = {!!} }
+in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD
+in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }

-- Power Set of X ( or constructible by λ y → odef X (od→ord y )

@@ -266,11 +266,20 @@
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 (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x))
+    Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x }
+       ; odmax = rmax ; <odmax = rmax<} where
+          rmax : Ordinal
+          rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))
+          rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
+          rmax< lt = proj1 lt
_∩_ : ( 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))}
+    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
-    Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  } ; odmax = {!!} ; <odmax = {!!} }
+    Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  }
+       ; odmax = osuc (od→ord U) ; <odmax = umax< } where
+           umax< :  {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U)
+           umax< {y} not = {!!}
_∈_ : ( A B : ZFSet  ) → Set n
A ∈ B = B ∋ A

@@ -356,7 +365,7 @@
sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt )
replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {X} {x} lt ; proj2 = lemma } where
-             lemma : odef (in-codomain X ψ) (od→ord (ψ x))
+             lemma : def (in-codomain X ψ) (od→ord (ψ x))
lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
@@ -489,7 +498,7 @@
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< (OPwr (Ord (od→ord A))) lemma7 )
-              lemma2 :  odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
+              lemma2 :  def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A  )))```