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

changeset 573:9ec37757a5a5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... still remains
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 03 May 2022 00:59:52 +0900
parents 427e36467a18
children 9084a26445a7
files src/zorn.agda
diffstat 1 files changed, 17 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Mon May 02 23:23:12 2022 +0900
+++ b/src/zorn.agda	Tue May 03 00:59:52 2022 +0900
@@ -541,7 +541,9 @@
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
-     ... | no ¬ox = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next
+     ... | no ¬ox = {!!} where
+       UnionZ : ZChain A ay f mf supO x
+       UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next
                      ; initial = u-initial ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} }  where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
             field
@@ -561,10 +563,22 @@
          u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
          u-chain∋x :  odef Uz y
          u-chain∋x = {!!}
-         Uz-mono : { a b : Ordinal } → (ua : odef Uz a) (ub : odef Uz b )  → a o< b → ZChain.chain (uzc ua) ⊆' ZChain.chain (uzc ub)
-         Uz-mono {a} {b} ua ub a<b ca = ZChain.is-max (uzc ub) (ZChain.chain∋x (uzc ub)) {!!}  {!!} {!!} {!!} where
+         Uz-mono : { a b : Ordinal } → (ua : odef Uz a) (ub : odef Uz b )  → a o< b → b o< x → ZChain.chain (uzc ua) ⊆' ZChain.chain (uzc ub)
+         Uz-mono {a} {b} ua ub a<b b<x {i} uai = {!!} where
              z30 : odef A b
              z30 = (ZChain.chain⊆A (uzc ub) (UZFChain.chain∋z ub))
+             supa : SUP A (ZChain.chain (uzc ua))
+             supa = supP (ZChain.chain (uzc ua)) (ZChain.chain⊆A (uzc ua)) (ZChain.f-total (uzc ua)) 
+             in-chain :   HasPrev A (ZChain.chain (uzc ua)) (SUP.A∋maximal supa) f ∨ IsSup A (ZChain.chain (uzc ua)) (SUP.A∋maximal supa)
+             in-chain = {!!}
+             z31 : ZChain.chain (uzc ua) ∋ SUP.sup supa
+             z31 = ZChain.is-max (uzc ua) (ZChain.chain∋x (uzc ua)) {!!} (SUP.A∋maximal supa) {!!} {!!}
+             ai : odef A i
+             ai = ZChain.chain⊆A (uzc ua) uai
+             -- (ZChain.initial (uzc ua) uai)
+             z32 : IsSup A (ZChain.chain (uzc ub)) ai
+             z32 = record { x<sup = {!!} }
+
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy = {!!}
          --- ux ⊆ uy ∨ uy ⊆ ux