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

diff -r c70cf01b29f9 -r 69f90d8d0607 src/ODC.agda
--- a/src/ODC.agda	Wed Mar 23 19:47:58 2022 +0900
+++ b/src/ODC.agda	Wed Mar 23 21:42:12 2022 +0900
@@ -106,20 +106,35 @@
 OrdP  x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
 OrdP  x y | tri> ¬a ¬b c = yes c
 
+open import Relation.Binary.HeterogeneousEquality as HE -- using (_≅_;refl)
+
+record Element (A : HOD) : Set (suc n) where
+    field
+       elm : HOD
+       is-elm : A ∋ elm
+
+open Element
+
 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 )
+TotalOrderSet A _<_ = Trichotomous (λ (x : Element A) y → elm x ≡ elm y ) (λ x y → elm x < elm y )  
+
+me : { A a : HOD } → A ∋ a → Element A
+me {A} {a} lt = record { elm = a ; is-elm = lt }
+
+-- elm-cmp : {A a b : HOD} → {_<_ : (x y : HOD) → Set n }  → A ∋ a →  A ∋ b →  TotalOrderSet A _<_  → Tri _ _ _
+-- elm-cmp {A} {a} {b} ax bx cmp = cmp (me ax) (me bx)
 
 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
       sup : HOD
       A∋maximal : A ∋ sup
-      x≤sup : (x : HOD) → B ∋ x → (x ≡ sup ) ∨ (x < sup )
+      x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )
 
 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
       maximal : HOD
       A∋maximal : HOD
-      ¬maximal<x : (x : HOD) → (b : A ∋ x ) → ¬ maximal < x
+      ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x
 
 record ZChain ( A : HOD ) (y : Ordinal)  (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
@@ -137,16 +152,19 @@
 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 = {!!} }
+     z01 : {B a b : HOD} → TotalOrderSet B _<_ → B ∋ a → B ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
+     z01 {B} {a} {b} Tri  B∋a  B∋b (case1 a=b) b<a with Tri (me  B∋a) (me B∋b) 
+     ... | tri< a₁ ¬b ¬c = ¬b  a=b
+     ... | tri≈ ¬a b₁ ¬c = ¬c b<a
+     ... | tri> ¬a ¬b c = ¬b a=b
+     z01 {B} {a} {b} Tri  B∋a  B∋b (case2 a<b) b<a with Tri (me  B∋a) (me B∋b) 
+     ... | tri< a₁ ¬b ¬c = ¬c b<a
+     ... | tri≈ ¬a b₁ ¬c = ¬c b<a
+     ... | tri> ¬a ¬b c = ¬a a<b
      ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (ZChain.B z) _<_ )
-     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
+     ZChain→¬SUP z sp = ⊥-elim {!!} where
+         z02 :  (x : HOD) → ZChain.B z ∋ x → ⊥
+         z02 x xe = ( z01 (ZChain.total z) xe {!!} (SUP.x≤sup sp xe) {!!} )
      ind :  (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y _<_ )
          →  ZChain A x _<_
      ind x prev with Oprev-p x