# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1667517441 -32400
# Node ID 1ef03eedd148af25f2af419fe1f03d0148f6dd09
# Parent  33891adf80ea9152e8c4ff8930cda997ae358733
...

diff -r 33891adf80ea -r 1ef03eedd148 src/zorn.agda
--- a/src/zorn.agda	Fri Nov 04 06:47:23 2022 +0900
+++ b/src/zorn.agda	Fri Nov 04 08:17:21 2022 +0900
@@ -668,15 +668,11 @@
                     chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
               m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )
-                      ⟪ record { x≤sup = λ {z} uz → IsMinSup.x≤sup (proj2 is-sup) ?  -- (chain-mono1 (o<→≤ b<x) uz) 
-                          ; minsup = m07 }  , m04 ⟫ where
-                 m10 : {s : Ordinal }  →  (odef A s ) 
-                    →  ( {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s) ) 
-                    →    {z : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s)
-                 m10 = ?
+                      ⟪ record { x≤sup = λ {z} uz → IsMinSup.x≤sup (proj2 is-sup) uz  
+                          ; minsup = m07 ; not-hp = m04 }  , m04 ⟫ where
                  m07 :  {s : Ordinal} → odef A s → ({z : Ordinal} →
                      odef (UnionCF A f mf ay (ZChain.supf zc) b) z → (z ≡ s) ∨ (z << s)) → b o≤ s
-                 m07 {s} as s-is-sup = ? -- IsSup.minsup (proj2 is-sup) as (m10 as s-is-sup)
+                 m07 {s} as s-is-sup = IsMinSup.minsup (proj2 is-sup) as s-is-sup
               m08 : {z : Ordinal} → (fcz : FClosure A f y z ) → z <= ZChain.supf zc b
               m08 {z} fcz = ZChain.fcy<sup zc (o<→≤ b<A) fcz
               m09 : {s z1 : Ordinal} → ZChain.supf zc s o< ZChain.supf zc b 
@@ -709,8 +705,8 @@
                  ; x=fy = HasPrev.x=fy nhp } )
               m05 : ZChain.supf zc b ≡ b
               m05 = ZChain.sup=u zc ab (o<→≤  m09)
-                      ⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj2 is-sup) ? -- (chain-mono1 (o<→≤ b<x) lt )
-                         ; minsup = ? } , m04 ⟫    -- ZChain on x
+                      ⟪ record { x≤sup = λ lt → IsMinSup.x≤sup (proj2 is-sup) lt 
+                         ; minsup = IsMinSup.minsup (proj2 is-sup) ; not-hp = m04 } , m04 ⟫    -- ZChain on x
               m06 : ChainP A f mf ay supf b 
               m06 = record { fcy<sup = m07 ;  order = m08 ; supu=u = m05 }
 
@@ -1356,30 +1352,27 @@
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
                uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 
 
-     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
-         → (zc : ZChain A f mf ay x ) 
-         → SUP A (UnionCF A f mf ay (ZChain.supf zc) x)
-     sp0 f mf ay zc = M→S (ZChain.supf zc) (msp0 f mf ay zc )
-
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  (zc : ZChain A f mf as0 (& A) )
-            → (sp1 : SUP A (ZChain.chain zc))   -- & (SUP.sup (sp0 f mf as0 zc  ))
-            → (ssp<as :  ZChain.supf zc (& (SUP.sup sp1)) o< ZChain.supf zc (& A))
-            → f (& (SUP.sup sp1))  ≡ & (SUP.sup sp1) 
+            → (sp1 : MinSUP A (ZChain.chain zc))   -- & (SUP.sup (sp0 f mf as0 zc  ))
+            → (ssp<as :  ZChain.supf zc (MinSUP.sup sp1) o< ZChain.supf zc (& A))
+            → f (MinSUP.sup sp1)  ≡ MinSUP.sup sp1
      fixpoint f mf zc sp1 ssp<as = z14 where
            chain = ZChain.chain zc
            supf = ZChain.supf zc
            sp : Ordinal
-           sp = & (SUP.sup sp1)
+           sp = MinSUP.sup sp1
            asp : odef A sp
-           asp = SUP.as sp1
+           asp = MinSUP.asm sp1
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) 
               →  HasPrev A chain f b  ∨  IsMinSup A (UnionCF A f mf ab (ZChain.supf zc) b) f ab
               → * a < * b  → odef chain b
            z10 = ? -- ZChain1.is-max (SZ1 f mf as0 zc (& A) )
            z22 : sp o< & A
            z22 = z09 asp
-           x≤sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 )
-           x≤sup bz = SUP.x≤sup sp1 bz 
+           x≤sup : {x : HOD} → chain ∋ x → (& x ≡ sp ) ∨ (x < * sp )
+           x≤sup bz with MinSUP.x≤sup sp1 bz 
+           ... | case1 eq = ?
+           ... | case2 lt = ?
            z12 : odef chain sp
            z12 with o≡? (& s) sp
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
@@ -1387,33 +1380,33 @@
                 (case2 z19 ) z13 where
                z13 :  * (& s) < * sp
                z13 with x≤sup ( ZChain.chain∋init zc )
-               ... | case1 eq = ⊥-elim ( ne (cong (&) eq) )
-               ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
+               ... | case1 eq = ⊥-elim ( ne ? )
+               ... | case2 lt = ? -- subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt
                z19 : IsMinSup A (UnionCF A f mf as0 (ZChain.supf zc) sp) f asp
-               z19 = record {   x≤sup = ? ; minsup = ? }  where
-                   z20 :  {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1))
-                   z20 {y} zy with x≤sup (subst (λ k → odef chain k ) (sym &iso) zy)
-                   ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
-                   ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
+               z19 = record {   x≤sup = z20 ; minsup = ?  ; not-hp = ? }  where
+                   z20 : {y : Ordinal} → odef (UnionCF A f mf as0 (ZChain.supf zc) sp) y → (y ≡ sp) ∨ (y << sp)
+                   z20 {y} zy with x≤sup (subst (λ k → odef chain k ) (sym &iso) ?)
+                   ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ? ) -- ( cong (&) y=p ))
+                   ... | case2 y<p = case2 ? -- (subst (λ k → * y < k ) (sym *iso) y<p )
            ztotal : IsTotalOrderSet (ZChain.chain zc)
            ztotal {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 as0 supf ( (proj2 ca)) ( (proj2 cb)) 
            z14 :  f sp ≡ sp
-           z14 with ztotal (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
+           z14 with ztotal (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) ?
            ... | tri< a ¬b ¬c = ⊥-elim z16 where
                z16 : ⊥
-               z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 ))
-               ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
-               ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
-           ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
+               z16 with proj1 (mf (( MinSUP.sup sp1)) ( MinSUP.asm sp1 ))
+               ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym ? ) ))
+               ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso ? ))
+           ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ (MinSUP.sup sp1) ) &iso ? -- ( cong (&) b )
            ... | tri> ¬a ¬b c = ⊥-elim z17 where
-               z15 : (* (f sp) ≡ SUP.sup sp1) ∨ (* (f sp) <  SUP.sup sp1 )
-               z15  = x≤sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
+               z15 : (f sp ≡ MinSUP.sup sp1) ∨ (* (f sp) < * (MinSUP.sup sp1) )
+               z15  = ? -- x≤sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
                z17 : ⊥
                z17 with z15
-               ... | case1 eq = ¬b eq
-               ... | case2 lt = ¬a lt
+               ... | case1 eq = ¬b ?
+               ... | case2 lt = ¬a ?
 
      tri : {n : Level} (u w : Ordinal ) { R : Set n }  → ( u o< w → R ) → ( u ≡  w → R ) → ( w o< u → R ) → R
      tri {_} u w p q r with trio< u w
@@ -1433,24 +1426,22 @@
      --
 
      z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥
-     z04 nmx zc = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as  sp1 ))))
-                                               (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) )
-           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc 
-               (sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc  )  ss<sa ))) -- x ≡ f x ̄
-           (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where          -- x < f x
+     z04 nmx zc = <-irr0  {* (cf nmx c)} {* c} 
+           (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (MinSUP.asm  msp1 )))) 
+           (subst (λ k → odef A k) ? (MinSUP.asm msp1) )
+           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc msp1  ss<sa ))) -- x ≡ f x ̄
+                (proj1 (cf-is-<-monotonic nmx c (MinSUP.asm msp1 ))) where          -- x < f x
 
           supf = ZChain.supf zc
           msp1 : MinSUP A (ZChain.chain zc)
           msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 
-          sp1 : SUP A (ZChain.chain zc)
-          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 
           c : Ordinal 
-          c = & ( SUP.sup sp1 )
-          mc = MinSUP.sup msp1
+          c = MinSUP.sup msp1 
+          mc = c
           mc<A : mc o< & A
           mc<A =  ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫
           c=mc : c ≡ mc
-          c=mc = &iso
+          c=mc = refl
           z20 : mc << cf nmx mc 
           z20 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1) )
           asc : odef A (supf mc)