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

diff -r dc7a95dd66c4 -r 00c71d1dc316 src/zorn.agda
--- a/src/zorn.agda	Fri Apr 08 17:47:24 2022 +0900
+++ b/src/zorn.agda	Fri Apr 08 22:03:01 2022 +0900
@@ -54,6 +54,20 @@
 PartialOrderSet A _<_ = (a b :  Element A)
      → (elm a < elm b → ((¬ elm b < elm a) ∧ (¬ (elm a ≡ elm b) ))) ∧ (elm a ≡ elm b → (¬ elm a < elm b) ∧ (¬ elm b < elm a))
 
+IsPartialOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
+IsPartialOrderSet A _<_ = IsPartialOrder _<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
+
+IsTotalOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
+IsTotalOrderSet A _<_ = IsTotalOrder _<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
+
 me : { A a : HOD } → A ∋ a → Element A
 me {A} {a} lt = record { elm = a ; is-elm = lt }
 
@@ -77,7 +91,6 @@
       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 
@@ -131,7 +144,7 @@
      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 → {!!} ) ( ZChain.injection z {!!} {!!} ? )  ⟩
+            {!!} ≡⟨ cong (λ k → {!!} ) {!!}  ⟩
             {!!} ≡⟨ {!!}   ⟩
             elm y ∎ where open ≡-Reasoning
      B-is-total :  (z : ZChain A (& A) _<_ ) → TotalOrderSet (B z) _<_ 
@@ -139,7 +152,7 @@
      ... | 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≈ {!!} (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)
      ZChain→¬SUP :  (z : ZChain A (& A) _<_ ) →  ¬ (SUP A (B z) _<_ )
      ZChain→¬SUP z sp = ⊥-elim {!!} where