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

changeset 717:d76047a8a89b

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, 16 Jul 2022 00:03:47 +0900
parents b0cad3ec7da0
children 300f9176edc2
files src/zorn.agda
diffstat 1 files changed, 8 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Jul 15 21:39:32 2022 +0900
+++ b/src/zorn.agda	Sat Jul 16 00:03:47 2022 +0900
@@ -741,16 +741,18 @@
               zc12 = ⟪ ab , record { u = UChain.u (proj2 za) ;  u<x = ? ; uchain = ? } ⟫
               -- ZChain.is-max (uzc za) ? ? ab (subst (λ k → HasPrev A k ab f ∨  IsSup A k ab ) cheq P)  a<b 
 
-          chain-mono : pchain ⊆'  UnionCF A f mf ay psupf x  
-          chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  ; u<x = UChain.u<x (proj2 za) ; uchain = zc11 }  ⟫ where
+          chain-mono : {x1 : Ordinal } → x1 o≤ x  → UnionCF A f mf ay psupf x1   ⊆'  UnionCF A f mf ay psupf x  
+          chain-mono {x} x1≤x {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  
+                 ; u<x = ? ; uchain = zc11 }  ⟫ where
               zc11 : Chain A f mf ay psupf (UChain.u (proj2 za)) a
               zc11 with UChain.uchain (proj2 za)
               ... | ch-init .a x = ch-init a x
-              ... | ch-is-sup is-sup fc = ch-is-sup ? (subst (λ k → FClosure A f k a ) ? fc )
+              ... | ch-is-sup is-sup fc = ch-is-sup ? fc
+              -- OrdTrans (UChain.u<x (proj2 za)) ?  
 
-          chain-≡ : UnionCF A f mf ay psupf x ⊆' pchain 
-             → UnionCF A f mf ay psupf x ≡ pchain 
-          chain-≡ lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono }
+          chain-≡ : {x1 : Ordinal } → x1 o≤ x  → UnionCF A f mf ay psupf x ⊆'  UnionCF A f mf ay psupf x1
+             → UnionCF A f mf ay psupf x ≡ UnionCF A f mf ay psupf x1 
+          chain-≡ {x1} x1≤x lt = ==→o≡ record { eq→ = lt ; eq← = chain-mono x1≤x }
 
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)