Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 489:dc7a95dd66c4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 08 Apr 2022 17:47:24 +0900 |
| parents | d2d704ab1a33 |
| children | 00c71d1dc316 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 4 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Fri Apr 08 17:36:42 2022 +0900 +++ b/src/zorn.agda Fri Apr 08 17:47:24 2022 +0900 @@ -77,6 +77,7 @@ fb : (x : Ordinal ) → x o< y → HOD A∋fb : (ox : Ordinal ) → (x<y : ox o< y ) → A ∋ fb ox x<y 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 + injection : {ox oz : Ordinal } → (x<y : ox o< y ) → (z<y : oz o< y ) → fb ox x<y ≡ fb oz z<y → ox ≡ oz Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n } → o∅ o< & A @@ -129,9 +130,9 @@ z12 z {a} {b} x y eq = {!!} 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 bx-inject z {x} {y} eq = begin - elm x ≡⟨ obx=fb z (is-elm x) ⟩ - ZChain.fb z (obx z (is-elm x)) (bx<A z (is-elm x)) ≡⟨ cong₂ (λ j k → ZChain.fb z j k ) ? ( HE.≅-to-≡ (z12 z ? ? eq) ) ⟩ - ZChain.fb z (obx z (is-elm y)) (bx<A z (is-elm y)) ≡⟨ sym ( obx=fb z (is-elm y) ) ⟩ + elm x ≡⟨ {!!} ⟩ + {!!} ≡⟨ cong (λ k → {!!} ) ( ZChain.injection z {!!} {!!} ? ) ⟩ + {!!} ≡⟨ {!!} ⟩ elm y ∎ where open ≡-Reasoning B-is-total : (z : ZChain A (& A) _<_ ) → TotalOrderSet (B z) _<_ B-is-total z x y with trio< (obx z (is-elm x)) (obx z (is-elm y))