# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657673410 -32400
# Node ID e9ddbf84d69979073a2c2c6f7d80852449eb87b4
# Parent  e59bcd41462df3240b7da2222b5d31c55dbd6c89
...

diff -r e59bcd41462d -r e9ddbf84d699 src/zorn.agda
--- a/src/zorn.agda	Wed Jul 13 08:43:12 2022 +0900
+++ b/src/zorn.agda	Wed Jul 13 09:50:10 2022 +0900
@@ -267,8 +267,8 @@
        (supf : Ordinal → Ordinal) (x : Ordinal)  (z : Ordinal) : Set n where 
    field
       u : Ordinal
-      u<x : (u o< x ) ∨ ( x o≤ y )
-      chain∋z : Chain A f mf ay supf u z
+      u<x : (u o< x ) ∨ ( u ≡ y )
+      uchain : Chain A f mf ay supf u z
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
@@ -472,43 +472,9 @@
      -- create all ZChains under o< x
      --
 
-     inititalChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
-         → x o≤ y  → ZChain A f mf ay x
-     inititalChain f mf {y} ay x x≤y = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy
-      ; initial = isy ; f-next = inext ; f-total = itotal ; is-max = ? } where
-          isupf : Ordinal → Ordinal
-          isupf z = y
-          cy : odef (UnionCF A f mf ay isupf x) y
-          cy = ⟪ ay , record { u = y ; u<x = case2 x≤y ; chain∋z = ch-init _ (init ay)  } ⟫
-          isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf x) z → * y ≤ * z
-          isy {z} ⟪ az , uz ⟫ with UChain.chain∋z uz 
-          ... | ch-init z fc = s≤fc y f mf fc 
-          ... | ch-is-sup is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
-          inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf x) a → odef (UnionCF A f mf ay isupf x) (f a)
-          inext {a} ua with UChain.chain∋z (proj2 ua)
-          ... | ch-init a fc = ⟪ proj2 (mf _ (proj1 ua))  , record { u = y ; u<x = case2 x≤y ; chain∋z = ch-init _ (fsuc _ fc ) } ⟫
-          ... | ch-is-sup is-sup fc = ⊥-elim ( <-irr (case1 refl) ( ChainP.fcy<sup is-sup (init ay) ) )
-          itotal : IsTotalOrderSet (UnionCF A f mf ay isupf x) 
-          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 (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
-          imax : {a b : Ordinal} → odef (UnionCF A f mf ay isupf x) a →
-            b o< osuc x → (ab : odef A b) →
-            HasPrev A (UnionCF A f mf ay isupf x) ab f ∨ IsSup A (UnionCF A f mf ay isupf x) ab →
-            * a < * b → odef (UnionCF A f mf ay isupf x) b
-          imax {a} {b} ua b<ox ab (case1 hasp) a<b = subst (λ k → odef  (UnionCF A f mf ay isupf x) k ) (sym (HasPrev.x=fy hasp)) ( inext (HasPrev.ay hasp) )
-          imax {a} {b} ua b<ox ab (case2 sup)  a<b = ?
-          -- with IsSup.x<sup sup (inext 
-          -- ... | case1 a=b = ?
-          -- ... | case2 a<b = ?
-          -- ⊥-elim ( <-irr (case2 ? ) ( IsSup  ) )
-
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
          → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x
-     ind f mf {y} ay x prev with trio< y x
-     ... | tri> ¬a ¬b c = ?
-     ... | tri≈ ¬a refl ¬c = ?
-     ... | tri< y<x ¬b ¬c with Oprev-p x
+     ind f mf {y} ay x prev with Oprev-p x
      ... | yes op = zc4 where
           --
           -- we have previous ordinal to use induction
@@ -526,57 +492,54 @@
           ptotal : IsTotalOrderSet pchain
           ptotal {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 (ZChain.supf zc) (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
-          psupf : Ordinal → Ordinal
-          psupf z with trio< z x 
-          ... | tri< a ¬b ¬c = ZChain.supf zc z
-          ... | tri≈ ¬a b ¬c = x
-          ... | tri> ¬a ¬b c = x
+               uz01 = chain-total A f mf ay (ZChain.supf zc) (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
           pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
-          pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = ? } ⟫ where
+          pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; uchain = fua } ⟫ where
                afa : odef A ( f a )
                afa = proj2 ( mf a aa )
-               fua : Chain A f mf ay psupf (UChain.u ua) (f a)
-               fua with UChain.chain∋z ua
+               fua : Chain A f mf ay (ZChain.supf zc)  (UChain.u ua) (f a)
+               fua with UChain.uchain ua
                ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
-               ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ ? ) (fsuc _ ? )
+               ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc )
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
-          pinit {a} ⟪ aa , ua ⟫  with UChain.chain∋z ua
+          pinit {a} ⟪ aa , ua ⟫  with UChain.uchain ua
           ... | ch-init a fc = s≤fc y f mf fc
-          ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) ? where -- (s≤fc _ f mf fc)  where
-               zc7 : y << psupf (UChain.u ua)
-               zc7 = ? -- ChainP.fcy<sup is-sup (init ay)
+          ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
+               zc7 : y << (ZChain.supf zc) (UChain.u ua)
+               zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
-          pcy = ⟪ ay , record { u =  y ; u<x = case1 y<x ; chain∋z = ch-init _ (init ay)  }  ⟫
+          pcy = ⟪ ay , record { u =  y ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
 
           -- if previous chain satisfies maximality, we caan reuse it
           --
-          no-extenion : ( {a b z : Ordinal} → (z<x : z o< x)  → 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 f mf ay x
-          no-extenion is-max  = record { initial = ? ; chain∋init = ? }
+          no-extenion : ( {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) →
+                    HasPrev A pchain ab f ∨  IsSup A pchain ab →
+                            * a < * b → odef pchain b ) → ZChain A f mf ay x
+          no-extenion is-max  = record { initial = pinit ; chain∋init = pcy 
+              ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal ; is-max = is-max }
 
           zc4 : ZChain A f mf ay x 
           zc4 with ODC.∋-p O A (* x)
-          ... | no noax = no-extenion zc1  where -- ¬ A ∋ p, just skip
-                zc1 : {a b z : Ordinal} → (z<x : z o< x) → 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
-                zc1 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
+          ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip
+                zc1 : {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) →
+                    HasPrev A pchain ab f ∨  IsSup A pchain ab →
+                            * a < * b → odef pchain b
+                zc1 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) )
-                ... | case2 lt = ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab P a<b
+                ... | case2 lt = ⟪ ab , record { u = ? ; u<x = ? ; uchain = ? } ⟫
+                -- ZChain.is-max zc ? (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab ? a<b
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) ax f )   
                -- we have to check adding x preserve is-max ZChain A y f mf x
-          ... | case1 pr = no-extenion zc7  where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
-                chain0 = ZChain.chain zc 
-                zc7 :  {a b z : Ordinal} → (z<x : z o< x) → 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
-                zc7 {a} {b} z<x za b<ox ab P a<b with osuc-≡< b<ox
-                ... | case2 lt = ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab P a<b
-                ... | 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))
+          ... | case1 pr = no-extenion ? where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
+                zc7 : {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) →
+                    HasPrev A pchain ab f ∨  IsSup A pchain ab →
+                            * a < * b → odef pchain b
+                zc7 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
+                ... | case2 lt = ? -- ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab P a<b
+                ... | 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 = pchain⊆A ; f-next = pnext ; f-total = ptotal
@@ -589,15 +552,15 @@
                 p-ismax {a} {b} ua b<ox ab (case2 sup)  a<b = ?
 
           ... | case2 ¬x=sup =  no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention
-                z18 :  {a b z : Ordinal} → (z<x : z o< x) → 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
-                z18 {a} {b} z<x za b<x ab p a<b with osuc-≡< b<x
-                ... | case2 lt = ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab p a<b 
+                z18 :  {a b : Ordinal} → odef pchain a → b o< osuc x → (ab : odef A b) →
+                            HasPrev A pchain ab f ∨ IsSup A pchain   ab →
+                            * a < * b → odef pchain b
+                z18 {a} {b} za b<x ab p a<b with osuc-≡< b<x
+                ... | case2 lt = ? -- ZChain.is-max zc za (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt ) ab p a<b 
                 ... | case1 b=x with p
-                ... | 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 ) } )
+                ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = ? ; 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 )  } ) 
+                      x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup ? )  } ) 
      ... | no op = zc5 where
           pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
           pzc z z<x = prev z z<x
@@ -611,26 +574,26 @@
           ptotal : IsTotalOrderSet pchain
           ptotal {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 psupf0 (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
+               uz01 = chain-total A f mf ay psupf0 (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
 
           pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
-          pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; chain∋z = ? } ⟫ where
+          pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; uchain = fua } ⟫ where
                afa : odef A ( f a )
                afa = proj2 ( mf a aa )
                fua : Chain A f mf ay psupf0 (UChain.u ua) (f a)
-               fua with UChain.chain∋z ua
+               fua with UChain.uchain ua
                ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
-               ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ ? ) (fsuc _ ? )
+               ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc )
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
-          pinit {a} ⟪ aa , ua ⟫  with UChain.chain∋z ua
+          pinit {a} ⟪ aa , ua ⟫  with UChain.uchain ua
           ... | ch-init a fc = s≤fc y f mf fc
-          ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) ? where -- (s≤fc _ f mf fc)  where
+          ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
                zc7 : y << psupf0 (UChain.u ua)
-               zc7 = ? -- ChainP.fcy<sup is-sup (init ay)
+               zc7 = ChainP.fcy<sup is-sup (init ay)
           pcy : odef pchain y
-          pcy = ⟪ ay , record { u =  y ; u<x = case1 y<x ; chain∋z = ch-init _ (init ay)  }  ⟫
+          pcy = ⟪ ay , record { u =  y ; u<x = case2 refl ; uchain = ch-init _ (init ay)  }  ⟫
 
           usup : SUP A pchain
           usup = supP pchain (λ lt → proj1 lt) ptotal