# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655779416 -32400
# Node ID 75578f19ed3c92a2e775eb37a3209f4bc981fc38
# Parent  c17d46ecb051e1bf3d3340874a36de4f6c2b23cd
...

diff -r c17d46ecb051 -r 75578f19ed3c src/zorn.agda
--- 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