# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656250037 -32400
# Node ID a7e538a7c87f3aff6aafc632373d493a9e334f5e
# Parent  b46a0a2b32e5ea55db30e1263cc510f3b44f0216
...

diff -r b46a0a2b32e5 -r a7e538a7c87f src/OrdUtil.agda
--- a/src/OrdUtil.agda	Sun Jun 26 20:11:28 2022 +0900
+++ b/src/OrdUtil.agda	Sun Jun 26 22:27:17 2022 +0900
@@ -41,9 +41,6 @@
 osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
 
 osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox  
-----   y < osuc y < x < osuc x
-----   y < osuc y = x < osuc x
-----   y < osuc y > x < osuc x   -> y = x ∨ x < y → ⊥
 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc
@@ -57,6 +54,11 @@
 osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox )
 osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox )
 
+ordtrans≤-< :  {ox oy oz : Ordinal } → ox o< osuc oy  → oy o< oz  → ox o< oz
+ordtrans≤-< {ox} {oy} {oz} x≤y y<z with  osuc-≡< x≤y
+... | case1 x=y = subst ( λ k → k o< oz ) (sym x=y) y<z
+... | case2 x<y = ordtrans x<y y<z
+
 open _∧_
 
 osuc2 :  ( x y : Ordinal  ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
diff -r b46a0a2b32e5 -r a7e538a7c87f src/zorn.agda
--- a/src/zorn.agda	Sun Jun 26 20:11:28 2022 +0900
+++ b/src/zorn.agda	Sun Jun 26 22:27:17 2022 +0900
@@ -594,17 +594,16 @@
           →  ∀ (x : Ordinal)  →   ind  x (λ y _ → TransFinite ind  y )  ≡ TransFinite ind  x
 
      record ZChain1 ( f : Ordinal → Ordinal )  ( y z : Ordinal ) : Set (Level.suc n) where
+      inductive
       field
          zc : { x : Ordinal } → x o< z → ZChain A y f x
-         chain-mono : {x y : Ordinal} → (x≤y : x o≤ y) → (y<z : y o< z ) →  ZChain.chain (zc ?)  ⊆' ZChain.chain (zc y<z ) 
+         chain-mono : {x y : Ordinal} → (x≤y : x o≤ y) → (y<z : y o< z ) →  ZChain.chain (zc {x} (ordtrans≤-< x≤y y<z))  ⊆' ZChain.chain (zc y<z ) 
          f-total : {x : Ordinal} → (x<z : x o< z ) → IsTotalOrderSet (ZChain.chain (zc x<z ) )
 
      SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y)
          → (z : Ordinal) → ZChain1 f y z
-     SZ1 f mf {y} ay z = TransFinite {λ w → {!!} w} {!!} z where
-         indp :  (x : Ordinal) →
-            ((y₁ : Ordinal) → y₁ o< x → ZChain1 f y y₁) →
-            ZChain1 f y x
+     SZ1 f mf {y} ay z = TransFinite {λ w → ZChain1 f y w } indp z where
+         indp :  (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZChain1 f y y₁) → ZChain1 f y x
          indp x prev with Oprev-p x
          ... | yes op  = sz02 where
              sz02 : ZChain1 f y ?
@@ -616,13 +615,6 @@
          ... | tri≈ ¬a b ¬c = {!!}
          ... | tri> ¬a ¬b y<x = {!!}
 
-     T⊆ : ( ind : (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → HOD ) → HOD ) 
-          → ( (x : Ordinal)  → ( prev : (y : Ordinal  ) → y o< x → HOD ) → {y : Ordinal } → (y<x : y o< x)  → prev y y<x ⊆' ind x prev  ) 
-          →  {x z : Ordinal} → z o≤ x  → TransFinite ind z ⊆' TransFinite ind x 
-     T⊆ = ? where -- {ψ} ind p⊆ {x} {z} z≤x = ? where -- TransFinite0 (λ x prev → indt x prev  ) x {z} z≤x where
-         -- indt : (x : Ordinal) → ( (y : Ordinal) → y o< x →  {z : Ordinal} → z o≤ y  → ψ z ⊆' ψ y ) →  {z : Ordinal} → z o≤ x  → ψ z ⊆' ψ x 
-         -- indt x prev {z} z≤x {i} zi = prev {!!} {!!} {z} z≤x zi
-
      zorn00 : Maximal A 
      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
@@ -633,18 +625,18 @@
          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 )
-     ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04 zc1 ) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx (ZChain1.zc zc0 <-osuc ) (ZChain1.f-total zc0 <-osuc) ) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A 
          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) ) ⟫
-         zorn04 : ZChain A (& s) (cf nmx) (& A)
-         zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
+         -- zorn04 : ZChain A (& s) (cf nmx) (& A)
+         -- zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
          zc0 : ZChain1  (cf nmx) (& s) (osuc (& A))
          zc0 = SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) (osuc (& A))
-         zc1 :  IsTotalOrderSet ( ZChain.chain (ZChain1.zc zc0 <-osuc ) )
-         zc1 =  ZChain1.f-total zc0 <-osuc 
+         -- zc1 :  IsTotalOrderSet ( ZChain.chain (ZChain1.zc zc0 <-osuc ) )
+         -- zc1 =  ZChain1.f-total zc0 <-osuc 
 
 -- usage (see filter.agda )
 --