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

changeset 605:b42f0e50a831

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 Tue, 14 Jun 2022 16:05:25 +0900
parents 021fcb324990
children 9bdb671cbffd
files src/zorn.agda
diffstat 1 files changed, 11 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jun 14 15:32:01 2022 +0900
+++ b/src/zorn.agda	Tue Jun 14 16:05:25 2022 +0900
@@ -402,6 +402,15 @@
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc
           c = & (SUP.sup sp1)
 
+     ys : {y : Ordinal} → (ay : odef A y)  (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → HOD
+     ys {y} ay f mf = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = {!!} }
+     init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x
+     init-chain {y} {x} ay f mf x≤y = record { chain = ys ay f mf ; chain⊆A = λ fx →  A∋fc y f mf fx
+                     ; f-total = i-total ; f-next = λ {x} sx → fsuc x sx ; chain∋sup = {!!}
+                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = init ay ; is-max = {!!} ; fc∨sup = {!!} } where
+               i-total : IsTotalOrderSet (ys ay f mf )
+               i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb)
+
      --
      -- create all ZChains under o< x
      --
@@ -422,15 +431,6 @@
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
 
-          ys : HOD
-          ys = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = {!!} }
-          init-chain : ZChain A y f y
-          init-chain = record { chain = ys ; chain⊆A = λ fx →  A∋fc y f mf fx
-                     ; f-total = i-total ; f-next = λ {x} sx → fsuc x sx ; chain∋sup = {!!}
-                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = init ay ; is-max = {!!} ; fc∨sup = {!!} } where
-               i-total : IsTotalOrderSet ys
-               i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb)
-
           fcs< :  (A : HOD) {w y : Ordinal} (ay : odef A y)   (c z : Ordinal) (x : Ordinal)
                 → z o< w → Fc∨sup  A ay f c z x → Fc∨sup  A ay f c w x 
           fcs< A ay c z x z<w (Finit x₁) = Finit x₁
@@ -586,9 +586,8 @@
                 ... | 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 with trio< x y
-     ... | tri< a ¬b ¬c = record { chain = {!!} ; chain⊆A = {!!}  ; f-total = {!!}  ; f-next = {!!} ; chain∋sup = {!!}
-                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }
-     ... | tri≈ ¬a b ¬c = {!!}
+     ... | tri< a ¬b ¬c = init-chain ay f mf {!!}
+     ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!}
      ... | tri> ¬a ¬b y<x = UnionZ where
        UnionZ : ZChain A y f x
        UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next ; chain∋sup = {!!}