# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649234801 -32400
# Node ID 419a3f4d5d97a9b575944740f4dbc5f14987b3f4
# Parent  ed29002a02b6e018d096b1eb01344742813d7ed2
...

diff -r ed29002a02b6 -r 419a3f4d5d97 src/zorn.agda
--- a/src/zorn.agda	Wed Apr 06 14:22:18 2022 +0900
+++ b/src/zorn.agda	Wed Apr 06 17:46:41 2022 +0900
@@ -75,7 +75,7 @@
 record ZChain ( A : HOD ) (y : Ordinal)  (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
       fb : Ordinal → HOD
-      A∋fb : (ox : Ordinal ) → ox o< y  → A ∋ fb ox
+      A∋fb : (ox : Ordinal ) → A ∋ fb ox
       monotonic : (ox oy : Ordinal ) → ox o< y → ox o< oy → fb ox < fb oy 
 
 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
@@ -103,14 +103,20 @@
      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 ) ⟫
      -- ZChain is not compatible with the SUP condition
+     record BX (y : Ordinal) (fb : Ordinal → HOD ) : Set n where
+        field
+            bx : Ordinal
+            is-fb : y ≡ & (fb bx )
      B :  (z : ZChain A (& A) _<_ ) → HOD
-     B = {!!}
+     B z = record { od = record { def = λ x → BX x ( ZChain.fb z )  } ; odmax = & A ; <odmax = {!!} }
+     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 {!!} where
+     ZChain→¬SUP z sp = ⊥-elim (z02 (ZChain.fb z {!!}) {!!} {!!} ) 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 → ⊥
-         z02 x xe s<x = {!!} -- z01 (incl (ZChain.B⊆A z) xe) (SUP.A∋maximal sp) (SUP.x≤sup sp xe) s<x 
+         z02 x xe s<x = z01 (incl (B⊆A z) xe) (SUP.A∋maximal sp) (SUP.x≤sup sp xe) s<x 
      ind :  HasMaximal =h= od∅
          → (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y _<_ )
          →  ZChain A x _<_