# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1660194477 -32400
# Node ID 2d84411a636e0a6a247b44d5c3fee046d954085c
# Parent  7c6612b753b9564944b1c1b2d42692bc3e949f90
...

diff -r 7c6612b753b9 -r 2d84411a636e src/zorn.agda
--- a/src/zorn.agda	Tue Aug 09 12:52:57 2022 +0900
+++ b/src/zorn.agda	Thu Aug 11 14:07:57 2022 +0900
@@ -238,7 +238,7 @@
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
       sup : HOD
-      A∋maximal : A ∋ sup
+      as : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
 --
@@ -328,7 +328,7 @@
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
       maximal : HOD
-      A∋maximal : A ∋ maximal
+      as : A ∋ maximal
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
 -- data UChain is total
@@ -432,7 +432,7 @@
      Gtx : { x : HOD} → A ∋ x → HOD
      Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = z07 } 
      z08  : ¬ Maximal A →  HasMaximal =h= od∅
-     z08 nmx  = record { eq→  = λ {x} lt → ⊥-elim ( nmx record {maximal = * x ; A∋maximal = subst (λ k → odef A k) (sym &iso) (proj1 lt)
+     z08 nmx  = record { eq→  = λ {x} lt → ⊥-elim ( nmx record {maximal = * x ; as = subst (λ k → odef A k) (sym &iso) (proj1 lt)
          ; ¬maximal<x = λ {y} ay → subst (λ k → ¬ (* x < k)) *iso (proj2 lt (& y) ay) } ) ; eq← =  λ {y} lt → ⊥-elim ( ¬x<0 lt )}
      x-is-maximal : ¬ Maximal A → {x : Ordinal} → (ax : odef A x) → & (Gtx (subst (λ k → odef A k ) (sym &iso) ax)) ≡ o∅ → (m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m))
      x-is-maximal nmx {x} ax nogt m am  = ⟪ subst (λ k → odef A k) &iso (subst (λ k → odef A k ) (sym &iso) ax) ,  ¬x<m  ⟫ where
@@ -559,17 +559,17 @@
               → * a < * b  → odef chain b
            z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
            z11 : & (SUP.sup sp1) o< & A
-           z11 = c<→o< ( SUP.A∋maximal sp1)
+           z11 = c<→o< ( SUP.as sp1)
            z12 : odef chain (& (SUP.sup sp1))
            z12 with o≡? (& s) (& (SUP.sup sp1))
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z11 (SUP.A∋maximal sp1)
+           ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z11 (SUP.as sp1)
                 (case2 z19 ) z13 where
                z13 :  * (& s) < * (& (SUP.sup sp1))
                z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
                ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
-               z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.A∋maximal sp1)
+               z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1)
                z19 = record {   x<sup = z20 }  where
                    z20 :  {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1))
                    z20 {y} zy with SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) zy)
@@ -580,7 +580,7 @@
            z14 with total (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
-               z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
+               z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 ))
                ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
                ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
            ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
@@ -600,10 +600,10 @@
      z04 :  (nmx : ¬ Maximal A ) 
            → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) 
            → IsTotalOrderSet (ZChain.chain zc) → ⊥
-     z04 nmx zc total = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1 ))))
-                                               (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) )
+     z04 nmx zc total = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as  sp1 ))))
+                                               (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) )
            (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc total ))) -- x ≡ f x ̄
-           (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1 ))) where          -- x < f x
+           (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where          -- x < f x
           sp1 : SUP A (ZChain.chain zc)
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total
           c = & (SUP.sup sp1)
@@ -622,48 +622,8 @@
        →  SUP A (uchain f mf ay)
      ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay) 
 
-     initChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
-     initChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy  ; sup = {!!} ; supf-is-sup = {!!} 
-      ; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ? ; csupf = {!!} } where
-          spi =  & (SUP.sup (ysup f mf ay))
-          isupf : Ordinal → Ordinal
-          isupf z = spi
-          sp = ysup f mf ay
-          asi = SUP.A∋maximal sp
-          cy : odef (UnionCF A f mf ay isupf o∅) y
-          cy = ⟪ ay , ch-init (init ay refl)  ⟫
-          y<sup : * y ≤ SUP.sup (ysup f mf ay)
-          y<sup = SUP.x<sup  (ysup f mf ay) (subst (λ k → FClosure A f y k ) (sym &iso) (init ay refl))
-          sup : {x : Ordinal} → x o< o∅ → SUP A (UnionCF A f mf ay isupf x)
-          sup {x} lt = ⊥-elim ( ¬x<0 lt )
-          isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
-          isy {z} ⟪ az , uz ⟫ with uz 
-          ... | ch-init fc = s≤fc y f mf fc 
-          ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup)  (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc )
-          inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
-          inext {a} ua with (proj2 ua)
-          ... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua))  , ch-init (fsuc _ fc )  ⟫
-          ... | ch-is-sup u u≤x is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) ,  ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
-          itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 
-          itotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
-               uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb)  
-          csupf : {z : Ordinal} → z o≤ o∅ → odef (UnionCF A f mf ay isupf z ) (isupf z)
-          csupf {z} z≤0 = ⟪ asi , ch-is-sup o∅ o∅≤z uz02 (init asi refl) ⟫ where
-               uz03 : {z : Ordinal } →  FClosure A f y z → (z ≡ isupf spi) ∨ (z << isupf spi)
-               uz03 {z} fc with SUP.x<sup sp (subst (λ k → FClosure A f y k ) (sym &iso) fc )
-               ... | case1 eq = case1 ( begin
-                  z ≡⟨ sym &iso  ⟩
-                  & (* z) ≡⟨ cong (&) eq  ⟩
-                  spi  ∎ ) where open ≡-Reasoning
-               ... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt )
-               uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
-               uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi )
-               uz02 :  ChainP A f mf ay isupf o∅
-               uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → {!!} ; supu=u = {!!} }
-
      SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B
-     SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; A∋maximal = SUP.A∋maximal sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt)    }
+     SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt)    }
 
      --
      -- create all ZChains under o< x
@@ -732,15 +692,33 @@
           -- if previous chain satisfies maximality, we caan reuse it
           --
           --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 
-          no-extension : ¬  sp1 ≡ x → ZChain A f mf ay x
+          no-extension : ¬  sp1 ≡ supf1 x → ZChain A f mf ay x
           no-extension ¬sp=x = record { supf = supf1 ;  sup = sup
-               ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = {!!} ; csupf = {!!} 
-              ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = {!!} }  where
+               ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = {!!} ; csupf = csupf
+              ;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
                  UnionCF⊆ : {z : Ordinal } → z o≤ x →  UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf0 x 
                  UnionCF⊆ {z} z≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-                 UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫
-                 UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with
-                      UnionCF⊆ {z} z≤x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ 
+                 UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤z record { fcy<sup = fc<s ; order = o1 ; supu=u = sp=u }  (init  au1 refl) ⟫ = zc30 where
+                     zc30 : odef (UnionCF A f mf ay supf0 x) (supf1 u1 )
+                     zc30 with trio< u1 px
+                     ... | tri< a ¬b ¬c = ⟪ au , ch-is-sup u1 (OrdTrans u1≤z z≤x)  ? (init au1 refl) ⟫ 
+                     ... | tri≈ ¬a b ¬c = ⟪ au , ch-is-sup u1 (OrdTrans u1≤z z≤x)  ? (init au1 refl) ⟫ 
+                     ... | tri> ¬a ¬b px<u1 = ? where
+                          zc31 : u1 ≡ x
+                          zc31 with trio< u1 x
+                          ... | tri< a ¬b ¬c = ⊥-elim (¬p<x<op ⟪ px<u1 , subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) a ⟫ )
+                          ... | tri≈ ¬a b ¬c = b
+                          ... | tri> ¬a ¬b c =  ⊥-elim (¬p<x<op ⟪ c , ordtrans≤-< u1≤z z≤x  ⟫ )
+                 UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤z u1-is-sup (fsuc xp fcu1) ⟫ with
+                      UnionCF⊆ {z} z≤x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤z u1-is-sup fcu1 ⟫ 
+                 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
+                 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
+                 UnionCF⊆R : {z : Ordinal } → z o≤ x →  UnionCF A f mf ay supf0 z ⊆' UnionCF A f mf ay supf1 x 
+                 UnionCF⊆R {z} z≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
+                 UnionCF⊆R {z} z≤x ⟪ au , ch-is-sup u1 u1≤z u1-is-sup (init  au1 refl) ⟫   
+                     = ⟪ au , ch-is-sup u1 (OrdTrans u1≤z z≤x) ? (init ? ?) ⟫
+                 UnionCF⊆R {z} z≤x ⟪ au , ch-is-sup u1 u1≤z u1-is-sup (fsuc xp fcu1) ⟫ with
+                      UnionCF⊆R {z} z≤x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤z u1-is-sup fcu1 ⟫ 
                  ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
                  ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
                  sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
@@ -755,7 +733,21 @@
                      zc11 = ZChain.sup=u zc ab ? ?
                  ... | tri≈ ¬a b ¬c = ? 
                  ... | tri> ¬a ¬b c = ?
-
+                 ptotal1 : IsTotalOrderSet pchain1
+                 ptotal1 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
+                     uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
+                     uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) 
+                 csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
+                 csupf {b} b≤x with trio< b px | inspect supf1 b
+                 ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫
+                 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫
+                 ... | tri> ¬a ¬b px<b | record { eq = eq1 } = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ supf1 k ) (sym zc30) (sym eq1) )) where  
+                     --   px< b ≤ x
+                     -- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1
+                     zc30 : x ≡ b
+                     zc30 with osuc-≡< b≤x
+                     ... | case1 eq = sym (eq)
+                     ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
@@ -764,10 +756,10 @@
           ... | case1 pr = no-extension {!!} -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} 
+                record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = csupf ; sup=u = {!!} 
                    ;  initial = {!!} ; chain∋init  = {!!} ; sup = {!!} ; supf-is-sup = {!!}   }  where
              supx : SUP A (UnionCF A f mf ay supf0 x)
-             supx = record { sup = * x ; A∋maximal = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} }
+             supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} }
              spx = & (SUP.sup supx )
              x=spx : x ≡ spx
              x=spx = {!!}
@@ -776,6 +768,16 @@
              ... | tri< a ¬b ¬c = ZChain.supf zc z
              ... | tri≈ ¬a b ¬c = x
              ... | tri> ¬a ¬b c = x
+             csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b)
+             csupf {b} b≤x with trio< b px | inspect psupf1 b
+             ... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫
+             ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫
+             ... | tri> ¬a ¬b c | record { eq = eq1 } = ? where -- b ≡ x, supf x ≡ sp
+                  zc30 : x ≡ b
+                  zc30 with trio< x b
+                  ... | tri< a ¬b ¬c = ?
+                  ... | tri≈ ¬a b ¬c = b
+                  ... | tri> ¬a ¬b c = ?
 
           ... | case2 ¬x=sup =  no-extension {!!} -- px is not f y' nor sup of former ZChain from y -- no extention
 
@@ -879,14 +881,14 @@
                  ... | tri≈ ¬a b ¬c = {!!}
                  ... | tri> ¬a ¬b c = {!!}
                  csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z)
-                 csupf {z} z<x with trio< z x
+                 csupf {z} z≤x with trio< z x
                  ... | tri< a ¬b ¬c = zc9 where
                      zc9 : odef (UnionCF A f mf ay supf1 z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
                      zc9 = {!!}
                      zc8 : odef (UnionCF A f mf ay (supfu a) z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
                      zc8 = ZChain.csupf  (pzc (osuc z) (ob<x lim a)) (o<→≤ <-osuc )
-                 ... | tri≈ ¬a b ¬c = {!!} -- ⊥-elim (¬a z<x)
-                 ... | tri> ¬a ¬b c = {!!} -- ⊥-elim (¬a z<x)
+                 ... | tri≈ ¬a b ¬c = ?
+                 ... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x)) 
 
           zc5 : ZChain A f mf ay x 
           zc5 with ODC.∋-p O A (* x)
@@ -905,7 +907,7 @@
 
      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
+     ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; as = 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))   -- Axiom of choice
@@ -918,7 +920,7 @@
          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) ) ⟫
+              zc5 = ⟪  Maximal.as 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 (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)
          zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) 
          total : IsTotalOrderSet (ZChain.chain zorn04)