diff --git a/src/foundation/symmetric-binary-relations.lagda.md b/src/foundation/symmetric-binary-relations.lagda.md
index 2af23d658b..c9688b1722 100644
--- a/src/foundation/symmetric-binary-relations.lagda.md
+++ b/src/foundation/symmetric-binary-relations.lagda.md
@@ -49,105 +49,105 @@ universe `𝒰`.
 ### Symmetric binary relations
 
 ```agda
-symmetric-binary-relation :
+Symmetric-Relation :
   {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
-symmetric-binary-relation l2 A = symmetric-operation A (UU l2)
+Symmetric-Relation l2 A = symmetric-operation A (UU l2)
 ```
 
 ### Action on symmetries of symmetric binary relations
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} (R : symmetric-binary-relation l2 A)
+  {l1 l2 : Level} {A : UU l1} (R : Symmetric-Relation l2 A)
   where
 
   abstract
-    equiv-tr-symmetric-binary-relation :
+    equiv-tr-Symmetric-Relation :
       (p q : unordered-pair A) → Eq-unordered-pair p q → R p ≃ R q
-    equiv-tr-symmetric-binary-relation p =
+    equiv-tr-Symmetric-Relation p =
       ind-Eq-unordered-pair p (λ q e → R p ≃ R q) id-equiv
 
-    compute-refl-equiv-tr-symmetric-binary-relation :
+    compute-refl-equiv-tr-Symmetric-Relation :
       (p : unordered-pair A) →
-      equiv-tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p) ＝
+      equiv-tr-Symmetric-Relation p p (refl-Eq-unordered-pair p) ＝
       id-equiv
-    compute-refl-equiv-tr-symmetric-binary-relation p =
+    compute-refl-equiv-tr-Symmetric-Relation p =
       compute-refl-ind-Eq-unordered-pair p (λ q e → R p ≃ R q) id-equiv
 
-    htpy-compute-refl-equiv-tr-symmetric-binary-relation :
+    htpy-compute-refl-equiv-tr-Symmetric-Relation :
       (p : unordered-pair A) →
       htpy-equiv
-        ( equiv-tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p))
+        ( equiv-tr-Symmetric-Relation p p (refl-Eq-unordered-pair p))
         ( id-equiv)
-    htpy-compute-refl-equiv-tr-symmetric-binary-relation p =
-      htpy-eq-equiv (compute-refl-equiv-tr-symmetric-binary-relation p)
+    htpy-compute-refl-equiv-tr-Symmetric-Relation p =
+      htpy-eq-equiv (compute-refl-equiv-tr-Symmetric-Relation p)
 
   abstract
-    tr-symmetric-binary-relation :
+    tr-Symmetric-Relation :
       (p q : unordered-pair A) → Eq-unordered-pair p q → R p → R q
-    tr-symmetric-binary-relation p q e =
-      map-equiv (equiv-tr-symmetric-binary-relation p q e)
+    tr-Symmetric-Relation p q e =
+      map-equiv (equiv-tr-Symmetric-Relation p q e)
 
-    tr-inv-symmetric-binary-relation :
+    tr-inv-Symmetric-Relation :
       (p q : unordered-pair A) → Eq-unordered-pair p q → R q → R p
-    tr-inv-symmetric-binary-relation p q e =
-      map-inv-equiv (equiv-tr-symmetric-binary-relation p q e)
+    tr-inv-Symmetric-Relation p q e =
+      map-inv-equiv (equiv-tr-Symmetric-Relation p q e)
 
-    is-section-tr-inv-symmetric-binary-relation :
+    is-section-tr-inv-Symmetric-Relation :
       (p q : unordered-pair A) (e : Eq-unordered-pair p q) →
-      tr-symmetric-binary-relation p q e ∘
-      tr-inv-symmetric-binary-relation p q e ~
+      tr-Symmetric-Relation p q e ∘
+      tr-inv-Symmetric-Relation p q e ~
       id
-    is-section-tr-inv-symmetric-binary-relation p q e =
-      is-section-map-inv-equiv (equiv-tr-symmetric-binary-relation p q e)
+    is-section-tr-inv-Symmetric-Relation p q e =
+      is-section-map-inv-equiv (equiv-tr-Symmetric-Relation p q e)
 
-    is-retraction-tr-inv-symmetric-binary-relation :
+    is-retraction-tr-inv-Symmetric-Relation :
       (p q : unordered-pair A) (e : Eq-unordered-pair p q) →
-      tr-inv-symmetric-binary-relation p q e ∘
-      tr-symmetric-binary-relation p q e ~
+      tr-inv-Symmetric-Relation p q e ∘
+      tr-Symmetric-Relation p q e ~
       id
-    is-retraction-tr-inv-symmetric-binary-relation p q e =
-      is-retraction-map-inv-equiv (equiv-tr-symmetric-binary-relation p q e)
+    is-retraction-tr-inv-Symmetric-Relation p q e =
+      is-retraction-map-inv-equiv (equiv-tr-Symmetric-Relation p q e)
 
-    compute-refl-tr-symmetric-binary-relation :
+    compute-refl-tr-Symmetric-Relation :
       (p : unordered-pair A) →
-      tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p) ＝ id
-    compute-refl-tr-symmetric-binary-relation p =
-      ap map-equiv (compute-refl-equiv-tr-symmetric-binary-relation p)
+      tr-Symmetric-Relation p p (refl-Eq-unordered-pair p) ＝ id
+    compute-refl-tr-Symmetric-Relation p =
+      ap map-equiv (compute-refl-equiv-tr-Symmetric-Relation p)
 
-    htpy-compute-refl-tr-symmetric-binary-relation :
+    htpy-compute-refl-tr-Symmetric-Relation :
       (p : unordered-pair A) →
-      tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p) ~ id
-    htpy-compute-refl-tr-symmetric-binary-relation p =
-      htpy-eq (compute-refl-tr-symmetric-binary-relation p)
+      tr-Symmetric-Relation p p (refl-Eq-unordered-pair p) ~ id
+    htpy-compute-refl-tr-Symmetric-Relation p =
+      htpy-eq (compute-refl-tr-Symmetric-Relation p)
 ```
 
 ### The underlying binary relation of a symmetric binary relation
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} (R : symmetric-binary-relation l2 A)
+  {l1 l2 : Level} {A : UU l1} (R : Symmetric-Relation l2 A)
   where
 
-  relation-symmetric-binary-relation : Relation l2 A
-  relation-symmetric-binary-relation x y = R (standard-unordered-pair x y)
+  relation-Symmetric-Relation : Relation l2 A
+  relation-Symmetric-Relation x y = R (standard-unordered-pair x y)
 
-  equiv-symmetric-relation-symmetric-binary-relation :
+  equiv-symmetric-relation-Symmetric-Relation :
     {x y : A} →
-    relation-symmetric-binary-relation x y ≃
-    relation-symmetric-binary-relation y x
-  equiv-symmetric-relation-symmetric-binary-relation {x} {y} =
-    equiv-tr-symmetric-binary-relation R
+    relation-Symmetric-Relation x y ≃
+    relation-Symmetric-Relation y x
+  equiv-symmetric-relation-Symmetric-Relation {x} {y} =
+    equiv-tr-Symmetric-Relation R
       ( standard-unordered-pair x y)
       ( standard-unordered-pair y x)
       ( swap-standard-unordered-pair x y)
 
-  symmetric-relation-symmetric-binary-relation :
+  symmetric-relation-Symmetric-Relation :
     {x y : A} →
-    relation-symmetric-binary-relation x y →
-    relation-symmetric-binary-relation y x
-  symmetric-relation-symmetric-binary-relation =
-    map-equiv equiv-symmetric-relation-symmetric-binary-relation
+    relation-Symmetric-Relation x y →
+    relation-Symmetric-Relation y x
+  symmetric-relation-Symmetric-Relation =
+    map-equiv equiv-symmetric-relation-Symmetric-Relation
 ```
 
 ### The forgetful functor from binary relations to symmetric binary relations
@@ -157,17 +157,17 @@ module _
   {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
   where
 
-  symmetric-binary-relation-Relation : symmetric-binary-relation l2 A
-  symmetric-binary-relation-Relation p =
+  symmetric-relation-Relation : Symmetric-Relation l2 A
+  symmetric-relation-Relation p =
     Σ ( type-unordered-pair p)
       ( λ i →
         R (element-unordered-pair p i) (other-element-unordered-pair p i))
 
-  unit-symmetric-binary-relation-Relation :
+  unit-symmetric-relation-Relation :
     (x y : A) → R x y →
-    relation-symmetric-binary-relation symmetric-binary-relation-Relation x y
-  pr1 (unit-symmetric-binary-relation-Relation x y r) = zero-Fin 1
-  pr2 (unit-symmetric-binary-relation-Relation x y r) =
+    relation-Symmetric-Relation symmetric-relation-Relation x y
+  pr1 (unit-symmetric-relation-Relation x y r) = zero-Fin 1
+  pr2 (unit-symmetric-relation-Relation x y r) =
     tr
       ( R x)
       ( inv (compute-other-element-standard-unordered-pair x y (zero-Fin 1)))
@@ -181,18 +181,18 @@ module _
   {l1 l2 l3 : Level} {A : UU l1}
   where
 
-  hom-symmetric-binary-relation :
-    symmetric-binary-relation l2 A → symmetric-binary-relation l3 A →
+  hom-Symmetric-Relation :
+    Symmetric-Relation l2 A → Symmetric-Relation l3 A →
     UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3)
-  hom-symmetric-binary-relation R S =
+  hom-Symmetric-Relation R S =
     (p : unordered-pair A) → R p → S p
 
-  hom-relation-hom-symmetric-binary-relation :
-    (R : symmetric-binary-relation l2 A) (S : symmetric-binary-relation l3 A) →
-    hom-symmetric-binary-relation R S →
+  hom-relation-hom-Symmetric-Relation :
+    (R : Symmetric-Relation l2 A) (S : Symmetric-Relation l3 A) →
+    hom-Symmetric-Relation R S →
     hom-Relation
-      ( relation-symmetric-binary-relation R)
-      ( relation-symmetric-binary-relation S)
-  hom-relation-hom-symmetric-binary-relation R S f x y =
+      ( relation-Symmetric-Relation R)
+      ( relation-Symmetric-Relation S)
+  hom-relation-hom-Symmetric-Relation R S f x y =
     f (standard-unordered-pair x y)
 ```