Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff 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 |
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