# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655139031 -32400
# Node ID 7a6d3f3493954aa0ba3c3c2bfd2bb46d21bc43d4
# Parent  2595d2f6487be61276e366779a5735b3484db4da
...

diff -r 2595d2f6487b -r 7a6d3f349395 src/zorn.agda
--- a/src/zorn.agda	Tue Jun 14 00:44:43 2022 +0900
+++ b/src/zorn.agda	Tue Jun 14 01:50:31 2022 +0900
@@ -240,15 +240,14 @@
 ... | case1 eq = subst (λ k → odef A k ) (sym (trans eq &iso)) ay
 ... | case2 eq = subst (λ k → odef A k ) (sym (trans eq &iso)) ay
 
-record FChain ( A : HOD ) ( f : Ordinal → Ordinal ) (p : Ordinal)   ( x : Ordinal ) : Set n where
+record FChain ( A : HOD ) ( f : Ordinal → Ordinal ) (p c : Ordinal)   ( x : Ordinal ) : Set n where
    field
-      ax : odef A x
-      fc∨sup :  FClosure A f p x ∨ ((a : Ordinal) → FClosure A f p a → (a ≡ x) ∨ (a << x) )
-      f-min : (x1 : Ordinal) → ( (a : Ordinal) → FClosure A f p a → (a ≡ x1 ) ∨ (a << x1) ) → FClosure A f p x1 ∨ ( x o≤ x1 )
+      fc∨sup :  FClosure A f p x
+      chain∋p : odef (* c) p 
 
-data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) : (x : Ordinal) → Set n where
-      Finit :  {z : Ordinal} → z ≡ y  → Fc∨sup A ay f z
-      Fc  :  {p x : Ordinal} → p o< osuc x → Fc∨sup A ay f p  → FChain A f p x →  Fc∨sup A ay f x
+data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) (c : Ordinal) : (x : Ordinal) → Set n where
+      Finit :  {z : Ordinal} → z ≡ y  → Fc∨sup A ay f c z
+      Fc  :  {p x : Ordinal} → p o< x → Fc∨sup A ay f c p  → FChain A f p c x →  Fc∨sup A ay f c x
 
 record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
    field
@@ -262,7 +261,7 @@
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
-      fc∨sup :  {c : Ordinal } → ( ca : odef chain c )  → Fc∨sup A (chain⊆A chain∋x) f c 
+      fc∨sup :  {c : Ordinal } → ( ca : odef chain c )  → Fc∨sup A (chain⊆A chain∋x) f (& chain) c 
 
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
@@ -591,31 +590,23 @@
                  → ((j : Ordinal) → j o< i →  odef (chain za) j → odef (chain zb) j)
                  → odef (chain za) i → odef (chain zb) i
             uind i previ zai = um01 where
-                FC : Fc∨sup A (chain⊆A za (chain∋x za)) f i 
+                FC : Fc∨sup A (chain⊆A za (chain∋x za)) f (& (chain za)) i 
                 FC = fc∨sup za zai 
-                -- y≤fc : {a p : Ordinal} → Fc∨sup A p f i → * y ≤ * p
-                -- y≤fc =  {!!}
                 um01 : odef (chain zb) i
                 um01 with FC
                 ... | Finit i=y = subst (λ k → odef (chain zb) k ) (sym i=y) ( chain∋x zb )
-                ... | Fc {p} {i} p≤i pFC fc with initial za zai
-                ... | case1 y=i = subst (λ k → odef (chain zb) k ) (subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) y=i)) ( chain∋x zb )
-                ... | case2 y<i with (FChain.fc∨sup fc) 
-                ... | case1 fc = um02 i fc where
+                ... | Fc {p} {i} p<i pFC FC with (FChain.fc∨sup FC) 
+                ... | fc = um02 i fc where
                      um02 : (i2 : Ordinal) → FClosure A f p i2 → odef (chain zb) i2
-                     um02 i2 (init ap i=p ) = subst (λ k → odef (chain zb) k ) (sym i=p) (previ p um03 um04 ) where
-                        um03 : p o< i
-                        um03 = {!!}
+                     um02 i2 (init ap i2=p ) = subst (λ k → odef (chain zb) k ) (sym i2=p) (previ p p<i um04 ) where
                         um04 : odef (chain za) p
-                        um04 = {!!}
+                        um04 = subst (λ k → odef k p ) *iso ( FChain.chain∋p FC )
                      um02 i (fsuc j fc) = f-next zb ( um02 j fc )
-                ... | case2 sup = {!!}
-                -- is-max zb (chain∋x zb) {!!} (chain⊆A za zai) {!!} y<i where
-                --     pFC0 : Fc∨sup A (chain⊆A za (chain∋x za)) f p
-                --     pFC0 = pFC
          u-total : IsTotalOrderSet Uz
-         u-total {x} {y} ux uy = {!!}
-         --- ux ⊆ uy ∨ uy ⊆ ux
+         u-total {x} {y} ux uy  with trio< (UZFChain.u ux) (UZFChain.u uy)
+         ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-mono (UZFChain.u ux) (UZFChain.u uy) {!!} {!!} (uzc ux) (uzc uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
+         ... | tri≈ ¬a b ¬c = tri≈ {!!} {!!} {!!}
+         ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux) {!!} {!!} (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
          
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM