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

changeset 583:f545b97ce7a8

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, 07 Jun 2022 12:59:08 +0900
parents 48e9d2e61bbe
children b684030c8a28 4dbaa071d695
files src/zorn.agda
diffstat 1 files changed, 21 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jun 07 02:18:25 2022 +0900
+++ b/src/zorn.agda	Tue Jun 07 12:59:08 2022 +0900
@@ -248,16 +248,32 @@
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
-      fc∨sup :  {a : Ordinal } → a o< osuc z →  ( ca : odef chain a ) → HasPrev A chain ( chain⊆A ca) f  ∨ IsSup A chain  ( chain⊆A ca)
+      fc∨sup :  {a : Ordinal } → ( ca : odef chain a ) → HasPrev A chain ( chain⊆A ca) f  ∨ IsSup A chain  ( chain⊆A ca)
 
 Uz-mono : ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) 
      → ( a b : Ordinal ) → a o< b → (za : ZChain A x f a) (zb : ZChain A x f b) 
      → ZChain.chain za  ⊆' ZChain.chain zb
-Uz-mono A x f a b a<b za zb {i} zai = TransFinite0 (ind i) a where
+Uz-mono A x f a b = TransFinite {λ a → a o< b → (za : ZChain A x f a) (zb : ZChain A x f b)
+     → ZChain.chain za  ⊆' ZChain.chain zb } ind a where
     open ZChain
-    ind : (i a : Ordinal) → ((y : Ordinal) → y o< a → odef (ZChain.chain zb) i) → odef (ZChain.chain zb) i 
-    ind = ?
-
+    ind :  (a : Ordinal)
+         → ((y : Ordinal) → y o< a →  y o< b → (za : ZChain A x f y) (zb : ZChain A x f b) → chain za ⊆' chain zb)
+         → a o< b → (za : ZChain A x f a) (zb : ZChain A x f b) → chain za ⊆' chain zb
+    ind a prev a<b za zb {i} zai with f-total za (subst (λ k → odef (chain za) k) (sym &iso) zai)
+                                     (subst (λ k → odef (chain za) k) (sym &iso) (chain∋x za) ) 
+    ... | tri< i<x ¬b ¬c with initial za zai
+    ... | case1 i=x = ⊥-elim ( ¬b (sym i=x))
+    ... | case2 x<i = ⊥-elim ( ¬c x<i)
+    ind a prev a<b za zb {i} zai | tri≈ ¬a b ¬c = subst (λ k → odef (chain zb) k ) (sym (*≡*→≡ b))(chain∋x zb)
+    ind a prev a<b za zb {i} zai | tri> ¬a ¬b x<i = um i zai where
+          um : (i : Ordinal ) → odef (chain za) i → odef (chain zb) i
+          um zai i with fc∨sup za zai
+          ... | case1 fc = {!!}
+          ... | case2 sup = {!!}
+          um01 : i o< osuc b
+          um01 = {!!}
+          um02 : {!!}
+          um02 =  is-max zb (chain∋x zb) {!!} (chain⊆A za zai)  {!!} x<i
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field