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

changeset 638:75578f19ed3c

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, 21 Jun 2022 11:43:36 +0900
parents c17d46ecb051
children cf5af048db99
files src/zorn.agda
diffstat 1 files changed, 3 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jun 21 11:21:27 2022 +0900
+++ b/src/zorn.agda	Tue Jun 21 11:43:36 2022 +0900
@@ -696,10 +696,12 @@
              ; chain-mono = mono sf ; f-total = {!!} } where -- TransFinite {λ w → ZChain1 f mf ay w} indp z where
          sf : Ordinal → HOD
          sf x = ZChain.supf (TransFinite (ind f mf ay) (& A)) x
+         sf' : Ordinal → HOD
+         sf' x = ZChain.supf (ind f mf ay (& A) {!!} )  x
          mono :  {x : Ordinal} {w : Ordinal} (sf : Ordinal → HOD) → x o≤ w → sf x ⊆' sf w 
          mono {a} {b} sf a≤b = TransFinite0 {λ b → a o≤ b → sf a ⊆' sf b } mind b a≤b where
             mind :  (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → a o≤ y₁ → sf a ⊆' sf y₁) → a o≤ x → sf a ⊆' sf x
-            mind = {!!}
+            mind x prev a≤x sai = {!!}
 
 
      zorn00 : Maximal A