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

diff -r d5c5d87b72df -r b172ab9f12bc OD.agda
--- 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))
diff -r d5c5d87b72df -r b172ab9f12bc Ordinals.agda
--- 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