# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651419883 -32400
# Node ID 33b1ade17f83db7ab803c895e2d9ff9e69883ae6
# Parent  666377324edde4a6e13334bf244adc1407ee8b0d
...

diff -r 666377324edd -r 33b1ade17f83 src/zorn.agda
--- a/src/zorn.agda	Sun May 01 09:36:44 2022 +0900
+++ b/src/zorn.agda	Mon May 02 00:44:43 2022 +0900
@@ -222,8 +222,8 @@
       ay : odef B y
       x=fy :  x ≡ f y 
 
-record IsSup (A B : HOD) (T : IsTotalOrderSet B) {x : Ordinal } ( B⊆A :  B ⊆' A )
-    (xa : odef A x)  (sup : (C : HOD ) → ( C ⊆' A) → IsTotalOrderSet C → Ordinal) ( f : Ordinal → Ordinal )  : Set n where
+record IsSup (A B : HOD) (T : IsTotalOrderSet B) ( B⊆A :  B ⊆' 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⊆B : (* chain) ⊆' B
@@ -267,6 +267,10 @@
 Zorn-lemma {A}  0<A supP = zorn00 where
      supO : (C : HOD ) → C ⊆' A → IsTotalOrderSet C → Ordinal
      supO C C⊆A TC = & ( SUP.sup ( supP  C  C⊆A TC ))
+     postulate
+        --- irrelevance of ⊆' and compare
+        sup== : {C C1 : HOD } → C ≡ C1 → {c  : C ⊆' A } {c1 : C1 ⊆' A } → {t  : IsTotalOrderSet C } {t1 : IsTotalOrderSet C1 }
+         → SUP.sup ( supP  C c t )  ≡  SUP.sup ( supP  C1 c1 t1 )
      z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
      z01 {a} {b} A∋a A∋b = <-irr
      z07 :   {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -329,7 +333,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 ) 
-              →  HasPrev A chain ab f ∨  IsSup A chain (ZChain.f-total zc) (ZChain.chain⊆A zc) ab supO f -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
+              →  HasPrev A chain ab f ∨  IsSup A chain (ZChain.f-total zc) (ZChain.chain⊆A zc) {b} ab supO 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
@@ -337,13 +341,12 @@
            z12 : odef chain (& (SUP.sup sp1))
            z12 with o≡? (& s) (& (SUP.sup sp1))
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋x zc )
-           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1)  (case2 z19 ) z13 where
+           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1)
+                (case2 record { chain = & chain ; chain⊆B = λ z → subst (λ  k → odef k _ ) *iso z ;  x=sup = cong (&) (sup== (sym *iso)) }  ) z13 where
                z13 :  * (& s) < * (& (SUP.sup sp1))
                z13 with SUP.x<sup sp1 ( ZChain.chain∋x zc )
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
                ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
-               z19 : IsSup A chain (ZChain.f-total zc) (ZChain.chain⊆A zc) (SUP.A∋maximal sp1) supO f
-               z19 = {!!}
            z14 :  f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
            z14 with ZChain.f-total zc  (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
@@ -386,6 +389,9 @@
           px = Oprev.oprev op
           zc0 : ZChain A ay f mf supO (Oprev.oprev op)
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay
+          zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px
+          zc0-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
+
           zc4 : ZChain A ay f mf supO x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax =  -- ¬ A ∋ p, just skip
@@ -397,7 +403,7 @@
                             * a < * b → odef (ZChain.chain zc0) b
                 zc11 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
-                ... | case2 lt = ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt )  ab P a<b
+                ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt)  ab P a<b
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax 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
@@ -405,26 +411,29 @@
                             HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0) (ZChain.f-total zc0) (ZChain.chain⊆A zc0) ab supO f →
                             * a < * b → odef (ZChain.chain zc0) b
                 zc17 {a} {b} za b<ox ab 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) ab P a<b
+                ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b
                 ... | 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
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) (ZChain.f-total zc0) (ZChain.chain⊆A zc0) ax supO f)
           ... | case1 x=sup = -- previous ordinal is a sup of a smaller ZChain
-                 record { chain = schain ; chain⊆A = {!!}  ; f-total = scmp ; f-next = scnext 
+                 record { chain = schain ; chain⊆A = s⊆A  ; f-total = scmp ; f-next = scnext 
                      ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = {!!} } where -- x is sup
                 sup0 = supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) 
                 sp = SUP.sup sup0 
                 chain = ZChain.chain zc0
                 sc<A : {y : Ordinal} → odef chain y ∨ FClosure A f (& sp) y → y o< & A
-                sc<A {y} (case1 zx) = {!!} -- subst (λ k → k o< (& A)) &iso ( c<→o< ( incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k) (sym &iso) zx )))
+                sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A zc0 (subst (λ k → odef chain k) (sym &iso) zx )))
                 sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) )
                 schain : HOD
                 schain = record { od = record { def = λ x → odef chain x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
                 A∋schain : {x : HOD } → schain ∋ x → A ∋ x
-                A∋schain (case1 zx ) = {!!} -- subst (λ k → odef A k ) &iso (incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k) (sym &iso) zx ))
+                A∋schain (case1 zx ) = ZChain.chain⊆A zc0 zx 
                 A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx 
+                s⊆A : schain ⊆' A
+                s⊆A {x} (case1 zx) = ZChain.chain⊆A zc0 zx
+                s⊆A {x} (case2 fx) = A∋fc (& sp) f mf fx 
                 cmp  : {a b : HOD} (za : odef chain (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a )
                 cmp {a} {b} za fb  with SUP.x<sup sup0 za | s≤fc (& sp) f mf fb  
                 ... | case1 sp=a | case1 sp=b = tri≈ (λ lt → <-irr (case1 (sym eq)) lt ) eq (λ lt → <-irr (case1 eq) lt ) where
@@ -458,7 +467,7 @@
                 ... | case2 sp<x | case1 y=sp = case2 (subst (λ k → k < * x ) (trans *iso (sym y=sp )) sp<x )
                 ... | case2 sp<x | case2 y<sp = case2 (ptrans y<sp (subst (λ k → k < * x ) *iso sp<x) )
                 A∋za : {a : Ordinal } → odef chain a → odef A a
-                A∋za za = {!!} -- (subst (λ k → odef A k ) &iso (incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k ) (sym &iso) za) ) )
+                A∋za za = ZChain.chain⊆A zc0 za 
                 za<sup :  {a : Ordinal } → odef chain a → ( * a ≡ sp ) ∨  ( * a < sp )
                 za<sup za =  SUP.x<sup sup0 (subst (λ k → odef chain k ) (sym &iso) za )
                 simm : {a b : Ordinal}  → odef schain a → odef schain b → ¬ (* a < * b) ∧ (* b < * (f a))
@@ -479,21 +488,21 @@
                 ... | 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 → (ab : odef A b) →
-                    HasPrev A schain ab f ∨ IsSup A (ZChain.chain zc0) (ZChain.f-total zc0) (ZChain.chain⊆A zc0) ab supO f
-                     → * a < * b → odef schain b
+                   HasPrev A schain ab f ∨ IsSup A schain scmp s⊆A ab (λ C C⊆A TC → & (SUP.sup (supP C C⊆A TC))) f 
+                    → * a < * b → odef schain b
                 s-ismax {a} {b} (case1 za) b<x ab (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 ab 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 ) ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b )
+                           case1 (ZChain.is-max zc0 za (zc0-b<x b b<x) ab (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 ab (case2 p) a<b with osuc-≡< b<x
                 ... | case1 b=x = case2 (subst (λ k → FClosure A f (& sp) k ) {!!} (init (SUP.A∋maximal sup0) ))
-                ... | case2 b<x = z22 p  where
+                ... | case2 b<x = {!!} where
                      z22 : IsSup A (ZChain.chain zc0) (ZChain.f-total zc0) (ZChain.chain⊆A zc0) ab supO f → odef schain b
                      z22 p = {!!}
-                -- case1 (ZChain.is-max zc0 za (subst (λ k → b o< k ) (sym ( Oprev.oprev=x op))  b<x ) ab {!!} a<b )
+                -- case1 (ZChain.is-max zc0 za (zc0-b<x b lt) ab {!!} a<b )
                 s-ismax {a} {b} (case2 sa) b<x ab 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
@@ -502,7 +511,7 @@
                             HasPrev A (ZChain.chain zc0) ab f ∨ IsSup A (ZChain.chain zc0) (ZChain.f-total zc0) (ZChain.chain⊆A zc0) ab supO f →
                             * a < * b → odef (ZChain.chain zc0) b
                 z18 {a} {b} za b<x ab 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 ) ab p a<b 
+                ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab p a<b 
                 ... | case1 b=x with p
                 ... | 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 {!!} )