# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649423945 -32400
# Node ID 646831f6b06d4301f3d710cfa940b74062669cee
# Parent  00c71d1dc316f2dbb174fdb8158dbc44d3700131
...

diff -r 00c71d1dc316 -r 646831f6b06d src/zorn.agda
--- a/src/zorn.agda	Fri Apr 08 22:03:01 2022 +0900
+++ b/src/zorn.agda	Fri Apr 08 22:19:05 2022 +0900
@@ -47,13 +47,6 @@
 
 open Element
 
-TotalOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
-TotalOrderSet A _<_ = Trichotomous (λ (x : Element A) y → elm x ≡ elm y ) (λ x y → elm x < elm y )  
-
-PartialOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
-PartialOrderSet A _<_ = (a b :  Element A)
-     → (elm a < elm b → ((¬ elm b < elm a) ∧ (¬ (elm a ≡ elm b) ))) ∧ (elm a ≡ elm b → (¬ elm a < elm b) ∧ (¬ elm b < elm a))
-
 IsPartialOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
 IsPartialOrderSet A _<_ = IsPartialOrder _<A_ _≡A_ where
    _<A_ : (x y : Element A ) → Set n
@@ -88,14 +81,15 @@
 
 record ZChain ( A : HOD ) (y : Ordinal)  (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
-      fb : (x : Ordinal ) → x o< y → HOD
-      A∋fb : (ox : Ordinal ) → (x<y : ox o< y )  → A ∋ fb ox x<y
-      monotonic : {ox oz : Ordinal } → (x<y : ox o< y ) → (z<y : oz o< y ) → ox o< oz → fb ox x<y < fb oz z<y
+      fb : (x : Ordinal ) → HOD
+      A∋fb : (ox : Ordinal ) → ox o< y → A ∋ fb ox 
+      total : {ox oz : Ordinal } → (x<y : ox o< y ) → (z<y : oz o< y ) → ( ox ≡ oz ) ∨ ( fb ox < fb oz ) ∨ ( fb oz < fb ox  )
+      monotonic : {ox oz : Ordinal } → (x<y : ox o< y ) → (z<y : oz o< y ) → ox o< oz → fb ox < fb oz 
 
 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
     → o∅ o< & A 
-    → PartialOrderSet A _<_
-    → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B  _<_  ) -- SUP condition
+    → IsPartialOrderSet A _<_
+    → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B _<_ → SUP A B  _<_  ) -- SUP condition
     → Maximal A _<_ 
 Zorn-lemma {A} {_<_} 0<A PO supP = zorn00 where
      someA : HOD
@@ -113,28 +107,28 @@
          z09 : {y : Ordinal} → (odef A y ∧ (x < (* y)))  → y o< & A
          z09 {y} P = subst (λ k → k o< & A) &iso (c<→o< {* y} (subst (λ k → odef A k) (sym &iso) (proj1 P)))
      z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
-     z01 {a} {b} A∋a A∋b (case1 a=b) b<a = proj1 (proj2 (PO (me A∋b) (me A∋a)) (sym a=b)) b<a
-     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = proj1 (proj1 (PO (me A∋b) (me A∋a)) b<a) a<b
+     z01 {a} {b} A∋a A∋b (case1 a=b) b<a = {!!} -- proj1 (proj2 (PO (me A∋b) (me A∋a)) (sym a=b)) b<a
+     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = {!!} -- proj1 (proj1 (PO (me A∋b) (me A∋a)) b<a) a<b
      -- ZChain is not compatible with the SUP condition
-     record BX (x y : Ordinal) (fb : ( x : Ordinal ) → (x o< y ) → HOD ) : Set n where
+     record BX (x y : Ordinal) (fb : ( x : Ordinal ) → HOD ) : Set n where
         field
             bx : Ordinal
             bx<y : bx o< y
-            is-fb : x ≡ & (fb bx bx<y )
+            is-fb : x ≡ & (fb bx )
      bx<A : (z : ZChain A (& A) _<_ ) → {x : Ordinal } → (bx : BX x (& A) ( ZChain.fb z ))  → BX.bx bx o< & A
      bx<A z {x} bx = BX.bx<y bx
      B :  (z : ZChain A (& A) _<_ ) → HOD
      B z = record { od = record { def = λ x → BX x (& A) ( ZChain.fb z )  } ; odmax = & A ; <odmax = {!!} }
-     z11 :  (z : ZChain A (& A) _<_ ) → (x : Element (B z)) → elm x ≡  ZChain.fb z (BX.bx (is-elm x)) (bx<A z (is-elm x))
+     z11 :  (z : ZChain A (& A) _<_ ) → (x : Element (B z)) → elm x ≡  ZChain.fb z ?
      z11 z x = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong (*) (BX.is-fb (is-elm x)) )
      obx : (z : ZChain A (& A) _<_ ) → {x : HOD} → B z ∋ x → Ordinal
      obx z {x} bx = BX.bx bx
-     obx=fb : (z : ZChain A (& A) _<_ ) → {x : HOD} → (bx : B z ∋ x ) → x ≡ ZChain.fb z ( obx z bx ) (bx<A z bx )
+     obx=fb : (z : ZChain A (& A) _<_ ) → {x : HOD} → (bx : B z ∋ x ) → x ≡ ZChain.fb z {!!}
      obx=fb z {x} bx = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (BX.is-fb bx)) 
      B⊆A : (z : ZChain A (& A) _<_ ) → B z ⊆ A
      B⊆A z = record { incl = λ {x} bx → subst (λ k → odef A k ) (sym (BX.is-fb bx)) (ZChain.A∋fb z (BX.bx bx) (BX.bx<y bx) ) }
-     PO-B : (z : ZChain A (& A) _<_ ) → PartialOrderSet (B z) _<_
-     PO-B z a b = PO record { elm = elm a ; is-elm = incl ( B⊆A z) (is-elm a) }  record { elm = elm b ; is-elm = incl ( B⊆A z) (is-elm b) }  
+     PO-B : (z : ZChain A (& A) _<_ ) → IsPartialOrderSet (B z) _<_
+     PO-B z = ? -- a b = {!!} -- PO record { elm = elm a ; is-elm = incl ( B⊆A z) (is-elm a) }  record { elm = elm b ; is-elm = incl ( B⊆A z) (is-elm b) }  
      bx-monotonic : (z : ZChain A (& A) _<_ ) → {x y : Element (B z)} → obx z (is-elm x) o< obx z (is-elm y) → elm x < elm y 
      bx-monotonic z {x} {y} a = subst₂ (λ j k → j < k ) (sym (z11 z x)) (sym (z11 z y)) (ZChain.monotonic z (bx<A z (is-elm x)) (bx<A z (is-elm y)) a ) 
      open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
@@ -147,13 +141,15 @@
             {!!} ≡⟨ cong (λ k → {!!} ) {!!}  ⟩
             {!!} ≡⟨ {!!}   ⟩
             elm y ∎ where open ≡-Reasoning
-     B-is-total :  (z : ZChain A (& A) _<_ ) → TotalOrderSet (B z) _<_ 
-     B-is-total z x y with trio< (obx z (is-elm x)) (obx z (is-elm y))
-     ... | tri< a ¬b ¬c = tri< z10 (λ eq → proj1 (proj2 (PO-B z x y) eq ) z10) (λ ¬c → proj1 (proj1 (PO-B z y x) ¬c ) z10) where
+     B-is-total :  (z : ZChain A (& A) _<_ ) → IsTotalOrderSet (B z) _<_ 
+     B-is-total = ?
+     B-Tri : (z : ZChain A (& A) _<_ ) → Trichotomous (λ (x : Element A) y → elm x ≡ elm y ) (λ x y → elm x < elm y )
+     B-Tri z x y with trio< (obx z ?) (obx z ?)
+     ... | tri< a ¬b ¬c = ? where -- tri< z10 (λ eq → proj1 (proj2 (PO-B z x y) eq ) z10) (λ ¬c → proj1 (proj1 (PO-B z y x) ¬c ) z10) where
           z10 : elm x < elm y
-          z10 = bx-monotonic z {x} {y} a
-     ... | tri≈ ¬a b ¬c = tri≈ {!!} (bx-inject z {x} {y} b) {!!}
-     ... | tri> ¬a ¬b c = tri> (λ ¬a → proj1 (proj1 (PO-B z x y) ¬a ) (bx-monotonic z {y} {x} c) ) (λ eq → proj2 (proj2 (PO-B z x y) eq ) (bx-monotonic z {y} {x} c)) (bx-monotonic z {y} {x} c)
+          z10 = ? -- bx-monotonic z {x} {y} a
+     ... | tri≈ ¬a b ¬c = ? -- tri≈ {!!} (bx-inject z {x} {y} b) {!!}
+     ... | tri> ¬a ¬b c = ? -- tri> (λ ¬a → proj1 (proj1 (PO-B z x y) ¬a ) (bx-monotonic z {y} {x} c) ) (λ eq → proj2 (proj2 (PO-B z x y) eq ) (bx-monotonic z {y} {x} c)) (bx-monotonic z {y} {x} c)
      ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (B z) _<_ )
      ZChain→¬SUP z sp = ⊥-elim {!!} where
          z03 : & (SUP.sup sp) o< osuc (& A)
@@ -223,7 +219,7 @@
 
 MaximumSubset : {L P : HOD} 
        → o∅ o< & L →  o∅ o< & P → P ⊆ L
-       → PartialOrderSet P _⊆'_
-       → ( (B : HOD) → B ⊆ P → TotalOrderSet B _⊆'_ → SUP P B _⊆'_ )
+       → IsPartialOrderSet P _⊆'_
+       → ( (B : HOD) → B ⊆ P → IsTotalOrderSet B _⊆'_ → SUP P B _⊆'_ )
        → Maximal P (_⊆'_)
 MaximumSubset {L} {P} 0<L 0<P P⊆L PO SP  = Zorn-lemma {P} {_⊆'_} 0<P PO SP