### diff OD.agda @ 339:feb0fcc430a9

...
author Shinji KONO Sun, 12 Jul 2020 19:55:37 +0900 bca043423554 639fbb6284d8
line wrap: on
line diff
```--- a/OD.agda	Sun Jul 12 12:32:42 2020 +0900
+++ b/OD.agda	Sun Jul 12 19:55:37 2020 +0900
@@ -103,12 +103,13 @@
sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal
sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ

---  another form of infinite
---  pair-ord< :  {x : Ordinal } → od→ord ( ord→od x , ord→od x ) o< next (od→ord x)
-
postulate  odAxiom : ODAxiom
open ODAxiom odAxiom

+-- possible restriction
+hod-ord< :  {x : HOD } → Set n
+hod-ord< {x} =  od→ord x o< next (odmax x)
+
-- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
¬OD-order : ( od→ord : OD  → Ordinal ) → ( ord→od : Ordinal  → OD ) → ( { x y : OD  }  → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥
¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
@@ -221,6 +222,9 @@
lemma {t} (case1 refl) = omax-x  _ _
lemma {t} (case2 refl) = omax-y  _ _

+--  another form of infinite
+pair-ord< :  {x : Ordinal } → Set n
+pair-ord< {x} =  od→ord ( ord→od x , ord→od x ) o< next x

-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
@@ -370,15 +374,23 @@
infinite : HOD
infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax }

-    -- infinite' : HOD
-    -- infinite' = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
-    --     u : (y : Ordinal ) → HOD
-    --     u y = Union (ord→od y , (ord→od y , ord→od y))
-    --     lemma : {y : Ordinal} → infinite-d y → y o< next o∅
-    --     lemma {o∅} iφ = {!!}
-    --     lemma (isuc {y} x) = {!!} where
-    --         lemma1 : od→ord (Union (ord→od y , (ord→od y , ord→od y))) o< od→ord (Union (u y , (u y , u y )))
-    --         lemma1 = {!!}
+    infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD
+    infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
+        u : (y : Ordinal ) → HOD
+        u y = Union (ord→od y , (ord→od y , ord→od y))
+        lemma : {y : Ordinal} → infinite-d y → y o< next o∅
+        lemma {o∅} iφ = proj1  next-limit
+        lemma (isuc {y} x) = lemma2 where
+            lemma0 : y o< next o∅
+            lemma0 = lemma x
+            lemma3 : odef (u y ) y
+            lemma3 = FExists _ (λ {z} t not → not (od→ord (ord→od y , ord→od y)) record { proj1 = case2 refl ; proj2 = lemma4 }) (λ not → not y (infinite-d y)) where
+                lemma4 : def (od (ord→od (od→ord (ord→od y , ord→od y)))) y
+                lemma4 = subst₂ ( λ j k → def (od j) k ) (sym oiso) diso (case1 refl)
+            lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
+            lemma1 = ho<
+            lemma2 : od→ord (u y) o< next o∅
+            lemma2 = {!!}

_=h=_ : (x y : HOD) → Set n```