# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649326095 -32400
# Node ID 4fa7c5104b683abf8b54ab731db41a2c80710171
# Parent  d2f204c5d67b4f2e7f17983832c051da4c10b665
...

diff -r d2f204c5d67b -r 4fa7c5104b68 src/zorn.agda
--- a/src/zorn.agda	Thu Apr 07 16:23:54 2022 +0900
+++ b/src/zorn.agda	Thu Apr 07 19:08:15 2022 +0900
@@ -74,9 +74,9 @@
 
 record ZChain ( A : HOD ) (y : Ordinal)  (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
-      fb : Ordinal → HOD
-      A∋fb : (ox : Ordinal ) → A ∋ fb ox
-      monotonic : {ox oy : Ordinal } → oy o< y → ox o< oy → fb ox < fb oy 
+      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
 
 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
     → o∅ o< & A 
@@ -102,27 +102,28 @@
      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
+     record BX (x y : Ordinal) (fb : ( x : Ordinal ) → (x o< y ) → HOD ) : Set n where
         field
             bx : Ordinal
-            is-fb : y ≡ & (fb bx )
+            bx<y : bx o< y
+            is-fb : x ≡ & (fb bx bx<y )
      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))
+     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)) {!!}
      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 : 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 ) 
+         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)) }
+     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
          z03 : & (SUP.sup sp) o< osuc (& A)