# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650293551 -32400
# Node ID 7e59e0aeaa73e581fe9e46d8a5ea1094e23bc794
# Parent  dea970e4526ecf635fc14ce5f4ba2858589ea1a0
give up for a while

diff -r dea970e4526e -r 7e59e0aeaa73 src/zorn.agda
--- a/src/zorn.agda	Mon Apr 18 11:09:52 2022 +0900
+++ b/src/zorn.agda	Mon Apr 18 23:52:31 2022 +0900
@@ -93,6 +93,7 @@
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
+-- Don't use Element other than Order, you'll be in a trouble
 -- postulate   -- may be proved by transfinite induction and functional extentionality
 --   ∋x-irr : (A : HOD) {x y : HOD} → x ≡ y → (ax : A ∋ x) (ay : A ∋ y ) → ax ≅ ay 
 --   odef-irr : (A : OD) {x y : Ordinal} → x ≡ y → (ax : def A x) (ay : def A y ) → ax ≅ ay 
@@ -106,6 +107,34 @@
 -- El-irr : {A : HOD} → {x y : Element A } → elm x ≡ elm y → x ≡ y
 -- El-irr {A} {x} {y} eq = El-irr2 A eq ( is-elm-irr A eq ) 
 
+record Set≈ (A B : Ordinal ) : Set n where
+   field
+       fun←  : {x : Ordinal } → odef (* A)  x → Ordinal
+       fun→  : {x : Ordinal } → odef (* B)  x → Ordinal
+       funB  : {x : Ordinal } → ( lt : odef (* A)  x ) → odef (* B) ( fun← lt )
+       funA  : {x : Ordinal } → ( lt : odef (* B)  x ) → odef (* A) ( fun→ lt )
+       fiso← : {x : Ordinal } → ( lt : odef (* B)  x ) → fun←  ( funA lt ) ≡ x
+       fiso→ : {x : Ordinal } → ( lt : odef (* A)  x ) → fun→  ( funB lt ) ≡ x
+
+open Set≈
+record OS≈ {A B : HOD} (TA : IsTotalOrderSet A ) (TB : IsTotalOrderSet B ) : Set (Level.suc n) where
+   field
+      iso : Set≈ (& A) (& B)
+      fmap : {x y : Ordinal} → (ax : odef A x) → (ay : odef A y) → * x < * y
+          → * (fun← iso (subst (λ k → odef k x) (sym *iso) ax)) < * (fun← iso (subst (λ k → odef k y) (sym *iso) ay))
+
+Cut< : ( A x : HOD )  → HOD
+Cut<  A x = record { od = record { def = λ y → ( odef A y ) ∧ ( x < * y ) } ; odmax = & A
+    ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (proj1 lt))) }
+
+Cut<TA : {A : HOD}   → (TA : IsTotalOrderSet A ) ( x : HOD )→  IsTotalOrderSet ( Cut< A x )
+Cut<TA {A} TA x =  record { isEquivalence = record { refl = refl ; trans = trans ; sym = sym }
+   ; trans = λ {x} {y} {z} → IsStrictTotalOrder.trans TA {me (proj1 (is-elm x))} {me (proj1 (is-elm y))} {me (proj1 (is-elm z))} ;
+        compare = λ x y → IsStrictTotalOrder.compare TA (me (proj1 (is-elm x))) (me (proj1 (is-elm y)))  }
+
+triTO : {A B : HOD} (TA : IsTotalOrderSet A ) (TB : IsTotalOrderSet B ) → {!!}
+triTO = {!!}
+
 record ZChain ( A : HOD ) (y : Ordinal)   : Set (Level.suc n) where
    field
       max : HOD
@@ -394,12 +423,57 @@
              y<z  = ic→< {A} PO y (subst (λ k → odef A k) &iso ay) (IChained.iy (proj2 icy))
                (subst (λ k → ic-connect k (IChained.iy (proj2 icy))) &iso (IChained.ic (proj2 icy)))
 
+
+record Indirect<  {x z : HOD} (x<z : x < z ) : Set (Level.suc n) where
+   field
+      y y1 : HOD
+      =∨< : ( y ≡ y1 ) ∨ ( y < y1 )
+      dirct : ¬ ( (x < y ) ∧ ( y1 < z ))
+
+record NChain ( A : HOD ) (f : { x : HOD} → A ∋ x → HOD) (min : HOD) : Set (Level.suc n) where
+   field
+      N : HOD
+      N⊆A : N ⊆ A
+      nmin : N ∋ min
+      is-min : (x : HOD) → N ∋ x → ( min ≡ x ) ∨ ( min < x )
+      total : IsTotalOrderSet N
+      A∋fx : { x : HOD} → (ax : A ∋ x ) → A ∋ f ax
+      atomic : { x y : HOD } → (nx : N ∋ x)  → (x<y : x < y)  → ¬ Indirect< x<y → y ≡ f (incl N⊆A nx )
+
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
       sup : HOD
       A∋maximal : A ∋ sup
       x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
+record Zfixpoint (A : HOD ) (f : { x : HOD} → A ∋ x → HOD) : Set (Level.suc n) where
+   field
+      fx  : HOD
+      afx : A ∋ fx 
+      is-fx : fx ≡ f afx 
+
+Zorn-fixpoint : { A : HOD } 
+    → o∅ o< & A 
+    → IsPartialOrderSet A 
+    → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
+    → (f : { x : HOD} → A ∋ x → HOD ) → ( A∋fx : {x : HOD}   (ax : A ∋ x ) → A ∋ f ax )
+    → (f≤ : {x : HOD} → (ax : A ∋ x ) → (x ≡ f ax ) ∨ (x < f ax ))
+    → Zfixpoint A f
+Zorn-fixpoint  = {!!}
+
+record Zmono (A : HOD ) : Set (Level.suc n) where
+   field
+      f : { x : HOD} → A ∋ x → HOD
+      A∋fx : { x : HOD} → (ax : A ∋ x ) → A ∋ f ax
+      monotonic : { x y : HOD} → (ax : A ∋ x )  → x < f ax
+
+Zorn-monotonic : { A : HOD } 
+    → o∅ o< & A 
+    → IsPartialOrderSet A 
+    → ¬ ( Maximal A )
+    → Zmono A
+Zorn-monotonic = {!!}
+
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
     → IsPartialOrderSet A 
@@ -423,13 +497,15 @@
               zc7 : A ∋ * (& (SUP.sup sup))
               zc7 = subst (λ k → odef A k ) (cong (&) (sym *iso)) (SUP.A∋maximal sup)
               sup-ics :  odef (IChainSet A ax) (& (SUP.sup sup))
-              sup-ics = ? -- SUP.A∋maximal sup
+              sup-ics = {!!} -- SUP.A∋maximal sup
               ncsup : (z : Ordinal) → (az : odef (IChainSet A ax) z)  → IChainSup> A {z} (subst (odef A) (sym &iso) (proj1 az)) 
               ncsup z az = InfiniteChain.c-infinite ifc z az
               nxa : A ∋ * nx
               nxa = {!!} -- cinext∈A A ax ifc (& (SUP.sup sup)) {!!}
           zc5 : InfiniteChain A max ax → ⊥
           zc5 ifc = zc6 ifc ( supP (InFCSet A ax ifc) (InFCSet⊆A A {x} ax ifc) (  ChainClosure-is-total  A {x} ax PO ifc ))
+     z03 : {x : Ordinal } → (ax : A ∋ * x ) → InfiniteChain A (& A)  ax  → ⊥
+     z03 {x}  ax ifc = {!!}
      -- ZChain is not compatible with the SUP condition
      ind : (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y ∨ Maximal A )
          →  ZChain A x ∨ Maximal A