@@ -31,13 +31,13 @@ module _
3131
3232 open BinaryRelation
3333
34- isStrictOrder→isStrictPoset : IsStrictOrder R → IsQuoset R
35- isStrictOrder→isStrictPoset strictorder = isquoset
36- (IsStrictOrder.is-set strictorder)
37- (IsStrictOrder.is-prop-valued strictorder)
38- (IsStrictOrder.is-irrefl strictorder)
39- (IsStrictOrder.is-trans strictorder)
40- (IsStrictOrder.is-asym strictorder)
34+ isStrictOrder→isQuoset : IsStrictOrder R → IsQuoset R
35+ isStrictOrder→isQuoset strictorder = isquoset
36+ (IsStrictOrder.is-set strictorder)
37+ (IsStrictOrder.is-prop-valued strictorder)
38+ (IsStrictOrder.is-irrefl strictorder)
39+ (IsStrictOrder.is-trans strictorder)
40+ (IsStrictOrder.is-asym strictorder)
4141
4242 private
4343 transrefl : isTrans R → isTrans (ReflClosure R)
@@ -102,7 +102,7 @@ module _
102102StrictOrder→Quoset : StrictOrder ℓ ℓ' → Quoset ℓ ℓ'
103103StrictOrder→Quoset (_ , strict)
104104 = quoset _ (StrictOrderStr._<_ strict)
105- (isStrictOrder→isStrictPoset (StrictOrderStr.isStrictOrder strict))
105+ (isStrictOrder→isQuoset (StrictOrderStr.isStrictOrder strict))
106106
107107StrictOrder→Apartness : StrictOrder ℓ ℓ' → Apartness ℓ ℓ'
108108StrictOrder→Apartness (_ , strict)
0 commit comments