# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1659317859 -32400
# Node ID 195c3c7de0216c4464c738824e8928efb5d5d028
# Parent  e8cf9c453431ea8ab7fa1a3fd4998f591e6dac8f
...

diff -r e8cf9c453431 -r 195c3c7de021 src/zorn.agda
--- a/src/zorn.agda	Mon Aug 01 09:38:00 2022 +0900
+++ b/src/zorn.agda	Mon Aug 01 10:37:39 2022 +0900
@@ -105,19 +105,19 @@
 ≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧  odef A (f x )
 
 data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where
-   init : odef A s → FClosure A f s s
+   init : {s1 : Ordinal } → odef A s → s ≡ s1  → FClosure A f s s1
    fsuc : (x : Ordinal) ( p :  FClosure A f s x ) → FClosure A f s (f x)
 
 A∋fc : {A : HOD} (s : Ordinal) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → odef A y
-A∋fc {A} s f mf (init as) = as
+A∋fc {A} s f mf (init as refl ) = as
 A∋fc {A} s f mf (fsuc y fcy) = proj2 (mf y ( A∋fc {A} s  f mf fcy ) )
 
 A∋fcs : {A : HOD} (s : Ordinal) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → odef A s
-A∋fcs {A} s f mf (init as) = as
+A∋fcs {A} s f mf (init as refl) = as
 A∋fcs {A} s f mf (fsuc y fcy) = A∋fcs {A} s f mf fcy 
 
 s≤fc : {A : HOD} (s : Ordinal ) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → * s ≤ * y
-s≤fc {A} s {.s} f mf (init x) = case1 refl
+s≤fc {A} s {.s} f mf (init x refl ) = case1 refl
 s≤fc {A} s {.(f x)} f mf (fsuc x fcy) with proj1 (mf x (A∋fc s f mf fcy ) )
 ... | case1 x=fx = subst (λ k → * s ≤ * k ) (*≡*→≡ x=fx) ( s≤fc {A} s f mf fcy )
 ... | case2 x<fx with s≤fc {A} s f mf fcy 
@@ -125,7 +125,7 @@
 ... | case2 s<x = case2 ( IsStrictPartialOrder.trans PO s<x x<fx )
 
 fcn : {A : HOD} (s : Ordinal) { x : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → FClosure A f s x → ℕ
-fcn s mf (init as) = zero
+fcn s mf (init as refl) = zero
 fcn {A} s {x} {f} mf (fsuc y p) with proj1 (mf y (A∋fc s f mf p))
 ... | case1 eq = fcn s mf p
 ... | case2 y<fy = suc (fcn s mf p )
@@ -134,11 +134,11 @@
      → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx  ≡ fcn s mf cy → * x ≡ * y
 fcn-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) (fcn s mf cy) eq cx cy refl refl where
      fc00 :  (i j : ℕ ) → i ≡ j  →  {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx  → j ≡ fcn s mf cy → * x ≡ * y
-     fc00 zero zero refl (init _) (init x₁) i=x i=y = refl
-     fc00 zero zero refl (init as) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) )
-     ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero zero refl (init as) cy i=x i=y )
-     fc00 zero zero refl (fsuc x cx) (init as) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) )
-     ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero zero refl cx (init as) i=x i=y )
+     fc00 zero zero refl (init _ refl) (init x₁ refl) i=x i=y = refl
+     fc00 zero zero refl (init as refl) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) )
+     ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero zero refl (init as refl) cy i=x i=y )
+     fc00 zero zero refl (fsuc x cx) (init as refl) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) )
+     ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero zero refl cx (init as refl) i=x i=y )
      fc00 zero zero refl (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
      ... | case1 x=fx  | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 zero zero refl cx cy  i=x i=y )
      fc00 (suc i) (suc j) i=j {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x j=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
@@ -211,7 +211,7 @@
            cxx :  FClosure A f s (f x)
            cxx = fsuc x cx 
            fc16 : (x : Ordinal ) → (cx : FClosure A f s x) → (fcn s mf cx  ≡ fcn s mf (fsuc x cx)) ∨ ( suc (fcn s mf cx ) ≡ fcn s mf (fsuc x cx))
-           fc16 x (init as) with proj1 (mf s as )
+           fc16 x (init as refl) with proj1 (mf s as )
            ... | case1 _ = case1 refl
            ... | case2 _ = case2 refl
            fc16 .(f x) (fsuc x cx ) with proj1 (mf (f x) (A∋fc s f mf (fsuc x cx)) )
@@ -230,8 +230,8 @@
       →  {p0 p1 : Ordinal → Ordinal}
       →  p0 u ≡ p1 u
       →  FClosure A f (p0 u) b → FClosure A f (p1 u) b 
-fc-conv A f {.(p0 u)} {u}  {p0} {p1} p0u=p1u (init ap0u) = subst (λ k → FClosure A f (p1 u) k) (sym p0u=p1u) 
-       ( init (subst (λ k → odef A k) p0u=p1u ap0u ))
+fc-conv A f {.(p0 u)} {u}  {p0} {p1} p0u=p1u (init ap0u refl) = subst (λ k → FClosure A f (p1 u) k) (sym p0u=p1u) 
+       ( init (subst (λ k → odef A k) p0u=p1u ap0u ) refl)
 fc-conv A f {_} {u}  {p0} {p1} p0u=p1u (fsuc z fc) = fsuc z (fc-conv A f {_} {u}  {p0} {p1} p0u=p1u fc)
 
 -- open import Relation.Binary.Properties.Poset as Poset
@@ -298,15 +298,15 @@
    = record { od = record { def = λ z → odef A z ∧ UChain A f mf ay supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
-        {init : Ordinal} (ay : odef A init)  ( z : Ordinal ) : Set (Level.suc n) where
+        {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
    field
       supf :  Ordinal → Ordinal 
    chain : HOD
    chain = UnionCF A f mf ay supf z
    field
       chain⊆A : chain ⊆' A
-      chain∋init : odef chain init
-      initial : {y : Ordinal } → odef chain y → * init ≤ * y
+      chain∋init : odef chain y
+      initial : {z : Ordinal } → odef chain z → * y ≤ * z
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-total : IsTotalOrderSet chain
 
@@ -315,29 +315,31 @@
       sup=u : {b : Ordinal} → (ab : odef A b) → b o< z  → IsSup A (UnionCF A f mf ay supf (osuc b)) ab → supf b ≡ b 
       csupf : (z : Ordinal ) → odef chain (supf z) 
       csupf' : {b : Ordinal } → b o≤ z → odef (UnionCF A f mf ay supf b) (supf b) 
-      fcy<sup  : {u w : Ordinal } → u o< z  → FClosure A f init w → (w ≡ supf u ) ∨ ( w << supf u ) -- different from order because y o< supf 
+      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 
       order : {b sup1 z1 : Ordinal} → b o< z → supf sup1 o< supf b → FClosure A f (supf sup1) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
    supf∈A : {u : Ordinal } → odef A (supf u)
    supf∈A = ?
-   fcy<sup'  : {u w : Ordinal } → u o< z  → FClosure A f init 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 ?) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} init 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 (o<→≤ u<z)) ⟪ subst (λ k → odef A k ) (sym &iso) (A∋fc {A} y f mf fc)  , ? ⟫ 
    ... | case1 eq = ?
    ... | case2 lt = ?
    fc∈A : {s z1 : Ordinal} → FClosure A f (supf s) z1 → odef chain z1
    fc∈A {s} (fsuc x fc) = f-next (fc∈A {s} fc )  -- (supf s) ≡ z1 → init (supf s)
    order' : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
-   order' {b} {s} {z1} b<z sf<sb fc with SUP.x<sup (sup (o<→≤ b<z)) (subst (λ k → odef (UnionCF A f mf ay supf b) k) (sym &iso) ( csupf' (o<→≤ b<z)) )
-   ... | case1 eq = case1 (begin
-     ? ≡⟨ ? ⟩
-     ? ∎ ) where open ≡-Reasoning
-   ... | case2 lt = case2 ? where
-        zc00 : ?
-        zc00 = ?
-   -- case2 ( subst (λ k → * z1 < k ) (subst₂ (λ j k → j ≡ k )  *iso ? (cong (*) (sym supf-is-sup)))  lt )
+   order' {b} {s} {.(f x)} b<z sf<sb (fsuc x fc) with proj1 (mf x (A∋fc _ f mf fc)) | order' b<z sf<sb fc
+   ... | case1 eq | t = ?
+   ... | case2 lt | t = ?
+   order' {b} {s} {z1} b<z sf<sb (init x refl) = ? where
+        zc01 : s o≤ z
+        zc01 = ?
+        zc00 : ( * (supf s)  ≡  SUP.sup (sup (o<→≤ b<z ))) ∨ ( * (supf s)  < SUP.sup ( sup (o<→≤ b<z )) )
+        zc00 with csupf' zc01 
+        ... | ⟪ ss , ch-init fc ⟫ = SUP.x<sup (sup (o<→≤ b<z)) ⟪ ? , ch-init ? ⟫
+        ... | ⟪ ss , ch-is-sup us is-sup fc  ⟫ = SUP.x<sup (sup (o<→≤ b<z)) ⟪ ? , ch-is-sup us ? ? ⟫
 
 
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) 
-        {init : Ordinal} (ay : odef A init)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
+        {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    field
       is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f mf ay (ZChain.supf zc) z) a ) →  b o< z  → (ab : odef A b) 
           → HasPrev A (UnionCF A f mf ay (ZChain.supf zc) z) ab f ∨  IsSup A (UnionCF A f mf ay (ZChain.supf zc) z) ab  
@@ -442,7 +444,7 @@
 
 init-uchain : (A : HOD)  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y ) 
     { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y
-init-uchain A f mf ay = ⟪ ay , ch-init (init ay)   ⟫
+init-uchain A f mf ay = ⟪ ay , ch-init (init ay refl)   ⟫
 
 ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
    → {x z : Ordinal } →  ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z )
@@ -559,7 +561,7 @@
                     m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
                     m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 
                          (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono1 x lt)  } ) a<b
-                 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫   where
+                 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl)) ⟫   where
                     b<A : b o< & A
                     b<A = z09 ab
                     m05 : b ≡ ZChain.supf zc b
@@ -595,7 +597,7 @@
                  m06 : ChainP A f mf ay (ZChain.supf zc) b b
                  m06 = record { fcy<sup = m07 ;  order = m08 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
-                 m04 = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab))  ⟫
+                 m04 = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab refl))  ⟫
 
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
@@ -684,9 +686,9 @@
           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)  ⟫
+          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))
+          y<sup = SUP.x<sup  (ysup f mf ay) (subst (λ k → FClosure A f y k ) (sym &iso) (init ay refl))
           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 
@@ -701,7 +703,7 @@
                uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb)  
 
           csupf : (z : Ordinal) → odef (UnionCF A f mf ay isupf o∅) (isupf z)
-          csupf z = ⟪ asi , ch-is-sup spi uz02 (init asi) ⟫ where
+          csupf z = ⟪ asi , ch-is-sup spi 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
@@ -750,9 +752,9 @@
           ... | ch-init fc = s≤fc y f mf fc
           ... | ch-is-sup u is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
                zc7 : y <= (ZChain.supf zc) u 
-               zc7 = ChainP.fcy<sup is-sup (init ay)
+               zc7 = ChainP.fcy<sup is-sup (init ay refl)
           pcy : odef pchain y
-          pcy = ⟪ ay , ch-init (init ay)    ⟫
+          pcy = ⟪ ay , ch-init (init ay refl)    ⟫
 
           supf0 = ZChain.supf zc
 
@@ -863,7 +865,7 @@
                 zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
                 zc12  = ZChain.csupf ozc z
                 zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
-                zc11 = ⟪ az , ch-is-sup z cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az) ) ⟫ where
+                zc11 = ⟪ az , ch-is-sup z cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az refl) ) ⟫ where
                       az : odef A ( ZChain.supf ozc z )
                       az = proj1 zc12
                       zc20 : {z1  : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
@@ -898,9 +900,9 @@
           ... | ch-init fc = s≤fc y f mf fc
           ... | ch-is-sup u is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc)  where
                zc7 : y <= psupf _
-               zc7 = ChainP.fcy<sup is-sup (init ay)
+               zc7 = ChainP.fcy<sup is-sup (init ay refl)
           pcy : odef pchain y
-          pcy = ⟪ ay , ch-init (init ay)    ⟫
+          pcy = ⟪ ay , ch-init (init ay refl)    ⟫
           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) )