# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649407644 -32400
# Node ID dc7a95dd66c49d64c8f27d79bfb1bbfb4244e549
# Parent  d2d704ab1a33ea6913f3a7a1d14bf5a7a3fe6086
...

diff -r d2d704ab1a33 -r dc7a95dd66c4 src/zorn.agda
--- a/src/zorn.agda	Fri Apr 08 17:36:42 2022 +0900
+++ b/src/zorn.agda	Fri Apr 08 17:47:24 2022 +0900
@@ -77,6 +77,7 @@
       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
+      injection : {ox oz : Ordinal } → (x<y : ox o< y ) → (z<y : oz o< y ) → fb ox x<y ≡ fb oz z<y → ox ≡ oz 
 
 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
     → o∅ o< & A 
@@ -129,9 +130,9 @@
      z12 z {a} {b} x y eq = {!!}
      bx-inject :  (z : ZChain A (& A) _<_ ) → {x y : Element (B z)} → BX.bx (is-elm x) ≡ BX.bx (is-elm y) → elm x ≡ elm y
      bx-inject z {x} {y} eq = begin
-            elm x ≡⟨ obx=fb z (is-elm x) ⟩
-            ZChain.fb z (obx z (is-elm x)) (bx<A z (is-elm x)) ≡⟨ cong₂ (λ j k → ZChain.fb z j k ) ? ( HE.≅-to-≡ (z12 z ? ? eq) ) ⟩
-            ZChain.fb z (obx z (is-elm y)) (bx<A z (is-elm y)) ≡⟨ sym ( obx=fb z (is-elm y) ) ⟩
+            elm x ≡⟨  {!!}   ⟩
+            {!!} ≡⟨ cong (λ k → {!!} ) ( ZChain.injection z {!!} {!!} ? )  ⟩
+            {!!} ≡⟨ {!!}   ⟩
             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))