Reorganize matrix code

1 files changed, 8 insertions, 8 deletions

diff --git a/Data/Vector/Bisemimodule.agda b/Data/Vector/Bisemimodule.agda
index d895459..e38536a 100644
--- a/Data/Vector/Bisemimodule.agda
+++ b/Data/Vector/Bisemimodule.agda
@@ -136,19 +136,19 @@ opaque
 
   unfolding _∙_ ⟨ε⟩
 
-  ∙-identityˡ : (V : Vector n) → ⟨ε⟩ ∙ V ≈ 0#
-  ∙-identityˡ [] = refl
-  ∙-identityˡ (x ∷ V) = begin
+  ∙-zeroˡ : (V : Vector n) → ⟨ε⟩ ∙ V ≈ 0#
+  ∙-zeroˡ [] = refl
+  ∙-zeroˡ (x ∷ V) = begin
       0# * x + ⟨ε⟩ ∙ V  ≈⟨ +-congʳ (zeroˡ x) ⟩
-      0# + ⟨ε⟩ ∙ V      ≈⟨ +-congˡ (∙-identityˡ V) ⟩
+      0# + ⟨ε⟩ ∙ V      ≈⟨ +-congˡ (∙-zeroˡ V) ⟩
       0# + 0#           ≈⟨ +-identityˡ 0# ⟩
       0#                ∎
 
-  ∙-identityʳ : (V : Vector n) → V ∙ ⟨ε⟩ ≈ 0#
-  ∙-identityʳ [] = refl
-  ∙-identityʳ (x ∷ V) = begin
+  ∙-zeroʳ : (V : Vector n) → V ∙ ⟨ε⟩ ≈ 0#
+  ∙-zeroʳ [] = refl
+  ∙-zeroʳ (x ∷ V) = begin
       x * 0# + V ∙ ⟨ε⟩  ≈⟨ +-congʳ (zeroʳ x) ⟩
-      0# + V ∙ ⟨ε⟩      ≈⟨ +-congˡ (∙-identityʳ V) ⟩
+      0# + V ∙ ⟨ε⟩      ≈⟨ +-congˡ (∙-zeroʳ V) ⟩
       0# + 0#           ≈⟨ +-identityˡ 0# ⟩
       0#                ∎