# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655682203 -32400
# Node ID 886e1f82cca0e4f21949c2a0100a58f84cf7250e
# Parent  d0938f220648a701d87e5580096254c82d133a62
...

diff -r d0938f220648 -r 886e1f82cca0 src/OrdUtil.agda
--- a/src/OrdUtil.agda	Mon Jun 20 07:49:35 2022 +0900
+++ b/src/OrdUtil.agda	Mon Jun 20 08:43:23 2022 +0900
@@ -153,8 +153,12 @@
 
 open _∧_
 
-o≤-refl :  { i  j : Ordinal } → i ≡ j → i o≤ j
-o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
+o≤-refl0 :  { i  j : Ordinal } → i ≡ j → i o≤ j
+o≤-refl0 {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
+
+o≤-refl :  { i : Ordinal } → i o≤ i
+o≤-refl {i} = subst (λ k → i o< osuc k ) refl <-osuc
+
 OrdTrans :  Transitive  _o≤_
 OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
 OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
@@ -168,7 +172,7 @@
    ; _∼_   = _o≤_
    ; isPreorder   = record {
         isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
-        ; reflexive     = o≤-refl
+        ; reflexive     = o≤-refl0
         ; trans         = OrdTrans 
      }
  }
@@ -230,14 +234,14 @@
 ≤next {x} {y} x≤y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc )
 ≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc )
 ≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y
-≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl refl   -- x = y < next x
-≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl (x<ny→≡next x<y c) -- x ≤ y < next x 
+≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl -- x = y < next x
+≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl0 (x<ny→≡next x<y c) -- x ≤ y < next x 
 
 x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y
 x<ny→≤next {x} {y} x<ny with trio< x y
 x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c =  ≤next (ordtrans a <-osuc )
-x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl refl
-x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl (sym ( x<ny→≡next c x<ny ))
+x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl 
+x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl0 (sym ( x<ny→≡next c x<ny ))
 
 omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y )
 omax<nomax {x} {y} with trio< x y
diff -r d0938f220648 -r 886e1f82cca0 src/zorn.agda
--- a/src/zorn.agda	Mon Jun 20 07:49:35 2022 +0900
+++ b/src/zorn.agda	Mon Jun 20 08:43:23 2022 +0900
@@ -325,13 +325,13 @@
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 
      zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc1 : ZChain1 A (& s) f (& A) ) → SUP A  (ZChain.chain (ZChain1.zc zc1)) 
-     zsup f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain1.f-total zc1 {!!} )   where
+     zsup f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain1.f-total zc1 {& A} {& A} o≤-refl )   where
            zc = ZChain1.zc zc1
      A∋zsup : (nmx : ¬ Maximal A ) (zc1 : ZChain1 A (& s) (cf nmx)  (& A) ) 
         →  A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc1 )))
      A∋zsup nmx zc1 = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal  (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc1 ) )
      sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc1 : ZChain1 A (& s) f  (& A) ) → SUP A (ZChain.chain (ZChain1.zc zc1))
-     sp0 f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain1.f-total zc1 {!!} )   where
+     sp0 f mf zc1 = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain1.f-total zc1 {& A} {& A} o≤-refl )   where
            zc = ZChain1.zc zc1
      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)
@@ -368,7 +368,7 @@
                    ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
                    -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ?  (SUP.x<sup sp1 ? ) }
            z14 :  f (& (SUP.sup (sp0 f mf zc1))) ≡ & (SUP.sup (sp0 f mf zc1))
-           z14 with ZChain1.f-total zc1 {!!}  (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
+           z14 with ZChain1.f-total zc1 {& A} {& A} o≤-refl (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 ))
@@ -434,7 +434,7 @@
                             ¬ (* x₁ < * y₁) ∧ (* y₁ < * (f x₁)) ) seq (ZChain.f-immediate zc0) ; chain∋x  = subst (λ k → odef k y ) seq (ZChain.chain∋x  zc0)
                              ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
                                  HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) seq is-max } 
-                     ; chain-mono = mono } where
+                     ; chain-mono = mono ; f-total = {!!} } where
                 supf0 : Ordinal → HOD
                 supf0 z with trio< z x
                 ... | tri< a ¬b ¬c = supf z
@@ -495,8 +495,8 @@
                 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
           ... | case1 is-sup = -- x is a sup of zc0 
-                record { zc = record { chain⊆A = {!!}  ; f-total = {!!} ; f-next = {!!} 
-                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} }  ; supf = supf0 ; chain-mono = mono } where 
+                record { zc = record { chain⊆A = {!!} ; f-next = {!!} 
+                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!} }  ; supf = supf0 ; chain-mono = mono ; f-total = {!!} } where 
                 sup0 : SUP A (ZChain.chain zc0) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
                         x21 :  {y : HOD} → ZChain.chain zc0 ∋ y → (y ≡ * x) ∨ (y < * x)
@@ -534,7 +534,7 @@
                         a<b : a < b
                         a<b = ptrans  (subst (λ k → a < k ) (sym *iso) a<sp ) ( subst₂ (λ j k → j < k ) refl *iso sp<b )
                 scmp : {a b : HOD} → odef schain (& a) → odef schain (& b) → Tri (a < b) (a ≡ b) (b < a )
-                scmp (case1 za) (case1 zb) = ZChain1.f-total zc1 {!!} za zb
+                scmp {a} {b} (case1 za) (case1 zb) = ZChain1.f-total zc1 {px} {px} o≤-refl za zb
                 scmp {a} {b} (case1 za) (case2 fb) = cmp za fb 
                 scmp  (case2 fa) (case1 zb) with  cmp zb fa
                 ... | tri< a ¬b ¬c = tri> ¬c (λ eq → ¬b (sym eq))  a
@@ -623,8 +623,8 @@
                 ... | 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 record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
-     ... | no ¬ox = record { supf = supf0 ; chain-mono = {!!}
-              ; zc  = record { chain⊆A = {!!} ; f-total = {!!}  ; f-next = {!!} 
+     ... | no ¬ox = record { supf = supf0 ; chain-mono = {!!} ; f-total = u-total
+              ; zc  = record { chain⊆A = {!!} ; f-next = {!!} 
                      ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} } }  where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
             field
@@ -661,18 +661,21 @@
          ... | tri< a ¬b ¬c = cong (λ k → ZChain1.supf (prev b k {y} ay) b) o<-irr --  b<x ≡ a
          ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
          ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
-         u-mono :  ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain1 A y f a) (zb : ZChain1 A y f b) → ZChain.chain (ZChain1.zc za)  ⊆' ZChain.chain (ZChain1.zc zb)
-         u-mono a b b<x a≤b za zb {i} zai = ZChain1.chain-mono zb a≤b <-osuc (uz01 zai) where
-              uz01 : odef (ZChain1.supf za a) i → odef (ZChain1.supf zb a) i
-              uz01 = {!!}
-         u-total : IsTotalOrderSet Uz
-         u-total {x} {y} ux uy  with trio< (UZFChain.u ux) (UZFChain.u uy)
-         ... | tri< a ¬b ¬c = ZChain1.f-total (uzc1 uy) {!!} (u-mono (UZFChain.u ux) (UZFChain.u uy)
-            (UZFChain.u<x uy) (ordtrans a <-osuc ) (uzc1 ux) (uzc1 uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
-         ... | tri≈ ¬a b ¬c = ZChain1.f-total (uzc1 ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
-            (UZFChain.u<x ux) (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc1 uy) (uzc1 ux) (UZFChain.chain∋z uy))
-         ... | tri> ¬a ¬b c = ZChain1.f-total (uzc1 ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
-            (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc1 uy) (uzc1 ux) (UZFChain.chain∋z uy)) 
+         u-mono :  {z : Ordinal} {y : Ordinal} → z o≤ y → y o≤ x → supf0 z ⊆' supf0 y
+         u-mono {z} {y} z≤y y≤x with trio< z x | trio< y x
+         ... | tri< a ¬b ¬c | t = {!!}
+         ... | tri≈ ¬a b ¬c | t = {!!}
+         ... | tri> ¬a ¬b c | t = ⊥-elim ( osuc-< y≤x {!!} )
+         u-total : {z : Ordinal}  → z o≤ x → IsTotalOrderSet (supf0 z)
+         u-total {z}  z<x ux uy  with trio< z x
+         ... | t = {!!}
+         -- with trio< (UZFChain.u ux) (UZFChain.u uy)
+         -- ... | tri< a ¬b ¬c = ZChain1.f-total (uzc1 uy) {!!} (u-mono (UZFChain.u ux) (UZFChain.u uy)
+         --    (UZFChain.u<x uy) (ordtrans a <-osuc ) (uzc1 ux) (uzc1 uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
+         -- ... | tri≈ ¬a b ¬c = ZChain1.f-total (uzc1 ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
+         --    (UZFChain.u<x ux) (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc1 uy) (uzc1 ux) (UZFChain.chain∋z uy))
+         -- ... | tri> ¬a ¬b c = ZChain1.f-total (uzc1 ux) {!!} (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
+         --    (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc1 uy) (uzc1 ux) (UZFChain.chain∋z uy)) 
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain1 A y f (& A)
      SZ f mf = TransFinite {λ z → {y : Ordinal } → (ay : odef A y ) → ZChain1 A y f z  } (ind f mf) (& A)