### diff OD.agda @ 190:6e778b0a7202

author Shinji KONO Fri, 26 Jul 2019 21:08:06 +0900 540b845ea2de 9eb6a8691f02
line wrap: on
line diff
```--- a/OD.agda	Thu Jul 25 14:42:19 2019 +0900
+++ b/OD.agda	Fri Jul 26 21:08:06 2019 +0900
@@ -198,7 +198,7 @@
-- Axiom of choice in intutionistic logic implies the exclude middle
--     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
--
-p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )
+p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )         -- assuming axiom of choice
p∨¬p {n} p with is-o∅ ( od→ord ( record { def = λ x → p } ))
p∨¬p {n} p | yes eq = case2 (¬p eq) where
ps = record { def = λ x → p }
@@ -213,13 +213,13 @@
lemma : ps ∋ minimul ps (λ eq →  ¬p (eqo∅ eq))
lemma = x∋minimul ps (λ eq →  ¬p (eqo∅ eq))

-∋-p : { n : Level } → ( p : Set (suc n) ) → Dec p
+∋-p : { n : Level } → ( p : Set (suc n) ) → Dec p   -- assuming axiom of choice
∋-p {n} p with p∨¬p p
∋-p {n} p | case1 x = yes x
∋-p {n} p | case2 x = no x

double-neg-eilm : {n  : Level } {A : Set (suc n)} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
-double-neg-eilm {n} {A} notnot with ∋-p  A
+double-neg-eilm {n} {A} notnot with ∋-p  A                         -- assuming axiom of choice
... | yes p = p
... | no ¬p = ⊥-elim ( notnot ¬p )

@@ -243,6 +243,24 @@
Def :  {n : Level} → (A :  OD {suc n}) → OD {suc n}
Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   -- Ord x does not help ord-power→

+
+_⊆_ : {n : Level} ( A B : OD {suc n}  ) → ∀{ x : OD {suc n} } →  Set (suc n)
+_⊆_ A B {x} = A ∋ x →  B ∋ x
+
+infixr  220 _⊆_
+
+subset-lemma : {n : Level} → {A x y : OD {suc n} } → (  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( _⊆_ x A {y} )
+subset-lemma {n} {A} {x} {y} = record {
+      proj1 = λ z lt → proj1 (z  lt)
+    ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
+   }
+
+Def=A→Set : {n : Level} → (A  :  Ordinal {suc n}) → Def (Ord A) == record { def = λ x → x o< A → Set n  }
+Def=A→Set {n} A  = record {
+              eq→ = λ {y} DAx y<A →  {!!}
+        ;  eq← = {!!} -- λ {y} f → {!!}
+    } where
+
-- Constructible Set on α
-- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y <  od→ord x }
-- L (Φ 0) = Φ
@@ -285,8 +303,6 @@
Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x)))  }
_∈_ : ( A B : ZFSet  ) → Set (suc n)
A ∈ B = B ∋ A
-    _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set (suc n)
-    _⊆_ A B {x} = A ∋ x →  B ∋ x
Power : OD {suc n} → OD {suc n}
Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
｛_｝ : ZFSet → ZFSet
@@ -302,7 +318,6 @@

infixr  200 _∈_
-- infixr  230 _∩_ _∪_
-    infixr  220 _⊆_
isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace infinite
isZF = record {
isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
@@ -446,6 +461,7 @@
lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))

+         --  assuming axiom of choice
regularity :  (x : OD) (not : ¬ (x == od∅)) →
(x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
proj1 (regularity x not ) = x∋minimul x not```