# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593443825 -32400
# Node ID d4802179a66f50519e20e933973b4ea128db052c
# Parent  b172ab9f12bc195e06e28b309d83f6fcaaf9282a
...

diff -r b172ab9f12bc -r d4802179a66f OD.agda
--- 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
diff -r b172ab9f12bc -r d4802179a66f Ordinals.agda
--- 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
+