### changeset 309:d4802179a66f

...
author Shinji KONO Tue, 30 Jun 2020 00:17:05 +0900 b172ab9f12bc 73a2a8ec9603 OD.agda Ordinals.agda 2 files changed, 14 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Tue Jun 30 00:05:16 2020 +0900
+++ b/OD.agda	Tue Jun 30 00:17:05 2020 +0900
@@ -57,15 +57,15 @@
--     HOD = { x | TC x ⊆ OD }
--  where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x.
--  This is not possible because we don't have V yet.
---  We simply assume V=OD here.
--
---  We also assumes ODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks.
---  ODs have an ovbious maximum, but Ordinals are not. This means, od→ord is not an on-to mapping.
---
---  ==→o≡ is necessary to prove axiom of extensionality.
+--  We also assumes HODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks.
+--  ODs have an ovbious maximum, but Ordinals are not. So HOD cannot be a maximum OD.
--
--  In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic,
--  we need explict assumption on sup.
+--  In order to allow sup on od→ord HOD, solutions of a HOD have to have a maximu.
+--
+--  ==→o≡ is necessary to prove axiom of extensionality.

data One : Set n where
OneObj : One
@@ -80,14 +80,6 @@
odmax : Ordinal
<odmax : {y : Ordinal} → def od y → y o< odmax

-record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
-  field
-    os→ : (x : Ordinal) → x o< maxordinal → Ordinal
-    os← : Ordinal → Ordinal
-    os←limit : (x : Ordinal) → os← x o< maxordinal
-    os-iso← : {x : Ordinal} →  os→  (os← x) (os←limit x) ≡ x
-    os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) →  os← (os→ x lt) ≡ x
-
open HOD

record ODAxiom : Set (suc n) where
@@ -99,7 +91,6 @@
oiso   :  {x : HOD }      → ord→od ( od→ord x ) ≡ x
diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
==→o≡ : { x y : HOD  } → (od x == od y) → x ≡ y
-  -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum )
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 ψ

@@ -282,7 +273,7 @@
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
-    A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }  ; odmax = {!!} ; <odmax = {!!} }
+    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 = {!!} }
_∈_ : ( A B : ZFSet  ) → Set n```
```--- a/Ordinals.agda	Tue Jun 30 00:05:16 2020 +0900
+++ b/Ordinals.agda	Tue Jun 30 00:17:05 2020 +0900
@@ -200,3 +200,11 @@
→ ¬ p
FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )

+        record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
+          field
+            os→ : (x : Ordinal) → x o< maxordinal → Ordinal
+            os← : Ordinal → Ordinal
+            os←limit : (x : Ordinal) → os← x o< maxordinal
+            os-iso← : {x : Ordinal} →  os→  (os← x) (os←limit x) ≡ x
+            os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) →  os← (os→ x lt) ≡ x
+```