# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651338912 -32400
# Node ID a64dad8d2e9359f865567896e93cff0c14922f73
# Parent  111d3b6411770b4cf46161f1af412551063c48f5
fix sp1

diff -r 111d3b641177 -r a64dad8d2e93 src/zorn.agda
--- a/src/zorn.agda	Sun May 01 01:17:54 2022 +0900
+++ b/src/zorn.agda	Sun May 01 02:15:12 2022 +0900
@@ -233,7 +233,7 @@
 SupCond A B _ _ = SUP A B  
 
 record ZChain ( A : HOD )  {x : Ordinal} (ax : odef A x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f )
-                 (sup : (C : Ordinal ) → (* C ⊆ A) → IsTotalOrderSet (* C) → Ordinal) ( z : Ordinal ) : Set (Level.suc n) where
+                 (sup : (C : HOD ) → ( C ⊆ A) → IsTotalOrderSet C → Ordinal) ( z : Ordinal ) : Set (Level.suc n) where
    field
       chain : HOD
       chain⊆A : chain ⊆ A
@@ -243,8 +243,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) (subst (λ k → k  ⊆ A) (sym *iso) chain⊆A)  (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b )
+          → Prev< A chain ba f ∨  ((sup  chain  chain⊆A  f-total) ≡ b )
           → * a < * b  → odef chain b
 
 Zorn-lemma : { A : HOD } 
@@ -252,8 +251,8 @@
     → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
     → Maximal A 
 Zorn-lemma {A}  0<A supP = zorn00 where
-     supO : (C : Ordinal ) → (* C) ⊆ A → IsTotalOrderSet (* C) → Ordinal
-     supO C C⊆A TC = & ( SUP.sup ( supP (* C)  C⊆A TC ))
+     supO : (C : HOD ) → C ⊆ A → IsTotalOrderSet C → Ordinal
+     supO C C⊆A TC = & ( SUP.sup ( supP  C  C⊆A TC ))
      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
@@ -302,9 +301,8 @@
      A∋zsup :  (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& 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 ) )
-     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) f mf supO (& A) ) → SUP A (* (& (ZChain.chain zc)))
-     sp0 f mf zc = supP (* (& (ZChain.chain zc))) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc))
-               (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc) )
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) f mf supO (& A) ) → SUP A (ZChain.chain zc)
+     sp0 f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain.f-total zc) 
      zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
      zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
 
@@ -317,8 +315,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) (subst (λ k → k  ⊆ A) (sym *iso) (ZChain.chain⊆A zc))  (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc)) ≡ b )
+              →  Prev< 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
@@ -328,7 +325,7 @@
            ... | 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 refl ) z13 where
                z13 :  * (& s) < * (& (SUP.sup sp1))
-               z13 with SUP.x<sup sp1 (subst (λ k → odef k (& s)) (sym *iso) ( ZChain.chain∋x zc ))
+               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
            z14 :  f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
@@ -341,7 +338,7 @@
            ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
            ... | tri> ¬a ¬b c = ⊥-elim z17 where
                z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) <  SUP.sup sp1)
-               z15  = SUP.x<sup sp1 (subst₂ (λ j k → odef j k ) (sym *iso) (sym &iso)  (ZChain.f-next zc z12 ))
+               z15  = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
                z17 : ⊥
                z17 with z15
                ... | case1 eq = ¬b eq
@@ -380,9 +377,7 @@
                      ; 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)))
-                       (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0))
-                       (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)))) ≡ b) →
+                    Prev< 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 ) )
@@ -391,9 +386,7 @@
           ... | 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))
-                             (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0))
-                             (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ b) →
+                            Prev< 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
@@ -470,28 +463,23 @@
                 ... | 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))
-                       (subst (λ k → k ⊆ A) (sym *iso) (record { incl = A∋schain }))
-                       (subst IsTotalOrderSet (sym *iso) scmp))) ≡ b)
+                    Prev< 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 (case1 Prev) a<b = {!!}
-                s-ismax {a} {b} (case2 sa) b<x ba (case1 Prev) a<b = {!!}
-                s-ismax {a} {b} (case1 za) b<x ba (case2 Sup) a<b = {!!}
-                s-ismax {a} {b} (case2 sa) b<x ba (case2 Sup) a<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 = ?
           ... | 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)))
-                               (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0))
-                               (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0))))
-                             ≡ b) →
+                            Prev< 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 ) } )
-                ... | case2 b=sup = ⊥-elim ( ¬x=sup {!!}) 
+                ... | 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
             field