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

changeset 494:45b19d35dc07

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 Apr 2022 08:30:33 +0900
parents 71436ccbc804
children 4203ba14fd53
files src/zorn.agda
diffstat 1 files changed, 21 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sat Apr 09 07:39:52 2022 +0900
+++ b/src/zorn.agda	Sat Apr 09 08:30:33 2022 +0900
@@ -48,33 +48,34 @@
 open Element
 
 IsPartialOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
-IsPartialOrderSet A _<_ = IsStrictPartialOrder _<A_ _≡A_ where
-   _<A_ : (x y : Element A ) → Set n
-   x <A y = elm x < elm y
+IsPartialOrderSet A _<_ = IsPartialOrder _≡A_ _≤A_  where
+   _≤A_ : (x y : Element A ) → Set (suc n)
+   x ≤A y = (elm x ≡ elm y) ∨ (elm x < elm y)
    _≡A_ : (x y : Element A ) → Set (suc n)
    x ≡A y = elm x ≡ elm y
 
 open _==_
 open _⊆_
 
+toA : { A B  : HOD } → B ⊆ A → (x : Element B) → Element A
+toA B⊆A x = record { elm = elm x ; is-elm = incl B⊆A (is-elm x) }
+
 ⊆-IsPartialOrderSet : { A B  : HOD } → B ⊆ A →  {_<_ : (x y : HOD) → Set n }  → IsPartialOrderSet A _<_ → IsPartialOrderSet B _<_
 ⊆-IsPartialOrderSet {A} {B} B⊆A {_<_} PA = record {
-       isEquivalence = record { refl = refl1 ; sym = {!!} ; trans = {!!} } ; irrefl = {!!} ; trans = {!!} ; <-resp-≈ = {!!} 
+       isPreorder =  record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans } ; reflexive = λ eq → case1 eq ; trans = λ {x} {y} {z} → trans1 {x} {y} {z} }
+     ; antisym = λ {x} {y} → anti {x} {y}
    } where
-       _<B_ : (x y : Element B ) → Set n
-       x <B y = elm x < elm y
-       _≡B_ : (x y : Element B ) → Set (suc n)
-       x ≡B y = elm x ≡ elm y
-       _≤B_ : (x y : Element B ) → Set (suc n)
-       x ≤B y = (elm x ≡ elm y) ∨ (elm x < elm y)
-       refl1 : Reflexive  _≤B_ 
-       refl1  = case1 refl -- IsEquivalence.refl ( IsStrictPartialOrder.isEquivalence PA ) 
-       -- refl1 {case2 lt} = ?
+   _≤B_ : (x y : Element B ) → Set (suc n)
+   x ≤B y = (elm x ≡ elm y) ∨ (elm x < elm y)
+   trans1 : {x y z : Element B} → x ≤B y → y ≤B z → x ≤B z 
+   trans1 {x} {y} {z} x<y y<z  = IsPreorder.trans (IsPartialOrder.isPreorder PA) {toA B⊆A x} {toA B⊆A y} {toA B⊆A z} x<y y<z 
+   anti : {x y : Element B} → x ≤B y →  y ≤B x  → elm x ≡ elm y
+   anti {x} {y} x<y y<x = IsPartialOrder.antisym PA {toA B⊆A x} {toA B⊆A y} x<y y<x
 
 IsTotalOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
-IsTotalOrderSet A _<_ = IsStrictTotalOrder _<A_ _≡A_ where
-   _<A_ : (x y : Element A ) → Set n
-   x <A y = elm x < elm y
+IsTotalOrderSet A _<_ = IsTotalOrder  _≡A_ _≤A_ where
+   _≤A_ : (x y : Element A ) → Set (suc n)
+   x ≤A y = (elm x ≡ elm y) ∨ (elm x < elm y)
    _≡A_ : (x y : Element A ) → Set (suc n)
    x ≡A y = elm x ≡ elm y
 
@@ -85,7 +86,7 @@
    field
       sup : HOD
       A∋maximal : A ∋ sup
-      x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
+      x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
@@ -143,7 +144,7 @@
      B⊆A : (z : ZChain A (& A) _<_ ) → B z ⊆ A
      B⊆A z = record { incl = λ {x} bx → subst (λ k → odef A k ) (sym (BX.is-fb bx)) (ZChain.A∋fb z (BX.bx bx) (BX.bx<y bx) ) }
      PO-B : (z : ZChain A (& A) _<_ ) → IsPartialOrderSet (B z) _<_
-     PO-B z = subst₂ (λ j k → IsStrictPartialOrder j k ) {!!} {!!} {!!} where
+     PO-B z = subst₂ (λ j k → IsPartialOrder j k ) {!!} {!!} {!!} where
            _<B_ = {!!}
            _≡B_ = {!!}
         -- a b = {!!} -- PO record { elm = elm a ; is-elm = incl ( B⊆A z) (is-elm a) }  record { elm = elm b ; is-elm = incl ( B⊆A z) (is-elm b) }  
@@ -173,7 +174,7 @@
          z03 : & (SUP.sup sp) o< osuc (& A)
          z03 = ordtrans (c<→o< (SUP.A∋maximal sp)) <-osuc
          z02 :  (x : HOD) → B z ∋ x → SUP.sup sp < x → ⊥
-         z02 x xe s<x = z01 (incl (B⊆A z) xe) (SUP.A∋maximal sp) (SUP.x≤sup sp xe) s<x 
+         z02 x xe s<x = z01 (incl (B⊆A z) xe) (SUP.A∋maximal sp) (SUP.x<sup sp xe) s<x 
      ind :  HasMaximal =h= od∅
          → (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y _<_ )
          →  ZChain A x _<_
@@ -187,7 +188,7 @@
           z04 :  {!!} -- (sup : HOD) (as : A ∋ sup) → & sup o< osuc x → sup < ZChain.fb zc1 as
           z04 sup as s<x with trio< (& sup) x
           ... | tri≈ ¬a b ¬c = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans b (sym &iso)) as) )  
-          ... | tri< a ¬b ¬c  = {!!} -- ZChain.¬x≤sup zc1 _ as ( subst (λ k → & sup o< k ) (sym (Oprev.oprev=x op)) a )
+          ... | tri< a ¬b ¬c  = {!!} -- ZChain.¬x<sup zc1 _ as ( subst (λ k → & sup o< k ) (sym (Oprev.oprev=x op)) a )
           ... | tri> ¬a ¬b c with  osuc-≡< s<x
           ... | case1 eq = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans eq (sym &iso)) as) )  
           ... | case2 lt = ⊥-elim (¬a lt )