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

changeset 670:f6a8de486bf3

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, 05 Jul 2022 08:22:32 +0900
parents 7d227d624aad
children f877150be143
files src/zorn.agda
diffstat 1 files changed, 4 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jul 05 05:43:27 2022 +0900
+++ b/src/zorn.agda	Tue Jul 05 08:22:32 2022 +0900
@@ -258,8 +258,8 @@
       u<x : u o< x
       chain∋z : Chain A f mf ay u z
 
-UnionCF : (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) (x : Ordinal) (chainf : (z : Ordinal ) →  Chain A f mf ay z z ) → HOD
-UnionCF A f mf ay x chainf = record { od = record { def = λ z → odef A z ∧  UChain A f mf ay x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
+UnionCF : (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) (x : Ordinal)  → HOD
+UnionCF A f mf ay x = record { od = record { def = λ z → odef A z ∧  UChain A f mf ay x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) ( z : Ordinal )  : Set (Level.suc n) where
    chain : HOD
@@ -541,7 +541,6 @@
                 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
                 ... | tri≈ ¬a b ¬c = refl
                 ... | tri> ¬a ¬b c = refl
-
           ... | case2 ¬x=sup = ? where -- x is not f y' nor sup of former ZChain from y -- no extention
                 z18 :  {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
                             HasPrev A (ZChain.chain zc) ab f ∨ IsSup A (ZChain.chain zc)   ab →
@@ -553,17 +552,10 @@
                 ... | 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 = zc5 where --- limit ordinal case
-          -- chainf : (zc : ZChain1 A f mf ay x ) → (z : Ordinal) → z o< x → HOD
-          -- chainf zc z z<x = ?
-          -- chainf : (z : Ordinal) → z o< x → HOD
-          -- chainf z z<x = ZChain.chain ( prev z z<x  )
-          -- chainq : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x )
-          -- chainq z z<x = ZChain.chain-uniq (  prev z z<x )
           uzc : HOD
-          uzc = UnionCF A f mf ay x ? 
+          uzc = UnionCF A f mf ay x 
           -- c-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → (w<x : w o< x ) → chainf z ? ⊆' chainf w w<x
-          -- c-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
-          -- ... | s | t = {!!}
+          -- c-mono {z} {w} z≤w w≤x {i} = ?
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
           ... | no noax = ? where -- ¬ A ∋ p, just skip