# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1663326730 -32400
# Node ID a639a0d9265965379947ea5d5936cc4636ec843b
# Parent  2eaa61279c361457744ca15372a04eba437433e0
...

diff -r 2eaa61279c36 -r a639a0d92659 src/zorn.agda
--- a/src/zorn.agda	Thu Sep 15 16:24:31 2022 +0900
+++ b/src/zorn.agda	Fri Sep 16 20:12:10 2022 +0900
@@ -52,10 +52,10 @@
 -- Partial Order on HOD ( possibly limited in A )
 --
 
-_<<_ : (x y : Ordinal ) → Set n    -- Set n order
+_<<_ : (x y : Ordinal ) → Set n 
 x << y = * x < * y
 
-_<=_ : (x y : Ordinal ) → Set n    -- Set n order
+_<=_ : (x y : Ordinal ) → Set n    -- we can't use * x ≡ * y, it is Set (Level.suc n). Level (suc n) troubles Chain
 x <= y = (x ≡ y ) ∨ ( * x < * y )
 
 POO : IsStrictPartialOrder _≡_ _<<_ 
@@ -409,17 +409,17 @@
    supf-idem : {x : Ordinal } → supf (supf x) ≡ supf x
    supf-idem = ?
 
-   x≤supfx : {x : Ordinal } → x o≤ supf x
+   x≤supfx : (x : Ordinal ) → x o≤ supf x
    x≤supfx = ?
 
    supf∈A : {b : Ordinal} → b o≤ z → odef A (supf b)
    supf∈A {b} b≤z = subst (λ k → odef A k ) (sym (supf-is-sup b≤z)) ( SUP.as ( sup b≤z ) )
 
-   fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
-   fcy<sup  {u} {w} u<z fc with SUP.x<sup (sup (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
+   fcy<sup  : {u w : Ordinal } → u o≤ z  → FClosure A f y w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
+   fcy<sup  {u} {w} u≤z fc with SUP.x<sup (sup u≤z) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  
        , ch-init (subst (λ k → FClosure A f y k) (sym &iso) fc ) ⟫ 
-   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup (o<→≤ u<z) ) ) ))
-   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup (o<→≤ u<z) ))) ) lt )
+   ... | case1 eq = case1 (subst (λ k → k ≡ supf u ) &iso  (trans (cong (&) eq) (sym (supf-is-sup u≤z ) ) ))
+   ... | case2 lt = case2 (subst (λ k → * w < k ) (subst (λ k → k ≡ _ ) *iso (cong (*) (sym (supf-is-sup u≤z ))) ) lt )
 
    -- ordering is not proved here but in ZChain1 
 
@@ -593,7 +593,7 @@
               m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )
                       ⟪ record { x<sup = λ {z} uz → IsSup.x<sup (proj2 is-sup) (chain-mono1 (o<→≤ b<x) uz )  }  , m04 ⟫
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
-              m08 {z} fcz = ZChain.fcy<sup zc b<A fcz
+              m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                            → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
               m09 {s} {z} s<b fcz = order b<A s<b fcz    
@@ -613,7 +613,7 @@
               m09 : b o< & A
               m09 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
               m07 : {z : Ordinal} → FClosure A f y z → z <= ZChain.supf zc b
-              m07 {z} fc = ZChain.fcy<sup zc  m09 fc
+              m07 {z} fc = ZChain.fcy<sup zc (o<→≤ m09) fc
               m08 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
                        → FClosure A f (ZChain.supf zc s) z1 → z1 <= ZChain.supf zc b
               m08 {s} {z1} s<b fc = order m09 s<b fc
@@ -758,54 +758,90 @@
           --           supf0 px ≡ supf0 x 
 
           no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A pchain x f) → ZChain A f mf ay x
-          no-extension P with osuc-≡< (ZChain.x≤supfx zc)
-          ... | case1 sfpx=px = ?
+          no-extension P with osuc-≡< (ZChain.x≤supfx zc px)
+          ... | case1 sfpx=px = ? where
                  pchainpx : HOD
-                 pchainpx = record { od = record { def = λ z →  UChain A f mf ay supf0 z x ∨ FClosure A f px z  } ; odmax = & A ; <odmax = zc00 } where
-                      zc00 : {z : Ordinal } → UChain A f mf ay supf0 z x ∨ FClosure A f px z → z o< & A
-                      zc00 = ?
+                 pchainpx = record { od = record { def = λ z →  (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z  } ; odmax = & A ; <odmax = zc00 } where
+                      zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → z o< & A
+                      zc00 {z} (case1 lt) = z07 lt 
+                      zc00 {z} (case2 fc) = z09 ( A∋fc px f mf fc )
+                 zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → odef A z
+                 zc01 {z} (case1 lt) = proj1 lt 
+                 zc01 {z} (case2 fc) = ( A∋fc px f mf fc )
+
+                 zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f px b → a <= b
+                 zc02 {a} {b} ca fb = zc05 fb where
+                    zc06 : & (SUP.sup (ZChain.sup zc o≤-refl)) ≡ px
+                    zc06 = trans (sym ( ZChain.supf-is-sup zc o≤-refl )) (sym sfpx=px)
+                    zc05 : {b : Ordinal } → FClosure A f px b → a <= b
+                    zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc px f mf fb ))
+                    ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb)
+                    ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) 
+                    zc05 (init b1 refl) with SUP.x<sup (ZChain.sup zc o≤-refl) 
+                             (subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca )
+                    ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 (cong (&) eq))
+                    ... | case2 lt = case2 (subst (λ k → (* a) < k ) (trans (sym *iso) (cong (*) zc06)) lt)
 
-                 sup1 : SUP A (pchainpx sfpx=px )
-                 sup1 = supP ? ? ?
+                 ptotal : IsTotalOrderSet pchainpx
+                 ptotal (case1 a) (case1 b) =  subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso 
+                          (chain-total A f mf ay supf0 (proj2 a) (proj2 b)) 
+                 ptotal {a0} {b0} (case1 a) (case2 b) with zc02 a b
+                 ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where
+                      eq1 : a0 ≡ b0
+                      eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+                 ... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where
+                      lt1 : a0 < b0
+                      lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
+                 ptotal {b0} {a0} (case2 b) (case1 a) with zc02 a b
+                 ... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where
+                      eq1 : a0 ≡ b0
+                      eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq )
+                 ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1  where
+                      lt1 : a0 < b0
+                      lt1 = subst₂ (λ j k → j < k ) *iso *iso lt
+                 ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp px f mf a b)
+
+                 sup1 : SUP A pchainpx 
+                 sup1 = supP pchainpx zc01 ptotal
 
                  sp1 : Ordinal
-                 sp1 = & (SUP.sup (sup1 sfpx=px ))
+                 sp1 = & (SUP.sup sup1 )
 
                  supf1 : Ordinal → Ordinal
                  supf1 z with trio< z px 
                  ... | tri< a ¬b ¬c = supf0 z
-                 ... | tri≈ ¬a b ¬c = supf0 z
-                 ... | tri> ¬a ¬b c = sp1 sfpx=px
+                 ... | tri≈ ¬a b ¬c = px
+                 ... | tri> ¬a ¬b c = sp1 
 
                  pchainp : HOD
-                 pchainp = UnionCF A f mf ay (supfp sfpx=px  ) x
+                 pchainp = UnionCF A f mf ay supf1  x
 
 
           ... | case2 px<spfx = record { supf = supf0 ;  asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 
               ; supf-< = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) }  where
 
-                 supfp : Ordinal → Ordinal
-                 supfp lt z with trio< z px 
+                 supf1 : Ordinal → Ordinal
+                 supf1 z with trio< z px 
                  ... | tri< a ¬b ¬c = supf0 z
-                 ... | tri≈ ¬a b ¬c = supf0 z
+                 ... | tri≈ ¬a b ¬c = supf0 px
                  ... | tri> ¬a ¬b c = supf0 px
 
-                 pchain1 : (sfpx=px : px o< supfp px ) → HOD
-                 pchain1 lt  = UnionCF A f mf ay supfp x
+                 pchain1 : HOD
+                 pchain1 = UnionCF A f mf ay supf1 x
 
                  zc10 :  {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
                  zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup  fc  ⟫
+                 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) ?  ?  ⟫
                  zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  (HasPrev A pchain x f )
                         → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z )
                  zc11 P {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ 
                  zc11 P {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ with trio< u1 px 
-                 ... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 u1<px u1-is-sup fc  ⟫ 
-                 ... | tri≈ ¬a eq ¬c  = case2 ⟪ subst (λ k → supf0 k ≡ k) eq s1u=u , subst (λ k → FClosure A f k z) zc12 fc ⟫ where
+                 ... | tri< u1<px ¬b ¬c = case1 ⟪ az , ch-is-sup u1 u1<px ? fc  ⟫ 
+                 ... | tri≈ ¬a eq ¬c  = case2 ⟪ subst (λ k → supf0 k ≡ k) eq s1u=u , subst (λ k → FClosure A f k z) zc12 ? ⟫ where
                         s1u=u : supf0 u1 ≡ u1
-                        s1u=u = ChainP.supu=u u1-is-sup
+                        s1u=u = ? -- ChainP.supu=u u1-is-sup
                         zc12 : supf0 u1 ≡ px 
-                        zc12 = trans (ChainP.supu=u u1-is-sup) eq
+                        zc12 = trans s1u=u eq
                  zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = ⊥-elim (¬sp=x zcsup) where
                         eq : u1 ≡ x 
                         eq with trio< u1 x
@@ -813,12 +849,11 @@
                         ... | tri≈ ¬a b ¬c = b
                         ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x c )
                         s1u=x : supf0 u1 ≡ x
-                        s1u=x = trans (ChainP.supu=u u1-is-sup) eq
+                        s1u=x = trans ? eq
                         zc13 : osuc px o< osuc u1
                         zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) ) 
                         x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x)
-                        x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x
-                                  ( ChainP.fcy<sup u1-is-sup {w} fc  )
+                        x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
                         x<sup {w} ⟪ az , ch-is-sup u u<x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u<x) zc13 ))
                         ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 (o<→≤ u<x) ) where
                                  zc14 : u ≡ osuc px
@@ -828,13 +863,13 @@
                                     supf0 u1 ≡⟨ s1u=x ⟩ 
                                     x ≡⟨ sym (Oprev.oprev=x op) ⟩ 
                                     osuc px ∎ where open ≡-Reasoning
-                        ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ( ChainP.order u1-is-sup lt fc ) 
+                        ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ?
                         zc12 : supf0 x ≡ u1
-                        zc12 = subst  (λ k → supf0 k ≡ u1) eq (ChainP.supu=u u1-is-sup)
+                        zc12 = subst  (λ k → supf0 k ≡ u1) eq ?
                         zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
                         zcsup = record { ax =  subst (λ k → odef A k) (trans zc12 eq) (ZChain.asupf zc)
                                  ; is-sup = record { x<sup = x<sup } }
-                 zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 (zc20 fc ) where
+                 zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 ? where
                         eq : u1 ≡ x 
                         eq with trio< u1 x
                         ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ )
@@ -845,7 +880,7 @@
                           zc14 : x ≡ z
                           zc14 = begin
                              x ≡⟨ sym eq ⟩
-                             u1 ≡⟨  sym (ChainP.supu=u u1-is-sup ) ⟩
+                             u1 ≡⟨  sym ? ⟩
                              supf0 u1 ≡⟨ su=z ⟩
                              z ∎ where open ≡-Reasoning
                           zc13 : odef pchain z
@@ -866,7 +901,7 @@
                      ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ )
                      zc32 = ZChain.sup zc o≤-refl 
                      zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32)
-                     zc34 ne {w} lt with zc11 P (subst (λ k → odef (UnionCF A f mf ay supf0 k) (& w)) zc30 lt) 
+                     zc34 ne {w} lt with zc11 P ? 
                      ... | case1 lt = SUP.x<sup zc32 lt 
                      ... | case2 ⟪ spx=px  , fc ⟫ = ⊥-elim ( ne spx=px )
                      zc33 : supf0 z ≡ & (SUP.sup zc32)
@@ -893,13 +928,13 @@
                      zcsup : xSUP (UnionCF A f mf ay supf0 px) x 
                      zcsup with zc30
                      ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → 
-                        IsSup.x<sup (proj1 is-sup) (zc10 lt)} } 
+                        IsSup.x<sup (proj1 is-sup) ?} } 
                      zc31 : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨  HasPrev A (UnionCF A f mf ay supf0 px) x f) → supf0 b ≡ b
                      zc31 (case1 ¬sp=x) with zc30
                      ... | refl = ⊥-elim (¬sp=x zcsup )
                      zc31 (case2 hasPrev ) with zc30
                      ... | refl = ⊥-elim ( proj2 is-sup record { ax = HasPrev.ax hasPrev ; y = HasPrev.y hasPrev 
-                                ; ay = zc10 (HasPrev.ay hasPrev) ; x=fy = HasPrev.x=fy hasPrev } ) 
+                                ; ay = ? ; x=fy = HasPrev.x=fy hasPrev } ) 
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
@@ -908,36 +943,7 @@
                -- we have to check adding x preserve is-max ZChain A y f mf x
           ... | case1 pr = no-extension (case2 pr) -- 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 = supf1 
-                   ; sup=u = {!!} ; supf-mono = {!!}
-                   ; sup = {!!} ; supf-is-sup = {!!}   }  where
-
-             supf0px=x : (ax : odef A x) → IsSup A (ZChain.chain zc ) ax → x ≡  & (SUP.sup (ZChain.sup zc o≤-refl ) )
-             supf0px=x is-sup = ? where
-                 zc50 : supf0 px ≡ & (SUP.sup (ZChain.sup zc o≤-refl ) )
-                 zc50 = ZChain.supf-is-sup zc ?
-
-             pchain⊆x : UnionCF A f mf ay supf0 px ⊆'  UnionCF A f mf ay supf1 x
-             pchain⊆x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ 
-             pchain⊆x ⟪ au , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ au , ch-is-sup u ? ? ? ⟫ 
-
-             supfx1 : {z : Ordinal } → x o≤ z →  supf1 z ≡ x
-             supfx1 {z} x≤z with trio< z px
-             ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc )))
-             ... | tri≈ ¬a b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → k o< x ) (sym b) (pxo<x op)))
-             ... | tri> ¬a ¬b c = refl
-            
-             pchain0=x : UnionCF A f mf ay supf0 px ≡ UnionCF A f mf ay supf1 px 
-             pchain0=x =  ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where
-                     zc10 :  {z : Ordinal} → OD.def (od pchain) z → odef (UnionCF A f mf ay supf1 px) z
-                     zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
-                     zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 ? ? ?  ⟫
-                     zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 px) z → OD.def (od pchain) z
-                     zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 
-                     zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ?
-
-
+          ... | case1 is-sup = ? -- x is a sup of zc 
           ... | case2 ¬x=sup =  no-extension (case1 nsup) where -- px is not f y' nor sup of former ZChain from y -- no extention
              nsup : ¬ xSUP (UnionCF A f mf ay supf0 px) x 
              nsup s = ¬x=sup z12 where