Members/kono/Proof/ZF-in-agda: OD.agda comparison

comparison OD.agda @ 190:6e778b0a7202

add filter

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 26 Jul 2019 21:08:06 +0900
parents	540b845ea2de
children	9eb6a8691f02

comparison

equal deleted inserted replaced

-:540b845ea2de
+:6e778b0a7202
 --
 -- 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 }
 lemma : ps == od∅ → p → ⊥
 lemma eq p0 = ¬x<0 {n} {od→ord ps} (eq→ eq p0 )
 eqo∅ : ps ==  od∅ {suc n} → od→ord ps ≡  o∅ {suc n}
 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq))
 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 )
 OrdP : {n : Level} →  ( x : Ordinal {suc n} ) ( y : OD {suc n} ) → Dec ( Ord x ∋ y )
 OrdP {n} x y with trio< x (od→ord y)
 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n}
 ZFSubset A x =  record { def = λ y → def A y ∧  def x y }   where
 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) = Φ
 -- L (OSuc lv n) = { Def ( L n )  }
 A ∩ B = record { def = λ x → def A x ∧ def B x }
 Union : OD {suc n} → OD {suc n}
 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
 ｛ x ｝ = ( x ,  x )
 infinite : OD {suc n}
 infinite = record { def = λ x → infinite-d x }
 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 }
 ;   pair  = pair
 ;   union→ = union→
 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))
 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
 proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where
 lemma1 : {x₁ : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁

Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison OD.agda @ 190:6e778b0a7202