### changeset 308:b172ab9f12bc

...
author Shinji KONO Tue, 30 Jun 2020 00:05:16 +0900 d5c5d87b72df d4802179a66f OD.agda Ordinals.agda 2 files changed, 24 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Mon Jun 29 23:09:14 2020 +0900
+++ b/OD.agda	Tue Jun 30 00:05:16 2020 +0900
@@ -78,7 +78,7 @@
field
od : OD
odmax : Ordinal
-    <odmax : {x : Ordinal} → def od x → x o< odmax
+    <odmax : {y : Ordinal} → def od y → y o< odmax

record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
field
@@ -122,11 +122,6 @@
od∅ : HOD
od∅  = Ord o∅

-sup-od : ( HOD → HOD ) →  HOD
-sup-od = {!!}
-sup-c< :  ( ψ : HOD  →  HOD ) → ∀ {x : HOD } → def (od ( sup-od ψ )) (od→ord ( ψ x ))
-sup-c< = {!!}
-
odef : HOD → Ordinal → Set n
odef A x = def ( od A ) x

@@ -144,7 +139,9 @@
x c< a = a ∋ x

cseq : {n : Level} →  HOD  →  HOD
-cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = {!!} } where
+cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
+    lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
+    lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc )

odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
odef-subst df refl refl = df
@@ -155,7 +152,6 @@
odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X
odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst  {X} {x}  lt (sym oiso) (sym diso) )) diso diso

-
-- avoiding lv != Zero error
orefl : { x : HOD  } → { y : Ordinal  } → od→ord x ≡ y → od→ord x ≡ y
orefl refl = refl
@@ -212,7 +208,11 @@
is-o∅ x | tri> ¬a ¬b c = no ¬b

_,_ : HOD  → HOD  → HOD
-x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = {!!} ; <odmax = {!!} }  --  Ord (omax (od→ord x) (od→ord y))
+x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x)  (od→ord y) ; <odmax = lemma }  where
+    lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y)
+    lemma {t} (case1 refl) = omax-x  _ _
+    lemma {t} (case2 refl) = omax-y  _ _
+

-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
@@ -223,7 +223,10 @@
-- Power Set of X ( or constructible by λ y → odef X (od→ord y )

ZFSubset : (A x : HOD  ) → HOD
-ZFSubset A x =  record { od = record { def = λ y → odef A y ∧  odef x y } ; odmax = {!!} ; <odmax = {!!} }  --   roughly x = A → Set
+ZFSubset A x =  record { od = record { def = λ y → odef A y ∧  odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma }  where --   roughly x = A → Set
+     lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
+     lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))
+

OPwr :  (A :  HOD ) → HOD
OPwr  A = Ord ( sup-o A {!!} ) --  ( λ x → od→ord ( ZFSubset A x) ) )
@@ -275,7 +278,7 @@
} where
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 = {!!} }
+    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))
_∩_ : ( A B : ZFSet  ) → ZFSet
@@ -359,6 +362,10 @@
proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
}
+         sup-od : ( HOD → HOD ) →  HOD
+         sup-od = {!!}
+         sup-c< :  ( ψ : HOD  →  HOD ) → ∀ {x : HOD } → def (od ( sup-od ψ )) (od→ord ( ψ x ))
+         sup-c< = {!!}
replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
replacement← {ψ} X x lt = record { proj1 =  {!!} ; proj2 = lemma } where -- sup-c< ψ {x}
lemma : odef (in-codomain X ψ) (od→ord (ψ x))```
```--- a/Ordinals.agda	Mon Jun 29 23:09:14 2020 +0900
+++ b/Ordinals.agda	Tue Jun 30 00:05:16 2020 +0900
@@ -120,13 +120,13 @@
maxα x y | tri> ¬a ¬b c = x
maxα x y | tri≈ ¬a refl ¬c = x

-        minα :    Ordinal  →  Ordinal  → Ordinal
-        minα  x y with trio<  x  y
-        minα x y | tri< a ¬b ¬c = x
-        minα x y | tri> ¬a ¬b c = y
-        minα x y | tri≈ ¬a refl ¬c = x
+        omin :    Ordinal  →  Ordinal  → Ordinal
+        omin  x y with trio<  x  y
+        omin x y | tri< a ¬b ¬c = x
+        omin x y | tri> ¬a ¬b c = y
+        omin x y | tri≈ ¬a refl ¬c = x

-        min1 :   {x y z : Ordinal  } → z o< x → z o< y → z o< minα x y
+        min1 :   {x y z : Ordinal  } → z o< x → z o< y → z o< omin x y
min1  {x} {y} {z} z<x z<y with trio<  x y
min1  {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
min1  {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x```