diff --git a/src/Algebra/Dioid/Bool.agda b/src/Algebra/Dioid/Bool.agda
index 244aece..1dad36e 100644
--- a/src/Algebra/Dioid/Bool.agda
+++ b/src/Algebra/Dioid/Bool.agda
@@ -19,8 +19,8 @@ _and_ : Bool -> Bool -> Bool
 true and true = true
 _ and _ = false
 
-boolDioid : Dioid -> Bool
-boolDioid zero = false
-boolDioid one  = true
-boolDioid (r + s) = boolDioid r or  boolDioid s
-boolDioid (r * s) = boolDioid r and boolDioid s
+bool-dioid : Dioid -> Bool
+bool-dioid zero = false
+bool-dioid one  = true
+bool-dioid (r + s) = bool-dioid r or  bool-dioid s
+bool-dioid (r * s) = bool-dioid r and bool-dioid s
diff --git a/src/Algebra/Dioid/Bool/Theorems.agda b/src/Algebra/Dioid/Bool/Theorems.agda
index 8b39b97..dfaa23a 100644
--- a/src/Algebra/Dioid/Bool/Theorems.agda
+++ b/src/Algebra/Dioid/Bool/Theorems.agda
@@ -80,22 +80,22 @@ right-distributivity {false} {true} {true} = reflexivity
 right-distributivity {false} {true} {false} = reflexivity
 right-distributivity {false} {false} {d} = reflexivity
 
-boolDioidLawful : ∀ {r s : Dioid} -> r Algebra.Dioid.≡ s -> boolDioid r ≡ boolDioid s
-boolDioidLawful {r} {.r} Algebra.Dioid.reflexivity = reflexivity
-boolDioidLawful {r} {s} (Algebra.Dioid.symmetry eq) = symmetry (boolDioidLawful eq)
-boolDioidLawful {r} {s} (Algebra.Dioid.transitivity eq eq₁) = transitivity (boolDioidLawful eq) (boolDioidLawful eq₁)
-boolDioidLawful {.(_ + _)} {.(_ + _)} (Algebra.Dioid.+left-congruence eq) = or-left-congruence (boolDioidLawful eq)
-boolDioidLawful {.(_ + _)} {.(_ + _)} (Algebra.Dioid.+right-congruence eq) = or-right-congruence (boolDioidLawful eq)
-boolDioidLawful {.(_ * _)} {.(_ * _)} (Algebra.Dioid.*left-congruence eq) = and-left-congruence (boolDioidLawful eq)
-boolDioidLawful {.(_ * _)} {.(_ * _)} (Algebra.Dioid.*right-congruence eq) = and-right-congruence (boolDioidLawful eq)
-boolDioidLawful {.(s + s)} {s} Algebra.Dioid.+idempotence = or-idempotence
-boolDioidLawful {.(_ + _)} {.(_ + _)} Algebra.Dioid.+commutativity = or-commutativity
-boolDioidLawful {.(_ + (_ + _))} {.(_ + _ + _)} Algebra.Dioid.+associativity = or-associativity
-boolDioidLawful {.(s + zero)} {s} Algebra.Dioid.+zero-identity = or-false-identity
-boolDioidLawful {.(_ * (_ * _))} {.(_ * _ * _)} Algebra.Dioid.*associativity = and-associativity
-boolDioidLawful {.(zero * _)} {.zero} Algebra.Dioid.*left-zero = reflexivity
-boolDioidLawful {.(_ * zero)} {.zero} Algebra.Dioid.*right-zero = and-right-false
-boolDioidLawful {.(one * s)} {s} Algebra.Dioid.*left-identity = and-left-true
-boolDioidLawful {.(s * one)} {s} Algebra.Dioid.*right-identity = and-right-true
-boolDioidLawful {.(_ * (_ + _))} {.(_ * _ + _ * _)} Algebra.Dioid.left-distributivity = left-distributivity
-boolDioidLawful {.((_ + _) * _)} {.(_ * _ + _ * _)} Algebra.Dioid.right-distributivity = right-distributivity
+bool-dioid-lawful : ∀ {r s : Dioid} -> r Algebra.Dioid.≡ s -> bool-dioid r ≡ bool-dioid s
+bool-dioid-lawful {r} {.r} Algebra.Dioid.reflexivity = reflexivity
+bool-dioid-lawful {r} {s} (Algebra.Dioid.symmetry eq) = symmetry (bool-dioid-lawful eq)
+bool-dioid-lawful {r} {s} (Algebra.Dioid.transitivity eq eq₁) = transitivity (bool-dioid-lawful eq) (bool-dioid-lawful eq₁)
+bool-dioid-lawful {.(_ + _)} {.(_ + _)} (Algebra.Dioid.+left-congruence eq) = or-left-congruence (bool-dioid-lawful eq)
+bool-dioid-lawful {.(_ + _)} {.(_ + _)} (Algebra.Dioid.+right-congruence eq) = or-right-congruence (bool-dioid-lawful eq)
+bool-dioid-lawful {.(_ * _)} {.(_ * _)} (Algebra.Dioid.*left-congruence eq) = and-left-congruence (bool-dioid-lawful eq)
+bool-dioid-lawful {.(_ * _)} {.(_ * _)} (Algebra.Dioid.*right-congruence eq) = and-right-congruence (bool-dioid-lawful eq)
+bool-dioid-lawful {.(s + s)} {s} Algebra.Dioid.+idempotence = or-idempotence
+bool-dioid-lawful {.(_ + _)} {.(_ + _)} Algebra.Dioid.+commutativity = or-commutativity
+bool-dioid-lawful {.(_ + (_ + _))} {.(_ + _ + _)} Algebra.Dioid.+associativity = or-associativity
+bool-dioid-lawful {.(s + zero)} {s} Algebra.Dioid.+zero-identity = or-false-identity
+bool-dioid-lawful {.(_ * (_ * _))} {.(_ * _ * _)} Algebra.Dioid.*associativity = and-associativity
+bool-dioid-lawful {.(zero * _)} {.zero} Algebra.Dioid.*left-zero = reflexivity
+bool-dioid-lawful {.(_ * zero)} {.zero} Algebra.Dioid.*right-zero = and-right-false
+bool-dioid-lawful {.(one * s)} {s} Algebra.Dioid.*left-identity = and-left-true
+bool-dioid-lawful {.(s * one)} {s} Algebra.Dioid.*right-identity = and-right-true
+bool-dioid-lawful {.(_ * (_ + _))} {.(_ * _ + _ * _)} Algebra.Dioid.left-distributivity = left-distributivity
+bool-dioid-lawful {.((_ + _) * _)} {.(_ * _ + _ * _)} Algebra.Dioid.right-distributivity = right-distributivity
diff --git a/src/Algebra/Dioid/ShortestDistance.agda b/src/Algebra/Dioid/ShortestDistance.agda
index e391ce3..a4de2eb 100644
--- a/src/Algebra/Dioid/ShortestDistance.agda
+++ b/src/Algebra/Dioid/ShortestDistance.agda
@@ -26,16 +26,16 @@ data _≡_ : (x y : ShortestDistance) -> Set where
   symmetry     : ∀ {x y   : ShortestDistance} -> x ≡ y ->          y ≡ x
   transitivity : ∀ {x y z : ShortestDistance} -> x ≡ y -> y ≡ z -> x ≡ z
 
-shortestDistanceDioid : Dioid -> ShortestDistance
-shortestDistanceDioid zero = Unreachable
-shortestDistanceDioid one  = Distance Nat.zero
-shortestDistanceDioid (r + s) with shortestDistanceDioid r
-... | Unreachable = shortestDistanceDioid s
-... | Distance n with shortestDistanceDioid s
+shortest-distance-dioid : Dioid -> ShortestDistance
+shortest-distance-dioid zero = Unreachable
+shortest-distance-dioid one  = Distance Nat.zero
+shortest-distance-dioid (r + s) with shortest-distance-dioid r
+... | Unreachable = shortest-distance-dioid s
+... | Distance n with shortest-distance-dioid s
 ... | Unreachable = Distance n
 ... | Distance m = Distance (Nat.min n m)
-shortestDistanceDioid (r * s) with shortestDistanceDioid r
+shortest-distance-dioid (r * s) with shortest-distance-dioid r
 ... | Unreachable = Unreachable
-... | Distance n with shortestDistanceDioid s
+... | Distance n with shortest-distance-dioid s
 ... | Unreachable = Unreachable
 ... | Distance m = Distance (n Nat.+ m)
diff --git a/src/Algebra/LabelledGraph/Theorems.agda b/src/Algebra/LabelledGraph/Theorems.agda
index f14a2d0..856f1f6 100644
--- a/src/Algebra/LabelledGraph/Theorems.agda
+++ b/src/Algebra/LabelledGraph/Theorems.agda
@@ -92,7 +92,7 @@ left-distributivity {_} {a} {b} {c} {r} =
 to-graph : ∀ {A} -> LabelledGraph A -> Graph A
 to-graph ε = Graph.ε
 to-graph (v x) = Graph.v x
-to-graph (x -[ r ]> y) with Bool.boolDioid r
+to-graph (x -[ r ]> y) with Bool.bool-dioid r
 ... | Bool.false = to-graph x Graph.+ to-graph y
 ... | Bool.true  = to-graph x Graph.* to-graph y