changeset 304:2c111bfcc89a

HOD using <maxod
author Shinji KONO Mon, 29 Jun 2020 18:31:56 +0900 7963b76df6e1 4804f3f3485f OD.agda 1 files changed, 20 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Mon Jun 29 17:56:06 2020 +0900
+++ b/OD.agda	Mon Jun 29 18:31:56 2020 +0900
@@ -77,7 +77,8 @@
record HOD : Set (suc n) where
field
od : OD
-    ¬odmax : ¬ (od ≡ Ords)
+    odmax : Ordinal
+    <odmax : {x : Ordinal} → def od x → x o< odmax

record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
field
@@ -89,12 +90,9 @@

open HOD

--- HOD→OD : {x : Ordinal} → HOD x → OD
--- HOD→OD hod = record { def = hdef {!!} }
-
record ODAxiom : Set (suc n) where
-  -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
field
+  -- HOD is isomorphic to Ordinal (by means of Goedel number)
od→ord : HOD  → Ordinal
ord→od : Ordinal  → HOD
c<→o<  :  {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y
@@ -114,22 +112,23 @@
-- maxod : {x : OD} → od→ord x o< od→ord Ords
-- maxod {x} = c<→o< OneObj

--- we have to avoid this contradiction
-
+-- we have not this contradiction
--- bad-bad = osuc-< <-osuc (c<→o< { record { def = λ x → One }} OneObj)
+-- bad-bad = osuc-< <-osuc (c<→o< { record { od = record { def = λ x → One };  <odmax = {!!} } } OneObj)

-- Ordinal in OD ( and ZFSet ) Transitive Set
Ord : ( a : Ordinal  ) → HOD
-Ord  a = record { od = record { def = λ y → y o< a } ; ¬odmax = ? }
+Ord  a = record { od = record { def = λ y → y o< a } ; odmax = a ; <odmax = lemma } where
+   lemma :  {x : Ordinal} → x o< a → x o< a
+   lemma {x} lt = lt

od∅ : HOD
od∅  = Ord o∅

sup-o  :  ( HOD → Ordinal ) →  Ordinal
-sup-o  = ?
+sup-o  = {!!}
sup-o< :  { ψ : HOD →  Ordinal } → ∀ {x : HOD } → ψ x  o<  sup-o ψ
-sup-o< = ?
+sup-o< = {!!}

odef : HOD → Ordinal → Set n
odef A x = def ( od A ) x
@@ -148,7 +147,7 @@
x c< a = a ∋ x

cseq : {n : Level} →  HOD  →  HOD
-cseq x = record { od = record { def = λ y → odef x (osuc y) } ; ¬odmax = ? } where
+cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = {!!} ; <odmax = {!!} } where

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
@@ -216,18 +215,18 @@
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 = ? }  --  Ord (omax (od→ord x) (od→ord y))
+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))

-- 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 = ? }
+in-codomain  X ψ = record { od = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  } ; odmax = {!!} ; <odmax = {!!} }

-- 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 = ? }  --   roughly x = A → Set
+ZFSubset A x =  record { od = record { def = λ y → odef A y ∧  odef x y } ; odmax = {!!} ; <odmax = {!!} }  --   roughly x = A → Set

OPwr :  (A :  HOD ) → HOD
OPwr  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A x) ) )
@@ -279,13 +278,13 @@
} 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 = ? }
+    Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = {!!} ; <odmax = {!!} }
Replace : HOD  → (HOD  → HOD  ) → HOD
-    Replace X ψ = record { od = record { def = λ x → (x o< sup-o  ( λ x → od→ord (ψ x))) ∧ odef (in-codomain X ψ) x } ; ¬odmax = ? }
+    Replace X ψ = record { od = record { def = λ x → (x o< sup-o  ( λ x → od→ord (ψ x))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} }
_∩_ : ( A B : ZFSet  ) → ZFSet
-    A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }  ; ¬odmax = ? }
+    A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }  ; odmax = {!!} ; <odmax = {!!} }
Union : HOD  → HOD
-    Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  } ; ¬odmax = ? }
+    Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  } ; odmax = {!!} ; <odmax = {!!} }
_∈_ : ( A B : ZFSet  ) → Set n
A ∈ B = B ∋ A
Power : HOD  → HOD
@@ -299,7 +298,7 @@
infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))

infinite : HOD
-    infinite = record { od = record { def = λ x → infinite-d x } ; ¬odmax = ? }
+    infinite = record { od = record { def = λ x → infinite-d x } ; odmax = {!!} ; <odmax = {!!} }

_=h=_ : (x y : HOD) → Set n
x =h= y  = od x == od y
@@ -364,7 +363,7 @@
; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
}
replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
-         replacement← {ψ} X x lt = record { proj1 =  ? ; proj2 = lemma } where -- sup-c< ψ {x}
+         replacement← {ψ} X x lt = record { proj1 =  {!!} ; proj2 = lemma } where -- sup-c< ψ {x}
lemma : odef (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))```