@@ -31,13 +31,13 @@ module _
31
31
32
32
open BinaryRelation
33
33
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)
41
41
42
42
private
43
43
transrefl : isTrans R → isTrans (ReflClosure R)
@@ -102,7 +102,7 @@ module _
102
102
StrictOrder→Quoset : StrictOrder ℓ ℓ' → Quoset ℓ ℓ'
103
103
StrictOrder→Quoset (_ , strict)
104
104
= quoset _ (StrictOrderStr._<_ strict)
105
- (isStrictOrder→isStrictPoset (StrictOrderStr.isStrictOrder strict))
105
+ (isStrictOrder→isQuoset (StrictOrderStr.isStrictOrder strict))
106
106
107
107
StrictOrder→Apartness : StrictOrder ℓ ℓ' → Apartness ℓ ℓ'
108
108
StrictOrder→Apartness (_ , strict)
0 commit comments