# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651350936 -32400
# Node ID 4d8a54e2861e69a0893cab84ed973f3e1fe7553a
# Parent  a64dad8d2e9359f865567896e93cff0c14922f73
...

diff -r a64dad8d2e93 -r 4d8a54e2861e src/zorn.agda
--- a/src/zorn.agda	Sun May 01 02:15:12 2022 +0900
+++ b/src/zorn.agda	Sun May 01 05:35:36 2022 +0900
@@ -205,7 +205,9 @@
 IsTotalOrderSet : ( A : HOD ) → Set (Level.suc n)
 IsTotalOrderSet A = {a b : HOD} → odef A (& a) → odef A (& b)  → Tri (a < b) (a ≡ b) (b < a )
 
-      
+⊆-IsTotalOrderSet : { A B : HOD } →  B ⊆ A  → IsTotalOrderSet A → IsTotalOrderSet B
+⊆-IsTotalOrderSet = {!!}
+
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
       maximal : HOD
@@ -217,12 +219,23 @@
 -- tree structure
 --
 
-record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
+record HasPrev (A B : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
    field
       y : Ordinal
       ay : odef B y
       x=fy :  x ≡ f y 
 
+_⊆'_ : ( A B : HOD ) → Set n
+_⊆'_ A B = (x : Ordinal ) → odef A x → odef B x
+
+record IsSup (A : HOD) (T : IsTotalOrderSet A) {x : Ordinal }
+    (xa : odef A x)  (sup : (C : HOD ) → ( C ⊆ A) → IsTotalOrderSet C → Ordinal) ( f : Ordinal → Ordinal )  : Set n where
+   field
+      chain : Ordinal
+      chain⊆A : (* chain) ⊆' A
+      -- ¬prev : ¬ HasPrev A (* chain) xa f
+      x=sup :  x ≡ sup  (* chain)  record { incl = λ {x} → chain⊆A (& x) } ( ⊆-IsTotalOrderSet {A} {* chain} record { incl = λ {x} → chain⊆A (& x) } T ) 
+
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
       sup : HOD
@@ -243,7 +256,7 @@
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ba : odef A b) 
-          → Prev< A chain ba f ∨  ((sup  chain  chain⊆A  f-total) ≡ b )
+          → HasPrev A chain ba f ∨  ((sup  chain  chain⊆A  f-total) ≡ b )
           → * a < * b  → odef chain b
 
 Zorn-lemma : { A : HOD } 
@@ -315,7 +328,7 @@
            chain = ZChain.chain zc
            sp1 = sp0 f mf zc
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) 
-              →  Prev< A chain ab f ∨  (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
+              →  HasPrev A chain ab f ∨  (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
               → * a < * b  → odef chain b
            z10 = ZChain.is-max zc
            z11 : & (SUP.sup sp1) o< & A
@@ -377,20 +390,20 @@
                      ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
                      ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 }  where -- no extention
                 zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ba : odef A b) →
-                    Prev< A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0))) ≡ b) →
+                    HasPrev A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0))) ≡ b) →
                             * a < * b → odef (ZChain.chain zc0) b
                 zc11 {a} {b} za b<ox ba P a<b with osuc-≡< b<ox
                 ... | case1 eq = ⊥-elim ( noapx (subst (λ k → odef A k) (trans eq (sym &iso)) ba ) )
                 ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt )  ba P a<b
-          ... | yes apx with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) apx f )   -- we have to check adding x preserve is-max ZChain A ay f mf supO x
+          ... | yes apx with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) apx f )   -- we have to check adding x preserve is-max ZChain A ay f mf supO x
           ... | case1 pr = zc9 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
                 chain = ZChain.chain zc0
                 zc17 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ba : odef A b) →
-                            Prev< A (ZChain.chain zc0) ba f ∨ (supO (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0) ≡ b) →
+                            HasPrev A (ZChain.chain zc0) ba f ∨ (supO (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0) ≡ b) →
                             * a < * b → odef (ZChain.chain zc0) b
                 zc17 {a} {b} za b<ox ba P a<b with osuc-≡< b<ox
                 ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt) ba P a<b
-                ... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (Prev<.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (Prev<.ay pr))
+                ... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
                 zc9 :  ZChain A ay f mf supO x
                 zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0
                      ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 }  -- no extention
@@ -463,22 +476,32 @@
                 ... | case2 sp<a | case2 b<sp = <-irr (case2 (ptrans b<sp (subst (λ k → k < * a) *iso sp<a ))) (proj1 p )
                 simm {a} {b} (case2 sa) (case2 sb) p = fcn-imm {A} (& sp) {a} {b} f mf sa sb p
                 s-ismax : {a b : Ordinal} → odef schain a → b o< osuc x → (ba : odef A b) →
-                    Prev< A schain ba f ∨ (& (SUP.sup (supP schain record { incl = A∋schain } scmp)) ≡ b)
+                    HasPrev A schain ba f ∨ (& (SUP.sup (supP schain record { incl = A∋schain } scmp)) ≡ b)
                      → * a < * b → odef schain b
-                s-ismax {a} {b} (case1 za) b<x ba p a<b with osuc-≡< b<x
-                ... | case2 b<x = case1 (ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  b<x ) ba ? a<b )
-                ... | case1 b=x = {!!}
-                s-ismax {a} {b} (case2 sa) b<x ba p a<b = ?
+                s-ismax {a} {b} (case1 za) b<x ba (case1 p) a<b with osuc-≡< b<x
+                ... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) ))
+                ... | case2 b<x = z21 p where
+                     z21 : HasPrev A schain ba f → odef schain b
+                     z21 record { y = y ; ay = (case1 zy) ; x=fy = x=fy } = 
+                           case1 (ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  b<x ) ba (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
+                     z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = subst (λ k → odef schain k) (sym x=fy) (case2 (fsuc y sy) )
+                s-ismax {a} {b} (case1 za) b<x ba (case2 p) a<b with osuc-≡< b<x
+                ... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) (sym (trans b=x x=sup )) (init (SUP.A∋maximal sup0) ))
+                ... | case2 b<x = z22 p  where
+                     z22 : & (SUP.sup (supP schain record { incl = A∋schain } scmp)) ≡ b → odef schain b
+                     z22 p = {!!}
+                -- case1 (ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  b<x ) ba {!!} a<b )
+                s-ismax {a} {b} (case2 sa) b<x ba p a<b = {!!}
           ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
                    record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
                      ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 }  where -- no extention
                 z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ba : odef A b) →
-                            Prev< A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0))) ≡ b) →
+                            HasPrev A (ZChain.chain zc0) ba f ∨ (& (SUP.sup (supP (ZChain.chain zc0) (ZChain.chain⊆A zc0) (ZChain.f-total zc0))) ≡ b) →
                             * a < * b → odef (ZChain.chain zc0) b
                 z18 {a} {b} za b<x ba p a<b with osuc-≡< b<x
                 ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  lt ) ba p a<b 
                 ... | case1 b=x with p
-                ... | case1 pr = ⊥-elim ( ¬fy<x record {y = Prev<.y pr ; ay = Prev<.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (Prev<.x=fy pr ) } )
+                ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup (sym (trans  b=sup  b=x )) )
      ... | no ¬ox =  {!!}  where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x