# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1671579579 -32400
# Node ID 6caa088346f02cdcf89d669f1ecaf0a64288bd7e
# Parent  87c2da3811c3b8c64a357c4e0942e211b1080b45
...

diff -r 87c2da3811c3 -r 6caa088346f0 src/zorn.agda
--- a/src/zorn.agda	Wed Dec 21 07:30:18 2022 +0900
+++ b/src/zorn.agda	Wed Dec 21 08:39:39 2022 +0900
@@ -5,7 +5,7 @@
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
 import OD hiding ( _⊆_ )
-module zorn1 {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where
+module zorn {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where
 
 --
 -- Zorn-lemma : { A : HOD }
@@ -294,13 +294,18 @@
           chain : HOD
           chain⊆A : chain ⊆ A
           f-total  : IsTotalOrderSet chain
-          cf : Ordinal → Ordinal 
-          is-cf : {x : Ordinal} → odef A x → odef A (cf x) ∧ ( * x < * (cf x) )
-          f-next  : {x : Ordinal } → odef chain x → odef chain (cf x)
-          fixpoint : (sp1 : MinSUP A chain ) → odef chain (MinSUP.sup sp1)
-       cf-is-<-monotonic : <-monotonic-f A cf
-       cf-is-<-monotonic x ax = ⟪ proj2 (is-cf ax ) , proj1 (is-cf ax ) ⟫
-       cf-is-≤-monotonic : ≤-monotonic-f A cf 
+          supf : Ordinal → Ordinal 
+          asupf : {z : Ordinal} → odef A (supf z) 
+          supf-< : {z : Ordinal} → odef A z →  * z < * (supf z) 
+          f-next  : {z : Ordinal } → odef chain z → odef chain (supf z)
+          supf→chain : Ordinal → Ordinal 
+          sc-iso : {z : Ordinal} → supf (supf→chain z) ≡ z
+          sc=chain : supf→chain x ≡ & chain
+          sc-mono : {a b : Ordinal} → a o< b → supf→chain a o< supf→chain b
+
+       cf-is-<-monotonic : <-monotonic-f A supf
+       cf-is-<-monotonic x ax = ⟪ supf-< ax , asupf ⟫
+       cf-is-≤-monotonic : ≤-monotonic-f A supf 
        cf-is-≤-monotonic x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic x ax  ))  , proj2 ( cf-is-<-monotonic x ax  ) ⟫
 
      SZ : ¬ Maximal A → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A ay x
@@ -330,18 +335,18 @@
      --
      fixpoint : (zc : ZChain A  as0 (& A))
             → (sp1 : MinSUP A (ZChain.chain zc))
-            → ZChain.cf zc (MinSUP.sup sp1)  ≡ MinSUP.sup sp1
+            → ZChain.supf zc (MinSUP.sup sp1)  ≡ MinSUP.sup sp1
      fixpoint zc sp1 = z14 where
            chain = ZChain.chain zc
            sp : Ordinal
            sp = MinSUP.sup sp1
            asp : odef A sp
            asp = MinSUP.as sp1
-           f = ZChain.cf zc
+           f = ZChain.supf zc
            mf : ≤-monotonic-f A f
            mf = ZChain.cf-is-≤-monotonic zc
            z12 : odef chain sp
-           z12 = ZChain.fixpoint zc sp1
+           z12 = ? -- ZChain.fixpoint zc sp1
            z14 :  f sp ≡ sp
            z14 with ZChain.f-total zc (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) (subst (λ k → odef chain k) (sym &iso) z12 )
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
@@ -365,14 +370,14 @@
      --
 
      ¬Maximal→¬cf-mono :  (nmx : ¬ Maximal A ) → (zc : ZChain A as0 (& A)) → ⊥
-     ¬Maximal→¬cf-mono nmx zc = <-irr0  {* (ZChain.cf zc c)} {* c}
-           (subst (λ k → odef A k ) (sym &iso) (proj1 (ZChain.is-cf zc (MinSUP.as  msp1 ))))
+     ¬Maximal→¬cf-mono nmx zc = <-irr0  {* (ZChain.supf zc c)} {* c}
+           (subst (λ k → odef A k ) (sym &iso) (ZChain.asupf zc ))
            (subst (λ k → odef A k) (sym &iso) (MinSUP.as msp1) )
            (case1 ( cong (*)( fixpoint zc msp1  ))) -- x ≡ f x ̄
                 (proj1 (ZChain.cf-is-<-monotonic zc c (MinSUP.as msp1 ))) where          -- x < f x
 
           msp1 : MinSUP A (ZChain.chain zc)
-          msp1 = msp0 (ZChain.cf zc) (ZChain.cf-is-<-monotonic zc) as0 zc
+          msp1 = msp0 (ZChain.supf zc) (ZChain.cf-is-<-monotonic zc) as0 zc
           c : Ordinal
           c = MinSUP.sup msp1