# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650601257 -32400
# Node ID 5ca59261a4aaae406a39f8eba42dae42d9dd742c
# Parent  06a655ca04b8bc70cc582a7d309c07aa533f4f9b
...

diff -r 06a655ca04b8 -r 5ca59261a4aa src/zorn.agda
--- a/src/zorn.agda	Fri Apr 22 12:52:25 2022 +0900
+++ b/src/zorn.agda	Fri Apr 22 13:20:57 2022 +0900
@@ -466,9 +466,9 @@
      sa : A ∋ * ( & s  )
      sa =  subst (λ k → odef A (& k) ) (sym *iso) ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))  )
      HasMaximal : HOD
-     HasMaximal = record { od = record { def = λ x → (m : Ordinal) →  odef A m → odef A x ∧ (¬ (* x < * m))} ; odmax = & A ; <odmax = {!!} } where
-         z07 :  {y : Ordinal} → ((m : Ordinal) → odef A y ∧ odef A m ∧ (¬ (* y < * m))) → y o< & A
-         z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 (p (& s)) )))
+     HasMaximal = record { od = record { def = λ x → odef A x ∧ ( (m : Ordinal) →  odef A m → ¬ (* x < * m)) }  ; odmax = & A ; <odmax = z07 } where
+         z07 :   {y : Ordinal} → odef A y ∧ ((m : Ordinal) → odef A m → ¬ (* y < * m)) → y o< & A
+         z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
      cf : ¬ Maximal A → Ordinal → Ordinal
      cf  = {!!}
      cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) →  odef A x → ( * x < * (cf nmx x) ) ∧  odef A (cf nmx x )
@@ -514,21 +514,21 @@
      ... | t = {!!}
 
      zorn00 : Maximal A 
-     zorn00 with is-o∅ ( & HasMaximal )
+     zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
      ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where
          -- yes we have the maximal
          zorn03 :  odef HasMaximal ( & ( ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
          zorn03 =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))
          zorn01 :  A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq))
-         zorn01 =  proj1 (zorn03 (& s) (subst (λ k → odef A (& k) ) *iso sa) ) 
+         zorn01  = proj1  zorn03  
          zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
-         zorn02 {x} ax m<x = proj2 (zorn03 (& x) ax) (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
+         zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
      ... | yes ¬Maximal = ⊥-elim ( z04 zorn03  zorn04 ) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          zorn04 : ¬ Maximal A 
          zorn04 mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
-              zc5 : (y : Ordinal) →  odef A y → odef A (& (Maximal.maximal mx )) ∧ (¬ (* (& (Maximal.maximal mx ))  < * y ))
-              zc5 y ay = ⟪  Maximal.A∋maximal mx , (λ mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) )  ⟫
+              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 : ZChain A sa (& A)
          zorn03 with TransFinite ind  (& A)
          ... | case1 zc = zc