# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1567648686 -32400
# Node ID 8b85949bde00dfb7e6643ceda0fb518fd1bb65c8
# Parent  f714fe999102242d15c9ae2c4ddebdb0506ee781
sup with limit give up

diff -r f714fe999102 -r 8b85949bde00 OD.agda
--- a/OD.agda	Thu Sep 05 01:28:52 2019 +0900
+++ b/OD.agda	Thu Sep 05 10:58:06 2019 +0900
@@ -75,8 +75,8 @@
   --   o<→c<  : {n : Level} {x y : Ordinal  } → x o< y → def (ord→od y) x 
   --   ord→od x ≡ Ord x results the same
   -- supermum as Replacement Axiom
-  sup-o  :  Ordinal → ( Ordinal  → Ordinal ) →  Ordinal 
-  sup-o< :  {X : Ordinal} → { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } → x o< X  →  ψ x  o<  sup-o X ψ 
+  sup-o  :  ( Ordinal  → Ordinal ) →  Ordinal 
+  sup-o< :  { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } → ψ x  o<  sup-o ψ 
   -- contra-position of mimimulity of supermum required in Power Set Axiom
   -- sup-x  : {n : Level } → ( Ordinal  → Ordinal ) →  Ordinal 
   -- sup-lb : {n : Level } → { ψ : Ordinal  →  Ordinal } → {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
@@ -106,14 +106,14 @@
 def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
 
-sup-od : OD → ( OD  → OD ) →  OD 
-sup-od X ψ = Ord ( sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x ))) )
+sup-od : ( OD  → OD ) →  OD 
+sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
 
-sup-c< : {X : OD } ( ψ : OD  →  OD ) → ∀ {x : OD } → X ∋ x  → def ( sup-od X ψ ) (od→ord ( ψ x ))
-sup-c<  {X} ψ {x} lt = def-subst  {_} {_} {Ord ( sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )}
+sup-c< :  ( ψ : OD  →  OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x ))
+sup-c<   ψ {x} = def-subst  {_} {_} {Ord ( sup-o  ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )}
         lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
-    lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (od→ord X) (λ x → od→ord (ψ (ord→od x)))
-    lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< (c<→o< lt) ) refl (sym diso)  )
+    lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x)))
+    lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< ) refl (sym diso)  )
 
 otrans : {n : Level} {a x y : Ordinal  } → def (Ord a) x → def (Ord x) y → def (Ord a) y
 otrans x<a y<x = ordtrans y<x x<a
@@ -337,8 +337,7 @@
 ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  --   roughly x = A → Set 
 
 Def :  (A :  OD ) → OD 
-Def  A = Ord ( sup-o (osuc (od→ord A)) ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
-
+Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
 
 _⊆_ :  ( A B : OD   ) → ∀{ x : OD  } →  Set n
 _⊆_ A B {x} = A ∋ x →  B ∋ x
@@ -369,7 +368,7 @@
     Select : (X : OD  ) → ((x : OD  ) → Set n ) → OD 
     Select X ψ = record { def = λ x →  ( def X x ∧ ψ ( ord→od x )) }
     Replace : OD  → (OD  → OD  ) → OD 
-    Replace X ψ = record { def = λ x → (x o< sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
+    Replace X ψ = record { def = λ x → (x o< sup-o  ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
     _∩_ : ( A B : ZFSet  ) → ZFSet
     A ∩ B = record { def = λ x → def A x ∧ def B x } 
     Union : OD  → OD   
@@ -449,7 +448,7 @@
             ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
            }
          replacement← : {ψ : OD → OD} (X x : OD) →  X ∋ x → Replace X ψ ∋ ψ x
-         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} lt ; proj2 = lemma } where
+         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; proj2 = lemma } where
              lemma : def (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→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
@@ -492,16 +491,8 @@
               lemma1 :  {a : Ordinal } { t : OD }
                  → (eq : ZFSubset (Ord a) t == t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
               lemma1  {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
-              lemma3 : {x : OD} → (lt : t ∋ x ) → Ord (od→ord t) ∋ x
-              lemma3 lt = c<→o< lt
-              lemma2 : ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → od→ord t o< osuc (od→ord (Ord a))
-              lemma2 t→A = lemma5 t→A where
-                  lemma6 : {t s : OD } → ({x : OD} → (t ∋ x → s ∋ x)) → {x : OD}  → Ord (od→ord t) ∋ x → Ord ( od→ord s)  ∋ x
-                  lemma6 = {!!}
-                  lemma5 : {t s : OD } → ({x : OD} → (t ∋ x → s ∋ x)) → od→ord t o< osuc ( od→ord s)
-                  lemma5 t→A = ⊆→o< ( λ z → lemma6 t→A )
-              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (osuc (od→ord (Ord a))) (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
-              lemma = sup-o<  (lemma2 t→A)
+              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o  (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
+              lemma = sup-o<  
 
          -- 
          -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first
@@ -538,11 +529,9 @@
                  ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
                     t
                  ∎
-              lemma5 : od→ord t o< od→ord (Def (Ord (od→ord A)))
-              lemma5 = {!!}
-              lemma1 : od→ord t o< sup-o (od→ord (Def (Ord (od→ord A)))) (λ x → od→ord (A ∩ ord→od x))
-              lemma1 = subst (λ k → od→ord k o< sup-o (od→ord (Def (Ord (od→ord A))))  (λ x → od→ord (A ∩ ord→od x)))
-                  lemma4 (sup-o< {od→ord (Def (Ord (od→ord A)))} {λ x → od→ord (A ∩ ord→od x)} {od→ord t} lemma5 )
+              lemma1 : od→ord t o< sup-o  (λ x → od→ord (A ∩ ord→od x))
+              lemma1 = subst (λ k → od→ord k o< sup-o   (λ x → od→ord (A ∩ ord→od x)))
+                  lemma4 (sup-o<  {λ x → od→ord (A ∩ ord→od x)} {od→ord t} )
               lemma2 :  def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
               lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
                   lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))