--- a/src/zorn.agda	Sat Apr 09 08:30:33 2022 +0900
+++ b/src/zorn.agda	Sat Apr 09 10:38:15 2022 +0900
@@ -48,29 +48,33 @@
 open Element
 
 IsPartialOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
-IsPartialOrderSet A _<_ = IsPartialOrder _≡A_ _≤A_  where
-   _≤A_ : (x y : Element A ) → Set (suc n)
-   x ≤A y = (elm x ≡ elm y) ∨ (elm x < elm y)
+IsPartialOrderSet A _<_ = IsStrictPartialOrder _≡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
 
 open _==_
 open _⊆_
 
-toA : { A B  : HOD } → B ⊆ A → (x : Element B) → Element A
-toA B⊆A x = record { elm = elm x ; is-elm = incl B⊆A (is-elm x) }
+isA : { A B  : HOD } → B ⊆ A → (x : Element B) → Element A
+isA B⊆A x = record { elm = elm x ; is-elm = incl B⊆A (is-elm x) }
 
 ⊆-IsPartialOrderSet : { A B  : HOD } → B ⊆ A →  {_<_ : (x y : HOD) → Set n }  → IsPartialOrderSet A _<_ → IsPartialOrderSet B _<_
 ⊆-IsPartialOrderSet {A} {B} B⊆A {_<_} PA = record {
-       isPreorder =  record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans } ; reflexive = λ eq → case1 eq ; trans = λ {x} {y} {z} → trans1 {x} {y} {z} }
-     ; antisym = λ {x} {y} → anti {x} {y}
+       isEquivalence = record { refl = refl ; sym = sym ; trans = trans } ; reflexive = λ eq → case1 eq ; trans = λ {x} {y} {z} → trans1 {x} {y} {z} 
+     ; irrefl = λ {x} {y} → irrefl1 {x} {y} ; trans = trans1 ; <-resp-≈ = resp0 
    } where
-   _≤B_ : (x y : Element B ) → Set (suc n)
-   x ≤B y = (elm x ≡ elm y) ∨ (elm x < elm y)
-   trans1 : {x y z : Element B} → x ≤B y → y ≤B z → x ≤B z 
-   trans1 {x} {y} {z} x<y y<z  = IsPreorder.trans (IsPartialOrder.isPreorder PA) {toA B⊆A x} {toA B⊆A y} {toA B⊆A z} x<y y<z 
-   anti : {x y : Element B} → x ≤B y →  y ≤B x  → elm x ≡ elm y
-   anti {x} {y} x<y y<x = IsPartialOrder.antisym PA {toA B⊆A x} {toA B⊆A y} x<y y<x
+   _<B_ : (x y : Element B ) → Set n
+   x <B y = elm x < elm y
+   trans1 : {x y z : Element B} → x <B y → y <B z → x <B z 
+   trans1 {x} {y} {z} x<y y<z  = IsStrictPartialOrder.trans PA {isA B⊆A x} {isA B⊆A y} {isA B⊆A z} x<y y<z 
+   irrefl1 : {x y : Element B} → elm x ≡ elm y → ¬ ( x <B y  )
+   irrefl1 {x} {y} x=y x<y = IsStrictPartialOrder.irrefl PA {isA B⊆A x} {isA B⊆A y} x=y x<y 
+   open import Data.Product
+   resp0 : ({x y z : Element B} → elm y ≡ elm z → x <B y → x <B z) × ({x y z : Element B} → elm y ≡ elm z → y <B x → z <B x) 
+   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 })
 
 IsTotalOrderSet : ( A : HOD ) →  (_<_ : (x y : HOD) → Set n )  → Set (suc n)
 IsTotalOrderSet A _<_ = IsTotalOrder  _≡A_ _≤A_ where
@@ -144,7 +148,7 @@
      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 → IsPartialOrder j k ) {!!} {!!} {!!} where
+     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) }