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

changeset 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
files src/zorn.agda
diffstat 1 files changed, 16 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Apr 08 17:47:24 2022 +0900
+++ b/src/zorn.agda	Fri Apr 08 22:03:01 2022 +0900
@@ -54,6 +54,20 @@
 PartialOrderSet A _<_ = (a b :  Element A)
      → (elm a < elm b → ((¬ elm b < elm a) ∧ (¬ (elm a ≡ elm b) ))) ∧ (elm a ≡ elm b → (¬ elm a < elm b) ∧ (¬ elm b < elm a))
 
+IsPartialOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
+IsPartialOrderSet A _<_ = IsPartialOrder _<A_ _≡A_ where
+   _<A_ : (x y : Element A ) → Set n
+   x <A y = elm x < elm y
+   _≡A_ : (x y : Element A ) → Set (suc n)
+   x ≡A y = elm x ≡ elm y
+
+IsTotalOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
+IsTotalOrderSet A _<_ = IsTotalOrder _<A_ _≡A_ where
+   _<A_ : (x y : Element A ) → Set n
+   x <A y = elm x < elm y
+   _≡A_ : (x y : Element A ) → Set (suc n)
+   x ≡A y = elm x ≡ elm y
+
 me : { A a : HOD } → A ∋ a → Element A
 me {A} {a} lt = record { elm = a ; is-elm = lt }
 
@@ -77,7 +91,6 @@
       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 
@@ -131,7 +144,7 @@
      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 ≡⟨  {!!}   ⟩
-            {!!} ≡⟨ cong (λ k → {!!} ) ( ZChain.injection z {!!} {!!} ? )  ⟩
+            {!!} ≡⟨ cong (λ k → {!!} ) {!!}  ⟩
             {!!} ≡⟨ {!!}   ⟩
             elm y ∎ where open ≡-Reasoning
      B-is-total :  (z : ZChain A (& A) _<_ ) → TotalOrderSet (B z) _<_ 
@@ -139,7 +152,7 @@
      ... | 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
           z10 : elm x < elm y
           z10 = bx-monotonic z {x} {y} a
-     ... | tri≈ ¬a b ¬c = tri≈ {!!} {!!} {!!}
+     ... | tri≈ ¬a b ¬c = tri≈ {!!} (bx-inject z {x} {y} b) {!!}
      ... | 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)
      ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (B z) _<_ )
      ZChain→¬SUP z sp = ⊥-elim {!!} where