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

diff -r 4fa7c5104b68 -r d2d704ab1a33 src/zorn.agda
--- a/src/zorn.agda	Thu Apr 07 19:08:15 2022 +0900
+++ b/src/zorn.agda	Fri Apr 08 17:36:42 2022 +0900
@@ -61,7 +61,7 @@
    field
       sup : HOD
       A∋maximal : A ∋ sup
-      x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total
+      x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 
 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
    field
@@ -107,23 +107,39 @@
             bx : Ordinal
             bx<y : bx o< y
             is-fb : x ≡ & (fb bx bx<y )
+     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)) {!!}
+     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 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 ) (bx<A z bx )
      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) }  
+     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 (_≅_ ) 
+     z12 : (z : ZChain A (& A) _<_ ) → {a b : HOD } → (x : BX (& a) (& A) (ZChain.fb z))  (y : BX (& b) (& A) (ZChain.fb z))
+          → obx z x ≡ obx z y → bx<A z x ≅ bx<A z y
+     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 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 {!!} {!!} 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< 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≈ {!!} {!!} {!!}
-     ... | 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) {!!} ) }
+     ... | 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)