# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657631737 -32400
# Node ID 29100f14bb97f5d8e304f558c3dbfb95875ea228
# Parent  3de5a1fb8011a0dad148d5f530b13c73897acd82
...

diff -r 3de5a1fb8011 -r 29100f14bb97 src/zorn.agda
--- a/src/zorn.agda	Tue Jul 12 15:49:49 2022 +0900
+++ b/src/zorn.agda	Tue Jul 12 22:15:37 2022 +0900
@@ -248,8 +248,8 @@
 
 record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (sup z : Ordinal) : Set n where
    field
-      y-init   : supf o∅  ≡ y
-      asup     : (x : Ordinal) → odef A (supf x)
+      -- y-init   : supf o∅  ≡ y
+      -- asup     : (x : Ordinal) → odef A (supf x)
       fcy<sup  : {z : Ordinal } → FClosure A f y z → z << supf sup
       csupz    : FClosure A f (supf sup) z 
       order    : {sup1 z1 : Ordinal} → (lt : sup1 o< sup ) → FClosure A f (supf sup1 ) z1 → z1 << supf sup
@@ -281,6 +281,7 @@
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
    field
       supf :  Ordinal → Ordinal 
+      is-sup : {b : Ordinal } → (ab : odef A b ) → IsSup A (UnionCF A f mf ay supf z ) ab → supf b ≡  b
       -- is-chain : {w : Ordinal } → Chain A f mf ay supf z w 
       -- supf-mono : (x y : Ordinal ) → x o≤ y  → supf x o≤ supf y
 
@@ -346,8 +347,8 @@
 
 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 )
-ChainP-next A f mf {y} ay supf {x} {z} cp = record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp 
-     ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
+ChainP-next A f mf {y} ay supf {x} {z} cp = record { -- asup = ChainP.asup cp --   y-init = ChainP.y-init cp ; 
+     fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
 
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
@@ -479,11 +480,13 @@
 
      sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
          → ((z : Ordinal) → z o< x → ZChain1 A f mf ay z ) → ZChain1 A f mf ay x
-     sind f mf {y} ay x prev  with trio< o∅ x
-     ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c )
-     ... | tri≈ ¬a b ¬c = record { supf = λ _ → y }
-     ... | tri< 0<x ¬b ¬c with Oprev-p x
-     ... | yes op = sc4 where
+     sind f mf {y} ay x prev = sc0 where
+        sc0 : ZChain1 A f mf ay x
+        sc0 with trio< y x
+        ... | tri> ¬a ¬b c = record { supf = λ _ → y ; is-sup = ? }
+        ... | tri≈ ¬a b ¬c = record { supf = λ _ → y ; is-sup = ? }
+        ... | tri< y<x ¬b ¬c with Oprev-p x
+        ... | yes op = sc4 where
           open ZChain1
           px = Oprev.oprev op
           px<x : px o< x
@@ -493,22 +496,47 @@
           pchain : HOD
           pchain  = UnionCF A f mf ay (ZChain1.supf sc) x
 
+          pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
+          pchain⊆A {y} ny = proj1 ny
+          psupf = ZChain1.supf sc
+          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 = 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
+            ... | 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 _ is-sup ) (fsuc _ fc)
+          ptotal : {a b : HOD } → odef pchain (& a) → odef pchain (& b)
+           →   Tri ( a <  b) ( a ≡  b) ( b <  a )
+          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 _ (UChain.chain∋z (proj2 ca)) (UChain.chain∋z (proj2 cb)) 
+          pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
+          pinit {a} ⟪ aa , ua ⟫  with UChain.chain∋z ua
+          ... | ch-init a fc = s≤fc y f mf fc
+          ... | ch-is-sup is-sup fc = ≤-ftrans (case2 zc7) (s≤fc _ f mf fc)  where
+             zc7 : y << psupf (UChain.u ua)
+             zc7 = ChainP.fcy<sup is-sup (init ay)
+          pcy : odef pchain y
+          pcy = ⟪ ay , record { u =  y ; u<x = y<x ; chain∋z = ch-init _ (init ay)  }  ⟫
+
           no-ext :  ZChain1 A f mf ay x
-          no-ext = record { supf = ZChain1.supf sc }  
+          no-ext = record { supf = ZChain1.supf sc ; is-sup = ? }  
           sc4 : ZChain1 A f mf ay x
           sc4 with ODC.∋-p O A (* x)
           ... | no noax = no-ext
           ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )   
           ... | case1 pr = no-ext
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A pchain ax )
-          ... | case1 is-sup = record { supf = psup1 } where
+          ... | case1 is-sup = record { supf = psup1 ; is-sup = ?} where
             psup1 : Ordinal → Ordinal
             psup1 z with trio< z x 
             ... | tri< a ¬b ¬c = ZChain1.supf sc z
             ... | tri≈ ¬a b ¬c = x
             ... | tri> ¬a ¬b c = x
           ... | case2 ¬x=sup = no-ext
-     ... | no ¬ox = sc4 where
+        ... | no ¬ox = sc4 where
           pzc : (z : Ordinal) → z o< x → ZChain1 A f mf ay z
           pzc z z<x = prev z z<x
           psupf : (z : Ordinal) → Ordinal
@@ -526,7 +554,7 @@
           usup = supP UZ (λ lt → proj1 lt) total-UZ 
           spu = & (SUP.sup usup)
           sc4 :  ZChain1 A f mf ay x
-          sc4 = record { supf = psup1 }  where
+          sc4 = record { supf = psup1 ; is-sup = ?}  where
             psup1 : Ordinal → Ordinal
             psup1 z with trio< z x 
             ... | tri< a ¬b ¬c = ZChain1.supf (pzc z a) z
@@ -569,7 +597,20 @@
             ( HasPrev A pchain ab f ∨ IsSup A pchain ab ) →
                 * a < * b → odef pchain b
         p-ismax {a} {b} ua b<ox ab (case1 hasp) a<b = ⟪ ab , ? ⟫
-        p-ismax {a} {b} ua b<ox ab (case2 sup)  a<b = ⟪ ab , ? ⟫
+        p-ismax {a} {b} ua b<ox ab (case2 sup)  a<b = ⟪ ab , record { u = b ; u<x =  ∈∧P→o< ⟪  ab , lift true  ⟫ ; chain∋z = zc5 }  ⟫ where
+             zc2 :  {sup1 z1 : Ordinal} → sup1 o< b →
+                FClosure A f (ZChain1.supf (zc0 (& A)) sup1) z1 → z1 << ZChain1.supf (zc0 (& A)) b
+             zc2 {sup1} {z1} s<b fsz = ? where
+                  zc8 : odef pchain z1
+                  zc8 = ?
+             zc4 : FClosure A f (ZChain1.supf (zc0 (& A)) b) b  --   
+             zc4 = subst (λ k → FClosure A f k b ) (sym (ZChain1.is-sup (zc0(& A)) ab sup )) (init ab)   
+             zc6 : {z : Ordinal} → FClosure A f y z → z << ZChain1.supf (zc0 (& A)) b
+             zc6 = ?
+             zc3 : ChainP A f mf ay (ZChain1.supf (zc0 (& A))) b b
+             zc3 = record { fcy<sup = zc6 ; csupz = zc4 ; order = zc2 }
+             zc5 :  Chain A f mf ay (ZChain1.supf (zc0 (& A))) b b
+             zc5 = ch-is-sup zc3 zc4
          
      SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f mf ay x
      SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f mf ay z} (sind f mf ay ) x