1 files changed, 4 insertions, 4 deletions
diff --git a/Data/Matrix/SemiadditiveDagger.agda b/Data/Matrix/SemiadditiveDagger.agda
index 017f05f..7ebc5da 100644
--- a/Data/Matrix/SemiadditiveDagger.agda
+++ b/Data/Matrix/SemiadditiveDagger.agda
@@ -26,7 +26,7 @@ open import Category.Semiadditive using (Semiadditive)
 open import Data.Matrix.Category R.semiring using (Mat; _·_; ≑-·; ·-Iˡ; ·-Iʳ; ·-𝟎ˡ; ·-𝟎ʳ; ·-∥; ∥-·-≑; ·-resp-≋; ·-assoc)
 open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; module ≋; ∥-cong; ≑-cong; ᵀ-cong)
 open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; 𝟎≑𝟎; 𝟎∥𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ)
-open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; mapRows; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!)
+open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!)
 open import Data.Matrix.Semiadditive R.semiring using (Mat-Semiadditive)
 open import Data.Matrix.Transform R.semiring using (I; Iᵀ; [_]_; _[_]; -[-]ᵀ; [-]--cong; [-]-[]ᵥ; [⟨⟩]-[]ₕ)
 open import Data.Nat using (ℕ)
@@ -56,7 +56,7 @@ opaque
   ∙-comm (x ∷ V) (w ∷ W) = +-cong (*-comm x w) (∙-comm V W)
 
 opaque
-  unfolding _[_] [_]_ _ᵀ []ᵥ _∷ₕ_ _≋_ _∷ᵥ_
+  unfolding _[_] [_]_ []ᵥ _∷ₕ_ _≋_ _∷ᵥ_
   [-]-ᵀ : (M : Matrix A B) (V : Vector A) →  M [ V ] ≊ [ V ] (M ᵀ)
   [-]-ᵀ [] V = ≊.sym (≊.reflexive ([-]-[]ᵥ V))
   [-]-ᵀ (M₀ ∷ M) V = begin
@@ -69,7 +69,7 @@ opaque
       open ≈-Reasoning (Vectorₛ _)
 
 opaque
-  unfolding []ᵥ mapRows _∷ₕ_ _∷ᵥ_ _ᵀ _≋_
+  unfolding []ᵥ _∷ₕ_ _∷ᵥ_ _≋_
   ·-ᵀ
       : {A B C : ℕ}
         (M : Matrix A B)
@@ -95,7 +95,7 @@ opaque
   ᵀ-involutive M = ≋.reflexive (M ᵀᵀ)
 
 opaque
-  unfolding Matrix _∥_ _ᵀ _≑_ _∷ₕ_
+  unfolding _∥_ _≑_ _∷ₕ_
   ∥-ᵀ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) ᵀ ≡ M ᵀ ≑ N ᵀ
   ∥-ᵀ {A} {zero} {B} [] [] = ≡.sym (replicate-++ A B [])
   ∥-ᵀ (M₀ ∷ M) (N₀ ∷ N) = begin