diff --git a/Equivalence.agda b/Equivalence.agda
index a17a438..c72631e 100644
--- a/Equivalence.agda
+++ b/Equivalence.agda
@@ -4,8 +4,18 @@ open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
 
-record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where
-    field
-        ≈-refl : {a : A} → a ≈ a
-        ≈-sym : {a b : A} → a ≈ b → b ≈ a
-        ≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c
+module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
+    IsReflexive : Set a
+    IsReflexive = ∀ {a : A} → a ≈ a
+
+    IsSymmetric : Set a
+    IsSymmetric = ∀ {a b : A} → a ≈ b → b ≈ a
+
+    IsTransitive : Set a
+    IsTransitive = ∀ {a b c : A} → a ≈ b → b ≈ c → a ≈ c
+
+    record IsEquivalence : Set a where
+        field
+            ≈-refl : IsReflexive
+            ≈-sym : IsSymmetric
+            ≈-trans : IsTransitive