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

comparison src/zorn.agda @ 490:00c71d1dc316

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
IsPartialOrder
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 08 Apr 2022 22:03:01 +0900
parents dc7a95dd66c4
children 646831f6b06d
comparison
equal deleted inserted replaced
489:dc7a95dd66c4 490:00c71d1dc316
52 52
53 PartialOrderSet : ( A : HOD ) → (_<_ : (x y : HOD) → Set n ) → Set (suc n) 53 PartialOrderSet : ( A : HOD ) → (_<_ : (x y : HOD) → Set n ) → Set (suc n)
54 PartialOrderSet A _<_ = (a b : Element A) 54 PartialOrderSet A _<_ = (a b : Element A)
55 → (elm a < elm b → ((¬ elm b < elm a) ∧ (¬ (elm a ≡ elm b) ))) ∧ (elm a ≡ elm b → (¬ elm a < elm b) ∧ (¬ elm b < elm a)) 55 → (elm a < elm b → ((¬ elm b < elm a) ∧ (¬ (elm a ≡ elm b) ))) ∧ (elm a ≡ elm b → (¬ elm a < elm b) ∧ (¬ elm b < elm a))
56 56
57 IsPartialOrderSet : ( A : HOD ) → (_<_ : (x y : HOD) → Set n ) → Set (suc n)
58 IsPartialOrderSet A _<_ = IsPartialOrder _<A_ _≡A_ where
59 _<A_ : (x y : Element A ) → Set n
60 x <A y = elm x < elm y
61 _≡A_ : (x y : Element A ) → Set (suc n)
62 x ≡A y = elm x ≡ elm y
63
64 IsTotalOrderSet : ( A : HOD ) → (_<_ : (x y : HOD) → Set n ) → Set (suc n)
65 IsTotalOrderSet A _<_ = IsTotalOrder _<A_ _≡A_ where
66 _<A_ : (x y : Element A ) → Set n
67 x <A y = elm x < elm y
68 _≡A_ : (x y : Element A ) → Set (suc n)
69 x ≡A y = elm x ≡ elm y
70
57 me : { A a : HOD } → A ∋ a → Element A 71 me : { A a : HOD } → A ∋ a → Element A
58 me {A} {a} lt = record { elm = a ; is-elm = lt } 72 me {A} {a} lt = record { elm = a ; is-elm = lt }
59 73
60 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where 74 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
61 field 75 field
75 record ZChain ( A : HOD ) (y : Ordinal) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where 89 record ZChain ( A : HOD ) (y : Ordinal) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
76 field 90 field
77 fb : (x : Ordinal ) → x o< y → HOD 91 fb : (x : Ordinal ) → x o< y → HOD
78 A∋fb : (ox : Ordinal ) → (x<y : ox o< y ) → A ∋ fb ox x<y 92 A∋fb : (ox : Ordinal ) → (x<y : ox o< y ) → A ∋ fb ox x<y
79 monotonic : {ox oz : Ordinal } → (x<y : ox o< y ) → (z<y : oz o< y ) → ox o< oz → fb ox x<y < fb oz z<y 93 monotonic : {ox oz : Ordinal } → (x<y : ox o< y ) → (z<y : oz o< y ) → ox o< oz → fb ox x<y < fb oz z<y
80 injection : {ox oz : Ordinal } → (x<y : ox o< y ) → (z<y : oz o< y ) → fb ox x<y ≡ fb oz z<y → ox ≡ oz
81 94
82 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n } 95 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
83 → o∅ o< & A 96 → o∅ o< & A
84 → PartialOrderSet A _<_ 97 → PartialOrderSet A _<_
85 → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B _<_ ) -- SUP condition 98 → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B _<_ ) -- SUP condition
129 → obx z x ≡ obx z y → bx<A z x ≅ bx<A z y 142 → obx z x ≡ obx z y → bx<A z x ≅ bx<A z y
130 z12 z {a} {b} x y eq = {!!} 143 z12 z {a} {b} x y eq = {!!}
131 bx-inject : (z : ZChain A (& A) _<_ ) → {x y : Element (B z)} → BX.bx (is-elm x) ≡ BX.bx (is-elm y) → elm x ≡ elm y 144 bx-inject : (z : ZChain A (& A) _<_ ) → {x y : Element (B z)} → BX.bx (is-elm x) ≡ BX.bx (is-elm y) → elm x ≡ elm y
132 bx-inject z {x} {y} eq = begin 145 bx-inject z {x} {y} eq = begin
133 elm x ≡⟨ {!!} ⟩ 146 elm x ≡⟨ {!!} ⟩
134 {!!} ≡⟨ cong (λ k → {!!} ) ( ZChain.injection z {!!} {!!} ? ) ⟩ 147 {!!} ≡⟨ cong (λ k → {!!} ) {!!} ⟩
135 {!!} ≡⟨ {!!} ⟩ 148 {!!} ≡⟨ {!!} ⟩
136 elm y ∎ where open ≡-Reasoning 149 elm y ∎ where open ≡-Reasoning
137 B-is-total : (z : ZChain A (& A) _<_ ) → TotalOrderSet (B z) _<_ 150 B-is-total : (z : ZChain A (& A) _<_ ) → TotalOrderSet (B z) _<_
138 B-is-total z x y with trio< (obx z (is-elm x)) (obx z (is-elm y)) 151 B-is-total z x y with trio< (obx z (is-elm x)) (obx z (is-elm y))
139 ... | tri< a ¬b ¬c = tri< z10 (λ eq → proj1 (proj2 (PO-B z x y) eq ) z10) (λ ¬c → proj1 (proj1 (PO-B z y x) ¬c ) z10) where 152 ... | tri< a ¬b ¬c = tri< z10 (λ eq → proj1 (proj2 (PO-B z x y) eq ) z10) (λ ¬c → proj1 (proj1 (PO-B z y x) ¬c ) z10) where
140 z10 : elm x < elm y 153 z10 : elm x < elm y
141 z10 = bx-monotonic z {x} {y} a 154 z10 = bx-monotonic z {x} {y} a
142 ... | tri≈ ¬a b ¬c = tri≈ {!!} {!!} {!!} 155 ... | tri≈ ¬a b ¬c = tri≈ {!!} (bx-inject z {x} {y} b) {!!}
143 ... | tri> ¬a ¬b c = tri> (λ ¬a → proj1 (proj1 (PO-B z x y) ¬a ) (bx-monotonic z {y} {x} c) ) (λ eq → proj2 (proj2 (PO-B z x y) eq ) (bx-monotonic z {y} {x} c)) (bx-monotonic z {y} {x} c) 156 ... | tri> ¬a ¬b c = tri> (λ ¬a → proj1 (proj1 (PO-B z x y) ¬a ) (bx-monotonic z {y} {x} c) ) (λ eq → proj2 (proj2 (PO-B z x y) eq ) (bx-monotonic z {y} {x} c)) (bx-monotonic z {y} {x} c)
144 ZChain→¬SUP : (z : ZChain A (& A) _<_ ) → ¬ (SUP A (B z) _<_ ) 157 ZChain→¬SUP : (z : ZChain A (& A) _<_ ) → ¬ (SUP A (B z) _<_ )
145 ZChain→¬SUP z sp = ⊥-elim {!!} where 158 ZChain→¬SUP z sp = ⊥-elim {!!} where
146 z03 : & (SUP.sup sp) o< osuc (& A) 159 z03 : & (SUP.sup sp) o< osuc (& A)
147 z03 = ordtrans (c<→o< (SUP.A∋maximal sp)) <-osuc 160 z03 = ordtrans (c<→o< (SUP.A∋maximal sp)) <-osuc