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

changeset 926:4b88d9a98d20

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 Thu, 20 Oct 2022 09:35:52 +0900
parents babd8ac79a91
children 0f2a85826cc7
files src/zorn.agda
diffstat 1 files changed, 18 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Oct 19 12:40:09 2022 +0900
+++ b/src/zorn.agda	Thu Oct 20 09:35:52 2022 +0900
@@ -1308,11 +1308,21 @@
             (supf : Ordinal → Ordinal )  → {x : Ordinal } → ZChainP f mf ay supf x → odef A x
      auzc f mf {y} ay supf {x} (zchain uz ucf) = proj1 ucf
 
+     zp-uz : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
+            (supf : Ordinal → Ordinal )  → {x : Ordinal } → ZChainP f mf ay supf x → Ordinal
+     zp-uz f mf ay supf (zchain uz _) = uz
+
+     uzc⊆zc :  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
+            (supf : Ordinal → Ordinal )  → {x : Ordinal } → (zp : ZChainP f mf ay supf x ) → UChain A f mf ay supf (zp-uz f mf ay supf zp) x 
+     uzc⊆zc f mf {y} ay supf {x} (zchain uz ⟪ ua , ch-init fc ⟫) = ch-init fc 
+     uzc⊆zc f mf {y} ay supf {x} (zchain uz ⟪ ua , ch-is-sup u u<x is-sup fc ⟫) with ChainP.supu=u is-sup
+     ... | eq = ch-is-sup u u<x is-sup fc 
+
      zc⊆uzc :  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
-            (supf : Ordinal → Ordinal )  → {x z ux : Ordinal } → UChain A f mf ay supf ux x → supf x o< supf z  → ZChainP f mf ay supf x
-     zc⊆uzc f mf {y} ay supf {x} ( ch-init fc ) _ = zchain x ⟪ A∋fc y f mf fc ,  ch-init fc ⟫
-     zc⊆uzc f mf {y} ay supf {x} {z} ( ch-is-sup u1 u1<x u1-is-sup fc ) sx<sz 
-        = zchain z ⟪ A∋fc (supf u1) f mf fc ,  ch-is-sup u1 ? u1-is-sup fc ⟫
+            (supf : Ordinal → Ordinal )  → {x ux : Ordinal } → UChain A f mf ay supf ux x → ZChainP f mf ay supf x
+     zc⊆uzc f mf {y} ay supf {x} ( ch-init fc ) = zchain x ⟪ A∋fc y f mf fc ,  ch-init fc ⟫
+     zc⊆uzc f mf {y} ay supf {x} ( ch-is-sup u1 u1<x u1-is-sup fc ) 
+        = zchain ? ⟪ A∋fc (supf u1) f mf fc ,  ch-is-sup u1 ? u1-is-sup fc ⟫
 
      UnionZF : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
             (supf : Ordinal → Ordinal )  → HOD
@@ -1322,9 +1332,10 @@
      uzctotal : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
          → ( supf : Ordinal → Ordinal )
          → IsTotalOrderSet (UnionZF f mf ay supf )
-     uzctotal f mf ay sz {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
-          uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-          uz01 = ?
+     uzctotal f mf ay supf {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (uz01 ca cb) where 
+          uz01 : {ua ub : Ordinal } → ZChainP f mf ay supf ua → ZChainP f mf ay supf ub 
+             → Tri (* ua < * ub) (* ua ≡ * ub) (* ub < * ua )
+          uz01 {ua} {ub} (zchain uza uca) (zchain uzb ucb) = chain-total A f mf ay supf (proj2 uca) (proj2 ucb)
 
      usp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
          → ( supf : Ordinal → Ordinal )