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

diff -r 7325484fc491 -r c9f80aea598e src/zorn.agda
--- a/src/zorn.agda	Sat Apr 23 17:46:12 2022 +0900
+++ b/src/zorn.agda	Sat Apr 23 18:05:12 2022 +0900
@@ -444,14 +444,11 @@
       x<z : * x < * z 
       z<y : * z < * y 
 
-IndirectSet< : (A : HOD) → {x y : Ordinal } (xa : odef A x) (ya : odef A y) → HOD
-IndirectSet< A {x} {y} xa ya = record { od = record { def = λ z → odef A z ∧ Indirect< A xa ya z } ; odmax = & A ; <odmax = {!!} }
-
-record Prev< (A : HOD) {x : Ordinal } (xa : odef A x) : Set n where
+record Prev< (A : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
    field
-      prev : Ordinal
-      aprev : odef A prev
-      direct : & (IndirectSet< A aprev xa ) ≡ o∅ 
+      y : Ordinal
+      ay : odef A y
+      x=fy :  x ≡ f y 
 
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
@@ -469,7 +466,9 @@
       chain⊆A : chain ⊆ A
       f-total : IsTotalOrderSet chain 
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
-      is-max :  {a b : Ordinal } → odef chain a → odef A b → a o< z → ( ? ∨ (sup (& chain)  (subst ? ? f-total) ≡ b )) → * a < * b  → odef chain b
+      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 ))
+          → * a < * b  → odef chain b
 
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
@@ -507,38 +506,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 {!!} (& 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) {!!} (& 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 {!!} (& 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) {!!}  (& 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 {!!} y )
+         →  ZChain A sa f mf {!!} 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 {!!} (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 {!!} 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 {!!} (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 {!!} 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
@@ -562,7 +561,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 {!!} (& A)
          zorn03 f mf = TransFinite (ind f mf)  (& A) 
 
 -- usage (see filter.agda )