Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ODC.agda @ 331:12071f79f3cf
HOD done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 05 Jul 2020 16:56:21 +0900 |
parents | 0faa7120e4b5 |
children | 7f919d6b045b |
comparison
equal
deleted
inserted
replaced
330:0faa7120e4b5 | 331:12071f79f3cf |
---|---|
21 open OD._==_ | 21 open OD._==_ |
22 open ODAxiom odAxiom | 22 open ODAxiom odAxiom |
23 | 23 |
24 open HOD | 24 open HOD |
25 | 25 |
26 open _∧_ | |
27 | |
26 _=h=_ : (x y : HOD) → Set n | 28 _=h=_ : (x y : HOD) → Set n |
27 x =h= y = od x == od y | 29 x =h= y = od x == od y |
28 | 30 |
29 postulate | 31 postulate |
30 -- mimimul and x∋minimal is an Axiom of choice | 32 -- mimimul and x∋minimal is an Axiom of choice |
38 -- | 40 -- |
39 -- Axiom of choice in intutionistic logic implies the exclude middle | 41 -- Axiom of choice in intutionistic logic implies the exclude middle |
40 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog | 42 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog |
41 -- | 43 -- |
42 | 44 |
43 ppp : { p : Set n } { a : HOD } → record { od = record { def = λ x → p } ; odmax = {!!} ; <odmax = {!!} } ∋ a → p | 45 pred-od : ( p : Set n ) → HOD |
44 ppp {p} {a} d = d | 46 pred-od p = record { od = record { def = λ x → (x ≡ o∅) ∧ p } ; |
47 odmax = osuc o∅; <odmax = λ x → subst (λ k → k o< osuc o∅) (sym (proj1 x)) <-osuc } | |
45 | 48 |
46 -- p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice | 49 ppp : { p : Set n } { a : HOD } → pred-od p ∋ a → p |
47 -- p∨¬p p with is-o∅ ( od→ord ( record { odef = λ x → p } )) | 50 ppp {p} {a} d = proj2 d |
48 -- p∨¬p p | yes eq = case2 (¬p eq) where | |
49 -- ps = record { odef = λ x → p } | |
50 -- lemma : ps =h= od∅ → p → ⊥ | |
51 -- lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 ) | |
52 -- ¬p : (od→ord ps ≡ o∅) → p → ⊥ | |
53 -- ¬p eq = lemma ( subst₂ (λ j k → j =h= k ) oiso o∅≡od∅ ( o≡→== eq )) | |
54 -- p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where | |
55 -- ps = record { odef = λ x → p } | |
56 -- eqo∅ : ps =h= od∅ → od→ord ps ≡ o∅ | |
57 -- eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) | |
58 -- lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq)) | |
59 -- lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq)) | |
60 | 51 |
61 postulate | 52 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice |
62 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice | 53 p∨¬p p with is-o∅ ( od→ord (pred-od p )) |
54 p∨¬p p | yes eq = case2 (¬p eq) where | |
55 ps = pred-od p | |
56 eqo∅ : ps =h= od∅ → od→ord ps ≡ o∅ | |
57 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) | |
58 lemma : ps =h= od∅ → p → ⊥ | |
59 lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } ) | |
60 ¬p : (od→ord ps ≡ o∅) → p → ⊥ | |
61 ¬p eq = lemma ( subst₂ (λ j k → j =h= k ) oiso o∅≡od∅ ( o≡→== eq )) | |
62 p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where | |
63 ps = pred-od p | |
64 eqo∅ : ps =h= od∅ → od→ord ps ≡ o∅ | |
65 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) | |
66 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq)) | |
67 lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq)) | |
63 | 68 |
64 decp : ( p : Set n ) → Dec p -- assuming axiom of choice | 69 decp : ( p : Set n ) → Dec p -- assuming axiom of choice |
65 decp p with p∨¬p p | 70 decp p with p∨¬p p |
66 decp p | case1 x = yes x | 71 decp p | case1 x = yes x |
67 decp p | case2 x = no x | 72 decp p | case2 x = no x |