little acorns

src/Relation/Binary/Properties/Preorder.agda

@@ -18,10 +18,14 @@ import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
 
 open Preorder P
 
+private
+  infix 4 _∼ᵒ_
+  _∼ᵒ_ = flip _∼_
+
 ------------------------------------------------------------------------
--- The inverse relation is also a preorder.
+-- The converse relation is also a preorder.
 
-converse-isPreorder : IsPreorder _≈_ (flip _∼_)
+converse-isPreorder : IsPreorder _≈_ _∼ᵒ_
 converse-isPreorder = EqAndOrd.isPreorder isPreorder
 
 converse-preorder : Preorder p₁ p₂ p₃
@@ -32,7 +36,7 @@ converse-preorder = EqAndOrd.preorder P
 
 InducedEquivalence : Setoid _ _
 InducedEquivalence = record
-  { _≈_           = λ x y → x ∼ y × y ∼ x
+  { _≈_           = λ x y → x ∼ y × x ∼ᵒ y
   ; isEquivalence = record
     { refl  = (refl , refl)
     ; sym   = swap