# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1648032478 -32400
# Node ID c70cf01b29f952e59e643d894f98203dd6e98fc5
# Parent  c65cb6c07a381b51e6c9b9689c68bf66ad2600a8
...

diff -r c65cb6c07a38 -r c70cf01b29f9 src/ODC.agda
--- a/src/ODC.agda	Wed Mar 23 16:42:42 2022 +0900
+++ b/src/ODC.agda	Wed Mar 23 19:47:58 2022 +0900
@@ -106,11 +106,13 @@
 OrdP  x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
 OrdP  x y | tri> ¬a ¬b c = yes c
 
+TotalOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
+TotalOrderSet A _<_ = {a b : HOD} → A ∋ a → A ∋ b → (a < b) ∨ (a ≡ b) ∨ (b < a )
+
 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
       sup : HOD
       A∋maximal : A ∋ sup
-      tri : {a b : HOD} → B ∋ a → B ∋ b → (a < b) ∨ (a ≡ b) ∨ (b < a )
       x≤sup : (x : HOD) → B ∋ x → (x ≡ sup ) ∨ (x < sup )
 
 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
@@ -123,20 +125,28 @@
    field
       B : HOD
       B⊆A : B ⊆ A 
-      tri : {a b : HOD} → B ∋ a → B ∋ b → (a < b) ∨ (a ≡ b) ∨ (b < a )
+      total : TotalOrderSet B _<_
       fb : {x : HOD } → A ∋ x  → HOD
       B∋fb : (x : HOD ) → (ax : A ∋ x)  → B ∋ fb ax
       ¬x≤sup : (sup : HOD) → (as : A ∋ sup ) → & sup o< y → sup < fb as
 
 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
     → o∅ o< & A 
-    → ( ( B : HOD) → (B⊆A : B ⊆ A) → SUP A B  _<_  )
+    → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B  _<_  )
     → Maximal A _<_ 
 Zorn-lemma {A} {_<_} 0<A supP = zorn00 where
      HasMaximal : HOD
      HasMaximal = record { od = record { def = λ x → (m : Ordinal) → odef A x ∧ odef A m ∧ (¬ (* x < * m))} ; odmax = & A ; <odmax = {!!} }
      ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (ZChain.B z) _<_ )
-     ZChain→¬SUP z sp = {!!}
+     ZChain→¬SUP z sp = ⊥-elim {!!}
+     zeron01 : {B a b : HOD} → TotalOrderSet B _<_ → B ∋ a → B ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
+     zeron01 {B} {a} {b} Tri s t (case1 a=b) v = {!!}
+     -- with Tri s t | inspect (Tri s) t
+     -- ... | case1 x | [ eq ] = {!!}
+     -- ... | case2 (case1 x) | [ eq ] = {!!}
+     -- ... | case2 (case2 x) | [ eq ] = {!!}
+     zeron01 {B} {a} {b} Tri s t (case2 a<b) v = {!!}
+     -- with Tri s t | inspect (Tri s) t
      ind :  (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y _<_ )
          →  ZChain A x _<_
      ind x prev with Oprev-p x
@@ -148,9 +158,10 @@
      zorn00 : Maximal A _<_
      zorn00 with is-o∅ ( & HasMaximal )
      ... | no not = record { maximal = minimal HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = {!!}; ¬maximal<x  = {!!} }
-     ... | yes ¬Maximal = ⊥-elim ( ZChain→¬SUP (z (& A)) ( supP (ZChain.B (z (& A))) (ZChain.B⊆A (z (& A))) ) ) where
+     ... | yes ¬Maximal = ⊥-elim ( ZChain→¬SUP (z (& A)) ( supP B (ZChain.B⊆A (z (& A))) (ZChain.total (z (& A)))) ) where
          z : (x : Ordinal) → ZChain A x _<_ 
          z = TransFinite ind 
+         B = ZChain.B (z (& A))
 
 open import zfc