### changeset 259:f714fe999102

...
author Shinji KONO Thu, 05 Sep 2019 01:28:52 +0900 63df67b6281c 8b85949bde00 OD.agda 1 files changed, 26 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Wed Sep 04 01:12:18 2019 +0900
+++ b/OD.agda	Thu Sep 05 01:28:52 2019 +0900
@@ -70,14 +70,13 @@
c<→o<  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o< od→ord y
oiso   :  {x : OD }      → ord→od ( od→ord x ) ≡ x
diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
-  -- we should prove this in agda, but simply put here
==→o≡ : { x y : OD  } → (x == y) → x ≡ y
-- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD
--   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
-  sup-o< :  { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } →  ψ x  o<  sup-o ψ
+  sup-o  :  Ordinal → ( Ordinal  → Ordinal ) →  Ordinal
+  sup-o< :  {X : Ordinal} → { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } → x o< X  →  ψ x  o<  sup-o X ψ
-- 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 ψ))
@@ -107,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
-sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
+sup-od : OD → ( OD  → OD ) →  OD
+sup-od X ψ = Ord ( sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od 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 )}
+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 )}
lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
-    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)  )
+    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)  )

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
@@ -338,7 +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 ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
+Def  A = Ord ( sup-o (osuc (od→ord A)) ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )

_⊆_ :  ( A B : OD   ) → ∀{ x : OD  } →  Set n
@@ -370,7 +369,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 ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
+    Replace X ψ = record { def = λ x → (x o< sup-o (od→ord X) ( λ 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
@@ -450,7 +449,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} ; proj2 = lemma } where
+         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} lt ; 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))
@@ -493,8 +492,16 @@
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 ))
-              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<
+              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)

--
-- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first
@@ -523,8 +530,6 @@
lemma0 {x} t∋x = c<→o< (t→A t∋x)
lemma3 : Def (Ord a) ∋ t
lemma3 = ord-power← a t lemma0
-              lt1 : od→ord (A ∩ ord→od (od→ord t)) o< sup-o (λ x → od→ord (A ∩ ord→od x))
-              lt1 = sup-o<  {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
lemma4 :  (A ∩ ord→od (od→ord t)) ≡ t
lemma4 = let open ≡-Reasoning in begin
A ∩ ord→od (od→ord t)
@@ -533,9 +538,11 @@
≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
t
∎
-              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})
+              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 )
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)) ```