--- a/src/filter.agda	Wed Apr 06 17:46:41 2022 +0900
+++ b/src/filter.agda	Thu Apr 07 15:53:37 2022 +0900
@@ -231,13 +231,6 @@
  
 open import zorn
 
--- MaximumSubset' : {L P : HOD}
---        → o∅ o< & L →  o∅ o< & P → P ⊆ L
---        → PartialOrderSet O P (_⊆'_ O)
---        → ( (B : HOD) → B ⊆ P → TotalOrderSet O B (_⊆'_ O) → SUP O P B (_⊆'_ O) )
---        → Maximal O P (_⊆'_ O)
--- MaximumSubset' {L} {P} 0<L 0<P P⊆L PO SP  = Zorn-lemma O {P} {_⊆'_ O } 0<P PO SP
-
 MaximumFilterExist : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
        → (F : Filter LP) → o∅ o< & L →  o∅ o< & (filter F)  →  (¬ (filter F ∋ od∅)) → MaximumFilter LP 
 MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = {!!} where

--- a/src/zorn.agda	Wed Apr 06 17:46:41 2022 +0900
+++ b/src/zorn.agda	Thu Apr 07 15:53:37 2022 +0900
@@ -76,7 +76,7 @@
    field
       fb : Ordinal → HOD
       A∋fb : (ox : Ordinal ) → A ∋ fb ox
-      monotonic : (ox oy : Ordinal ) → ox o< y → ox o< oy → fb ox < fb oy 
+      monotonic : {ox oy : Ordinal } → ox o< y → ox o< oy → fb ox < fb oy 
 
 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
     → o∅ o< & A 
@@ -99,9 +99,8 @@
          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 (PO (me  A∋b) (me A∋a)) b<a ⟪ a<b , (λ b=a → proj1 (proj2 (PO (me  A∋b) (me A∋a)) b=a ) 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
      -- ZChain is not compatible with the SUP condition
      record BX (y : Ordinal) (fb : Ordinal → HOD ) : Set n where
         field
@@ -109,10 +108,23 @@
             is-fb : y ≡ & (fb bx )
      B :  (z : ZChain A (& A) _<_ ) → HOD
      B z = record { od = record { def = λ x → BX x ( 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))
+     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 )
+     obx=fb z {x} bx = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (BX.is-fb bx)) 
+     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 {!!} {!!} where
+         z10 : elm x < elm y 
+         z10 = subst₂ (λ j k → j < k ) (sym (z11 z x)) (sym (z11 z y)) (ZChain.monotonic z {!!} a ) 
+     ... | tri≈ ¬a b ¬c = tri≈ {!!} {!!} {!!}
+     ... | tri> ¬a ¬b c = tri> {!!} {!!} {!!}
      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)) }
      ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (B z) _<_ )
-     ZChain→¬SUP z sp = ⊥-elim (z02 (ZChain.fb z {!!}) {!!} {!!} ) where
+     ZChain→¬SUP z sp = ⊥-elim {!!} where
          z03 : & (SUP.sup sp) o< osuc (& A)
          z03 = ordtrans (c<→o< (SUP.A∋maximal sp)) <-osuc
          z02 :  (x : HOD) → B z ∋ x → SUP.sup sp < x → ⊥