# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657484321 -32400
# Node ID 46d05d12df5789d96fc0f38a990535cb4510c1d4
# Parent  33f90b48321170dc9428192d3bcba76b181ea638
...

diff -r 33f90b483211 -r 46d05d12df57 src/zorn.agda
--- a/src/zorn.agda	Mon Jul 11 04:53:45 2022 +0900
+++ b/src/zorn.agda	Mon Jul 11 05:18:41 2022 +0900
@@ -245,7 +245,7 @@
    field
       u : Ordinal
       u<x : u o< x
-      chain∋z : odef (chain u u<x) z
+      chain∋z : odef (chain u u<x ) 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 )))
@@ -260,16 +260,15 @@
 --    minimum index is y not ϕ 
 --
 
-record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {x y : Ordinal} (ay : odef A y) (chainf : (z : Ordinal ) → z o< x → HOD) (sup z : Ordinal) : Set n where
+record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD) (sup z : Ordinal) : Set n where
    field
       asup    : odef A sup
       y<sup   : y o< sup
       y<<sup  : y << sup
-      sup<x   : sup o< x
-      csupz   : odef (chainf sup sup<x) z
-      order : (sup1 z1 : Ordinal) → (lt : sup1 o< sup ) → odef (chainf sup1 (ordtrans lt sup<x ) ) z1 → z1 << z
+      csupz   : odef (chainf sup) z
+      order : (sup1 z1 : Ordinal) → (lt : sup1 o< sup ) → odef (chainf sup1 ) z1 → z1 << z
 
-data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {x y : Ordinal} (ay : odef A y) (chainf : (z : Ordinal ) → z o< x → HOD) : Ordinal →  Ordinal → Set n where
+data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD) : Ordinal →  Ordinal → Set n where
     ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay chainf y z 
     ch-is-sup : {sup z : Ordinal } 
          → ( is-sup : ChainP A f mf ay chainf sup z)
@@ -279,13 +278,13 @@
    field
       psup :  Ordinal → Ordinal 
       p≤z : (x : Ordinal ) →   odef A (psup x)
-      chainf : (x : Ordinal) → x o< z  → HOD
-      is-chain : (x w : Ordinal) → (x<z : x o< z) → odef (chainf x x<z) w → Chain A f mf ay chainf (psup x) w 
+      chainf : (x : Ordinal) → HOD
+      is-chain : (x w : Ordinal) → (x<z : x o< z) → odef (chainf x) w → Chain A f mf ay chainf (psup x) w 
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)  
           (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where
    chain : HOD
-   chain = UnionCF A (& A) ( λ x _ → ZChain1.chainf (zc0 (& A)) x ? )  
+   chain = UnionCF A (& A) ( λ x _ → ZChain1.chainf (zc0 (& A)) x )  
    field
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
@@ -309,21 +308,21 @@
 --
 -- data Chain is total
 
-chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {x y : Ordinal} (ay : odef A y) (chainf : (z : Ordinal ) → z o< x → HOD)
+chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {x y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD)
    {s s1 a b : Ordinal } ( ca : Chain A f mf ay chainf s a ) ( cb : Chain A f mf ay chainf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
 chain-total A f mf {x} {y} ay chainf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
      ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay chainf xa a → Chain A f mf ay chainf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
           ct00 : * a < * xb
-          ct00 = ?
+          ct00 = {!!}
           ct01 : * a < * b 
           ct01 with s≤fc xb f mf fcb 
           ... | case1 eq =  subst (λ k → * a < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
      ct-ind xa xb {a} {b} (ch-is-sup supa fca) (ch-init b fcb)= tri> (λ lt → <-irr (case2 ct01) lt) (λ eq → <-irr (case1 eq) ct01) ct01    where
           ct00 : * b < * xa
-          ct00 = ?
+          ct00 = {!!}
           ct01 : * b < * a 
           ct01 with s≤fc xa f mf fca 
           ... | case1 eq =  subst (λ k → * b < k ) eq ct00
@@ -331,7 +330,7 @@
      ct-ind xa xb {a} {b} (ch-is-sup supa fca) (ch-is-sup supb fcb) with trio< xa xb
      ... | tri< a₁ ¬b ¬c = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
           ct03 : * a < * xb
-          ct03 = ?
+          ct03 = {!!}
           ct02 : * a < * b 
           ct02 with s≤fc xb f mf fcb 
           ... | case1 eq =  subst (λ k → * a < k ) eq ct03
@@ -339,7 +338,7 @@
      ... | tri≈ ¬a  refl ¬c = fcn-cmp xa f mf fca fcb
      ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
           ct05 : * b < * xa
-          ct05 = ?
+          ct05 = {!!}
           ct04 : * b < * a 
           ct04 with s≤fc xa f mf fca 
           ... | case1 eq =  subst (λ k → * b < k ) eq ct05
@@ -482,7 +481,7 @@
           sc : ZChain1 A f mf ay px
           sc = prev px px<x
           pchain : HOD
-          pchain  = chainf sc px ?
+          pchain  = chainf sc px 
 
           no-ext :  ZChain1 A f mf ay x
           no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 }  where
@@ -494,10 +493,10 @@
             p≤z1 z with o≤? z x
             ... | yes _  = ZChain1.p≤z sc z
             ... | no _  = ZChain1.p≤z sc x
-            chainf1 : (z : Ordinal ) → z o< x → HOD
-            chainf1 z z<x with o≤? z x
-            ... | yes _  = ZChain1.chainf sc z ?
-            ... | no _ = ZChain1.chainf sc x ?
+            chainf1 : (z : Ordinal ) → HOD
+            chainf1 z with o≤? z x
+            ... | yes _  = ZChain1.chainf sc z 
+            ... | no _ = ZChain1.chainf sc x 
             is-chain1 : {!!}
             is-chain1 = {!!}
           sc4 : ZChain1 A f mf ay x
@@ -513,7 +512,7 @@
           ... | case2 ¬x=sup = no-ext
      ... | no ¬ox = sc4 where
           pchainf : (z : Ordinal) → z o< x → HOD
-          pchainf z z<x = ZChain1.chainf (prev z z<x) z ? 
+          pchainf z z<x = ZChain1.chainf (prev z z<x) z  
           pzc : (z : Ordinal) → z o< x → ZChain1 A f mf ay z
           pzc z z<x = prev z z<x
           UZ : HOD
@@ -521,14 +520,14 @@
           total-UZ : IsTotalOrderSet UZ
           total-UZ {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 pchainf
-                   (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) _ _  ? (UChain.chain∋z (proj2 ca))) 
-                   (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) _ _  ? (UChain.chain∋z (proj2 cb)))
+               uz01 = chain-total A f mf ay {!!} {!!} {!!}
+                   -- (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) _ _  (UChain.chain∋z (proj2 ca))) 
+                   -- (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) _ _  (UChain.chain∋z (proj2 cb)))
           usup : SUP A UZ
           usup = supP UZ (λ lt → proj1 lt) total-UZ 
           spu = & (SUP.sup usup)
           sc4 :  ZChain1 A f mf ay x
-          sc4 = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 }  where
+          sc4 = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = {!!} }  where
             psup1 : Ordinal → Ordinal
             psup1 z with o≤? x z
             ... | yes _ = spu
@@ -541,9 +540,9 @@
             chainf1 z with o≤? x z
             ... | yes _  = record { od = record { def = λ w → odef A w ∧ FClosure A f spu w  } ; odmax = & A ; <odmax = {!!} }
             ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z
-            is-chain1 : (z w : Ordinal) → odef (chainf1 z) w → Chain A f mf ay (psup1 z ) w
+            is-chain1 : (z w : Ordinal) → odef (chainf1 z) w → Chain A f mf ay {!!} (psup1 z ) w
             is-chain1 z w lt with o≤? x z
-            ... | no z<x = ZChain1.is-chain (pzc z (o¬≤→< z<x)) z w lt
+            ... | no z<x = {!!} -- ZChain1.is-chain (pzc z (o¬≤→< z<x)) z w ? ?
             is-chain1 z w ⟪ ax , ux ⟫ | yes _ = ch-is-sup {!!} ux where
                 y<spu : y << spu
                 y<spu = {!!}
@@ -551,7 +550,7 @@
                 lty = {!!}
                 aspu : odef A spu
                 aspu = SUP.A∋maximal usup
-                is-sup : (x1 w₁ : Ordinal) → x1 o< & (SUP.sup usup) → Chain A f mf ay x1 w₁ → w₁ << & (SUP.sup usup)
+                is-sup : (x1 w₁ : Ordinal) → x1 o< & (SUP.sup usup) → Chain A f mf ay {!!} x1 w₁ → w₁ << & (SUP.sup usup)
                 is-sup = {!!}
 
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)