# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650706520 -32400
# Node ID b83dde5dbd3308e1579c026abb0b5e19f2847123
# Parent  c9f80aea598e63f88686426b2ba5efe1fe3e1618
...

diff -r c9f80aea598e -r b83dde5dbd33 src/zorn.agda
--- a/src/zorn.agda	Sat Apr 23 18:05:12 2022 +0900
+++ b/src/zorn.agda	Sat Apr 23 18:35:20 2022 +0900
@@ -460,14 +460,15 @@
 SupCond A B _ _ = SUP A B  
 
 record ZChain ( A : HOD ) {x : Ordinal} (ax : A ∋ * x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f )
-         (sup : (C : Ordinal ) → IsTotalOrderSet (* C) → Ordinal) (z : Ordinal)  : Set (Level.suc n) where
+         (sup : (C : Ordinal ) → (* C ⊆ A) → IsTotalOrderSet (* C) → Ordinal) (z : Ordinal)  : Set (Level.suc n) where
    field
       chain : HOD
       chain⊆A : chain ⊆ A
       f-total : IsTotalOrderSet chain 
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       is-max :  {a b : Ordinal } → (ca : odef chain a ) → odef A b → a o< z
-          → ( Prev< A (incl chain⊆A (subst (λ k → odef chain k ) (sym &iso) ca)) f ∨ (sup (& chain)  (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b ))
+          → ( Prev< A (incl chain⊆A (subst (λ k → odef chain k ) (sym &iso) ca)) f
+               ∨ (sup (& chain) (subst (λ k → k  ⊆ A) (sym *iso) chain⊆A)  (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b ))
           → * a < * b  → odef chain b
 
 Zorn-lemma : { A : HOD } 
@@ -476,6 +477,8 @@
     → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
     → Maximal A 
 Zorn-lemma {A}  0<A PO supP = zorn00 where
+     supO : (C : Ordinal ) → (* C) ⊆ A → IsTotalOrderSet (* C) → Ordinal
+     supO C C⊆A TC = & ( SUP.sup ( supP (* C)  C⊆A TC ))
      z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
      z01 {a} {b} A∋a A∋b (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋a} (sym a=b) b<a
      z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋b} refl
@@ -506,38 +509,38 @@
      cf-is-<-monotonic nmx x ax = ⟪ {!!} , {!!} ⟫
      cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
-     zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc : ZChain A sa f mf {!!} (& A)) → SUP A  (ZChain.chain zc) 
+     zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc : ZChain A sa f mf supO (& A)) → SUP A  (ZChain.chain zc) 
      zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc  )   
      -- zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf )  ) )
-     A∋zsup :  (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) {!!} (& A)) 
+     A∋zsup :  (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) 
         →  A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) ))
      A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal  (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )
-     z03 :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf {!!} (& A)) → f (& ( SUP.sup (zsup f mf zc ))) ≡ & (SUP.sup (zsup f mf zc ))
+     z03 :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf supO (& A)) → f (& ( SUP.sup (zsup f mf zc ))) ≡ & (SUP.sup (zsup f mf zc ))
      z03 = {!!}
-     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) {!!}  (& A)) → ⊥
+     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) → ⊥
      z04 nmx zc = z01  {* (cf nmx c)} {* c} {!!} (A∋zsup nmx zc ) (case1 ( cong (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc )))
            (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup nmx zc )))) where
           c = & (SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ))
      -- ZChain is not compatible with the SUP condition
-     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A sa f mf {!!} y )
-         →  ZChain A sa f mf {!!} x 
+     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A sa f mf supO y )
+         →  ZChain A sa f mf supO x 
      ind f mf x prev with Oprev-p x
      ... | yes op with ODC.∋-p O A (* x)
      ... | no ¬Ax = zc1 where
           -- we have previous ordinal and ¬ A ∋ x, use previous Zchain
           px = Oprev.oprev op
-          zc0 : ZChain A sa f mf {!!} (Oprev.oprev op) 
+          zc0 : ZChain A sa f mf supO (Oprev.oprev op) 
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
-          zc1 : ZChain A sa f mf {!!} x 
+          zc1 : ZChain A sa f mf supO x 
           zc1 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 ; is-max = {!!} }
      ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x
           px = Oprev.oprev op
-          zc0 : ZChain A sa f mf {!!} (Oprev.oprev op) 
+          zc0 : ZChain A sa f mf supO (Oprev.oprev op) 
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
           --   x is in the previous chain, use the same
           --   x has some y which y < x ∧ f y ≡ x
           --   x has no y which y < x 
-          zc4 : ZChain A sa f mf {!!} x
+          zc4 : ZChain A sa f mf supO x
           zc4 = record { chain = {!!} ; chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} ; is-max = {!!} }
      ind f mf x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
      ... | tri< a ¬b ¬c = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
@@ -561,7 +564,7 @@
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
               zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 
               zc5 = ⟪  Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫
-         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → ZChain A sa f mf {!!} (& A)
+         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → ZChain A sa f mf supO (& A)
          zorn03 f mf = TransFinite (ind f mf)  (& A) 
 
 -- usage (see filter.agda )