# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656553224 -32400
# Node ID 6df8b836e9831596b5e3c4358434b35dc6392e6f
# Parent  4186c0331abb3b8108092ca666c313bdf439e9c6
...

diff -r 4186c0331abb -r 6df8b836e983 src/zorn.agda
--- a/src/zorn.agda	Thu Jun 30 06:57:05 2022 +0900
+++ b/src/zorn.agda	Thu Jun 30 10:40:24 2022 +0900
@@ -230,7 +230,7 @@
       x=fy :  x ≡ f y 
 
 record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x)     : Set n where
-   ield
+   field
       x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
 record ZChain1 ( z : Ordinal ) : Set (Level.suc n) where
@@ -249,7 +249,7 @@
       chain∋init : odef chain init
       initial : {y : Ordinal } → odef chain y → * init ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
-      f-total : {x : Ordinal} → IsTotalOrderSet chain
+      f-total : IsTotalOrderSet chain
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
@@ -408,17 +408,22 @@
          → ((z : Ordinal) → z o< x → ZChain1 z ) → ZChain1 x
      sind f mf {y} ay x prev  with Oprev-p x
      ... | yes op = sc4 where
+          open ZChain1
           px = Oprev.oprev op
           sc : ZChain1 px
           sc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
+          no-ext : ZChain1 x
+          no-ext = record { supf = s01 ; chain-mono = ? } where
+                s01 : Ordinal → HOD
+                s01 z = supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )) z
 
           sc4 : ZChain1 x
           sc4 with ODC.∋-p O A (* x)
-          ... | no noax = ?
+          ... | no noax = {!!}
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.supf sc x) ax f )   
-          ... | case1 pr = ?
+          ... | case1 pr = {!!}
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.supf sc x) ax )
-          ... | case1 is-sup = ? where
+          ... | case1 is-sup = {!!} where
                 -- A∋sc -- x is a sup of zc 
                 sup0 : SUP A (ZChain1.supf sc x )
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
@@ -430,8 +435,8 @@
                 sp = SUP.sup sup0 
                 schain : HOD
                 schain = record { od = record { def = λ x → odef (ZChain1.supf sc x) x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
-          ... | case2 ¬x=sup = ?
-     ... | no ¬ox = ? 
+          ... | case2 ¬x=sup = {!!}
+     ... | no ¬ox = {!!} 
 
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (zc0 : ZChain0 A) → (x : Ordinal)
          → ((z : Ordinal) → z o< x → ZChain A y f zc0 z) → ZChain A y f zc0 x
@@ -455,12 +460,13 @@
           no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc) ab f ∨  IsSup A (ZChain.chain zc) ab →
                             * a < * b → odef (ZChain.chain zc) b ) → ZChain A y f zc0 x
-          no-extenion is-max = record { supf = supf0 ;  chain⊆A = subst (λ k → k ⊆' A ) ? (ZChain.chain⊆A zc)
-                     ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) ? (ZChain.initial zc)
-                     ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) ? (ZChain.f-next zc) 
-                     ; chain∋init  = subst (λ k → odef k y ) ? (ZChain.chain∋init  zc) ; pmono = {!!} 
-                             ; 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  ) ? is-max } where
+          no-extenion is-max = record { chain⊆A = ? -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc)
+                     ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) {!!} (ZChain.initial zc)
+                     ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) {!!} (ZChain.f-next zc) 
+                     ; f-total = ? 
+                     ; chain∋init  = subst (λ k → odef k y ) {!!} (ZChain.chain∋init  zc) 
+                     ; 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  ) {!!} is-max } where
                 supf0 : Ordinal → HOD
                 supf0 z with trio< z x
                 ... | tri< a ¬b ¬c = supf z
@@ -497,8 +503,8 @@
                 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr))
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc) ax )
           ... | case1 is-sup = -- x is a sup of zc 
-                record {  chain⊆A = {!!} ; f-next = {!!}  ; pmono = {!!}
-                     ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!}   ; supf = supf0 } where
+                record {  chain⊆A = {!!} ; f-next = {!!}  ; f-total = {!!}
+                     ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!}   } where
                 sup0 : SUP A (ZChain.chain zc) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
                         x21 :  {y : HOD} → ZChain.chain zc ∋ y → (y ≡ * x) ∨ (y < * x)
@@ -606,8 +612,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 { chain⊆A = ? ; f-next = ? ; chain = ?
-                     ; initial = ? ; chain∋init  = ? ; is-max = {!!} }   where --- limit ordinal case
+     ... | no ¬ox = record { chain⊆A = {!!} ; f-next = {!!} ; f-total = ?
+                     ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!} }   where --- limit ordinal case
          supf : Ordinal → HOD
          supf = ZChain1.supf zc0
          Uz⊆A : {z : Ordinal} → UZFChain A f zc0 x y prev z ∨ FClosure A f y z → odef A z
@@ -626,12 +632,15 @@
          u-initial {z} (case2 u) = s≤fc _ f mf u
          u-chain∋init :  odef Uz y
          u-chain∋init = case2 ( init ay )
-
          supf0 : Ordinal → HOD
          supf0 z with trio< z x
          ... | tri< a ¬b ¬c = ZChain1.supf zc0 z
          ... | tri≈ ¬a b ¬c = Uz 
          ... | tri> ¬a ¬b c = Uz
+         u-mono :  {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w
+         u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x
+         ... | s | t = ?
+
          seq : Uz ≡ supf0 x
          seq with trio< x x
          ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
@@ -674,7 +683,9 @@
          zorn04 : ZChain A (& s) (cf nmx) zc0 (& A)
          zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) 
          total : IsTotalOrderSet (ZChain.chain zorn04)
-         total =  ZChain.f-total (SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) ) 
+         total {a} {b} = zorn06  where
+             zorn06 :  odef (ZChain.chain zorn04) (& a) → odef (ZChain.chain zorn04) (& b) → Tri (a < b) (a ≡ b) (b < a)
+             zorn06 = ZChain.f-total (SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) ) 
 
 -- usage (see filter.agda )
 --