We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent bef7264 commit 62a09e8Copy full SHA for 62a09e8
src/Relation/Binary/Consequences.agda
@@ -121,8 +121,8 @@ module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where
121
irrefl (antisym x<y y<x) x<y
122
123
asym⇒antisym : Asymmetric _<_ → Antisymmetric _≈_ _<_
124
- asym⇒antisym asym x<y y<x = contradiction y<x (asym x<y)
125
-
+ asym⇒antisym asym x<y y<x = contradiction y<x (asym x<y)
+
126
asym⇒irr : _<_ Respects₂ _≈_ → Symmetric _≈_ →
127
Asymmetric _<_ → Irreflexive _≈_ _<_
128
asym⇒irr (respʳ , respˡ) sym asym {x} {y} x≈y x<y =
0 commit comments