# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649480209 -32400
# Node ID c03d80290855b20afcfd49028648b5e6c56e2aa1
# Parent  4203ba14fd5369a99aacff17dab5775511834e24
total of B

diff -r 4203ba14fd53 -r c03d80290855 src/zorn.agda
--- a/src/zorn.agda	Sat Apr 09 10:38:15 2022 +0900
+++ b/src/zorn.agda	Sat Apr 09 13:56:49 2022 +0900
@@ -76,10 +76,12 @@
    resp0 = Data.Product._,_  (λ {x} {y} {z} → proj₁ (IsStrictPartialOrder.<-resp-≈ PA) {isA B⊆A x } {isA B⊆A y }{isA B⊆A z }) 
                              (λ {x} {y} {z} → proj₂ (IsStrictPartialOrder.<-resp-≈ PA) {isA B⊆A x } {isA B⊆A y }{isA B⊆A z })
 
+open import Relation.Binary.Properties.Poset as Poset
+
 IsTotalOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
-IsTotalOrderSet A _<_ = IsTotalOrder  _≡A_ _≤A_ where
-   _≤A_ : (x y : Element A ) → Set (suc n)
-   x ≤A y = (elm x ≡ elm y) ∨ (elm x < elm y)
+IsTotalOrderSet A _<_ = IsStrictTotalOrder  _≡A_ _<A_ where
+   _<A_ : (x y : Element A ) → Set n
+   x <A y = elm x < elm y
    _≡A_ : (x y : Element A ) → Set (suc n)
    x ≡A y = elm x ≡ elm y
 
@@ -127,8 +129,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 (proj1 (PO (me A∋b) (me A∋a)) b<a) a<b
+     z01 {a} {b} A∋a A∋b (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋a} (sym a=b) b<a
+     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋b} refl (IsStrictPartialOrder.trans PO {me A∋b} {me A∋a} {me A∋b}  b<a a<b)
      -- ZChain is not compatible with the SUP condition
      record BX (x y : Ordinal) (fb : ( x : Ordinal ) → HOD ) : Set n where
         field
@@ -137,8 +139,10 @@
             is-fb : x ≡ & (fb bx )
      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
+     z12 : (z : ZChain A (& A) _<_ ) →  {y : Ordinal} → BX y (& A) (ZChain.fb z) → y o< & A
+     z12 z {y} bx = subst (λ k → k o< & A) (sym (BX.is-fb bx)) (c<→o< (ZChain.A∋fb z (BX.bx 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 = {!!} }
+     B z = record { od = record { def = λ x → BX x (& A) ( ZChain.fb z )  } ; odmax = & A ; <odmax = z12 z } 
      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
@@ -148,31 +152,33 @@
      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) _<_ ) → IsPartialOrderSet (B z) _<_
-     PO-B z = subst₂ (λ j k → IsStrictPartialOrder j k ) {!!} {!!} {!!} where
-           _<B_ = {!!}
-           _≡B_ = {!!}
-        -- 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) }  
+     PO-B z = ⊆-IsPartialOrderSet (B⊆A z) PO
      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 ≡⟨  {!!}   ⟩
-            {!!} ≡⟨ cong (λ k → {!!} ) {!!}  ⟩
-            {!!} ≡⟨ {!!}   ⟩
-            elm y ∎ where open ≡-Reasoning
+     bcmp : (z : ZChain A (& A) _<_ ) → Trichotomous (λ (x : Element (B z)) y → elm x ≡ elm y ) (λ x y → elm x < elm y )
+     bcmp z x y with trio< (obx z (is-elm x)) (obx z (is-elm y))
+     ... | tri< a ¬b ¬c = tri< z15 (λ eq → z01 (incl (B⊆A z) (is-elm y)) (incl (B⊆A z) (is-elm x))(case1 (sym eq)) z15 ) z17 where
+          z15 :  elm x < elm y
+          z15 =  bx-monotonic z {x} {y} a
+          z17 : elm y < elm x → ⊥
+          z17 lt =  z01 (incl (B⊆A z) (is-elm y)) (incl (B⊆A z) (is-elm x))(case2 lt) z15 
+     ... | tri≈ ¬a b ¬c = tri≈ (IsStrictPartialOrder.irrefl PO {isA (B⊆A z) x} {isA (B⊆A z) y} z14) z14 z16 where
+          z14 :  elm x ≡ elm y
+          z14 = begin
+                elm x ≡⟨ obx=fb z (is-elm x) ⟩
+                ZChain.fb z (BX.bx (is-elm x)) ≡⟨ cong (ZChain.fb z) b ⟩
+                ZChain.fb z (BX.bx (is-elm y)) ≡⟨ sym ( obx=fb z (is-elm y)) ⟩
+                elm y ∎ where open ≡-Reasoning 
+          z16 = IsStrictPartialOrder.irrefl PO {isA (B⊆A z) y} {isA (B⊆A z) x} (sym z14)
+     ... | tri> ¬a ¬b c = tri> z17 (λ eq → z01 (incl (B⊆A z) (is-elm x)) (incl (B⊆A z) (is-elm y))(case1 eq) z15 ) z15 where
+          z15 :  elm y < elm x
+          z15 =  bx-monotonic z {y} {x} c
+          z17 : elm x < elm y → ⊥
+          z17 lt =  z01 (incl (B⊆A z) (is-elm x)) (incl (B⊆A z) (is-elm y))(case2 lt) z15 
      B-is-total :  (z : ZChain A (& A) _<_ ) → IsTotalOrderSet (B z) _<_ 
-     B-is-total = {!!}
-     B-Tri : (z : ZChain A (& A) _<_ ) → Trichotomous (λ (x : Element A) y → elm x ≡ elm y ) (λ x y → elm x < elm y )
-     B-Tri z x y with trio< (obx z {!!}) (obx z {!!})
-     ... | tri< a ¬b ¬c = {!!} where -- 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≈ {!!} (bx-inject z {x} {y} b) {!!}
-     ... | 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)
+     B-is-total zc = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
+         ; trans = λ {x} {y} {z} x<y y<z → IsStrictPartialOrder.trans PO {isA (B⊆A zc) x} {isA (B⊆A zc) y} {isA (B⊆A zc) z} x<y y<z
+         ; compare = bcmp zc }
      ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (B z) _<_ )
      ZChain→¬SUP z sp = ⊥-elim {!!} where
          z03 : & (SUP.sup sp) o< osuc (& A)