Reorganize matrix code

16 files changed, 1549 insertions, 1793 deletions

diff --git a/Data/Mat/Category.agda b/Data/Mat/Category.agda
deleted file mode 100644
index 2407d28..0000000
--- a/Data/Mat/Category.agda
+++ /dev/null
@@ -1,434 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Algebra.Bundles using (Semiring)
-open import Level using (Level; 0ℓ; _⊔_)
-
-module Data.Mat.Category {c ℓ : Level} (Rig : Semiring c ℓ) where
-
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-import Data.Vec.Relation.Binary.Equality.Setoid as PW
-
-open import Categories.Category using (Category)
-open import Categories.Category.Helper using (categoryHelper)
-open import Data.Nat using (ℕ)
-open import Data.Vec using (Vec; zipWith; foldr; foldr′; map; replicate)
-open import Data.Mat.Util
-  using
-    ( foldr-cong ; zipWith-cong ; transpose ; transpose-involutive ; map-replicate
-    ; zipWith-map ; map-zipWith ; zipWith-map-map ; transpose-zipWith ; transpose-cong
-    )
-open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise)
-open import Data.Vec.Properties using (map-id; map-∘; map-cong; zipWith-replicate₁)
-open import Relation.Binary using (Rel; IsEquivalence; Setoid)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≗_; _≡_; module ≡-Reasoning)
-open import Function using (_∘_; id)
-
-open Vec
-open ℕ
-
-open Semiring Rig renaming (Carrier to R)
-module V = PW setoid
-
-private
-  variable
-    n m o p : ℕ
-
-opaque
-  -- Vectors over the rig
-  Vector : ℕ → Set c
-  Vector = Vec R
-
-opaque
-  -- N by M matrices over the rig
-  Matrix : Rel ℕ c
-  Matrix n m = Vec (Vector n) m
-
-opaque
-
-  unfolding Vector
-
-  -- Pointwise equality of vectors
-  _≊_ : Rel (Vector n) (c ⊔ ℓ)
-  _≊_ {n} A B = A V.≋ B
-
-  ≊-setoid : ℕ → Setoid c (c ⊔ ℓ)
-  ≊-setoid n = record
-      { Carrier = Vector n
-      ; _≈_ = _≊_ {n}
-      ; isEquivalence = record
-          { refl = V.≋-refl
-          ; sym = V.≋-sym
-          ; trans = V.≋-trans
-          }
-    }
-
-module ≊ {n} = Setoid (≊-setoid n)
-
-infix 4 _≊_
-
-module M {n} = PW (≊-setoid n)
-
-opaque
-
-  unfolding Matrix ≊-setoid
-
-  -- Pointwise equality of matrices
-  _≋_ : Rel (Matrix n m) (c ⊔ ℓ)
-  _≋_ {n} {m} A B = A M.≋ B
-
-  ≋-setoid : ℕ → ℕ → Setoid c (c ⊔ ℓ)
-  ≋-setoid n m = record
-      { Carrier = Matrix n m
-      ; _≈_ = _≋_ {n} {m}
-      ; isEquivalence = record
-          { refl = M.≋-refl
-          ; sym = M.≋-sym
-          ; trans = M.≋-trans
-          }
-    }
-
-  ≋-isEquivalence : IsEquivalence (_≋_ {n} {m})
-  ≋-isEquivalence {n} {m} = Setoid.isEquivalence (≋-setoid n m)
-
-module ≋ {n} {m} = Setoid (≋-setoid n m)
-
-infix 4 _≋_
-
-opaque
-  unfolding Vector
-  -- Sum the elements of a vector
-  sum : Vector n → R
-  sum = foldr′ _+_ 0#
-
-opaque
-  unfolding sum _≊_
-  sum-cong : {x y : Vector n} → x ≊ y → sum x ≈ sum y
-  sum-cong = foldr-cong {A = setoid} (λ _ → setoid) +-cong refl
-
-opaque
-  unfolding sum
-  -- Dot product of two vectors
-  _∙_ : Vector n → Vector n → R
-  _∙_ v w = sum (zipWith _*_ v w)
-
-infix 8 _∙_
-
-opaque
-  unfolding Vector
-  -- Pointwise sum of two vectors
-  _⊕_ : Vector n → Vector n → Vector n
-  _⊕_ = zipWith _+_
-
-infixl 6 _⊕_
-
-opaque
-  unfolding Vector
-  -- Scaling a vector
-  _⟨_⟩ : R → Vector n → Vector n
-  _⟨_⟩ r = map (r *_)
-
-infix 9 _⟨_⟩
-
-opaque
-  unfolding _∙_ _≊_
-  ∙-cong : {v₁ v₂ w₁ w₂ : Vector n} → v₁ ≊ v₂ → w₁ ≊ w₂ → v₁ ∙ w₁ ≈ v₂ ∙ w₂
-  ∙-cong {n} ≋v ≋w = sum-cong (zipWith-cong *-cong ≋v ≋w)
-
-opaque
-  unfolding Vector
-  -- The zero vector
-  zeros : Vector n
-  zeros {n} = replicate n 0#
-
-opaque
-  unfolding Matrix Vector
-  -- The identity matrix
-  I : Matrix n n
-  I {zero} = []
-  I {suc n} = (1# ∷ zeros) ∷ map (0# ∷_) I
-
-opaque
-  unfolding Matrix Vector
-  _[_] : Matrix n m → Vector n → Vector m
-  _[_] M V = map (_∙ V) M
-
-opaque
-  unfolding Matrix Vector
-  [_]_ : Vector m → Matrix n m → Vector n
-  [_]_ V M = map (V ∙_) (transpose M)
-
-opaque
-  unfolding Matrix
-  mapRows : (Vector n → Vector m) → Matrix n p → Matrix m p
-  mapRows = map
-
-opaque
-  unfolding Matrix Vector
-  _ᵀ : Matrix n m → Matrix m n
-  _ᵀ = transpose
-
-infix 10 _ᵀ
-
-opaque
-  unfolding _ᵀ
-  _ᵀᵀ : (M : Matrix n m) → M ᵀ ᵀ ≡ M
-  _ᵀᵀ M = transpose-involutive M
-
-infix 10 _ᵀᵀ
-
-opaque
-  unfolding mapRows _ᵀ _[_] [_]_
-  -[-]ᵀ : (A : Matrix m o) (B : Matrix n m) → mapRows (A [_]) (B ᵀ) ≡ (mapRows ([_] B) A) ᵀ
-  -[-]ᵀ [] B = map-replicate [] (transpose B)
-  -[-]ᵀ (A₀ ∷ A) B = begin
-      map (λ V → A₀ ∙ V ∷ map (_∙ V) A) (B ᵀ)             ≡⟨ zipWith-map (A₀ ∙_) (A [_]) _∷_ (B ᵀ) ⟨
-      zipWith _∷_ ([ A₀ ] B) (map (A [_]) (B ᵀ))          ≡⟨ ≡.cong (zipWith _∷_ ([ A₀ ] B)) (-[-]ᵀ A B) ⟩
-      zipWith _∷_ ([ A₀ ] B) (transpose (map ([_] B) A))  ∎
-    where
-      open ≡-Reasoning
-
--- matrix multiplication
-_·_ : {n m o : ℕ} → Matrix m o → Matrix n m → Matrix n o
-_·_ A B = mapRows ([_] B) A
-
--- alternative form
-_·′_ : Matrix m o → Matrix n m → Matrix n o
-_·′_ A B = (mapRows (A [_]) (B ᵀ)) ᵀ
-
-infixr 9 _·_ _·′_
-
-·-·′ : (A : Matrix m o) (B : Matrix n m) → A · B ≡ A ·′ B
-·-·′ A B = begin
-    mapRows ([_] B) A       ≡⟨ mapRows ([_] B) A ᵀᵀ ⟨
-    mapRows ([_] B) A ᵀ ᵀ   ≡⟨ ≡.cong (_ᵀ) (-[-]ᵀ A B) ⟨
-    mapRows (A [_]) (B ᵀ) ᵀ ∎
-  where
-    open ≡-Reasoning
-
-opaque
-  unfolding _∙_ zeros
-
-  ∙-zerosˡ : (V : Vector n) → zeros ∙ V ≈ 0#
-  ∙-zerosˡ [] = refl
-  ∙-zerosˡ (x ∷ V) = begin
-      0# * x + zeros ∙ V  ≈⟨ +-congʳ (zeroˡ x) ⟩
-      0# + zeros ∙ V      ≈⟨ +-identityˡ (zeros ∙ V) ⟩
-      zeros ∙ V           ≈⟨ ∙-zerosˡ V ⟩
-      0#                  ∎
-    where
-      open ≈-Reasoning setoid
-
-  ∙-zerosʳ : (V : Vector n) → V ∙ zeros ≈ 0#
-  ∙-zerosʳ [] = refl
-  ∙-zerosʳ (x ∷ V) = begin
-      x * 0# + V ∙ zeros  ≈⟨ +-congʳ (zeroʳ x) ⟩
-      0# + V ∙ zeros      ≈⟨ +-identityˡ (V ∙ zeros) ⟩
-      V ∙ zeros           ≈⟨ ∙-zerosʳ V ⟩
-      0#                  ∎
-    where
-      open ≈-Reasoning setoid
-
-opaque
-  unfolding _∙_ _⊕_
-  ∙-distribʳ : (A B C : Vector n) → (A ⊕ B) ∙ C ≈ A ∙ C + B ∙ C
-  ∙-distribʳ [] [] [] = sym (+-identityˡ 0#)
-  ∙-distribʳ (a ∷ A) (b ∷ B) (c ∷ C) = begin
-      (a + b) * c + (zipWith _+_ A B ∙ C) ≈⟨ +-congˡ (∙-distribʳ A B C) ⟩
-      (a + b) * c + (A ∙ C + B ∙ C)       ≈⟨ +-congʳ (distribʳ c a b) ⟩
-      a * c + b * c + (A ∙ C + B ∙ C)     ≈⟨ +-assoc _ _ _ ⟩
-      a * c + (b * c + (A ∙ C + B ∙ C))   ≈⟨ +-congˡ (+-assoc _ _ _) ⟨
-      a * c + (b * c + A ∙ C + B ∙ C)     ≈⟨ +-congˡ (+-congʳ (+-comm _ _)) ⟩
-      a * c + (A ∙ C + b * c + B ∙ C)     ≈⟨ +-congˡ (+-assoc _ _ _) ⟩
-      a * c + (A ∙ C + (b * c + B ∙ C))   ≈⟨ +-assoc _ _ _ ⟨
-      a * c + A ∙ C + (b * c + B ∙ C)     ∎
-    where
-      open ≈-Reasoning setoid
-
-opaque
-  unfolding _⟨_⟩ _∙_
-  *-∙ˡ : (r : R) (A B : Vector n) → r * A ∙ B ≈ r ⟨ A ⟩ ∙ B
-  *-∙ˡ r [] [] = zeroʳ r
-  *-∙ˡ r (a ∷ A) (b ∷ B) = begin
-      r * (a * b + A ∙ B)           ≈⟨ distribˡ r (a * b) (A ∙ B) ⟩
-      r * (a * b) + r * A ∙ B       ≈⟨ +-congʳ (*-assoc r a b) ⟨
-      r * a * b + r * A ∙ B         ≈⟨ +-congˡ (*-∙ˡ r A B )⟩
-      r * a * b + map (r *_) A ∙ B  ∎
-    where
-      open ≈-Reasoning setoid
-
-module _  where
-
-  open ≈-Reasoning setoid
-
-  opaque
-    unfolding [_]_ _[_] zeros _∙_ _≋_ _ᵀ _⊕_ _⟨_⟩
-
-    []-∙ : (V : Vector m) (M : Matrix n m) (W : Vector n) → [ V ] M ∙ W ≈ V ∙ M [ W ]
-    []-∙ {n = n} [] M@[] W = begin
-        map (zeros ∙_) (M ᵀ) ∙ W  ≈⟨ ∙-cong (PW.map⁺ (λ {x} _ → ∙-zerosˡ x) {xs = M ᵀ} ≋.refl) ≊.refl ⟩
-        map (λ _ → 0#) (M ᵀ) ∙ W  ≡⟨ ≡.cong (_∙ W) (map-replicate 0# (M ᵀ)) ⟩
-        zeros ∙ W                 ≈⟨ ∙-zerosˡ W ⟩
-        0#                        ∎
-    []-∙ (V₀ ∷ V) (M₀ ∷ M) W = begin
-        [ V₀ ∷ V ] (M₀ ∷ M) ∙ W                         ≡⟨ ≡.cong (_∙ W) (map-zipWith ((V₀ ∷ V) ∙_) _∷_ M₀ (M ᵀ)) ⟩
-        (zipWith (λ x y → V₀ * x + V ∙ y) M₀ (M ᵀ)) ∙ W ≡⟨ ≡.cong (_∙ W) (zipWith-map-map (V₀ *_) (V ∙_) _+_ M₀ (M ᵀ)) ⟩
-        (V₀ ⟨ M₀ ⟩ ⊕ [ V ] M) ∙ W                       ≈⟨ ∙-distribʳ (map (V₀ *_) M₀) ([ V ] M) W ⟩
-        V₀ ⟨ M₀ ⟩ ∙ W + [ V ] M ∙ W                     ≈⟨ +-congʳ (*-∙ˡ V₀ M₀ W) ⟨
-        V₀ * (M₀ ∙ W) + ([ V ] M) ∙ W                   ≈⟨ +-congˡ ([]-∙ V M W) ⟩
-        (V₀ ∷ V) ∙ (M₀ ∷ M) [ W ] ∎
-
-opaque
-  unfolding _≊_ _[_]
-  -[-]-cong : {x y : Vector n} (A : Matrix n m) → x ≊ y → A [ x ] ≊ A [ y ]
-  -[-]-cong {x = x} {y} A ≋V = PW.map⁺ (λ ≋w → ∙-cong ≋w ≋V) {xs = A} M.≋-refl
-
-opaque
-  unfolding _≊_ [_]_ _ᵀ _≋_
-  [-]--cong : {x y : Vector m} {A B : Matrix n m} → x ≊ y → A ≋ B → [ x ] A ≊ [ y ] B
-  [-]--cong {x = x} {y} ≋V A≋B = PW.map⁺ (λ ≋w → ∙-cong ≋V ≋w) (transpose-cong setoid A≋B)
-
-opaque
-  unfolding mapRows _[_] _≊_
-  ·-[] : {A B C : ℕ} (M : Matrix A B) (N : Matrix B C) (V : Vector A) → (N · M) [ V ] ≊ N [ M [ V ] ]
-  ·-[] {A} {B} {zero} M [] V = PW.[]
-  ·-[] {A} {B} {suc C} M (N₀ ∷ N) V = []-∙ N₀ M V PW.∷ ·-[] M N V
-
-opaque
-  unfolding [_]_ _ᵀ mapRows _≋_
-  []-· : {A B C : ℕ} (V : Vector C) (M : Matrix A B) (N : Matrix B C) → [ V ] (N · M) ≊ [ [ V ] N ] M
-  []-· {A} {B} {C} V M N = begin
-      [ V ] (map ([_] M) N)           ≡⟨ ≡.cong (map (V ∙_)) (-[-]ᵀ N M) ⟨
-      map (V ∙_) (map (N [_]) (M ᵀ))  ≡⟨ map-∘ (V ∙_) (N [_]) (M ᵀ) ⟨
-      map ((V ∙_) ∘ (N [_])) (M ᵀ)    ≈⟨ PW.map⁺ (λ {W} ≋W → trans ([]-∙ V N W) (∙-cong ≊.refl (-[-]-cong N ≋W))) {xs = M ᵀ} ≋.refl ⟨
-      map ([ V ] N ∙_) (M ᵀ)          ∎
-    where
-      open ≈-Reasoning (≊-setoid A)
-
-opaque
-  unfolding mapRows _≋_ _ᵀ
-  ·-assoc : {A B C D : ℕ} {f : Matrix A B} {g : Matrix B C} {h : Matrix C D} → (h · g) · f ≋ h · g · f
-  ·-assoc {A} {B} {C} {D} {f} {g} {h} = begin
-      map ([_] f) (map ([_] g) h)   ≡⟨ map-∘ ([_] f) ([_] g) h ⟨
-      map (λ v → [ [ v ] g ] f) h   ≈⟨ PW.map⁺ (λ {x} x≊y → ≊.trans ([]-· x f g) ([-]--cong ([-]--cong x≊y ≋.refl) ≋.refl)) {xs = h} M.≋-refl ⟨
-      map (λ v → [ v ] (g · f)) h  ∎
-    where
-      open ≈-Reasoning (≋-setoid A D)
-
-opaque
-  unfolding _≋_ _ᵀ _≊_ ≊-setoid I zeros
-  transpose-I : I ᵀ ≡ I {n}
-  transpose-I {zero} = ≡.refl
-  transpose-I {suc n} = begin
-      zipWith _∷_ (1# ∷ zeros) ((map (0# ∷_) I) ᵀ)        ≡⟨ ≡.cong (zipWith _∷_ (1# ∷ zeros) ∘ (_ᵀ)) (zipWith-replicate₁ _∷_ 0# I) ⟨
-      zipWith _∷_ (1# ∷ zeros) ((zipWith _∷_ zeros I) ᵀ)  ≡⟨ ≡.cong (zipWith _∷_ (1# ∷ zeros)) (transpose-zipWith zeros I) ⟩
-      (1# ∷ zeros) ∷ zipWith _∷_ zeros (I ᵀ)              ≡⟨ ≡.cong ((1# ∷ zeros) ∷_) (zipWith-replicate₁ _∷_ 0# (I ᵀ)) ⟩
-      (1# ∷ zeros) ∷ map (0# ∷_) (I ᵀ)                    ≡⟨ ≡.cong (((1# ∷ zeros) ∷_) ∘ map (0# ∷_)) (transpose-I) ⟩
-      (1# ∷ zeros) ∷ map (0# ∷_) I ∎
-    where
-      open ≡-Reasoning
-
-opaque
-  unfolding Vector [_]_ I ≊-setoid _∙_ zeros ≋-setoid mapRows _ᵀ
-  [-]I : {n : ℕ} (V : Vector n) → [ V ] I ≊ V
-  [-]I {zero} [] = ≊.refl
-  [-]I {suc n} (x ∷ V) = begin
-      map ((x ∷ V) ∙_) (zipWith _∷_ (1# ∷ zeros) (map (0# ∷_ ) I ᵀ))      ≡⟨ ≡.cong (map ((x ∷ V) ∙_) ∘ zipWith _∷_ (1# ∷ zeros) ∘ _ᵀ) (zipWith-replicate₁ _∷_ 0# I) ⟨
-      map ((x ∷ V) ∙_) (zipWith _∷_ (1# ∷ zeros) (zipWith _∷_ zeros I ᵀ)) ≡⟨ ≡.cong (map ((x ∷ V) ∙_) ∘ zipWith _∷_ (1# ∷ zeros)) (transpose-zipWith zeros I) ⟩
-      map ((x ∷ V) ∙_) (zipWith _∷_ (1# ∷ zeros) (zeros ∷ I ᵀ))           ≡⟨ ≡.cong (map ((x ∷ V) ∙_) ∘ zipWith _∷_ (1# ∷ zeros) ∘ (zeros ∷_)) transpose-I ⟩
-      map ((x ∷ V) ∙_) (zipWith _∷_ (1# ∷ zeros) (zeros ∷ I))             ≡⟨⟩
-      map ((x ∷ V) ∙_) ((1# ∷ zeros) ∷ zipWith _∷_ zeros I)               ≡⟨ ≡.cong (map ((x ∷ V) ∙_) ∘ ((1# ∷ zeros) ∷_)) (zipWith-replicate₁ _∷_ 0# I) ⟩
-      map ((x ∷ V) ∙_) ((1# ∷ zeros) ∷ map (0# ∷_) I)                     ≡⟨⟩
-      (x ∷ V) ∙ (1# ∷ zeros) ∷ map ((x ∷ V) ∙_) ((map (0# ∷_) I))         ≡⟨⟩
-      x * 1# + V ∙ zeros ∷ map ((x ∷ V) ∙_) (map (0# ∷_) I)               ≈⟨ +-congʳ (*-identityʳ x) PW.∷ ≊.refl ⟩
-      x + V ∙ zeros ∷ map ((x ∷ V) ∙_) (map (0# ∷_) I)                    ≈⟨ +-congˡ (∙-zerosʳ V) PW.∷ ≊.refl ⟩
-      x + 0# ∷ map ((x ∷ V) ∙_) (map (0# ∷_) I)                           ≈⟨ +-identityʳ x PW.∷ ≊.refl ⟩
-      x ∷ map ((x ∷ V) ∙_) (map (0# ∷_) I)                                ≡⟨ ≡.cong (x ∷_) (map-∘ ((x ∷ V) ∙_) (0# ∷_) I) ⟨
-      x ∷ map (λ u → (x ∷ V) ∙ (0# ∷ u)) I                                ≡⟨⟩
-      x ∷ map (λ u → x * 0# + V ∙ u) I                                    ≈⟨ refl PW.∷ PW.map⁺ (λ ≋V → trans (+-congʳ (zeroʳ x)) (+-congˡ (∙-cong {v₁ = V} ≊.refl ≋V))) {xs = I} ≋.refl ⟩
-      x ∷ map (λ u → 0# + V ∙ u) I                                        ≈⟨ refl PW.∷ PW.map⁺ (λ {z} ≋V → trans (+-identityˡ (V ∙ z)) (∙-cong {v₁ = V} ≊.refl ≋V)) {xs = I} ≋.refl ⟩
-      x ∷ map (V ∙_) I                                                    ≡⟨ ≡.cong (λ y → x ∷ map (V ∙_) y) transpose-I ⟨
-      x ∷ map (V ∙_) (I ᵀ)                                                ≈⟨ refl PW.∷ ([-]I V) ⟩
-      x ∷ V                                                               ∎
-    where
-      open ≈-Reasoning (≊-setoid (suc n))
-
-opaque
-  unfolding Vector _≊_ I _[_] _∙_ _≋_
-  transform-with-I : {n : ℕ} (V : Vector n) → I [ V ] ≊ V
-  transform-with-I {zero} [] = PW.[]
-  transform-with-I {suc n} (x ∷ V) = hd PW.∷ tl
-    where
-      hd : (1# ∷ zeros) ∙ (x ∷ V) ≈ x
-      hd = begin
-          1# * x + zeros ∙ V  ≈⟨ +-congʳ (*-identityˡ x) ⟩
-          x + zeros ∙ V       ≈⟨ +-congˡ (∙-zerosˡ V) ⟩
-          x + 0#              ≈⟨ +-identityʳ x ⟩
-          x                   ∎
-        where
-          open ≈-Reasoning setoid
-      tl : map (_∙ (x ∷ V)) (map (0# ∷_ ) I) ≊ V
-      tl = begin
-          map (_∙ (x ∷ V)) (map (0# ∷_) I)  ≡⟨ map-∘ (_∙ (x ∷ V)) (0# ∷_) I ⟨
-          map (λ t → 0# * x + t ∙ V) I      ≈⟨ PW.map⁺ (λ ≋X → trans (+-congʳ (zeroˡ x)) (+-congˡ (∙-cong ≋X ≊.refl))) {xs = I} ≋.refl ⟩
-          map (λ t → 0# + t ∙ V) I          ≈⟨ PW.map⁺ (λ {t} ≋X → trans (+-identityˡ (t ∙ V)) (∙-cong ≋X ≊.refl)) {xs = I} ≋.refl ⟩
-          map (_∙ V) I                      ≈⟨ transform-with-I V ⟩
-          V ∎
-        where
-          open ≈-Reasoning (≊-setoid n)
-
-opaque
-  unfolding mapRows _[_] _ᵀ _≋_ _≊_ [_]_
-  map--[-]-I : (M : Matrix n m) → mapRows (M [_]) I ≋ M ᵀ
-  map--[-]-I {n} {m} [] = ≋.reflexive (map-replicate [] I)
-  map--[-]-I {n} {suc m} (M₀ ∷ M) = begin
-      map ((M₀ ∷ M) [_]) I                        ≡⟨⟩
-      map (λ V → M₀ ∙ V ∷ M [ V ]) I              ≡⟨ zipWith-map (M₀ ∙_) (M [_]) _∷_ I ⟨
-      zipWith _∷_ (map (M₀ ∙_) I) (map (M [_]) I) ≈⟨ zipWith-cong PW._∷_ (≊.reflexive (≡.sym (≡.cong (map (M₀ ∙_)) (transpose-I)))) (map--[-]-I M) ⟩
-      zipWith _∷_ ([ M₀ ] I) (M ᵀ)                ≈⟨ zipWith-cong PW._∷_ ([-]I M₀) ≋.refl ⟩
-      zipWith _∷_ M₀ (M ᵀ)                        ∎
-    where
-      open ≈-Reasoning (≋-setoid (suc m) n)
-
-opaque
-  unfolding mapRows ≋-setoid _ᵀ
-  ·-identityˡ : {f : Matrix n m} → I · f ≋ f
-  ·-identityˡ {A} {B} {f} = begin
-      I · f               ≡⟨ ·-·′ I f ⟩
-      map (I [_]) (f ᵀ) ᵀ ≈⟨ transpose-cong setoid (PW.map⁺ (λ {x} ≊V → ≊.trans (transform-with-I x) ≊V) {xs = f ᵀ} ≋.refl) ⟩
-      map id (f ᵀ) ᵀ      ≡⟨ ≡.cong (_ᵀ) (map-id (f ᵀ)) ⟩
-      f ᵀ ᵀ               ≡⟨ f ᵀᵀ ⟩
-      f                   ∎
-    where
-      open ≈-Reasoning (≋-setoid A B)
-
-opaque
-  unfolding _≋_ mapRows ≊-setoid ≋-setoid _≊_ _ᵀ
-  ·-identityʳ : {f : Matrix n m} → f · I ≋ f
-  ·-identityʳ {A} {B} {f} = begin
-      f · I               ≡⟨ ·-·′ f I ⟩
-      map (f [_]) (I ᵀ) ᵀ ≈⟨ transpose-cong setoid (≋.reflexive (≡.cong (map (f [_])) transpose-I)) ⟩
-      map (f [_]) I ᵀ     ≈⟨ transpose-cong setoid (map--[-]-I f) ⟩
-      f ᵀ ᵀ               ≡⟨ f ᵀᵀ ⟩
-      f ∎
-    where
-      open ≈-Reasoning (≋-setoid A B)
-
-opaque
-  unfolding _ᵀ _≋_ mapRows
-  ·-resp-≋ : {X X′ : Matrix n p} {Y Y′ : Matrix m n} → X ≋ X′ → Y ≋ Y′ → X · Y ≋ X′ · Y′
-  ·-resp-≋ ≋X ≋Y = PW.map⁺ (λ {_} {y} ≋V → [-]--cong ≋V ≋Y) ≋X
-
--- The category of matrices over a rig
-Mat : Category 0ℓ c (c ⊔ ℓ)
-Mat = categoryHelper record
-    { Obj = ℕ
-    ; _⇒_ = Matrix
-    ; _≈_ = _≋_
-    ; id = I
-    ; _∘_ = _·_
-    ; assoc = λ {A B C D f g h} → ·-assoc {f = f} {g} {h}
-    ; identityˡ = ·-identityˡ
-    ; identityʳ = ·-identityʳ
-    ; equiv = ≋-isEquivalence
-    ; ∘-resp-≈ = ·-resp-≋
-    }
diff --git a/Data/Mat/Cocartesian.agda b/Data/Mat/Cocartesian.agda
deleted file mode 100644
index 5ea92b3..0000000
--- a/Data/Mat/Cocartesian.agda
+++ /dev/null
@@ -1,623 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Algebra.Bundles using (Semiring)
-open import Level using (Level)
-
-module Data.Mat.Cocartesian {c ℓ : Level} (Rig : Semiring c ℓ) where
-
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
-
-open import Data.Mat.Category Rig
-  using
-   ( Mat; Matrix; Vector; zeros; I; _≊_; module ≊; ≊-setoid; _≋_; module ≋; ≋-setoid
-   ; _ᵀ; mapRows; _·_; _∙_; _ᵀᵀ; _⊕_; ·-identityʳ; ∙-zerosʳ; ∙-zerosˡ
-   )
-  renaming ([_]_ to [_]′_)
-
-open import Categories.Category.Cocartesian Mat using (Cocartesian)
-open import Categories.Object.Coproduct Mat using (Coproduct)
-open import Categories.Object.Initial Mat using (Initial)
-open import Data.Mat.Util using (replicate-++; zipWith-map; transpose-zipWith; zipWith-cong)
-open import Data.Nat as ℕ using (ℕ)
-open import Data.Product using (_,_; Σ-syntax)
-open import Data.Vec using (Vec; map; zipWith; replicate; _++_; head; tail)
-open import Data.Vec.Properties using (zipWith-replicate; map-cong; map-const; map-id)
-open import Function using (id; _∘_)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
-
-open Semiring Rig renaming (Carrier to R)
-open Vec
-open ℕ.ℕ
-
-private
-  variable
-    A B C D : ℕ
-    A₁ A₂ B₁ B₂ : ℕ
-
-opaque
-  unfolding Vector
-  _+++_ : Vector A → Vector B → Vector (A ℕ.+ B)
-  _+++_ = _++_
-
-opaque
-  unfolding Matrix Vector
-  _∥_ : Matrix A C → Matrix B C → Matrix (A ℕ.+ B) C
-  _∥_ M N = zipWith _++_ M N
-
-opaque
-  unfolding Matrix
-  [_] : Vector A → Matrix A 1
-  [_] V = V ∷ []
-
-opaque
-  unfolding Matrix Vector
-  ⟦_⟧ : R → Matrix 1 1
-  ⟦_⟧ x = [ x ∷ [] ]
-
-[_]ᵀ : Vector A → Matrix 1 A
-[_]ᵀ V = [ V ] ᵀ
-
-opaque
-  unfolding Vector
-  ⟨⟩ : Vector 0
-  ⟨⟩ = []
-
-opaque
-  unfolding Vector
-  _∷′_ : R → Vector A → Vector (suc A)
-  _∷′_ = _∷_
-
-infixr 5 _∷′_
-
-infixr 7 _∥_
-
-opaque
-  unfolding Matrix
-  _≑_ : Matrix A B → Matrix A C → Matrix A (B ℕ.+ C)
-  _≑_ M N = M ++ N
-
-infixr 6 _≑_
-
-opaque
-  unfolding Matrix
-  _∷ᵥ_ : Vector A → Matrix A B → Matrix A (suc B)
-  _∷ᵥ_ V M = V ∷ M
-
-infixr 5 _∷ᵥ_
-
-opaque
-  unfolding Matrix Vector
-  _∷ₕ_ : Vector B → Matrix A B → Matrix (suc A) B
-  _∷ₕ_ V M = zipWith _∷_ V M
-
-infixr 5 _∷ₕ_
-
-opaque
-  unfolding Matrix
-  headᵥ : Matrix A (suc B) → Vector A
-  headᵥ (V ∷ _) = V
-
-opaque
-  unfolding Matrix
-  tailᵥ : Matrix A (suc B) → Matrix A B
-  tailᵥ (_ ∷ M) = M
-
-opaque
-  unfolding Matrix Vector
-  headₕ : Matrix (suc A) B → Vector B
-  headₕ M = map head M
-
-opaque
-  unfolding Matrix Vector
-  tailₕ : Matrix (suc A) B → Matrix A B
-  tailₕ M = map tail M
-
-opaque
-  unfolding _∷ᵥ_ headᵥ tailᵥ
-  head-∷-tailᵥ : (M : Matrix A (suc B)) → headᵥ M ∷ᵥ tailᵥ M ≡ M
-  head-∷-tailᵥ (_ ∷ _) = ≡.refl
-
-opaque
-  unfolding _∷ₕ_ headₕ tailₕ
-  head-∷-tailₕ : (M : Matrix (suc A) B) → headₕ M ∷ₕ tailₕ M ≡ M
-  head-∷-tailₕ M = begin
-      zipWith _∷_ (map head M) (map tail M) ≡⟨ zipWith-map head tail _∷_ M ⟩
-      map (λ x → head x ∷ tail x) M         ≡⟨ map-cong (λ { (_ ∷ _) → ≡.refl }) M ⟩
-      map id M                              ≡⟨ map-id M ⟩
-      M ∎
-    where
-      open ≡-Reasoning
-
-opaque
-  unfolding Matrix
-  []ₕ : Matrix A 0
-  []ₕ = []
-
-opaque
-  unfolding []ₕ _ᵀ
-  []ᵥ : Matrix 0 B
-  []ᵥ = []ₕ ᵀ
-
-opaque
-  unfolding []ᵥ
-  []ᵥ-ᵀ : []ᵥ ᵀ ≡ []ₕ {A}
-  []ᵥ-ᵀ = []ₕ ᵀᵀ
-
-opaque
-  unfolding []ₕ
-  []ₕ-! : (E : Matrix A 0) → E ≡ []ₕ
-  []ₕ-! [] = ≡.refl
-
-opaque
-  unfolding []ᵥ
-  []ᵥ-! : (E : Matrix 0 B) → E ≡ []ᵥ
-  []ᵥ-! [] = ≡.refl
-  []ᵥ-! ([] ∷ E) = ≡.cong ([] ∷_) ([]ᵥ-! E)
-
-opaque
-  unfolding Matrix Vector
-  _∷[_,_]_ : R → Vector B → Vector A → Matrix A B → Matrix (suc A) (suc B)
-  _∷[_,_]_ v C R M = (v ∷ R) ∷ᵥ (C ∷ₕ M)
-
-opaque
-  unfolding Matrix
-  𝟎 : Matrix A B
-  𝟎 {A} {B} = replicate B zeros
-
-opaque
-  unfolding 𝟎 _ᵀ zeros _∷ₕ_ _∥_
-  𝟎ᵀ : 𝟎 ᵀ ≡ 𝟎 {A} {B}
-  𝟎ᵀ {zero} = ≡.refl
-  𝟎ᵀ {suc A} = begin
-      zeros ∷ₕ (𝟎 ᵀ)  ≡⟨ ≡.cong (zeros ∷ₕ_) 𝟎ᵀ ⟩
-      zeros ∷ₕ 𝟎      ≡⟨ zipWith-replicate _∷_ 0# zeros ⟩
-      𝟎               ∎
-    where
-      open ≡-Reasoning
-
-opaque
-  unfolding _∥_ []ᵥ
-  []ᵥ-∥ : (M : Matrix A B) → []ᵥ ∥ M ≡ M
-  []ᵥ-∥ [] = ≡.refl
-  []ᵥ-∥ (M₀ ∷ M) = ≡.cong (M₀ ∷_) ([]ᵥ-∥ M)
-
-opaque
-  unfolding _≑_ []ₕ
-  []ₕ-≑ : (M : Matrix A B) → []ₕ ≑ M ≡ M
-  []ₕ-≑ _ = ≡.refl
-
-opaque
-  unfolding _∷ₕ_ _ᵀ _∷ᵥ_
-  ∷ₕ-ᵀ : (V : Vector A) (M : Matrix B A) → (V ∷ₕ M) ᵀ ≡ V ∷ᵥ M ᵀ
-  ∷ₕ-ᵀ = transpose-zipWith
-
-opaque
-  unfolding _∷ₕ_ _ᵀ _∷ᵥ_
-  ∷ᵥ-ᵀ : (V : Vector B) (M : Matrix B A) → (V ∷ᵥ M) ᵀ ≡ V ∷ₕ M ᵀ
-  ∷ᵥ-ᵀ V M = ≡.refl
-
-opaque
-  unfolding _∷ₕ_ _∥_
-  ∷ₕ-∥ : (V : Vector C) (M : Matrix A C) (N : Matrix B C) → V ∷ₕ (M ∥ N) ≡ (V ∷ₕ M) ∥ N
-  ∷ₕ-∥ [] [] [] = ≡.refl
-  ∷ₕ-∥ (x ∷ V) (M₀ ∷ M) (N₀ ∷ N) = ≡.cong ((x ∷ M₀ ++ N₀) ∷_) (∷ₕ-∥ V M N)
-
-opaque
-  unfolding _∷ᵥ_ _≑_
-  ∷ᵥ-≑ : (V : Vector A) (M : Matrix A B) (N : Matrix A C) → V ∷ᵥ (M ≑ N) ≡ (V ∷ᵥ M) ≑ N
-  ∷ᵥ-≑ V M N = ≡.refl
-
-opaque
-  unfolding zeros [_]′_ Matrix _∙_
-  [-]- : (V : Vector 0) (E : Matrix A 0) → [ V ]′ E ≡ zeros
-  [-]- {zero} _ [] = ≡.refl
-  [-]- {suc A} [] [] = ≡.cong (0# ∷_) ([-]- [] [])
-
-opaque
-  unfolding ⟨⟩ _+++_
-  ⟨⟩-+++ : (V : Vector A) → ⟨⟩ +++ V ≡ V
-  ⟨⟩-+++ V = ≡.refl
-
-opaque
-  unfolding _∷′_ _+++_
-  ∷-+++ : (x : R) (M : Vector A) (N : Vector B) → (x ∷′ M) +++ N ≡ x ∷′ (M +++ N)
-  ∷-+++ x M N = ≡.refl
-
-opaque
-  unfolding []ₕ [_]′_ _ᵀ []ᵥ ⟨⟩
-  [-]-[]ᵥ : (V : Vector A) → [ V ]′ []ᵥ ≡ ⟨⟩
-  [-]-[]ᵥ [] = ≡.refl
-  [-]-[]ᵥ (x ∷ V) = ≡.cong (map ((x ∷ V) ∙_)) []ᵥ-ᵀ
-
-opaque
-  unfolding [_]′_ _ᵀ _∷ᵥ_ _∷′_
-  [-]-∷ₕ : (V M₀ : Vector B) (M : Matrix A B) → [ V ]′ (M₀ ∷ₕ M) ≡ V ∙ M₀ ∷′ ([ V ]′ M)
-  [-]-∷ₕ V M₀ M = ≡.cong (map (V ∙_)) (∷ₕ-ᵀ M₀ M)
-    where
-      open ≡-Reasoning
-
-[-]--∥
-    : (V : Vector C)
-      (M : Matrix A C)
-      (N : Matrix B C)
-    → [ V ]′ (M ∥ N) ≡ ([ V ]′ M) +++ ([ V ]′ N)
-[-]--∥ {C} {zero} V M N rewrite []ᵥ-! M = begin
-    [ V ]′ ([]ᵥ ∥ N)            ≡⟨ ≡.cong ([ V ]′_) ([]ᵥ-∥ N) ⟩
-    [ V ]′ N                    ≡⟨ ⟨⟩-+++ ([ V ]′ N) ⟨
-    ⟨⟩ +++ ([ V ]′ N)           ≡⟨ ≡.cong (_+++ ([ V ]′ N)) ([-]-[]ᵥ V) ⟨
-    ([ V ]′ []ᵥ) +++ ([ V ]′ N) ∎
-  where
-    open ≡-Reasoning
-[-]--∥ {C} {suc A} V M N
-  rewrite ≡.sym (head-∷-tailₕ M)
-  using M₀ ← headₕ M
-  using M ← tailₕ M = begin
-    [ V ]′ ((M₀ ∷ₕ M) ∥ N)                ≡⟨ ≡.cong ([ V ]′_) (∷ₕ-∥ M₀ M N) ⟨
-    [ V ]′ (M₀ ∷ₕ (M ∥ N))                ≡⟨ [-]-∷ₕ V M₀ (M ∥ N) ⟩
-    V ∙ M₀ ∷′ ([ V ]′ (M ∥ N))            ≡⟨ ≡.cong (V ∙ M₀ ∷′_) ([-]--∥ V M N) ⟩
-    V ∙ M₀ ∷′ (([ V ]′ M) +++ ([ V ]′ N)) ≡⟨ ∷-+++ (V ∙ M₀) ([ V ]′ M) ([ V ]′ N) ⟨
-    (V ∙ M₀ ∷′ [ V ]′ M) +++ ([ V ]′ N)   ≡⟨ ≡.cong (_+++ ([ V ]′ N)) ([-]-∷ₕ V M₀ M) ⟨
-    ([ V ]′ (M₀ ∷ₕ M)) +++ ([ V ]′ N)     ∎
-  where
-    open ≡-Reasoning
-
-opaque
-  unfolding _∥_ mapRows _+++_
-  ·-∥
-      : (M : Matrix C D)
-        (N : Matrix A C)
-        (P : Matrix B C)
-      → M · (N ∥ P) ≡ M · N ∥ M · P
-  ·-∥ {C} {D} {A} {B} [] N P = ≡.refl
-  ·-∥ {C} {D} {A} {B} (M₀ ∷ M) N P = ≡.cong₂ _∷_ ([-]--∥ M₀ N P) (·-∥ M N P)
-
-opaque
-  unfolding _≑_ mapRows
-  ≑-· : (M : Matrix B C)
-        (N : Matrix B D)
-        (P : Matrix A B)
-      → (M ≑ N) · P ≡ (M · P) ≑ (N · P)
-  ≑-· [] N P = ≡.refl
-  ≑-· (M₀ ∷ M) N P = ≡.cong ([ M₀ ]′ P ∷_) (≑-· M N P)
-
-opaque
-  unfolding Matrix
-  _[+]_ : Matrix A B → Matrix A B → Matrix A B
-  _[+]_ = zipWith _⊕_
-
-opaque
-  unfolding _+++_ _≑_ _∷ₕ_
-  ∷ₕ-≑ : (V : Vector A) (W : Vector B) (M : Matrix C A) (N : Matrix C B) → (V +++ W) ∷ₕ (M ≑ N) ≡ (V ∷ₕ M) ≑ (W ∷ₕ N)
-  ∷ₕ-≑ [] W [] N = ≡.refl
-  ∷ₕ-≑ (x ∷ V) W (M₀ ∷ M) N = ≡.cong ((x ∷ M₀) ∷_) (∷ₕ-≑ V W M N)
-
-opaque
-  unfolding _+++_ _∙_
-  ∙-+++ : (W Y : Vector A) (X Z : Vector B) → (W +++ X) ∙ (Y +++ Z) ≈ W ∙ Y + X ∙ Z
-  ∙-+++ [] [] X Z = sym (+-identityˡ (X ∙ Z))
-  ∙-+++ (w ∷ W) (y ∷ Y) X Z = begin
-      w * y + (W ++ X) ∙ (Y ++ Z) ≈⟨ +-congˡ (∙-+++ W Y X Z) ⟩
-      w * y + (W ∙ Y + X ∙ Z)     ≈⟨ +-assoc _ _ _ ⟨
-      (w * y + W ∙ Y) + X ∙ Z     ∎
-    where
-      open ≈-Reasoning setoid
-
-opaque
-  unfolding []ᵥ _≑_
-  []ᵥ-≑ : []ᵥ {A} ≑ []ᵥ {B} ≡ []ᵥ
-  []ᵥ-≑ {A} {B} = replicate-++ A B []
-
-opaque
-  unfolding _⊕_ ⟨⟩
-  ⟨⟩-⊕ : ⟨⟩ ⊕ ⟨⟩ ≡ ⟨⟩
-  ⟨⟩-⊕ = ≡.refl
-
-opaque
-  unfolding ≊-setoid _∷′_ _⊕_
-  [+++]-≑
-      : (V : Vector B)
-        (W : Vector C)
-        (M : Matrix A B)
-        (N : Matrix A C)
-      → [ V +++ W ]′ (M ≑ N)
-      ≊ [ V ]′ M ⊕ [ W ]′ N
-  [+++]-≑ {B} {C} {zero} V W M N
-    rewrite []ᵥ-! M
-    rewrite []ᵥ-! N = begin
-      [ V +++ W ]′ ([]ᵥ {B} ≑ []ᵥ)  ≡⟨ ≡.cong ([ V +++ W ]′_) []ᵥ-≑ ⟩
-      [ V +++ W ]′ []ᵥ              ≡⟨ [-]-[]ᵥ (V +++ W) ⟩
-      ⟨⟩                            ≡⟨ ⟨⟩-⊕ ⟨
-      ⟨⟩ ⊕ ⟨⟩                       ≡⟨ ≡.cong₂ _⊕_ ([-]-[]ᵥ V) ([-]-[]ᵥ W) ⟨
-      [ V ]′ []ᵥ ⊕ [ W ]′ []ᵥ       ∎
-    where
-      open ≈-Reasoning (≊-setoid 0)
-  [+++]-≑ {B} {C} {suc A} V W M N
-    rewrite ≡.sym (head-∷-tailₕ M)
-    rewrite ≡.sym (head-∷-tailₕ N)
-    using M₀ ← headₕ M
-    using M ← tailₕ M
-    using N₀ ← headₕ N
-    using N ← tailₕ N = begin
-      [ V +++ W ]′ ((M₀ ∷ₕ M) ≑ (N₀ ∷ₕ N))              ≡⟨ ≡.cong ([ V +++ W ]′_) (∷ₕ-≑ M₀ N₀ M N) ⟨
-      [ V +++ W ]′ ((M₀ +++ N₀) ∷ₕ (M ≑ N))             ≡⟨ [-]-∷ₕ (V +++ W) (M₀ +++ N₀) (M ≑ N) ⟩
-      (V +++ W) ∙ (M₀ +++ N₀) ∷′ ([ V +++ W ]′ (M ≑ N)) ≈⟨ ∙-+++ V M₀ W N₀ PW.∷ [+++]-≑ V W M N ⟩
-      (V ∙ M₀ ∷′ [ V ]′ M) ⊕ (W ∙ N₀ ∷′ [ W ]′ N)       ≡⟨ ≡.cong₂ _⊕_ ([-]-∷ₕ V M₀ M) ([-]-∷ₕ W N₀ N) ⟨
-      ([ V ]′ (M₀ ∷ₕ M)) ⊕ ([ W ]′ (N₀ ∷ₕ N))           ∎
-    where
-      open ≈-Reasoning (≊-setoid (suc A))
-
-opaque
-  unfolding _∥_ _+++_ mapRows _[+]_ ≋-setoid
-  ∥-·-≑
-      : (W : Matrix A C)
-        (X : Matrix B C)
-        (Y : Matrix D A)
-        (Z : Matrix D B)
-      → (W ∥ X) · (Y ≑ Z) ≋ (W · Y) [+] (X · Z)
-  ∥-·-≑ [] [] Y Z = PW.[]
-  ∥-·-≑ {A} {C} {B} {D} (W₀ ∷ W) (X₀ ∷ X) Y Z = [+++]-≑ W₀ X₀ Y Z PW.∷ ∥-·-≑ W X Y Z
-    where
-      open ≈-Reasoning (≋-setoid A B)
-
-opaque
-  unfolding _⊕_ _≊_
-  ⊕-cong : {V V′ W W′ : Vector A} → V ≊ V′ → W ≊ W′ → V ⊕ W ≊ V′ ⊕ W′
-  ⊕-cong = zipWith-cong +-cong
-
-opaque
-  unfolding _[+]_ _≋_
-  [+]-cong : {M M′ N N′ : Matrix A B} → M ≋ M′ → N ≋ N′ → M [+] N ≋ M′ [+] N′
-  [+]-cong = zipWith-cong ⊕-cong
-
-opaque
-  unfolding ⟨⟩ []ₕ [_]′_ zeros _∙_
-  [⟨⟩]-[]ₕ : [ ⟨⟩ ]′ ([]ₕ {A}) ≡ zeros {A}
-  [⟨⟩]-[]ₕ {zero} = ≡.refl
-  [⟨⟩]-[]ₕ {suc A} = ≡.cong (0# ∷_) [⟨⟩]-[]ₕ
-
-opaque
-  unfolding Vector ⟨⟩ zeros []ᵥ [_]′_ _ᵀ _∷ₕ_ 𝟎 _≊_
-  [-]-𝟎 : (V : Vector A) →  [ V ]′ (𝟎 {B}) ≊ zeros
-  [-]-𝟎 {A} {zero} V = ≊.reflexive (≡.cong (map (V ∙_)) 𝟎ᵀ)
-  [-]-𝟎 {A} {suc B} V = begin
-      map (V ∙_) (𝟎 ᵀ)          ≡⟨ ≡.cong (map (V ∙_)) 𝟎ᵀ ⟩
-      V ∙ zeros ∷ map (V ∙_) 𝟎  ≡⟨ ≡.cong ((V ∙ zeros ∷_) ∘ map (V ∙_)) 𝟎ᵀ ⟨
-      V ∙ zeros ∷ [ V ]′ 𝟎      ≈⟨ ∙-zerosʳ V PW.∷ ([-]-𝟎 V) ⟩
-      0# ∷ zeros                ∎
-    where
-      open ≈-Reasoning (≊-setoid (suc B))
-
-opaque
-  unfolding _⊕_ zeros _≊_
-  ⊕-zerosʳ : (V : Vector A) → V ⊕ zeros ≊ V
-  ⊕-zerosʳ [] = PW.[]
-  ⊕-zerosʳ (x ∷ V) = +-identityʳ x PW.∷ ⊕-zerosʳ V
-
-opaque
-  unfolding _⊕_ zeros _≊_
-  ⊕-zerosˡ : (V : Vector A) → zeros ⊕ V ≊ V
-  ⊕-zerosˡ [] = PW.[]
-  ⊕-zerosˡ (x ∷ V) = +-identityˡ x PW.∷ ⊕-zerosˡ V
-
-opaque
-  unfolding Matrix _[+]_ _≋_ 𝟎
-  [+]-𝟎ʳ : (M : Matrix A B) → M [+] 𝟎 ≋ M
-  [+]-𝟎ʳ [] = PW.[]
-  [+]-𝟎ʳ (M₀ ∷ M) = ⊕-zerosʳ M₀ PW.∷ [+]-𝟎ʳ M
-
-opaque
-  unfolding Matrix _[+]_ _≋_ 𝟎
-  [+]-𝟎ˡ : (M : Matrix A B) → 𝟎 [+] M ≋ M
-  [+]-𝟎ˡ [] = PW.[]
-  [+]-𝟎ˡ (M₀ ∷ M) = ⊕-zerosˡ M₀ PW.∷ [+]-𝟎ˡ M
-
-
-opaque
-  unfolding ≋-setoid mapRows 𝟎
-  ·-𝟎ʳ : (M : Matrix A B) →  M · 𝟎 {C} ≋ 𝟎
-  ·-𝟎ʳ [] = ≋.refl
-  ·-𝟎ʳ (M₀ ∷ M) = begin
-      [ M₀ ]′ 𝟎 ∷ M · 𝟎 ≈⟨ [-]-𝟎 M₀ PW.∷ ·-𝟎ʳ M ⟩
-      zeros ∷ 𝟎         ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-
-opaque
-  unfolding Matrix zeros ≊-setoid _∷′_ ⟨⟩
-  [zeros]- : (M : Matrix A B) → [ zeros ]′ M ≊ zeros
-  [zeros]- {zero} M rewrite []ᵥ-! M = ≊.reflexive ([-]-[]ᵥ zeros)
-  [zeros]- {suc A} M
-    rewrite ≡.sym (head-∷-tailₕ M)
-    using M₀ ← headₕ M
-    using M ← tailₕ M = begin
-      [ zeros ]′ (M₀ ∷ₕ M)      ≡⟨ [-]-∷ₕ zeros M₀ M ⟩
-      zeros ∙ M₀ ∷ [ zeros ]′ M ≈⟨ ∙-zerosˡ M₀ PW.∷ [zeros]- M ⟩
-      0# ∷ zeros                ∎
-    where
-      open ≈-Reasoning (≊-setoid _)
-
-opaque
-  unfolding ≋-setoid mapRows 𝟎 _ᵀ []ᵥ
-  ·-𝟎ˡ : (M : Matrix A B) →  𝟎 {B} {C} · M ≋ 𝟎
-  ·-𝟎ˡ {A} {B} {zero} M = PW.[]
-  ·-𝟎ˡ {A} {B} {suc C} M = [zeros]- M PW.∷ ·-𝟎ˡ M
-
-opaque
-  unfolding ≋-setoid
-  inj₁ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (I ≑ 𝟎) ≋ M
-  inj₁ {A} {C} M N = begin
-      (M ∥ N) · (I ≑ 𝟎)   ≈⟨ ∥-·-≑ M N I 𝟎 ⟩
-      (M · I) [+] (N · 𝟎) ≈⟨ [+]-cong ·-identityʳ (·-𝟎ʳ N) ⟩
-      M [+] 𝟎             ≈⟨ [+]-𝟎ʳ M ⟩
-      M ∎
-    where
-      open ≈-Reasoning (≋-setoid A C)
-
-opaque
-  unfolding ≋-setoid
-  inj₂ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (𝟎 ≑ I) ≋ N
-  inj₂ {A} {C} {B} M N = begin
-      (M ∥ N) · (𝟎 ≑ I)   ≈⟨ ∥-·-≑ M N 𝟎 I ⟩
-      (M · 𝟎) [+] (N · I) ≈⟨ [+]-cong (·-𝟎ʳ M) ·-identityʳ ⟩
-      𝟎 [+] N             ≈⟨ [+]-𝟎ˡ N ⟩
-      N ∎
-    where
-      open ≈-Reasoning (≋-setoid B C)
-
-opaque
-  unfolding Matrix
-  split-∥ : (A : ℕ) → (M : Matrix (A ℕ.+ B) C) → Σ[ M₁ ∈ Matrix A C ] Σ[ M₂ ∈ Matrix B C ] M₁ ∥ M₂ ≡ M
-  split-∥ zero M = []ᵥ , M , []ᵥ-∥ M
-  split-∥ (suc A) M′
-    rewrite ≡.sym (head-∷-tailₕ M′)
-    using M₀ ← headₕ M′
-    using M ← tailₕ M′
-    with split-∥ A M
-  ... | M₁ , M₂ , M₁∥M₂≡M = M₀ ∷ₕ M₁ , M₂ , (begin
-      (M₀ ∷ₕ M₁) ∥ M₂ ≡⟨ ∷ₕ-∥ M₀ M₁ M₂ ⟨
-      M₀ ∷ₕ M₁ ∥ M₂   ≡⟨ ≡.cong (M₀ ∷ₕ_) M₁∥M₂≡M ⟩
-      M₀ ∷ₕ M ∎)
-    where
-      open ≡-Reasoning
-
-opaque
-  unfolding _≋_ _∷ₕ_
-  ∷ₕ-cong : {V V′ : Vector B} {M M′ : Matrix A B} → V ≊ V′ → M ≋ M′ → V ∷ₕ M ≋ V′ ∷ₕ M′
-  ∷ₕ-cong PW.[] PW.[] = PW.[]
-  ∷ₕ-cong (≈x PW.∷ ≊V) (≊M₀ PW.∷ ≋M) = (≈x PW.∷ ≊M₀) PW.∷ (∷ₕ-cong ≊V ≋M)
-
-opaque
-  unfolding Vector
-  head′ : Vector (suc A) → R
-  head′ = head
-
-opaque
-  unfolding Vector
-  tail′ : Vector (suc A) → Vector A
-  tail′ = tail
-
-opaque
-  unfolding _≊_ head′
-  head-cong : {V V′ : Vector (suc A)} → V ≊ V′ → head′ V ≈ head′ V′
-  head-cong (≈x PW.∷ _) = ≈x
-
-opaque
-  unfolding _≊_ tail′
-  tail-cong : {V V′ : Vector (suc A)} → V ≊ V′ → tail′ V ≊ tail′ V′
-  tail-cong (_ PW.∷ ≊V) = ≊V
-
-opaque
-  unfolding _≋_ headₕ head′
-  ≋headₕ : {M M′ : Matrix (suc A) B} → M ≋ M′ → headₕ M ≊ headₕ M′
-  ≋headₕ M≋M′ = PW.map⁺ head-cong M≋M′
-
-opaque
-  unfolding _≋_ tailₕ tail′
-  ≋tailₕ : {M M′ : Matrix (suc A) B} → M ≋ M′ → tailₕ M ≋ tailₕ M′
-  ≋tailₕ M≋M′ = PW.map⁺ tail-cong M≋M′
-
-opaque
-  unfolding _≋_ _≊_ _∷ₕ_
-  _≋∷ₕ_ : {V V′ : Vector B} → V ≊ V′ → {M M′ : Matrix A B} → M ≋ M′ → V ∷ₕ M ≋ V′ ∷ₕ M′
-  _≋∷ₕ_ PW.[] PW.[] = PW.[]
-  _≋∷ₕ_ (≈x PW.∷ ≊V) (≊M₀ PW.∷ ≋M) = (≈x PW.∷ ≊M₀) PW.∷ (≊V ≋∷ₕ ≋M)
-
-opaque
-  unfolding _≋_ _∥_ []ᵥ _∷ₕ_
-  ∥-cong : {M M′ : Matrix A C} {N N′ : Matrix B C} → M ≋ M′ → N ≋ N′ → M ∥ N ≋ M′ ∥ N′
-  ∥-cong {zero} {C} {B} {M} {M′} {N} {N′} ≋M ≋N
-    rewrite []ᵥ-! M
-    rewrite []ᵥ-! M′ = begin
-      ([]ᵥ ∥ N)   ≡⟨ []ᵥ-∥ N ⟩
-      N           ≈⟨ ≋N ⟩
-      N′          ≡⟨ []ᵥ-∥ N′ ⟨
-      ([]ᵥ ∥ N′)  ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-  ∥-cong {suc A} {C} {B} {M} {M′} {N} {N′} ≋M ≋N
-    rewrite ≡.sym (head-∷-tailₕ M)
-    using M₀ ← headₕ M
-    using M- ← tailₕ M
-    rewrite ≡.sym (head-∷-tailₕ M′)
-    using M₀′ ← headₕ M′
-    using M-′ ← tailₕ M′ = begin
-      (M₀ ∷ₕ M-) ∥ N     ≡⟨ ∷ₕ-∥ M₀ M- N ⟨
-      M₀ ∷ₕ M- ∥ N       ≈⟨ ∷ₕ-cong ≊M₀ (∥-cong ≋M- ≋N) ⟩
-      M₀′ ∷ₕ M-′ ∥ N′    ≡⟨ ∷ₕ-∥ M₀′ M-′ N′ ⟩
-      (M₀′ ∷ₕ M-′) ∥ N′  ∎
-    where
-      ≊M₀ : M₀ ≊ M₀′
-      ≊M₀ = begin
-          headₕ M             ≡⟨ ≡.cong headₕ (head-∷-tailₕ M) ⟨
-          headₕ (M₀ ∷ₕ M-)    ≈⟨ ≋headₕ ≋M ⟩
-          headₕ (M₀′ ∷ₕ M-′)  ≡⟨ ≡.cong headₕ (head-∷-tailₕ M′) ⟩
-          headₕ M′            ∎
-        where
-          open ≈-Reasoning (≊-setoid _)
-      ≋M- : M- ≋ M-′
-      ≋M- = begin
-          tailₕ M             ≡⟨ ≡.cong tailₕ (head-∷-tailₕ M) ⟨
-          tailₕ (M₀ ∷ₕ M-)    ≈⟨ ≋tailₕ ≋M ⟩
-          tailₕ (M₀′ ∷ₕ M-′)  ≡⟨ ≡.cong tailₕ (head-∷-tailₕ M′) ⟩
-          tailₕ M′            ∎
-        where
-          open ≈-Reasoning (≋-setoid _ _)
-      open ≈-Reasoning (≋-setoid _ _)
-
-opaque
-  unfolding _≋_ _≑_
-  ≑-cong : {M M′ : Matrix A B} {N N′ : Matrix A C} → M ≋ M′ → N ≋ N′ → M ≑ N ≋ M′ ≑ N′
-  ≑-cong PW.[] ≋N = ≋N
-  ≑-cong (M₀≊M₀′ PW.∷ ≋M) ≋N = M₀≊M₀′ PW.∷ ≑-cong ≋M ≋N
-
-opaque
-  unfolding ≋-setoid
-  uniq
-      : (H : Matrix (A ℕ.+ B) C)
-        (M : Matrix A C)
-        (N : Matrix B C)
-      → H · (I ≑ 𝟎) ≋ M
-      → H · (𝟎 ≑ I) ≋ N
-      → M ∥ N ≋ H
-  uniq {A} {B} {C} H M N eq₁ eq₂
-    with (H₁ , H₂ , H₁∥H₂≡H) ← split-∥ A H
-    rewrite ≡.sym H₁∥H₂≡H = begin
-      M ∥ N                                         ≈⟨ ∥-cong eq₁ eq₂ ⟨
-      (H₁ ∥ H₂) · (I {A} ≑ 𝟎) ∥ (H₁ ∥ H₂) · (𝟎 ≑ I) ≈⟨ ∥-cong (inj₁ H₁ H₂) (inj₂ H₁ H₂) ⟩
-      (H₁ ∥ H₂) ∎
-    where
-      open ≈-Reasoning (≋-setoid (A ℕ.+ B) C)
-
-coproduct : Coproduct A B
-coproduct {A} {B} = record
-    { A+B = A ℕ.+ B
-    ; i₁ = I ≑ 𝟎
-    ; i₂ = 𝟎 ≑ I
-    ; [_,_] = _∥_
-    ; inject₁ = λ {a} {b} {c} → inj₁ b c
-    ; inject₂ = λ {a} {b} {c} → inj₂ b c
-    ; unique = λ eq₁ eq₂ → uniq _ _ _ eq₁ eq₂
-    }
-
-opaque
-  unfolding _≋_
-  !-unique : (E : Matrix 0 B) → []ᵥ ≋ E
-  !-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E))
-
-initial : Initial
-initial = record
-    { ⊥ = 0
-    ; ⊥-is-initial = record
-        { ! = []ᵥ
-        ; !-unique = !-unique
-        }
-    }
-
-Mat-Cocartesian : Cocartesian
-Mat-Cocartesian = record
-    { initial = initial
-    ; coproducts = record
-        { coproduct = coproduct
-        }
-    }
diff --git a/Data/Mat/Dagger-2-Poset.agda b/Data/Mat/Dagger-2-Poset.agda
deleted file mode 100644
index cb939d1..0000000
--- a/Data/Mat/Dagger-2-Poset.agda
+++ /dev/null
@@ -1,79 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Algebra using (Idempotent; CommutativeSemiring)
-open import Level using (Level)
-
-module Data.Mat.Dagger-2-Poset
-    {c ℓ : Level}
-    (Rig : CommutativeSemiring c ℓ)
-    (let module Rig = CommutativeSemiring Rig)
-    (+-idem : Idempotent Rig._≈_ Rig._+_)
-  where
-
-import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-
-open import Data.Mat.Util using (transpose-cong; replicate-++)
-open import Data.Mat.Category Rig.semiring
-  using
-    ( Mat; _ᵀ; transpose-I; I; _≋_; module ≋; _≊_; Matrix; Vector
-    ; ≋-setoid; _·_; ·-identityˡ; ·-identityʳ; ·-resp-≋; ·-assoc; _⊕_
-    )
-open import Data.Mat.Cocartesian Rig.semiring
-  using
-    ( 𝟎 ; _∥_; _≑_; ∥-cong; ≑-cong; ≑-·; ·-𝟎ˡ; ·-∥; ∥-·-≑
-    ; _[+]_; [+]-cong; [+]-𝟎ʳ; [+]-𝟎ˡ
-    )
-open import Data.Mat.SemiadditiveDagger Rig using (∥-ᵀ; Mat-SemiadditiveDagger)
-open import Category.Dagger.Semiadditive Mat using (IdempotentSemiadditiveDagger)
-open import Category.Dagger.2-Poset using (dagger-2-poset; Dagger-2-Poset)
-open import Data.Nat using (ℕ)
-open import Data.Vec using (Vec)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
-
-open Vec
-
-private
-  variable
-    A B : ℕ
-
-opaque
-  unfolding _≊_ _⊕_
-  ⊕-idem : (V : Vector A) → V ⊕ V ≊ V
-  ⊕-idem [] = PW.[]
-  ⊕-idem (v ∷ V) = +-idem v PW.∷ ⊕-idem V
-
-opaque
-  unfolding _≋_ _[+]_
-  [+]-idem : (M : Matrix A B) → M [+] M ≋ M
-  [+]-idem [] = PW.[]
-  [+]-idem (M₀ ∷ M) = ⊕-idem M₀ PW.∷ [+]-idem M
-
-opaque
-  unfolding ≋-setoid
-  idem : (M : Matrix A B) → (I ∥ I) · (((I ≑ 𝟎) · M) ∥ ((𝟎 ≑ I) · M)) · (I ∥ I) ᵀ ≋ M
-  idem M = begin
-      (I ∥ I) · (((I ≑ 𝟎) · M) ∥ ((𝟎 ≑ I) · M)) · (I ∥ I) ᵀ     ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · (h₁ ∥ h₂) · (I ∥ I) ᵀ) (≑-· I 𝟎 M) (≑-· 𝟎 I M) ⟩
-      (I ∥ I) · ((I · M ≑ 𝟎 · M) ∥ (𝟎 · M ≑ I · M)) · (I ∥ I) ᵀ ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ (∥-cong (≑-cong ·-identityˡ (·-𝟎ˡ M)) (≑-cong (·-𝟎ˡ M) ·-identityˡ)) ≋.refl) ⟩
-      (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (I ∥ I) ᵀ                 ≡⟨ ≡.cong (λ h → (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · h) (∥-ᵀ I I) ⟩
-      (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (I ᵀ ≑ I ᵀ)               ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (h₁ ≑ h₂)) transpose-I transpose-I ⟩
-      (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (I ≑ I)                   ≈⟨ ·-assoc ⟨
-      ((I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M))) · (I ≑ I)                 ≡⟨ ≡.cong (_· (I ≑ I)) (·-∥ (I ∥ I) (M ≑ 𝟎) (𝟎 ≑ M)) ⟩
-      (((I ∥ I) · (M ≑ 𝟎)) ∥ ((I ∥ I) · (𝟎 ≑ M))) · (I ≑ I)     ≈⟨ ∥-·-≑ ((I ∥ I) · (M ≑ 𝟎)) ((I ∥ I) · (𝟎 ≑ M)) I I ⟩
-      (((I ∥ I) · (M ≑ 𝟎)) · I) [+] (((I ∥ I) · (𝟎 ≑ M)) · I)   ≈⟨ [+]-cong ·-identityʳ ·-identityʳ ⟩
-      ((I ∥ I) · (M ≑ 𝟎)) [+] ((I ∥ I) · (𝟎 ≑ M))               ≈⟨ [+]-cong (∥-·-≑ I I M 𝟎) (∥-·-≑ I I 𝟎 M) ⟩
-      ((I · M) [+] (I · 𝟎)) [+] ((I · 𝟎) [+] (I · M))           ≈⟨ [+]-cong ([+]-cong ·-identityˡ ·-identityˡ) ([+]-cong ·-identityˡ ·-identityˡ) ⟩
-      (M [+] 𝟎) [+] (𝟎 [+] M)                                   ≈⟨ [+]-cong ([+]-𝟎ʳ M) ([+]-𝟎ˡ M) ⟩
-      M [+] M                                                   ≈⟨ [+]-idem M ⟩
-      M ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-
-Mat-IdempotentSemiadditiveDagger : IdempotentSemiadditiveDagger
-Mat-IdempotentSemiadditiveDagger = record
-    { semiadditiveDagger = Mat-SemiadditiveDagger
-    ; idempotent = idem _
-    }
-
-Mat-Dagger-2-Poset : Dagger-2-Poset
-Mat-Dagger-2-Poset = dagger-2-poset Mat-IdempotentSemiadditiveDagger
diff --git a/Data/Mat/SemiadditiveDagger.agda b/Data/Mat/SemiadditiveDagger.agda
deleted file mode 100644
index 65aeee6..0000000
--- a/Data/Mat/SemiadditiveDagger.agda
+++ /dev/null
@@ -1,503 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Algebra.Bundles using (CommutativeSemiring)
-open import Level using (Level)
-
-module Data.Mat.SemiadditiveDagger {c ℓ : Level} (Rig : CommutativeSemiring c ℓ) where
-
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-import Data.Nat.Properties as ℕ-Props
-
-module Rig = CommutativeSemiring Rig
-
-open import Data.Mat.Util using (transpose-cong; replicate-++)
-open import Data.Mat.Category Rig.semiring
-  using
-    ( Mat; _ᵀ; transpose-I; I; _≋_; module ≋; _≊_; module ≊; Matrix; Vector
-    ; [_]_; _[_]; _·_; ≋-setoid; ≊-setoid; mapRows; zeros; _∙_
-    ; ∙-cong; _ᵀᵀ; -[-]ᵀ
-    ; [-]--cong
-    ; ·-identityˡ
-    ; ·-identityʳ
-    )
-open import Data.Mat.Cocartesian Rig.semiring
-  using
-    ( Mat-Cocartesian; []ᵥ; []ₕ; [-]-[]ᵥ; ⟨⟩; _∷ₕ_; ∷ₕ-cong; _∷ᵥ_
-    ; [-]-∷ₕ; _∷′_; ∷ₕ-ᵀ; ∷ᵥ-ᵀ; 𝟎; _∥_; _≑_; []ᵥ-∥; []ₕ-≑; []ₕ-!
-    ; _+++_; ∷ₕ-≑; []ᵥ-ᵀ; ∥-cong; ≑-cong; ≑-·; ·-𝟎ʳ; ·-𝟎ˡ; 𝟎ᵀ; ·-∥
-    ; headₕ; tailₕ; head-∷-tailₕ; [⟨⟩]-[]ₕ
-    ; ∷ₕ-∥; []ᵥ-!; _[+]_; ∥-·-≑; [+]-cong; [+]-𝟎ʳ; [+]-𝟎ˡ
-    )
-
-open import Category.Dagger.Semiadditive Mat using (DaggerCocartesianMonoidal; SemiadditiveDagger)
-open import Data.Nat as ℕ using (ℕ)
-open import Data.Vec using (Vec; map; replicate)
-open import Function using (_∘_)
-open import Data.Vec.Properties using (map-cong; map-const)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
-
-open ℕ.ℕ
-open Vec
-open Rig renaming (Carrier to R)
-
-private
-  variable
-    A B C D E F : ℕ
-
-opaque
-  unfolding _≋_
-  Iᵀ : I ᵀ ≋ I {A}
-  Iᵀ = ≋.reflexive transpose-I
-
-import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
-
-opaque
-  unfolding Vector _∙_
-  ∙-comm : (V W : Vector A) → V ∙ W ≈ W ∙ V
-  ∙-comm [] [] = refl
-  ∙-comm (x ∷ V) (w ∷ W) = +-cong (*-comm x w) (∙-comm V W)
-
-opaque
-  unfolding _[_] [_]_ _ᵀ []ᵥ ⟨⟩ _∷ₕ_ _≊_ _≋_ _∷ᵥ_
-  [-]-ᵀ : (M : Matrix A B) (V : Vector A) →  M [ V ] ≊ [ V ] (M ᵀ)
-  [-]-ᵀ [] V = ≊.sym (≊.reflexive ([-]-[]ᵥ V))
-  [-]-ᵀ (M₀ ∷ M) V = begin
-      M₀ ∙ V ∷ map (_∙ V) M         ≈⟨ ∙-comm M₀ V PW.∷ (PW.map⁺ (λ {x} ≊V → trans (∙-comm x V) (∙-cong ≊.refl ≊V)) ≋.refl) ⟩
-      V ∙ M₀ ∷ map (V ∙_) M         ≡⟨⟩
-      map (V ∙_) (M₀ ∷ᵥ M)          ≡⟨ ≡.cong (map (V ∙_) ∘ (M₀ ∷ᵥ_)) (M ᵀᵀ) ⟨
-      map (V ∙_) (M₀ ∷ᵥ M ᵀ ᵀ)      ≡⟨ ≡.cong (map (V ∙_)) (∷ₕ-ᵀ M₀ (M ᵀ)) ⟨
-      map (V ∙_) ((M₀ ∷ₕ (M ᵀ)) ᵀ)  ∎
-    where
-      open ≈-Reasoning (≊-setoid _)
-
-opaque
-  unfolding ≋-setoid []ᵥ mapRows ⟨⟩ _∷ₕ_ _∷ᵥ_
-  ·-ᵀ
-      : {A B C : ℕ}
-        (M : Matrix A B)
-        (N : Matrix B C)
-      → (N · M) ᵀ ≋ M ᵀ · N ᵀ
-  ·-ᵀ {A} {B} {zero} M [] = begin
-      []ᵥ                   ≡⟨ map-const (M ᵀ) ⟨⟩ ⟨
-      map (λ _ → ⟨⟩) (M ᵀ)  ≡⟨ map-cong [-]-[]ᵥ (M ᵀ) ⟨
-      map ([_] []ᵥ) (M ᵀ)   ∎
-    where
-      open ≈-Reasoning (≋-setoid 0 A)
-  ·-ᵀ {A} {B} {suc C} M (N₀ ∷ N) = begin
-      map ([_] M) (N₀ ∷ᵥ N) ᵀ       ≡⟨ -[-]ᵀ (N₀ ∷ᵥ N) M ⟨
-      map ((N₀ ∷ᵥ N) [_]) (M ᵀ)     ≈⟨ PW.map⁺ (λ {V} ≋V → ≊.trans ([-]-ᵀ (N₀ ∷ᵥ N) V) ([-]--cong {A = (N₀ ∷ᵥ N) ᵀ} ≋V ≋.refl)) ≋.refl ⟩
-      map ([_] ((N₀ ∷ᵥ N) ᵀ)) (M ᵀ) ≡⟨ map-cong (λ V → ≡.cong ([ V ]_) (∷ᵥ-ᵀ N₀ N)) (M ᵀ) ⟩
-      map ([_] (N₀ ∷ₕ N ᵀ)) (M ᵀ)   ∎
-    where
-      open ≈-Reasoning (≋-setoid (suc C) A)
-
-opaque
-  unfolding _ᵀ _≋_
-  ᵀ-cong : {M M′ : Matrix A B} → M ≋ M′ → M ᵀ ≋ M′ ᵀ
-  ᵀ-cong ≋M = transpose-cong setoid ≋M
-
-opaque
-  unfolding _≋_
-  ᵀ-involutive : (M : Matrix A B) → (M ᵀ) ᵀ ≋ M
-  ᵀ-involutive M = ≋.reflexive (M ᵀᵀ)
-
-opaque
-  unfolding _≋_
-  ≋λᵀ : ([]ᵥ ∥ I) ᵀ ≋ 𝟎 ≑ I {A}
-  ≋λᵀ = begin
-      ([]ᵥ ∥ I) ᵀ ≡⟨ ≡.cong (_ᵀ) ([]ᵥ-∥ I) ⟩
-      I ᵀ         ≈⟨ Iᵀ ⟩
-      I           ≡⟨ []ₕ-≑ I ⟨
-      []ₕ ≑ I     ≡⟨ ≡.cong (_≑ I) ([]ₕ-! 𝟎) ⟨
-      𝟎 ≑ I       ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-
-opaque
-  unfolding Matrix _∥_ _ᵀ _≑_ _+++_ _∷ₕ_
-  ∥-ᵀ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) ᵀ ≡ M ᵀ ≑ N ᵀ
-  ∥-ᵀ {A} {zero} {B} [] [] = ≡.sym (replicate-++ A B [])
-  ∥-ᵀ (M₀ ∷ M) (N₀ ∷ N) = begin
-      (M₀ +++ N₀) ∷ₕ ((M ∥ N) ᵀ) ≡⟨ ≡.cong ((M₀ +++ N₀) ∷ₕ_) (∥-ᵀ M N) ⟩
-      (M₀ +++ N₀) ∷ₕ (M ᵀ ≑ N ᵀ) ≡⟨ ∷ₕ-≑ M₀ N₀ (M ᵀ) (N ᵀ) ⟩
-      (M₀ ∷ₕ M ᵀ) ≑ (N₀ ∷ₕ N ᵀ) ∎
-    where
-      open ≡-Reasoning
-
-≑-ᵀ : (M : Matrix A B) (N : Matrix A C) → (M ≑ N) ᵀ ≡ M ᵀ ∥ N ᵀ
-≑-ᵀ M N = begin
-    (M ≑ N) ᵀ           ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ≑ h₂) ᵀ) (M ᵀᵀ) (N ᵀᵀ) ⟨
-    (M ᵀ ᵀ ≑ N ᵀ ᵀ ) ᵀ  ≡⟨ ≡.cong (_ᵀ) (∥-ᵀ (M ᵀ) (N ᵀ)) ⟨
-    (M ᵀ ∥ N ᵀ ) ᵀ ᵀ    ≡⟨ (M ᵀ ∥ N ᵀ ) ᵀᵀ ⟩
-    M ᵀ ∥ N ᵀ           ∎
-  where
-    open ≡-Reasoning
-
-opaque
-  unfolding _≋_
-  ≋ρᵀ : (I ∥ []ᵥ) ᵀ ≋ I {A} ≑ 𝟎
-  ≋ρᵀ {A} = begin
-      (I ∥ []ᵥ) ᵀ ≡⟨ ∥-ᵀ I []ᵥ ⟩
-      I ᵀ ≑ []ᵥ ᵀ ≡⟨ ≡.cong (I ᵀ ≑_) []ᵥ-ᵀ ⟩
-      I ᵀ ≑ []ₕ   ≡⟨ ≡.cong (_≑ []ₕ) transpose-I ⟩
-      I  ≑ []ₕ    ≡⟨ ≡.cong (I ≑_) ([]ₕ-! 𝟎) ⟨
-      I ≑ 𝟎       ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-
-open import Data.Vec using () renaming (cast to castVec)
-open import Data.Vec.Properties using (++-assoc-eqFree) renaming (cast-is-id to castVec-is-id)
-
-opaque
-  unfolding Matrix Vector
-  cast₁ : .(A ≡ B) → Matrix A C → Matrix B C
-  cast₁ eq = map (castVec eq)
-
-opaque
-  unfolding Matrix
-  cast₂ : .(B ≡ C) → Matrix A B → Matrix A C
-  cast₂ eq [] = castVec eq []
-  cast₂ {B} {suc C} {A} eq (x ∷ M) = x ∷ cast₂ (ℕ-Props.suc-injective eq) M
-
-opaque
-  unfolding cast₁
-  cast₁-is-id : .(eq : A ≡ A) (M : Matrix A B) → cast₁ eq M ≡ M
-  cast₁-is-id _ [] = ≡.refl
-  cast₁-is-id _ (M₀ ∷ M) = ≡.cong₂ _∷_ (castVec-is-id _ M₀) (cast₁-is-id _ M)
-
-opaque
-  unfolding cast₂
-  cast₂-is-id : .(eq : B ≡ B) (M : Matrix A B) → cast₂ eq M ≡ M
-  cast₂-is-id _ [] = ≡.refl
-  cast₂-is-id eq (M₀ ∷ M) = ≡.cong (M₀ ∷_) (cast₂-is-id (ℕ-Props.suc-injective eq) M)
-
-opaque
-  unfolding cast₂
-  cast₂-trans : .(eq₁ : B ≡ C) (eq₂ : C ≡ D) (M : Matrix A B) → cast₂ eq₂ (cast₂ eq₁ M) ≡ cast₂ (≡.trans eq₁ eq₂) M
-  cast₂-trans {zero} {zero} {zero} {A} eq₁ eq₂ [] = ≡.refl
-  cast₂-trans {suc B} {suc C} {suc D} {A} eq₁ eq₂ (M₀ ∷ M) = ≡.cong (M₀ ∷_) (cast₂-trans (ℕ-Props.suc-injective eq₁) (ℕ-Props.suc-injective eq₂) M)
-
-opaque
-  unfolding _∥_ cast₁
-  ∥-assoc
-      : (X : Matrix A D)
-        (Y : Matrix B D)
-        (Z : Matrix C D)
-      → cast₁ (ℕ-Props.+-assoc A B C) ((X ∥ Y) ∥ Z) ≡ X ∥ Y ∥ Z
-  ∥-assoc [] [] [] = cast₁-is-id ≡.refl []
-  ∥-assoc (X₀ ∷ X) (Y₀ ∷ Y) (Z₀ ∷ Z) = ≡.cong₂ _∷_ (++-assoc-eqFree X₀ Y₀ Z₀) (∥-assoc X Y Z)
-
-opaque
-  unfolding _≑_ cast₂
-  ≑-assoc
-      : (X : Matrix A B)
-        (Y : Matrix A C)
-        (Z : Matrix A D)
-      → cast₂ (ℕ-Props.+-assoc B C D) ((X ≑ Y) ≑ Z) ≡ X ≑ Y ≑ Z
-  ≑-assoc [] Y Z = cast₂-is-id ≡.refl (Y ≑ Z)
-  ≑-assoc (X₀ ∷ X) Y Z = ≡.cong (X₀ ∷_) (≑-assoc X Y Z)
-
-≑-sym-assoc
-    : (X : Matrix A B)
-      (Y : Matrix A C)
-      (Z : Matrix A D)
-    → cast₂ (≡.sym (ℕ-Props.+-assoc B C D)) (X ≑ Y ≑ Z) ≡ (X ≑ Y) ≑ Z
-≑-sym-assoc {A} {B} {C} {D} X Y Z = begin
-    cast₂ _ (X ≑ Y ≑ Z)                 ≡⟨ ≡.cong (cast₂ _) (≑-assoc X Y Z) ⟨
-    cast₂ _ (cast₂ assoc ((X ≑ Y) ≑ Z)) ≡⟨ cast₂-trans assoc (≡.sym assoc) ((X ≑ Y) ≑ Z) ⟩
-    cast₂ _ ((X ≑ Y) ≑ Z)               ≡⟨ cast₂-is-id _ ((X ≑ Y) ≑ Z) ⟩
-    (X ≑ Y) ≑ Z                         ∎
-  where
-    open ≡-Reasoning
-    assoc : B ℕ.+ C ℕ.+ D ≡ B ℕ.+ (C ℕ.+ D)
-    assoc = ℕ-Props.+-assoc B C D
-
-opaque
-  unfolding _∥_ _≑_ _+++_
-  ∥-≑ : {A₁ B₁ A₂ B₂ : ℕ}
-        (W : Matrix A₁ B₁)
-        (X : Matrix A₂ B₁)
-        (Y : Matrix A₁ B₂)
-        (Z : Matrix A₂ B₂)
-      → W ∥ X ≑ Y ∥ Z ≡ (W ≑ Y) ∥ (X ≑ Z)
-  ∥-≑ {A₁} {ℕ.zero} {A₂} {B₂} [] [] Y Z = ≡.refl
-  ∥-≑ {A₁} {suc B₁} {A₂} {B₂} (W₀ ∷ W) (X₀ ∷ X) Y Z = ≡.cong ((W₀ +++ X₀) ∷_) (∥-≑ W X Y Z)
-
-∥-≑⁴
-    : (R : Matrix A D)
-      (S : Matrix B D)
-      (T : Matrix C D)
-      (U : Matrix A E)
-      (V : Matrix B E)
-      (W : Matrix C E)
-      (X : Matrix A F)
-      (Y : Matrix B F)
-      (Z : Matrix C F)
-    → (R ∥ S ∥ T) ≑
-      (U ∥ V ∥ W) ≑
-      (X ∥ Y ∥ Z)
-    ≡ (R ≑ U ≑ X) ∥
-      (S ≑ V ≑ Y) ∥
-      (T ≑ W ≑ Z)
-∥-≑⁴ R S T U V W X Y Z = begin
-    R ∥ S ∥ T ≑ U ∥ V ∥ W ≑ X ∥ Y ∥ Z               ≡⟨ ≡.cong (R ∥ S ∥ T ≑_) (∥-≑ U (V ∥ W) X (Y ∥ Z)) ⟩
-    R ∥ S ∥ T ≑ (U ≑ X) ∥ (V ∥ W ≑ Y ∥ Z)           ≡⟨ ≡.cong (λ h → (R ∥ S ∥ T ≑ (U ≑ X) ∥ h)) (∥-≑ V W Y Z) ⟩
-    R ∥ S ∥ T ≑ (U ≑ X) ∥ (V ≑ Y) ∥ (W ≑ Z)         ≡⟨ ∥-≑ R (S ∥ T) (U ≑ X) ((V ≑ Y) ∥ (W ≑ Z)) ⟩
-    (R ≑ (U ≑ X)) ∥ ((S ∥ T) ≑ ((V ≑ Y) ∥ (W ≑ Z))) ≡⟨ ≡.cong ((R ≑ U ≑ X) ∥_) (∥-≑ S T (V ≑ Y) (W ≑ Z)) ⟩
-    (R ≑ U ≑ X) ∥ (S ≑ V ≑ Y) ∥ (T ≑ W ≑ Z)         ∎
-  where
-    open ≡-Reasoning
-
-opaque
-  unfolding Vector
-  cast : .(A ≡ B) → Vector A → Vector B
-  cast = castVec
-
-opaque
-  unfolding cast cast₂ _∷ₕ_
-  cast₂-∷ₕ : .(eq : B ≡ C) (V : Vector B) (M : Matrix A B) → cast eq V ∷ₕ cast₂ eq M ≡ cast₂ eq (V ∷ₕ M)
-  cast₂-∷ₕ {zero} {zero} {A} _ [] [] = ≡.sym (cast₂-is-id ≡.refl ([] ∷ₕ []))
-  cast₂-∷ₕ {suc B} {suc C} {A} eq (x ∷ V) (M₀ ∷ M) = ≡.cong ((x ∷ M₀) ∷_) (cast₂-∷ₕ _ V M)
-
-opaque
-  unfolding []ᵥ cast₂
-  cast₂-[]ᵥ : .(eq : A ≡ B) → cast₂ eq []ᵥ ≡ []ᵥ
-  cast₂-[]ᵥ {zero} {zero} _ = ≡.refl
-  cast₂-[]ᵥ {suc A} {suc B} eq = ≡.cong ([] ∷_) (cast₂-[]ᵥ (ℕ-Props.suc-injective eq))
-
-cast₂-∥ : .(eq : C ≡ D) (M : Matrix A C) (N : Matrix B C) → cast₂ eq M ∥ cast₂ eq N ≡ cast₂ eq (M ∥ N)
-cast₂-∥ {C} {D} {zero} {B} eq M N
-  rewrite ([]ᵥ-! M) = begin
-    cast₂ _ []ᵥ ∥ cast₂ _ N ≡⟨ ≡.cong (_∥ cast₂ _ N) (cast₂-[]ᵥ _) ⟩
-    []ᵥ ∥ cast₂ _ N         ≡⟨ []ᵥ-∥ (cast₂ _ N) ⟩
-    cast₂ _ N               ≡⟨ ≡.cong (cast₂ _) ([]ᵥ-∥ N) ⟨
-    cast₂ _ ([]ᵥ ∥ N)       ∎
-  where
-    open ≡-Reasoning
-cast₂-∥ {C} {D} {suc A} {B} eq M N
-  rewrite ≡.sym (head-∷-tailₕ M)
-  using M₀ ← headₕ M
-  using M ← tailₕ M = begin
-    cast₂ _ (M₀ ∷ₕ M) ∥ (cast₂ _ N)         ≡⟨ ≡.cong (_∥ (cast₂ eq N)) (cast₂-∷ₕ eq M₀ M) ⟨
-    (cast _ M₀ ∷ₕ cast₂ _ M) ∥ (cast₂ _ N)  ≡⟨ ∷ₕ-∥ (cast _ M₀) (cast₂ _ M) (cast₂ _ N) ⟨
-    cast _ M₀ ∷ₕ (cast₂ _ M ∥ cast₂ _ N)    ≡⟨ ≡.cong (cast eq M₀ ∷ₕ_) (cast₂-∥ _ M N) ⟩
-    cast _ M₀ ∷ₕ cast₂ _ (M ∥ N)            ≡⟨ cast₂-∷ₕ eq M₀ (M ∥ N) ⟩
-    cast₂ _ (M₀ ∷ₕ (M ∥ N))                 ≡⟨ ≡.cong (cast₂ eq) (∷ₕ-∥ M₀ M N) ⟩
-    cast₂ _ ((M₀ ∷ₕ M) ∥ N)                 ∎
-  where
-    open ≡-Reasoning
-
-opaque
-  unfolding 𝟎 _≑_
-  𝟎≑𝟎 : 𝟎 {A} {B} ≑ 𝟎 {A} {C} ≡ 𝟎
-  𝟎≑𝟎 {B = zero} = ≡.refl
-  𝟎≑𝟎 {B = suc B} = ≡.cong (zeros ∷_) (𝟎≑𝟎 {B = B})
-
-opaque
-  unfolding _∷ₕ_ 𝟎 zeros
-  zeros∷ₕ𝟎 : zeros ∷ₕ 𝟎 {A} {B} ≡ 𝟎
-  zeros∷ₕ𝟎 {A} {zero} = ≡.refl
-  zeros∷ₕ𝟎 {A} {suc B} = ≡.cong (zeros ∷_) zeros∷ₕ𝟎
-
-𝟎∥𝟎 : 𝟎 {A} {C} ∥ 𝟎 {B} {C} ≡ 𝟎
-𝟎∥𝟎 {zero} {C} rewrite []ᵥ-! (𝟎 {0} {C}) = []ᵥ-∥ 𝟎
-𝟎∥𝟎 {suc A} {C} {B} = begin
-    𝟎 ∥ 𝟎                 ≡⟨ ≡.cong (_∥ 𝟎) (zeros∷ₕ𝟎 {A} {C}) ⟨
-    (zeros ∷ₕ 𝟎 {A}) ∥ 𝟎  ≡⟨ ∷ₕ-∥ zeros 𝟎 𝟎 ⟨
-    zeros ∷ₕ 𝟎 {A} ∥ 𝟎    ≡⟨ ≡.cong (zeros ∷ₕ_) 𝟎∥𝟎 ⟩
-    zeros ∷ₕ 𝟎            ≡⟨ zeros∷ₕ𝟎 ⟩
-    𝟎 ∎
-  where
-    open ≡-Reasoning
-
-opaque
-  unfolding _≋_
-  ≋αᵀ : (((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎)) ∥ (𝟎 {_} {A} ≑ I {B ℕ.+ C}) · (𝟎 ≑ I {C})) ᵀ
-      ≋ (I {A ℕ.+ B} ≑ 𝟎) · (I {A} ≑ 𝟎) ∥ (I {A ℕ.+ B} ≑ 𝟎) · (𝟎 ≑ I {B}) ∥ (𝟎 ≑ I {C})
-  ≋αᵀ {A} {B} {C} = begin
-      (((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ
-          ≡⟨ ∥-ᵀ ((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ⟩
-      ((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ
-          ≡⟨ ≡.cong (_≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ) (∥-ᵀ (I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C}))) ⟩
-      ((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ᵀ ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ
-          ≡⟨ ≡.cong (λ h → (h ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ) (≑-ᵀ I 𝟎) ⟩
-      (I {A} ᵀ ∥ 𝟎 {A} {B ℕ.+ C} ᵀ ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ
-          ≡⟨ ≡.cong (λ h → (h ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ) (≡.cong₂ _∥_ Iᵀ′ 𝟎ᵀ) ⟩
-      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ
-          ≈⟨ ≑-cong (≑-cong ≋.refl (·-ᵀ (I ≑ 𝟎) (𝟎 ≑ I))) (·-ᵀ (𝟎 ≑ I) (𝟎 ≑ I)) ⟩
-      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ≑ 𝟎 {B} {C}) ᵀ · (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) ᵀ) ≑ (𝟎 {C} {B} ≑ I {C}) ᵀ · (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) ᵀ
-          ≡⟨ ≡.cong₂ _≑_ (≡.cong₂ (λ h₁ h₂ → I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ h₁ · h₂) (≑-ᵀ I 𝟎) (≑-ᵀ 𝟎 I)) (≡.cong₂ _·_ (≑-ᵀ 𝟎 I) (≑-ᵀ 𝟎 I)) ⟩
-      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ᵀ ∥ 𝟎 {B} {C} ᵀ) · (𝟎 {B ℕ.+ C} {A} ᵀ ∥ I {B ℕ.+ C} ᵀ)) ≑ (𝟎 {C} {B} ᵀ ∥ I {C} ᵀ) · (𝟎 {B ℕ.+ C} {A} ᵀ ∥ I {B ℕ.+ C} ᵀ)
-          ≡⟨ ≡.cong₂ _≑_ (≡.cong₂ (λ h₁ h₂ → I {A} ∥ 𝟎 ≑ h₁ · h₂) (≡.cong₂ _∥_ Iᵀ′ 𝟎ᵀ) (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ′)) (≡.cong₂ _·_ (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ′) (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ′)) ⟩
-      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ∥ 𝟎 {C} {B}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})
-          ≡⟨ ≡.cong (λ h → (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ h) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})) (·-∥ (I ∥ 𝟎) 𝟎 I) ⟩
-      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ∥ 𝟎 {C} {B}) · 𝟎 {A} {B ℕ.+ C} ∥ (I {B} ∥ 𝟎 {C} {B}) · I {B ℕ.+ C}) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})
-          ≈⟨ ≑-cong (≑-cong ≋.refl (∥-cong (·-𝟎ʳ (I ∥ 𝟎)) ·-identityʳ)) ≋.refl ⟩
-      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})
-          ≡⟨ ≡.cong ((I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑_) (·-∥ (𝟎 ∥ I) 𝟎 I) ⟩
-      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B} {C} ∥ I {C}) · I {B ℕ.+ C}
-          ≈⟨ ≑-cong ≋.refl (∥-cong (·-𝟎ʳ (𝟎 ∥ I)) ·-identityʳ) ⟩
-      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ 𝟎 {A} {C} ∥ 𝟎 {B} {C} ∥ I {C}
-          ≡⟨ ≡.cong (λ h → (I {A} ∥ h ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ 𝟎 {A} {C} ∥ 𝟎 {B} {C} ∥ I {C}) 𝟎∥𝟎 ⟨
-      (I {A} ∥ 𝟎 {B} ∥ 𝟎 {C} ≑ 𝟎 {A} ∥ I {B} ∥ 𝟎 {C}) ≑ 𝟎 {A} ∥ 𝟎 {B} ∥ I {C}
-          ≡⟨ ≑-sym-assoc (I {A} ∥ 𝟎 {B} ∥ 𝟎 {C}) (𝟎 {A} ∥ I {B} ∥ 𝟎 {C}) (𝟎 {A} ∥ 𝟎 {B} ∥ I {C}) ⟨
-      cast₂ _ (I {A} ∥ 𝟎 {B} ∥ 𝟎 {C} ≑ 𝟎 {A} ∥ I {B} ∥ 𝟎 {C} ≑ 𝟎 {A} ∥ 𝟎 {B} ∥ I {C})
-          ≡⟨ ≡.cong (cast₂ _) (∥-≑⁴ I 𝟎 𝟎 𝟎 I 𝟎 𝟎 𝟎 I) ⟩
-      cast₂ (≡.sym assoc) ((I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) ∥ (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})))
-          ≡⟨ cast₂-∥ (≡.sym assoc) ((I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C}))) ((𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})))  ⟨
-      (cast₂ (≡.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C}))) ∥ cast₂ (≡.sym assoc) ((𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})))
-          ≡⟨ ≡.cong (cast₂ (≡.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) ∥_) (cast₂-∥ (≡.sym assoc) (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) (𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})) ⟨
-      cast₂ (≡.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) ∥ cast₂ (≡.sym assoc) (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ cast₂ (≡.sym assoc) (𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})
-          ≡⟨ ≡.cong₂ _∥_ (≑-sym-assoc I 𝟎 𝟎) (≡.cong₂ _∥_ (≑-sym-assoc 𝟎 I 𝟎) (≑-sym-assoc 𝟎 𝟎 I)) ⟩
-      ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B}) ≑ I {C})
-          ≡⟨ ≡.cong (λ h → ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) ∥ (h ≑ I {C})) 𝟎≑𝟎 ⟩
-      ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})
-          ≈⟨ ∥-cong ≋.refl (∥-cong (≑-cong ·-identityˡ (·-𝟎ˡ (𝟎 ≑ I))) ≋.refl) ⟨
-      ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ (((I {A ℕ.+ B} · (𝟎 {B} {A} ≑ I {B})) ≑ (𝟎 {A ℕ.+ B} {C} · (𝟎 {B} {A} ≑ I {B})))) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})
-          ≡⟨ ≡.cong (λ h → ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ h ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})) (≑-· I 𝟎 (𝟎 ≑ I)) ⟨
-      ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})
-          ≈⟨ ∥-cong (≑-cong ·-identityˡ (·-𝟎ˡ (I ≑ 𝟎))) ≋.refl ⟨
-      ((I {A ℕ.+ B} · (I {A} ≑ 𝟎 {A} {B})) ≑ (𝟎 {A ℕ.+ B} {C} · (I {A} ≑ 𝟎 {A} {B}))) ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})
-          ≡⟨ ≡.cong (λ h → h ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})) (≑-· I 𝟎 (I ≑ 𝟎)) ⟨
-      (I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (I {A} ≑ 𝟎 {A} {B}) ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C}) ∎
-    where
-      assoc : A ℕ.+ B ℕ.+ C ≡ A ℕ.+ (B ℕ.+ C)
-      assoc = ℕ-Props.+-assoc A B C
-      Iᵀ′ : {A : ℕ} → I ᵀ ≡ I {A}
-      Iᵀ′ = transpose-I
-      open ≈-Reasoning (≋-setoid _ _)
-
-opaque
-  unfolding ≋-setoid
-  ≋σᵀ : ((𝟎 ≑ I {A}) ∥ (I {B} ≑ 𝟎)) ᵀ ≋ (𝟎 ≑ I {B}) ∥ (I {A} ≑ 𝟎)
-  ≋σᵀ {A} {B} = begin
-      ((𝟎 ≑ I) ∥ (I ≑ 𝟎)) ᵀ       ≡⟨ ∥-ᵀ (𝟎 ≑ I) (I ≑ 𝟎) ⟩
-      (𝟎 ≑ I {A}) ᵀ ≑ (I ≑ 𝟎) ᵀ   ≡⟨ ≡.cong₂ _≑_ (≑-ᵀ 𝟎 I) (≑-ᵀ I 𝟎) ⟩
-      𝟎 ᵀ ∥ (I {A}) ᵀ ≑ I ᵀ ∥ 𝟎 ᵀ ≡⟨ ≡.cong₂ _≑_ (≡.cong₂ _∥_ 𝟎ᵀ transpose-I) (≡.cong₂ _∥_ transpose-I 𝟎ᵀ) ⟩
-      𝟎 ∥ I {A} ≑ I ∥ 𝟎           ≡⟨ ∥-≑ 𝟎 I I 𝟎 ⟩
-      (𝟎 ≑ I {B}) ∥ (I ≑ 𝟎)       ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-
-opaque
-  unfolding ≋-setoid
-  ≋⊗  : (M : Matrix A B)
-        (N : Matrix C D)
-      → (I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N
-      ≋ (M ≑ 𝟎) ∥ (𝟎 ≑ N)
-  ≋⊗ M N = begin
-      (I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N         ≡⟨ ≡.cong₂ _∥_ (≑-· I 𝟎 M) (≑-· 𝟎 I N)  ⟩
-      (I · M ≑ 𝟎 · M) ∥ (𝟎 · N ≑ I · N) ≈⟨ ∥-cong (≑-cong ·-identityˡ (·-𝟎ˡ M)) (≑-cong (·-𝟎ˡ N) ·-identityˡ) ⟩
-      (M ≑ 𝟎) ∥ (𝟎 ≑ N)                 ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-
-opaque
-  unfolding ≋-setoid
-  ᵀ-resp-⊗
-      : {M : Matrix A B}
-        {N : Matrix C D}
-      → ((I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N) ᵀ
-      ≋ (I ≑ 𝟎) · M ᵀ ∥ (𝟎 ≑ I) · N ᵀ
-  ᵀ-resp-⊗ {M = M} {N = N} = begin
-      ((I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N) ᵀ ≈⟨ ᵀ-cong (≋⊗ M N) ⟩
-      ((M ≑ 𝟎) ∥ (𝟎 ≑ N)) ᵀ         ≡⟨ ≡.cong (_ᵀ) (∥-≑ M 𝟎 𝟎 N) ⟨
-      ((M ∥ 𝟎) ≑ (𝟎 ∥ N)) ᵀ         ≡⟨ ≑-ᵀ (M ∥ 𝟎) (𝟎 ∥ N) ⟩
-      (M ∥ 𝟎) ᵀ ∥ (𝟎 ∥ N) ᵀ         ≡⟨ ≡.cong₂ _∥_ (∥-ᵀ M 𝟎) (∥-ᵀ 𝟎 N) ⟩
-      (M ᵀ ≑ 𝟎 ᵀ) ∥ (𝟎 ᵀ ≑ N ᵀ)     ≡⟨ ≡.cong₂ (λ h₁ h₂ → (M ᵀ ≑ h₁) ∥ (h₂ ≑ N ᵀ)) 𝟎ᵀ 𝟎ᵀ ⟩
-      (M ᵀ ≑ 𝟎) ∥ (𝟎 ≑ N ᵀ)         ≈⟨ ≋⊗ (M ᵀ) (N ᵀ) ⟨
-      (I ≑ 𝟎) · M ᵀ ∥ (𝟎 ≑ I) · N ᵀ ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-
-Mat-DaggerCocartesian : DaggerCocartesianMonoidal
-Mat-DaggerCocartesian = record
-    { cocartesian = Mat-Cocartesian
-    ; dagger = record
-        { _† = λ M → M ᵀ
-        ; †-identity = Iᵀ
-        ; †-homomorphism = λ {f = f} {g} → ·-ᵀ f g
-        ; †-resp-≈ = ᵀ-cong
-        ; †-involutive = ᵀ-involutive
-        }
-    ; λ≅† = ≋λᵀ
-    ; ρ≅† = ≋ρᵀ
-    ; α≅† = ≋αᵀ
-    ; σ≅† = ≋σᵀ
-    ; †-resp-⊗ = ᵀ-resp-⊗
-    }
-
-opaque
-  unfolding ≋-setoid
-  p₁-i₁ : (I ≑ 𝟎) ᵀ · (I ≑ 𝟎 {A} {B}) ≋ I
-  p₁-i₁ = begin
-      (I ≑ 𝟎) ᵀ · (I ≑ 𝟎)   ≡⟨ ≡.cong (_· (I ≑ 𝟎)) (≑-ᵀ I 𝟎) ⟩
-      (I ᵀ ∥ 𝟎 ᵀ) · (I ≑ 𝟎) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (I ≑ 𝟎)) transpose-I 𝟎ᵀ ⟩
-      (I ∥ 𝟎) · (I ≑ 𝟎)     ≈⟨ ∥-·-≑ I 𝟎 I 𝟎 ⟩
-      (I · I) [+] (𝟎 · 𝟎)   ≈⟨ [+]-cong ·-identityˡ (·-𝟎ˡ 𝟎) ⟩
-      I [+] 𝟎               ≈⟨ [+]-𝟎ʳ I ⟩
-      I                     ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-
-opaque
-  unfolding ≋-setoid
-  p₂-i₂ : (𝟎 {A} {B} ≑ I) ᵀ · (𝟎 ≑ I) ≋ I
-  p₂-i₂ = begin
-      (𝟎 ≑ I) ᵀ · (𝟎 ≑ I)   ≡⟨ ≡.cong (_· (𝟎 ≑ I)) (≑-ᵀ 𝟎 I) ⟩
-      (𝟎 ᵀ ∥ I ᵀ) · (𝟎 ≑ I) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (𝟎 ≑ I)) 𝟎ᵀ transpose-I ⟩
-      (𝟎 ∥ I) · (𝟎 ≑ I)     ≈⟨ ∥-·-≑ 𝟎 I 𝟎 I ⟩
-      (𝟎 · 𝟎) [+] (I · I)   ≈⟨ [+]-cong (·-𝟎ˡ 𝟎) ·-identityˡ ⟩
-      𝟎 [+] I               ≈⟨ [+]-𝟎ˡ I ⟩
-      I                     ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-
-opaque
-  unfolding 𝟎 mapRows ⟨⟩
-  []ᵥ·[]ₕ : []ᵥ · []ₕ ≡ 𝟎 {A} {B}
-  []ᵥ·[]ₕ {A} {B} = begin
-      map ([_] []ₕ) []ᵥ     ≡⟨ map-cong (λ { [] → [⟨⟩]-[]ₕ }) []ᵥ ⟩
-      map (λ _ → zeros) []ᵥ ≡⟨ map-const []ᵥ zeros ⟩
-      replicate B zeros     ∎
-    where
-      open ≡-Reasoning
-
-opaque
-  unfolding ≋-setoid
-  p₂-i₁ : (𝟎 {A} ≑ I) ᵀ · (I ≑ 𝟎 {B}) ≋ []ᵥ · []ᵥ ᵀ
-  p₂-i₁ = begin
-      (𝟎 ≑ I) ᵀ · (I ≑ 𝟎)   ≡⟨ ≡.cong (_· (I ≑ 𝟎)) (≑-ᵀ 𝟎 I) ⟩
-      (𝟎 ᵀ ∥ I ᵀ) · (I ≑ 𝟎) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (I ≑ 𝟎)) 𝟎ᵀ transpose-I ⟩
-      (𝟎 ∥ I) · (I ≑ 𝟎)     ≈⟨ ∥-·-≑ 𝟎 I I 𝟎 ⟩
-      (𝟎 · I) [+] (I · 𝟎)   ≈⟨ [+]-cong (·-𝟎ˡ I) (·-𝟎ʳ I) ⟩
-      𝟎 [+] 𝟎               ≈⟨ [+]-𝟎ˡ 𝟎 ⟩
-      𝟎                     ≡⟨ []ᵥ·[]ₕ ⟨
-      []ᵥ · []ₕ             ≡⟨ ≡.cong ([]ᵥ ·_) []ᵥ-ᵀ ⟨
-      []ᵥ · []ᵥ ᵀ           ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-
-opaque
-  unfolding ≋-setoid
-  p₁-i₂ : (I ≑ 𝟎 {A}) ᵀ · (𝟎 {B} ≑ I) ≋ []ᵥ · []ᵥ ᵀ
-  p₁-i₂ = begin
-      (I ≑ 𝟎) ᵀ · (𝟎 ≑ I)   ≡⟨ ≡.cong (_· (𝟎 ≑ I)) (≑-ᵀ I 𝟎) ⟩
-      (I ᵀ ∥ 𝟎 ᵀ) · (𝟎 ≑ I) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (𝟎 ≑ I)) transpose-I 𝟎ᵀ ⟩
-      (I ∥ 𝟎) · (𝟎 ≑ I)     ≈⟨ ∥-·-≑ I 𝟎 𝟎 I ⟩
-      (I · 𝟎) [+] (𝟎 · I)   ≈⟨ [+]-cong (·-𝟎ʳ I) (·-𝟎ˡ I) ⟩
-      𝟎 [+] 𝟎               ≈⟨ [+]-𝟎ˡ 𝟎 ⟩
-      𝟎                     ≡⟨ []ᵥ·[]ₕ ⟨
-      []ᵥ · []ₕ             ≡⟨ ≡.cong ([]ᵥ ·_) []ᵥ-ᵀ ⟨
-      []ᵥ · []ᵥ ᵀ           ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-
-Mat-SemiadditiveDagger : SemiadditiveDagger
-Mat-SemiadditiveDagger = record
-    { daggerCocartesianMonoidal = Mat-DaggerCocartesian
-    ; p₁-i₁ = p₁-i₁
-    ; p₂-i₂ = p₂-i₂
-    ; p₂-i₁ = p₂-i₁
-    ; p₁-i₂ = p₁-i₂
-    }
diff --git a/Data/Mat/Util.agda b/Data/Mat/Util.agda
deleted file mode 100644
index 4570b44..0000000
--- a/Data/Mat/Util.agda
+++ /dev/null
@@ -1,134 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-{-# OPTIONS --hidden-argument-puns #-}
-
-module Data.Mat.Util where
-
-import Data.Vec.Relation.Binary.Equality.Setoid as ≋
-import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-
-open import Data.Nat using (ℕ; _+_)
-open import Data.Setoid using (∣_∣)
-open import Data.Vec using (Vec; zipWith; foldr; map; replicate; _++_)
-open import Level using (Level)
-open import Relation.Binary using (Rel; Setoid; Monotonic₂)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≗_; _≡_; module ≡-Reasoning)
-
-open ℕ
-open Vec
-
-private
-  variable
-    n m o p : ℕ
-    ℓ : Level
-    A B C D E : Set ℓ
-
-transpose : Vec (Vec A n) m → Vec (Vec A m) n
-transpose [] = replicate _ []
-transpose (row ∷ mat) = zipWith _∷_ row (transpose mat)
-
-transpose-empty : (m : ℕ) (E : Vec (Vec A 0) m) → transpose E ≡ []
-transpose-empty zero [] = ≡.refl
-transpose-empty (suc m) ([] ∷ E) = ≡.cong (zipWith _∷_ []) (transpose-empty m E)
-
-transpose-zipWith : (V : Vec A m) (M : Vec (Vec A n) m) → transpose (zipWith _∷_ V M) ≡ V ∷ transpose M
-transpose-zipWith [] [] = ≡.refl
-transpose-zipWith (x ∷ V) (M₀ ∷ M) = ≡.cong (zipWith _∷_ (x ∷ M₀)) (transpose-zipWith V M)
-
-transpose-involutive : (M : Vec (Vec A n) m) → transpose (transpose M) ≡ M
-transpose-involutive {n} [] = transpose-empty n (replicate n [])
-transpose-involutive (V ∷ M) = begin
-    transpose (zipWith _∷_ V (transpose M)) ≡⟨ transpose-zipWith V (transpose M) ⟩
-    V ∷ transpose (transpose M)             ≡⟨ ≡.cong (V ∷_) (transpose-involutive M) ⟩
-    V ∷ M ∎
-  where
-    open ≡.≡-Reasoning
-
-map-replicate : (x : A) (v : Vec B n) → map (λ _ → x) v ≡ replicate n x
-map-replicate x [] = ≡.refl
-map-replicate x (y ∷ v) = ≡.cong (x ∷_) (map-replicate x v)
-
-replicate-++ : (n m : ℕ) (x : A) → replicate n x ++ replicate m x ≡ replicate (n + m) x
-replicate-++ zero _ x = ≡.refl
-replicate-++ (suc n) m x = ≡.cong (x ∷_) (replicate-++ n m x)
-
-zipWith-map-map
-    : (f : A → C)
-      (g : B → D)
-      (_⊕_ : C → D → E)
-      (v : Vec A n)
-      (w : Vec B n)
-    → zipWith (λ x y → f x ⊕ g y) v w ≡ zipWith _⊕_ (map f v) (map g w)
-zipWith-map-map f g _⊕_ [] [] = ≡.refl
-zipWith-map-map f g _⊕_ (x ∷ v) (y ∷ w) = ≡.cong (f x ⊕ g y ∷_) (zipWith-map-map f g _⊕_ v w)
-
-zipWith-map
-    : (f : A → B)
-      (g : A → C)
-      (_⊕_ : B → C → D)
-      (v : Vec A n)
-    → zipWith _⊕_ (map f v) (map g v) ≡ map (λ x → f x ⊕ g x) v
-zipWith-map f g _⊕_ [] = ≡.refl
-zipWith-map f g _⊕_ (x ∷ v) = ≡.cong (f x ⊕ g x ∷_) (zipWith-map f g _⊕_ v)
-
-map-zipWith
-    : (f : C → D)
-      (_⊕_ : A → B → C)
-      (v : Vec A n)
-      (w : Vec B n)
-    → map f (zipWith _⊕_ v w) ≡ zipWith (λ x y → f (x ⊕ y)) v w
-map-zipWith f _⊕_ [] [] = ≡.refl
-map-zipWith f _⊕_ (x ∷ v) (y ∷ w) = ≡.cong (f (x ⊕ y) ∷_) (map-zipWith f _⊕_ v w)
-
-module _ {c₁ c₂ ℓ₁ ℓ₂ : Level} {A : Setoid c₁ ℓ₁} (B : ℕ → Setoid c₂ ℓ₂) where
-
-  private
-    module A = Setoid A
-    module B {n : ℕ} = Setoid (B n)
-    module V = ≋ A
-
-  foldr-cong
-      : {f g : {k : ℕ} → ∣ A ∣ → ∣ B k ∣ → ∣ B (suc k) ∣}
-      → ({k : ℕ} {w x : ∣ A ∣} {y z : ∣ B k ∣} → w A.≈ x → y B.≈ z → f w y B.≈ g x z)
-      → {d e : ∣ B zero ∣}
-      → d B.≈ e
-      → {n : ℕ}
-        {xs ys : Vec ∣ A ∣ n}
-      → (xs V.≋ ys)
-      → foldr (λ k → ∣ B k ∣) f d xs B.≈ foldr (λ k → ∣ B k ∣) g e ys
-  foldr-cong _ d≈e PW.[] = d≈e
-  foldr-cong cong d≈e (≈v₀ PW.∷ ≋v) = cong ≈v₀ (foldr-cong cong d≈e ≋v)
-
-module _
-    {a b c ℓ₁ ℓ₂ ℓ₃ : Level}
-    {A : Set a} {B : Set b} {C : Set c}
-    {f : A → B → C}
-    {_∼₁_ : Rel A ℓ₁}
-    {_∼₂_ : Rel B ℓ₂}
-    {_∼₃_ : Rel C ℓ₃}
-  where
-  zipWith-cong
-      : {n : ℕ}
-        {ws xs : Vec A n}
-        {ys zs : Vec B n}
-      → Monotonic₂ _∼₁_ _∼₂_ _∼₃_ f
-      → PW.Pointwise _∼₁_ ws xs
-      → PW.Pointwise _∼₂_ ys zs
-      → PW.Pointwise _∼₃_ (zipWith f ws ys) (zipWith f xs zs)
-  zipWith-cong cong PW.[] PW.[] = PW.[]
-  zipWith-cong cong (x∼y PW.∷ xs) (a∼b PW.∷ ys) = cong x∼y a∼b PW.∷ zipWith-cong cong xs ys
-
-module _ {c ℓ : Level} (A : Setoid c ℓ) where
-
-  private
-    module A = Setoid A
-    module V = ≋ A
-    module M {n} = ≋ (V.≋-setoid n)
-
-  transpose-cong
-      : {n m : ℕ}
-      → {M₁ M₂ : Vec (Vec ∣ A ∣ n) m}
-      → M₁ M.≋ M₂
-      → transpose M₁ M.≋ transpose M₂
-  transpose-cong PW.[] = M.≋-refl
-  transpose-cong (R₁≋R₂ PW.∷ M₁≋M₂) = zipWith-cong PW._∷_ R₁≋R₂ (transpose-cong M₁≋M₂)
diff --git a/Data/Matrix/Cast.agda b/Data/Matrix/Cast.agda
new file mode 100644
index 0000000..a171c7a
--- /dev/null
+++ b/Data/Matrix/Cast.agda
@@ -0,0 +1,162 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_)
+open import Relation.Binary using (Setoid)
+
+module Data.Matrix.Cast {c ℓ : Level} (S : Setoid c ℓ) where
+
+module S = Setoid S
+
+open import Data.Matrix.Core S using (Matrix; _∥_; _≑_; _∷ₕ_; []ᵥ; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥; head-∷-tailₕ; headₕ; tailₕ)
+open import Data.Nat using (ℕ; _+_)
+open import Data.Nat.Properties using (suc-injective; +-assoc)
+open import Data.Vec using (Vec; map) renaming (cast to castVec)
+open import Data.Vec.Properties using (++-assoc-eqFree) renaming (cast-is-id to castVec-is-id)
+open import Data.Vector.Core S using (Vector; _++_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
+
+open Vec
+open ℕ
+
+private
+  variable
+    A B C D E F : ℕ
+
+opaque
+  unfolding Matrix Vector
+  cast₁ : .(A ≡ B) → Matrix A C → Matrix B C
+  cast₁ eq = map (castVec eq)
+
+opaque
+  unfolding Matrix
+  cast₂ : .(B ≡ C) → Matrix A B → Matrix A C
+  cast₂ eq [] = castVec eq []
+  cast₂ {B} {suc C} {A} eq (x ∷ M) = x ∷ cast₂ (suc-injective eq) M
+
+opaque
+  unfolding cast₁
+  cast₁-is-id : .(eq : A ≡ A) (M : Matrix A B) → cast₁ eq M ≡ M
+  cast₁-is-id _ [] = ≡.refl
+  cast₁-is-id _ (M₀ ∷ M) = ≡.cong₂ _∷_ (castVec-is-id _ M₀) (cast₁-is-id _ M)
+
+opaque
+  unfolding cast₂
+  cast₂-is-id : .(eq : B ≡ B) (M : Matrix A B) → cast₂ eq M ≡ M
+  cast₂-is-id _ [] = ≡.refl
+  cast₂-is-id eq (M₀ ∷ M) = ≡.cong (M₀ ∷_) (cast₂-is-id (suc-injective eq) M)
+
+opaque
+  unfolding cast₂
+  cast₂-trans : .(eq₁ : B ≡ C) (eq₂ : C ≡ D) (M : Matrix A B) → cast₂ eq₂ (cast₂ eq₁ M) ≡ cast₂ (≡.trans eq₁ eq₂) M
+  cast₂-trans {zero} {zero} {zero} {A} eq₁ eq₂ [] = ≡.refl
+  cast₂-trans {suc B} {suc C} {suc D} {A} eq₁ eq₂ (M₀ ∷ M) = ≡.cong (M₀ ∷_) (cast₂-trans (suc-injective eq₁) (suc-injective eq₂) M)
+
+opaque
+  unfolding _∥_ cast₁
+  ∥-assoc
+      : (X : Matrix A D)
+        (Y : Matrix B D)
+        (Z : Matrix C D)
+      → cast₁ (+-assoc A B C) ((X ∥ Y) ∥ Z) ≡ X ∥ Y ∥ Z
+  ∥-assoc [] [] [] = cast₁-is-id ≡.refl []
+  ∥-assoc (X₀ ∷ X) (Y₀ ∷ Y) (Z₀ ∷ Z) = ≡.cong₂ _∷_ (++-assoc-eqFree X₀ Y₀ Z₀) (∥-assoc X Y Z)
+
+opaque
+  unfolding _≑_ cast₂
+  ≑-assoc
+      : (X : Matrix A B)
+        (Y : Matrix A C)
+        (Z : Matrix A D)
+      → cast₂ (+-assoc B C D) ((X ≑ Y) ≑ Z) ≡ X ≑ Y ≑ Z
+  ≑-assoc [] Y Z = cast₂-is-id ≡.refl (Y ≑ Z)
+  ≑-assoc (X₀ ∷ X) Y Z = ≡.cong (X₀ ∷_) (≑-assoc X Y Z)
+
+≑-sym-assoc
+    : (X : Matrix A B)
+      (Y : Matrix A C)
+      (Z : Matrix A D)
+    → cast₂ (≡.sym (+-assoc B C D)) (X ≑ Y ≑ Z) ≡ (X ≑ Y) ≑ Z
+≑-sym-assoc {A} {B} {C} {D} X Y Z = begin
+    cast₂ _ (X ≑ Y ≑ Z)                 ≡⟨ ≡.cong (cast₂ _) (≑-assoc X Y Z) ⟨
+    cast₂ _ (cast₂ assoc ((X ≑ Y) ≑ Z)) ≡⟨ cast₂-trans assoc (≡.sym assoc) ((X ≑ Y) ≑ Z) ⟩
+    cast₂ _ ((X ≑ Y) ≑ Z)               ≡⟨ cast₂-is-id _ ((X ≑ Y) ≑ Z) ⟩
+    (X ≑ Y) ≑ Z                         ∎
+  where
+    open ≡-Reasoning
+    assoc : B + C + D ≡ B + (C + D)
+    assoc = +-assoc B C D
+
+opaque
+  unfolding _∥_ _≑_
+  ∥-≑ : {A₁ B₁ A₂ B₂ : ℕ}
+        (W : Matrix A₁ B₁)
+        (X : Matrix A₂ B₁)
+        (Y : Matrix A₁ B₂)
+        (Z : Matrix A₂ B₂)
+      → W ∥ X ≑ Y ∥ Z ≡ (W ≑ Y) ∥ (X ≑ Z)
+  ∥-≑ {A₁} {ℕ.zero} {A₂} {B₂} [] [] Y Z = ≡.refl
+  ∥-≑ {A₁} {suc B₁} {A₂} {B₂} (W₀ ∷ W) (X₀ ∷ X) Y Z = ≡.cong ((W₀ ++ X₀) ∷_) (∥-≑ W X Y Z)
+
+∥-≑⁴
+    : (R : Matrix A D)
+      (S : Matrix B D)
+      (T : Matrix C D)
+      (U : Matrix A E)
+      (V : Matrix B E)
+      (W : Matrix C E)
+      (X : Matrix A F)
+      (Y : Matrix B F)
+      (Z : Matrix C F)
+    → (R ∥ S ∥ T) ≑
+      (U ∥ V ∥ W) ≑
+      (X ∥ Y ∥ Z)
+    ≡ (R ≑ U ≑ X) ∥
+      (S ≑ V ≑ Y) ∥
+      (T ≑ W ≑ Z)
+∥-≑⁴ R S T U V W X Y Z = begin
+    R ∥ S ∥ T ≑ U ∥ V ∥ W ≑ X ∥ Y ∥ Z               ≡⟨ ≡.cong (R ∥ S ∥ T ≑_) (∥-≑ U (V ∥ W) X (Y ∥ Z)) ⟩
+    R ∥ S ∥ T ≑ (U ≑ X) ∥ (V ∥ W ≑ Y ∥ Z)           ≡⟨ ≡.cong (λ h → (R ∥ S ∥ T ≑ (U ≑ X) ∥ h)) (∥-≑ V W Y Z) ⟩
+    R ∥ S ∥ T ≑ (U ≑ X) ∥ (V ≑ Y) ∥ (W ≑ Z)         ≡⟨ ∥-≑ R (S ∥ T) (U ≑ X) ((V ≑ Y) ∥ (W ≑ Z)) ⟩
+    (R ≑ (U ≑ X)) ∥ ((S ∥ T) ≑ ((V ≑ Y) ∥ (W ≑ Z))) ≡⟨ ≡.cong ((R ≑ U ≑ X) ∥_) (∥-≑ S T (V ≑ Y) (W ≑ Z)) ⟩
+    (R ≑ U ≑ X) ∥ (S ≑ V ≑ Y) ∥ (T ≑ W ≑ Z)         ∎
+  where
+    open ≡-Reasoning
+
+opaque
+  unfolding Vector
+  cast : .(A ≡ B) → Vector A → Vector B
+  cast = castVec
+
+opaque
+  unfolding cast cast₂ _∷ₕ_
+  cast₂-∷ₕ : .(eq : B ≡ C) (V : Vector B) (M : Matrix A B) → cast eq V ∷ₕ cast₂ eq M ≡ cast₂ eq (V ∷ₕ M)
+  cast₂-∷ₕ {zero} {zero} {A} _ [] [] = ≡.sym (cast₂-is-id ≡.refl ([] ∷ₕ []))
+  cast₂-∷ₕ {suc B} {suc C} {A} eq (x ∷ V) (M₀ ∷ M) = ≡.cong ((x ∷ M₀) ∷_) (cast₂-∷ₕ _ V M)
+
+opaque
+  unfolding []ᵥ cast₂
+  cast₂-[]ᵥ : .(eq : A ≡ B) → cast₂ eq []ᵥ ≡ []ᵥ
+  cast₂-[]ᵥ {zero} {zero} _ = ≡.refl
+  cast₂-[]ᵥ {suc A} {suc B} eq = ≡.cong ([] ∷_) (cast₂-[]ᵥ (suc-injective eq))
+
+cast₂-∥ : .(eq : C ≡ D) (M : Matrix A C) (N : Matrix B C) → cast₂ eq M ∥ cast₂ eq N ≡ cast₂ eq (M ∥ N)
+cast₂-∥ {C} {D} {zero} {B} eq M N
+  rewrite ([]ᵥ-! M) = begin
+    cast₂ _ []ᵥ ∥ cast₂ _ N ≡⟨ ≡.cong (_∥ cast₂ _ N) (cast₂-[]ᵥ _) ⟩
+    []ᵥ ∥ cast₂ _ N         ≡⟨ []ᵥ-∥ (cast₂ _ N) ⟩
+    cast₂ _ N               ≡⟨ ≡.cong (cast₂ _) ([]ᵥ-∥ N) ⟨
+    cast₂ _ ([]ᵥ ∥ N)       ∎
+  where
+    open ≡-Reasoning
+cast₂-∥ {C} {D} {suc A} {B} eq M N
+  rewrite ≡.sym (head-∷-tailₕ M)
+  using M₀ ← headₕ M
+  using M ← tailₕ M = begin
+    cast₂ _ (M₀ ∷ₕ M) ∥ (cast₂ _ N)         ≡⟨ ≡.cong (_∥ (cast₂ eq N)) (cast₂-∷ₕ eq M₀ M) ⟨
+    (cast _ M₀ ∷ₕ cast₂ _ M) ∥ (cast₂ _ N)  ≡⟨ ∷ₕ-∥ (cast _ M₀) (cast₂ _ M) (cast₂ _ N) ⟨
+    cast _ M₀ ∷ₕ (cast₂ _ M ∥ cast₂ _ N)    ≡⟨ ≡.cong (cast eq M₀ ∷ₕ_) (cast₂-∥ _ M N) ⟩
+    cast _ M₀ ∷ₕ cast₂ _ (M ∥ N)            ≡⟨ cast₂-∷ₕ eq M₀ (M ∥ N) ⟩
+    cast₂ _ (M₀ ∷ₕ (M ∥ N))                 ≡⟨ ≡.cong (cast₂ eq) (∷ₕ-∥ M₀ M N) ⟩
+    cast₂ _ ((M₀ ∷ₕ M) ∥ N)                 ∎
+  where
+    open ≡-Reasoning
diff --git a/Data/Matrix/Category.agda b/Data/Matrix/Category.agda
new file mode 100644
index 0000000..5a33440
--- /dev/null
+++ b/Data/Matrix/Category.agda
@@ -0,0 +1,177 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (Semiring)
+open import Level using (Level; 0ℓ; _⊔_)
+
+module Data.Matrix.Category {c ℓ : Level} (R : Semiring c ℓ) where
+
+module R = Semiring R
+
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Categories.Category using (Category)
+open import Categories.Category.Helper using (categoryHelper)
+open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; ≋-isEquiv; _ᵀ; -ᵀ-cong; _∷ₕ_; mapRows; _ᵀᵀ; module ≋; _∥_; _≑_)
+open import Data.Matrix.Monoid R.+-monoid using (𝟎; _[+]_)
+open import Data.Matrix.Transform R using ([_]_; _[_]; -[-]-cong; [-]--cong; -[-]ᵀ; []-∙; [-]--∥; [++]-≑; I; Iᵀ; I[-]; map--[-]-I; [-]-𝟎; [⟨0⟩]-)
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec; map)
+open import Data.Vec.Properties using (map-id; map-∘)
+open import Data.Vector.Bisemimodule R using (_∙_; ∙-cong)
+open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; module ≊; _≊_)
+open import Data.Vector.Monoid R.+-monoid using () renaming (⟨ε⟩ to ⟨0⟩)
+open import Function using (id)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
+
+open R
+open Vec
+open ℕ
+
+private
+  variable
+    n m p : ℕ
+    A B C D : ℕ
+
+-- matrix multiplication
+_·_ : Matrix m p → Matrix n m → Matrix n p
+_·_ A B = mapRows ([_] B) A
+
+-- alternative form
+_·′_ : Matrix m p → Matrix n m → Matrix n p
+_·′_ A B = mapRows (A [_]) (B ᵀ) ᵀ
+
+infixr 9 _·_ _·′_
+
+·-·′ : (A : Matrix m p) (B : Matrix n m) → A · B ≡ A ·′ B
+·-·′ A B = begin
+    mapRows ([_] B) A       ≡⟨ mapRows ([_] B) A ᵀᵀ ⟨
+    mapRows ([_] B) A ᵀ ᵀ   ≡⟨ ≡.cong (_ᵀ) (-[-]ᵀ A B) ⟨
+    mapRows (A [_]) (B ᵀ) ᵀ ∎
+  where
+    open ≡-Reasoning
+
+opaque
+
+  unfolding _[_]
+
+  ·-[] : {A B C : ℕ} (M : Matrix A B) (N : Matrix B C) (V : Vector A) → (N · M) [ V ] ≊ N [ M [ V ] ]
+  ·-[] {A} {B} {zero} M [] V = PW.[]
+  ·-[] {A} {B} {suc C} M (N₀ ∷ N) V = []-∙ N₀ M V PW.∷ ·-[] M N V
+
+opaque
+
+  unfolding [_]_
+
+  []-· : {A B C : ℕ} (V : Vector C) (M : Matrix A B) (N : Matrix B C) → [ V ] (N · M) ≊ [ [ V ] N ] M
+  []-· {A} {B} {C} V M N = begin
+      [ V ] (map ([_] M) N)           ≡⟨ ≡.cong (map (V ∙_)) (-[-]ᵀ N M) ⟨
+      map (V ∙_) (map (N [_]) (M ᵀ))  ≡⟨ map-∘ (V ∙_) (N [_]) (M ᵀ) ⟨
+      map (λ h → V ∙ N [ h ]) (M ᵀ)   ≈⟨ PW.map⁺ (λ {W} ≋W → trans ([]-∙ V N W) (∙-cong ≊.refl (-[-]-cong N ≋W))) {xs = M ᵀ} ≋.refl ⟨
+      map ([ V ] N ∙_) (M ᵀ)          ∎
+    where
+      open ≈-Reasoning (Vectorₛ A)
+
+opaque
+
+  unfolding _∥_
+
+  ·-∥
+      : (M : Matrix C D)
+        (N : Matrix A C)
+        (P : Matrix B C)
+      → M · (N ∥ P) ≡ M · N ∥ M · P
+  ·-∥ {C} {D} {A} {B} [] N P = ≡.refl
+  ·-∥ {C} {D} {A} {B} (M₀ ∷ M) N P = ≡.cong₂ _∷_ ([-]--∥ M₀ N P) (·-∥ M N P)
+
+opaque
+
+  unfolding _≑_
+
+  ≑-· : (M : Matrix B C)
+        (N : Matrix B D)
+        (P : Matrix A B)
+      → (M ≑ N) · P ≡ (M · P) ≑ (N · P)
+  ≑-· [] N P = ≡.refl
+  ≑-· (M₀ ∷ M) N P = ≡.cong ([ M₀ ] P ∷_) (≑-· M N P)
+
+opaque
+
+  unfolding _[+]_
+
+  ∥-·-≑
+      : (W : Matrix A C)
+        (X : Matrix B C)
+        (Y : Matrix D A)
+        (Z : Matrix D B)
+      → (W ∥ X) · (Y ≑ Z) ≋ (W · Y) [+] (X · Z)
+  ∥-·-≑ [] [] Y Z = PW.[]
+  ∥-·-≑ {A} {C} {B} {D} (W₀ ∷ W) (X₀ ∷ X) Y Z = [++]-≑ W₀ X₀ Y Z PW.∷ ∥-·-≑ W X Y Z
+    where
+      open ≈-Reasoning (Matrixₛ A B)
+
+opaque
+
+  unfolding Matrix
+
+  ·-resp-≋ : {X X′ : Matrix n p} {Y Y′ : Matrix m n} → X ≋ X′ → Y ≋ Y′ → X · Y ≋ X′ · Y′
+  ·-resp-≋ ≋X ≋Y = PW.map⁺ (λ {_} {y} ≋V → [-]--cong ≋V ≋Y) ≋X
+
+  ·-assoc : {A B C D : ℕ} {f : Matrix A B} {g : Matrix B C} {h : Matrix C D} → (h · g) · f ≋ h · g · f
+  ·-assoc {A} {B} {C} {D} {f} {g} {h} = begin
+      map ([_] f) (map ([_] g) h) ≡⟨ map-∘ ([_] f) ([_] g) h ⟨
+      map (λ v → [ [ v ] g ] f) h ≈⟨ PW.map⁺ (λ {x} x≊y → ≊.trans ([]-· x f g) ([-]--cong ([-]--cong x≊y ≋.refl) ≋.refl)) {xs = h} ≋.refl ⟨
+      map (λ v → [ v ] (g · f)) h ∎
+    where
+      open ≈-Reasoning (Matrixₛ A D)
+
+  ·-Iˡ : {f : Matrix n m} → I · f ≋ f
+  ·-Iˡ {A} {B} {f} = begin
+      I · f               ≡⟨ ·-·′ I f ⟩
+      map (I [_]) (f ᵀ) ᵀ ≈⟨ -ᵀ-cong (PW.map⁺ (λ {x} ≊V → ≊.trans (I[-] x) ≊V) {xs = f ᵀ} ≋.refl) ⟩
+      map id (f ᵀ) ᵀ      ≡⟨ ≡.cong (_ᵀ) (map-id (f ᵀ)) ⟩
+      f ᵀ ᵀ               ≡⟨ f ᵀᵀ ⟩
+      f                   ∎
+    where
+      open ≈-Reasoning (Matrixₛ A B)
+
+  ·-Iʳ : {f : Matrix n m} → f · I ≋ f
+  ·-Iʳ {A} {B} {f} = begin
+      f · I               ≡⟨ ·-·′ f I ⟩
+      map (f [_]) (I ᵀ) ᵀ ≈⟨ -ᵀ-cong (≋.reflexive (≡.cong (map (f [_])) Iᵀ)) ⟩
+      map (f [_]) I ᵀ     ≈⟨ -ᵀ-cong (map--[-]-I f) ⟩
+      f ᵀ ᵀ               ≡⟨ f ᵀᵀ ⟩
+      f ∎
+    where
+      open ≈-Reasoning (Matrixₛ A B)
+
+opaque
+
+  unfolding 𝟎
+
+  ·-𝟎ʳ : (M : Matrix A B) →  M · 𝟎 {C} ≋ 𝟎
+  ·-𝟎ʳ [] = ≋.refl
+  ·-𝟎ʳ (M₀ ∷ M) = begin
+      [ M₀ ] 𝟎 ∷ M · 𝟎  ≈⟨ [-]-𝟎 M₀ PW.∷ ·-𝟎ʳ M ⟩
+      ⟨0⟩ ∷ 𝟎           ∎
+    where
+      open ≈-Reasoning (Matrixₛ _ _)
+
+  ·-𝟎ˡ : (M : Matrix A B) →  𝟎 {B} {C} · M ≋ 𝟎
+  ·-𝟎ˡ {A} {B} {zero} M = PW.[]
+  ·-𝟎ˡ {A} {B} {suc C} M = [⟨0⟩]- M PW.∷ ·-𝟎ˡ M
+
+-- The category of matrices over a rig
+Mat : Category 0ℓ c (c ⊔ ℓ)
+Mat = categoryHelper record
+    { Obj = ℕ
+    ; _⇒_ = Matrix
+    ; _≈_ = _≋_
+    ; id = I
+    ; _∘_ = _·_
+    ; assoc = λ {A B C D f g h} → ·-assoc {f = f} {g} {h}
+    ; identityˡ = ·-Iˡ
+    ; identityʳ = ·-Iʳ
+    ; equiv = ≋-isEquiv
+    ; ∘-resp-≈ = ·-resp-≋
+    }
diff --git a/Data/Matrix/Core.agda b/Data/Matrix/Core.agda
new file mode 100644
index 0000000..d97cb20
--- /dev/null
+++ b/Data/Matrix/Core.agda
@@ -0,0 +1,266 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_)
+open import Relation.Binary using (Setoid; Rel; IsEquivalence)
+
+module Data.Matrix.Core {c ℓ : Level} (S : Setoid c ℓ) where
+
+import Data.Vec.Relation.Binary.Equality.Setoid as PW-≈
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Data.Matrix.Vec using (transpose)
+open import Data.Nat using (ℕ; _+_)
+open import Data.Vec as Vec using (Vec; map; zipWith; head; tail; replicate)
+open import Data.Vec.Properties using (map-cong; map-id)
+open import Data.Vector.Core S using (Vector; Vectorₛ; _++_; ⟨⟩; ⟨⟩-!; _≊_)
+open import Data.Vector.Vec using (zipWith-map; replicate-++)
+open import Function using (id)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
+
+open Setoid S
+open ℕ
+open Vec.Vec
+
+private
+  variable
+    n m p : ℕ
+    A B C : ℕ
+
+private
+
+  module PW-≊ {n} = PW-≈ (Vectorₛ n)
+
+opaque
+
+  -- Matrices over a setoid
+  Matrix : Rel ℕ c
+  Matrix n m = Vec (Vector n) m
+
+  -- Pointwise equality of matrices
+  _≋_ : Rel (Matrix n m) (c ⊔ ℓ)
+  _≋_ {n} {m} A B = A PW-≊.≋ B
+
+  -- Pointwise equivalence is an equivalence relation
+  ≋-isEquiv : IsEquivalence (_≋_ {n} {m})
+  ≋-isEquiv {n} {m} = PW-≊.≋-isEquivalence m
+
+  mapRows : (Vector n → Vector m) → Matrix n p → Matrix m p
+  mapRows = map
+
+  _∥_ : Matrix A C → Matrix B C → Matrix (A + B) C
+  _∥_ M N = zipWith _++_ M N
+
+  infixr 7 _∥_
+
+  _≑_ : Matrix A B → Matrix A C → Matrix A (B + C)
+  _≑_ M N = M Vec.++ N
+
+  infixr 6 _≑_
+
+  _∷ᵥ_ : Vector A → Matrix A B → Matrix A (suc B)
+  _∷ᵥ_ V M = V Vec.∷ M
+
+  infixr 5 _∷ᵥ_
+
+  opaque
+
+    unfolding Vector
+
+    _∷ₕ_ : Vector B → Matrix A B → Matrix (suc A) B
+    _∷ₕ_ V M = zipWith _∷_ V M
+
+    infixr 5 _∷ₕ_
+
+    ∷ₕ-cong : {V V′ : Vector B} {M M′ : Matrix A B} → V ≊ V′ → M ≋ M′ → V ∷ₕ M ≋ V′ ∷ₕ M′
+    ∷ₕ-cong PW.[] PW.[] = PW.[]
+    ∷ₕ-cong (≈x PW.∷ ≊V) (≊M₀ PW.∷ ≋M) = (≈x PW.∷ ≊M₀) PW.∷ (∷ₕ-cong ≊V ≋M)
+
+    headₕ : Matrix (suc A) B → Vector B
+    headₕ M = map Vec.head M
+
+    tailₕ : Matrix (suc A) B → Matrix A B
+    tailₕ M = map Vec.tail M
+
+    head-∷-tailₕ : (M : Matrix (suc A) B) → headₕ M ∷ₕ tailₕ M ≡ M
+    head-∷-tailₕ M = begin
+        zipWith _∷_ (map Vec.head M) (map Vec.tail M) ≡⟨ zipWith-map head tail _∷_ M ⟩
+        map (λ x → head x ∷ tail x) M                 ≡⟨ map-cong (λ { (_ ∷ _) → ≡.refl }) M ⟩
+        map id M                                      ≡⟨ map-id M ⟩
+        M ∎
+      where
+        open ≡-Reasoning
+
+    []ᵥ : Matrix 0 B
+    []ᵥ = replicate _ []
+
+    []ᵥ-! : (E : Matrix 0 B) → E ≡ []ᵥ
+    []ᵥ-! [] = ≡.refl
+    []ᵥ-! ([] ∷ E) = ≡.cong ([] ∷_) ([]ᵥ-! E)
+
+    []ᵥ-≑ : []ᵥ {A} ≑ []ᵥ {B} ≡ []ᵥ
+    []ᵥ-≑ {A} {B} = replicate-++ A B []
+
+    []ᵥ-∥ : (M : Matrix A B) → []ᵥ ∥ M ≡ M
+    []ᵥ-∥ [] = ≡.refl
+    []ᵥ-∥ (M₀ ∷ M) = ≡.cong (M₀ ∷_) ([]ᵥ-∥ M)
+
+    ∷ₕ-∥ : (V : Vector C) (M : Matrix A C) (N : Matrix B C) → V ∷ₕ (M ∥ N) ≡ (V ∷ₕ M) ∥ N
+    ∷ₕ-∥ [] [] [] = ≡.refl
+    ∷ₕ-∥ (x ∷ V) (M₀ ∷ M) (N₀ ∷ N) = ≡.cong ((x ∷ M₀ ++ N₀) ∷_) (∷ₕ-∥ V M N)
+
+    ∷ₕ-≑ : (V : Vector A) (W : Vector B) (M : Matrix C A) (N : Matrix C B) → (V ++ W) ∷ₕ (M ≑ N) ≡ (V ∷ₕ M) ≑ (W ∷ₕ N)
+    ∷ₕ-≑ [] W [] N = ≡.refl
+    ∷ₕ-≑ (x ∷ V) W (M₀ ∷ M) N = ≡.cong ((x ∷ M₀) ∷_) (∷ₕ-≑ V W M N)
+
+  headᵥ : Matrix A (suc B) → Vector A
+  headᵥ (V ∷ _) = V
+
+  tailᵥ : Matrix A (suc B) → Matrix A B
+  tailᵥ (_ ∷ M) = M
+
+  head-∷-tailᵥ : (M : Matrix A (suc B)) → headᵥ M ∷ᵥ tailᵥ M ≡ M
+  head-∷-tailᵥ (_ ∷ _) = ≡.refl
+
+  []ₕ : Matrix A 0
+  []ₕ = []
+
+  []ₕ-! : (E : Matrix A 0) → E ≡ []ₕ
+  []ₕ-! [] = ≡.refl
+
+  []ₕ-≑ : (M : Matrix A B) → []ₕ ≑ M ≡ M
+  []ₕ-≑ _ = ≡.refl
+
+  ∷ᵥ-≑ : (V : Vector A) (M : Matrix A B) (N : Matrix A C) → V ∷ᵥ (M ≑ N) ≡ (V ∷ᵥ M) ≑ N
+  ∷ᵥ-≑ V M N = ≡.refl
+
+infix 4 _≋_
+
+module ≋ {n} {m} = IsEquivalence (≋-isEquiv {n} {m})
+
+Matrixₛ : ℕ → ℕ → Setoid c (c ⊔ ℓ)
+Matrixₛ n m = record
+    { Carrier = Matrix n m
+    ; _≈_ = _≋_ {n} {m}
+    ; isEquivalence = ≋-isEquiv
+  }
+
+opaque
+
+  unfolding Vector
+
+  head′ : Vector (suc A) → Carrier
+  head′ = head
+
+  head-cong : {V V′ : Vector (suc A)} → V ≊ V′ → head′ V ≈ head′ V′
+  head-cong (≈x PW.∷ _) = ≈x
+
+  tail′ : Vector (suc A) → Vector A
+  tail′ = tail
+
+  tail-cong : {V V′ : Vector (suc A)} → V ≊ V′ → tail′ V ≊ tail′ V′
+  tail-cong (_ PW.∷ ≊V) = ≊V
+
+opaque
+
+  unfolding headₕ head′
+
+  ≋headₕ : {M M′ : Matrix (suc A) B} → M ≋ M′ → headₕ M ≊ headₕ M′
+  ≋headₕ M≋M′ = PW.map⁺ head-cong M≋M′
+
+  ≋tailₕ : {M M′ : Matrix (suc A) B} → M ≋ M′ → tailₕ M ≋ tailₕ M′
+  ≋tailₕ M≋M′ = PW.map⁺ tail-cong M≋M′
+
+opaque
+  unfolding _≋_ _∥_ []ᵥ _∷ₕ_
+  ∥-cong : {M M′ : Matrix A C} {N N′ : Matrix B C} → M ≋ M′ → N ≋ N′ → M ∥ N ≋ M′ ∥ N′
+  ∥-cong {zero} {C} {B} {M} {M′} {N} {N′} ≋M ≋N
+    rewrite []ᵥ-! M
+    rewrite []ᵥ-! M′ = begin
+      ([]ᵥ ∥ N)   ≡⟨ []ᵥ-∥ N ⟩
+      N           ≈⟨ ≋N ⟩
+      N′          ≡⟨ []ᵥ-∥ N′ ⟨
+      ([]ᵥ ∥ N′)  ∎
+    where
+      open ≈-Reasoning (Matrixₛ _ _)
+  ∥-cong {suc A} {C} {B} {M} {M′} {N} {N′} ≋M ≋N
+    rewrite ≡.sym (head-∷-tailₕ M)
+    using M₀ ← headₕ M
+    using M- ← tailₕ M
+    rewrite ≡.sym (head-∷-tailₕ M′)
+    using M₀′ ← headₕ M′
+    using M-′ ← tailₕ M′ = begin
+      (M₀ ∷ₕ M-) ∥ N     ≡⟨ ∷ₕ-∥ M₀ M- N ⟨
+      M₀ ∷ₕ M- ∥ N       ≈⟨ ∷ₕ-cong ≊M₀ (∥-cong ≋M- ≋N) ⟩
+      M₀′ ∷ₕ M-′ ∥ N′    ≡⟨ ∷ₕ-∥ M₀′ M-′ N′ ⟩
+      (M₀′ ∷ₕ M-′) ∥ N′  ∎
+    where
+      ≊M₀ : M₀ ≊ M₀′
+      ≊M₀ = begin
+          headₕ M             ≡⟨ ≡.cong headₕ (head-∷-tailₕ M) ⟨
+          headₕ (M₀ ∷ₕ M-)    ≈⟨ ≋headₕ ≋M ⟩
+          headₕ (M₀′ ∷ₕ M-′)  ≡⟨ ≡.cong headₕ (head-∷-tailₕ M′) ⟩
+          headₕ M′            ∎
+        where
+          open ≈-Reasoning (Vectorₛ _)
+      ≋M- : M- ≋ M-′
+      ≋M- = begin
+          tailₕ M             ≡⟨ ≡.cong tailₕ (head-∷-tailₕ M) ⟨
+          tailₕ (M₀ ∷ₕ M-)    ≈⟨ ≋tailₕ ≋M ⟩
+          tailₕ (M₀′ ∷ₕ M-′)  ≡⟨ ≡.cong tailₕ (head-∷-tailₕ M′) ⟩
+          tailₕ M′            ∎
+        where
+          open ≈-Reasoning (Matrixₛ _ _)
+      open ≈-Reasoning (Matrixₛ _ _)
+
+opaque
+  unfolding _≑_
+  ≑-cong : {M M′ : Matrix A B} {N N′ : Matrix A C} → M ≋ M′ → N ≋ N′ → M ≑ N ≋ M′ ≑ N′
+  ≑-cong PW.[] ≋N = ≋N
+  ≑-cong (M₀≊M₀′ PW.∷ ≋M) ≋N = M₀≊M₀′ PW.∷ ≑-cong ≋M ≋N
+
+opaque
+
+  unfolding Matrix
+
+  _ᵀ : Matrix n m → Matrix m n
+  _ᵀ [] = []ᵥ
+  _ᵀ (M₀ ∷ M) = M₀ ∷ₕ M ᵀ
+
+  infix 10 _ᵀ
+
+  -ᵀ-cong : {M₁ M₂ : Matrix n m} → M₁ ≋ M₂ → M₁ ᵀ ≋ M₂ ᵀ
+  -ᵀ-cong PW.[] = ≋.refl
+  -ᵀ-cong (≊M₀ PW.∷ ≋M) = ∷ₕ-cong ≊M₀ (-ᵀ-cong ≋M)
+
+  opaque
+
+    unfolding []ᵥ []ₕ
+
+    []ᵥ-ᵀ : []ᵥ ᵀ ≡ []ₕ {A}
+    []ᵥ-ᵀ {zero} = ≡.refl
+    []ᵥ-ᵀ {suc A} = ≡.cong (zipWith _∷_ []) ([]ᵥ-ᵀ)
+
+  opaque
+
+    unfolding _∷ₕ_ Vector
+
+    ∷ₕ-ᵀ : (V : Vector A) (M : Matrix B A) → (V ∷ₕ M) ᵀ ≡ V ∷ᵥ M ᵀ
+    ∷ₕ-ᵀ [] [] = ≡.refl
+    ∷ₕ-ᵀ (x ∷ V) (M₀ ∷ M) = ≡.cong ((x ∷ M₀) ∷ₕ_) (∷ₕ-ᵀ V M)
+
+  ∷ᵥ-ᵀ : (V : Vector B) (M : Matrix B A) → (V ∷ᵥ M) ᵀ ≡ V ∷ₕ M ᵀ
+  ∷ᵥ-ᵀ V M = ≡.refl
+
+  opaque
+
+    _ᵀᵀ : (M : Matrix n m) → M ᵀ ᵀ ≡ M
+    _ᵀᵀ [] = []ᵥ-ᵀ
+    _ᵀᵀ (M₀ ∷ M) = begin
+        (M₀ ∷ₕ M ᵀ) ᵀ ≡⟨ ∷ₕ-ᵀ M₀ (M ᵀ)  ⟩
+        M₀ ∷ᵥ M ᵀ ᵀ   ≡⟨ ≡.cong (M₀ ∷ᵥ_) (M ᵀᵀ) ⟩
+        M₀ ∷ᵥ M       ∎
+      where
+        open ≡-Reasoning
+
+  infix 10 _ᵀᵀ
diff --git a/Data/Matrix/Dagger-2-Poset.agda b/Data/Matrix/Dagger-2-Poset.agda
new file mode 100644
index 0000000..cddf183
--- /dev/null
+++ b/Data/Matrix/Dagger-2-Poset.agda
@@ -0,0 +1,72 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (Idempotent; CommutativeSemiring)
+open import Level using (Level)
+
+module Data.Matrix.Dagger-2-Poset
+    {c ℓ : Level}
+    (R : CommutativeSemiring c ℓ)
+    (let module R = CommutativeSemiring R)
+    (+-idem : Idempotent R._≈_ R._+_)
+  where
+
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Category.Dagger.2-Poset using (dagger-2-poset; Dagger-2-Poset)
+open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger)
+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)
+open import Data.Matrix.Monoid R.+-monoid using (𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ)
+open import Data.Matrix.Transform R.semiring using (I; Iᵀ)
+open import Data.Matrix.SemiadditiveDagger R using (∥-ᵀ; Mat-SemiadditiveDagger)
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec)
+open import Data.Vector.Core R.setoid using (Vector; _≊_)
+open import Data.Vector.Monoid R.+-monoid using (_⊕_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+open Vec
+
+private
+  variable
+    A B : ℕ
+
+opaque
+  unfolding _≊_ _⊕_
+  ⊕-idem : (V : Vector A) → V ⊕ V ≊ V
+  ⊕-idem [] = PW.[]
+  ⊕-idem (v ∷ V) = +-idem v PW.∷ ⊕-idem V
+
+opaque
+  unfolding _≋_ _[+]_
+  [+]-idem : (M : Matrix A B) → M [+] M ≋ M
+  [+]-idem [] = PW.[]
+  [+]-idem (M₀ ∷ M) = ⊕-idem M₀ PW.∷ [+]-idem M
+
+idem : (M : Matrix A B) → (I ∥ I) · (((I ≑ 𝟎) · M) ∥ ((𝟎 ≑ I) · M)) · (I ∥ I) ᵀ ≋ M
+idem M = begin
+    (I ∥ I) · (((I ≑ 𝟎) · M) ∥ ((𝟎 ≑ I) · M)) · (I ∥ I) ᵀ     ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · (h₁ ∥ h₂) · (I ∥ I) ᵀ) (≑-· I 𝟎 M) (≑-· 𝟎 I M) ⟩
+    (I ∥ I) · ((I · M ≑ 𝟎 · M) ∥ (𝟎 · M ≑ I · M)) · (I ∥ I) ᵀ ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ (∥-cong (≑-cong ·-Iˡ (·-𝟎ˡ M)) (≑-cong (·-𝟎ˡ M) ·-Iˡ)) ≋.refl) ⟩
+    (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (I ∥ I) ᵀ                 ≡⟨ ≡.cong (λ h → (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · h) (∥-ᵀ I I) ⟩
+    (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (I ᵀ ≑ I ᵀ)               ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (h₁ ≑ h₂)) Iᵀ Iᵀ ⟩
+    (I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M)) · (I ≑ I)                   ≈⟨ ·-assoc ⟨
+    ((I ∥ I) · ((M ≑ 𝟎) ∥ (𝟎 ≑ M))) · (I ≑ I)                 ≡⟨ ≡.cong (_· (I ≑ I)) (·-∥ (I ∥ I) (M ≑ 𝟎) (𝟎 ≑ M)) ⟩
+    (((I ∥ I) · (M ≑ 𝟎)) ∥ ((I ∥ I) · (𝟎 ≑ M))) · (I ≑ I)     ≈⟨ ∥-·-≑ ((I ∥ I) · (M ≑ 𝟎)) ((I ∥ I) · (𝟎 ≑ M)) I I ⟩
+    (((I ∥ I) · (M ≑ 𝟎)) · I) [+] (((I ∥ I) · (𝟎 ≑ M)) · I)   ≈⟨ [+]-cong ·-Iʳ ·-Iʳ ⟩
+    ((I ∥ I) · (M ≑ 𝟎)) [+] ((I ∥ I) · (𝟎 ≑ M))               ≈⟨ [+]-cong (∥-·-≑ I I M 𝟎) (∥-·-≑ I I 𝟎 M) ⟩
+    ((I · M) [+] (I · 𝟎)) [+] ((I · 𝟎) [+] (I · M))           ≈⟨ [+]-cong ([+]-cong ·-Iˡ ·-Iˡ) ([+]-cong ·-Iˡ ·-Iˡ) ⟩
+    (M [+] 𝟎) [+] (𝟎 [+] M)                                   ≈⟨ [+]-cong ([+]-𝟎ʳ M) ([+]-𝟎ˡ M) ⟩
+    M [+] M                                                   ≈⟨ [+]-idem M ⟩
+    M ∎
+  where
+    open ≈-Reasoning (Matrixₛ _ _)
+
+Mat-IdempotentSemiadditiveDagger : IdempotentSemiadditiveDagger Mat
+Mat-IdempotentSemiadditiveDagger = record
+    { semiadditiveDagger = Mat-SemiadditiveDagger
+    ; idempotent = idem _
+    }
+
+Mat-Dagger-2-Poset : Dagger-2-Poset
+Mat-Dagger-2-Poset = dagger-2-poset Mat-IdempotentSemiadditiveDagger
diff --git a/Data/Matrix/Monoid.agda b/Data/Matrix/Monoid.agda
new file mode 100644
index 0000000..b7638f6
--- /dev/null
+++ b/Data/Matrix/Monoid.agda
@@ -0,0 +1,93 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (Monoid)
+open import Level using (Level)
+
+module Data.Matrix.Monoid {c ℓ : Level} (M : Monoid c ℓ) where
+
+module M = Monoid M
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+
+open import Data.Matrix.Core M.setoid using (Matrix; _≋_; _ᵀ; _∷ₕ_; []ᵥ; _≑_; _∥_; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥)
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec; replicate; zipWith)
+open import Data.Vec.Properties using (zipWith-replicate)
+open import Data.Vector.Monoid M using (_⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ; ⟨ε⟩)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
+
+open M
+open Vec
+open ℕ
+
+private
+  variable
+    A B C : ℕ
+
+opaque
+
+  unfolding Matrix
+
+  𝟎 : Matrix A B
+  𝟎 {A} {B} = replicate B ⟨ε⟩
+
+  opaque
+
+    unfolding _ᵀ []ᵥ ⟨ε⟩
+
+    𝟎ᵀ : 𝟎 ᵀ ≡ 𝟎 {A} {B}
+    𝟎ᵀ {zero} = ≡.refl
+    𝟎ᵀ {suc A} = let open ≡-Reasoning in begin
+        ⟨ε⟩ ∷ₕ (𝟎 ᵀ)  ≡⟨ ≡.cong (⟨ε⟩ ∷ₕ_) 𝟎ᵀ ⟩
+        ⟨ε⟩ ∷ₕ 𝟎      ≡⟨ zipWith-replicate _∷_ ε ⟨ε⟩ ⟩
+        𝟎             ∎
+
+  opaque
+
+    unfolding _≑_
+
+    𝟎≑𝟎 : 𝟎 {A} {B} ≑ 𝟎 {A} {C} ≡ 𝟎
+    𝟎≑𝟎 {B = zero} = ≡.refl
+    𝟎≑𝟎 {B = suc B} = ≡.cong (⟨ε⟩ ∷_) (𝟎≑𝟎 {B = B})
+
+  opaque
+
+    unfolding _∷ₕ_ ⟨ε⟩
+
+    ⟨ε⟩∷ₕ𝟎 : ⟨ε⟩ ∷ₕ 𝟎 {A} {B} ≡ 𝟎
+    ⟨ε⟩∷ₕ𝟎 {A} {zero} = ≡.refl
+    ⟨ε⟩∷ₕ𝟎 {A} {suc B} = ≡.cong (⟨ε⟩ ∷_) ⟨ε⟩∷ₕ𝟎
+
+𝟎∥𝟎 : 𝟎 {A} {C} ∥ 𝟎 {B} {C} ≡ 𝟎
+𝟎∥𝟎 {zero} {C} rewrite []ᵥ-! (𝟎 {0} {C}) = []ᵥ-∥ 𝟎
+𝟎∥𝟎 {suc A} {C} {B} = begin
+    𝟎 ∥ 𝟎               ≡⟨ ≡.cong (_∥ 𝟎) (⟨ε⟩∷ₕ𝟎 {A} {C}) ⟨
+    (⟨ε⟩ ∷ₕ 𝟎 {A}) ∥ 𝟎  ≡⟨ ∷ₕ-∥ ⟨ε⟩ 𝟎 𝟎 ⟨
+    ⟨ε⟩ ∷ₕ 𝟎 {A} ∥ 𝟎    ≡⟨ ≡.cong (⟨ε⟩ ∷ₕ_) 𝟎∥𝟎 ⟩
+    ⟨ε⟩ ∷ₕ 𝟎            ≡⟨ ⟨ε⟩∷ₕ𝟎 ⟩
+    𝟎                   ∎
+  where
+    open ≡-Reasoning
+
+opaque
+
+  unfolding Matrix
+
+  _[+]_ : Matrix A B → Matrix A B → Matrix A B
+  _[+]_ = zipWith _⊕_
+
+  [+]-cong : {M M′ N N′ : Matrix A B} → M ≋ M′ → N ≋ N′ → M [+] N ≋ M′ [+] N′
+  [+]-cong = PW.zipWith-cong ⊕-cong
+
+  opaque
+
+    unfolding 𝟎
+
+    [+]-𝟎ˡ : (M : Matrix A B) → 𝟎 [+] M ≋ M
+    [+]-𝟎ˡ [] = PW.[]
+    [+]-𝟎ˡ (M₀ ∷ M) = ⊕-identityˡ M₀ PW.∷ [+]-𝟎ˡ M
+
+    [+]-𝟎ʳ : (M : Matrix A B) → M [+] 𝟎 ≋ M
+    [+]-𝟎ʳ [] = PW.[]
+    [+]-𝟎ʳ (M₀ ∷ M) = ⊕-identityʳ M₀ PW.∷ [+]-𝟎ʳ M
diff --git a/Data/Matrix/SemiadditiveDagger.agda b/Data/Matrix/SemiadditiveDagger.agda
new file mode 100644
index 0000000..220ff2e
--- /dev/null
+++ b/Data/Matrix/SemiadditiveDagger.agda
@@ -0,0 +1,389 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles using (CommutativeSemiring)
+open import Level using (Level)
+
+module Data.Matrix.SemiadditiveDagger {c ℓ : Level} (R : CommutativeSemiring c ℓ) where
+
+module R = CommutativeSemiring R
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+import Data.Nat.Properties as ℕ-Props
+import Data.Nat as ℕ
+
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Object.Coproduct using (Coproduct)
+open import Categories.Object.Initial using (Initial)
+open import Category.Dagger.Semiadditive using (DaggerCocartesianMonoidal; SemiadditiveDagger)
+open import Data.Matrix.Cast R.setoid using (cast₂; cast₂-∥; ∥-≑; ∥-≑⁴; ≑-sym-assoc)
+open import Data.Matrix.Category R.semiring using (Mat; _·_; ≑-·; ·-Iˡ; ·-Iʳ; ·-𝟎ˡ; ·-𝟎ʳ; ·-∥; ∥-·-≑)
+open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _ᵀ; _ᵀᵀ; _≋_; module ≋; mapRows; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; ∥-cong; ≑-cong; -ᵀ-cong; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; []ᵥ-!)
+open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; 𝟎≑𝟎; 𝟎∥𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ)
+open import Data.Matrix.Transform R.semiring using (I; Iᵀ; [_]_; _[_]; -[-]ᵀ; [-]--cong; [-]-[]ᵥ; [⟨⟩]-[]ₕ)
+open import Data.Nat using (ℕ)
+open import Data.Product using (_,_; Σ-syntax)
+open import Data.Vec using (Vec; map; replicate)
+open import Data.Vec.Properties using (map-cong; map-const)
+open import Data.Vector.Bisemimodule R.semiring using (_∙_ ; ∙-cong)
+open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; ⟨⟩; _++_; module ≊; _≊_)
+open import Data.Vector.Monoid R.+-monoid using () renaming (⟨ε⟩ to ⟨0⟩)
+open import Data.Vector.Vec using (replicate-++)
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
+
+open R
+open Vec
+open ℕ.ℕ
+
+private
+  variable
+    A B C D E F : ℕ
+
+opaque
+  unfolding Vector _∙_
+  ∙-comm : (V W : Vector A) → V ∙ W ≈ W ∙ V
+  ∙-comm [] [] = refl
+  ∙-comm (x ∷ V) (w ∷ W) = +-cong (*-comm x w) (∙-comm V W)
+
+opaque
+  unfolding _[_] [_]_ _ᵀ []ᵥ ⟨⟩ _∷ₕ_ _≊_ _≋_ _∷ᵥ_
+  [-]-ᵀ : (M : Matrix A B) (V : Vector A) →  M [ V ] ≊ [ V ] (M ᵀ)
+  [-]-ᵀ [] V = ≊.sym (≊.reflexive ([-]-[]ᵥ V))
+  [-]-ᵀ (M₀ ∷ M) V = begin
+      M₀ ∙ V ∷ map (_∙ V) M         ≈⟨ ∙-comm M₀ V PW.∷ (PW.map⁺ (λ {x} ≊V → trans (∙-comm x V) (∙-cong ≊.refl ≊V)) ≋.refl) ⟩
+      V ∙ M₀ ∷ map (V ∙_) M         ≡⟨⟩
+      map (V ∙_) (M₀ ∷ᵥ M)          ≡⟨ ≡.cong (map (V ∙_) ∘ (M₀ ∷ᵥ_)) (M ᵀᵀ) ⟨
+      map (V ∙_) (M₀ ∷ᵥ M ᵀ ᵀ)      ≡⟨ ≡.cong (map (V ∙_)) (∷ₕ-ᵀ M₀ (M ᵀ)) ⟨
+      map (V ∙_) ((M₀ ∷ₕ (M ᵀ)) ᵀ)  ∎
+    where
+      open ≈-Reasoning (Vectorₛ _)
+
+opaque
+  unfolding []ᵥ mapRows ⟨⟩ _∷ₕ_ _∷ᵥ_ _ᵀ
+  ·-ᵀ
+      : {A B C : ℕ}
+        (M : Matrix A B)
+        (N : Matrix B C)
+      → (N · M) ᵀ ≋ M ᵀ · N ᵀ
+  ·-ᵀ {A} {B} {zero} M [] = begin
+      []ᵥ                   ≡⟨ map-const (M ᵀ) ⟨⟩ ⟨
+      map (λ _ → ⟨⟩) (M ᵀ)  ≡⟨ map-cong [-]-[]ᵥ (M ᵀ) ⟨
+      map ([_] []ᵥ) (M ᵀ)   ∎
+    where
+      open ≈-Reasoning (Matrixₛ 0 A)
+  ·-ᵀ {A} {B} {suc C} M (N₀ ∷ N) = begin
+      map ([_] M) (N₀ ∷ N) ᵀ        ≡⟨ -[-]ᵀ (N₀ ∷ N) M ⟨
+      map ((N₀ ∷ N) [_]) (M ᵀ)      ≈⟨ PW.map⁺ (λ {V} ≋V → ≊.trans ([-]-ᵀ (N₀ ∷ N) V) ([-]--cong {A = (N₀ ∷ᵥ N) ᵀ} ≋V ≋.refl)) ≋.refl ⟩
+      map ([_] ((N₀ ∷ N) ᵀ)) (M ᵀ)  ≡⟨ map-cong (λ V → ≡.cong ([ V ]_) (∷ᵥ-ᵀ N₀ N)) (M ᵀ) ⟩
+      map ([_] (N₀ ∷ₕ N ᵀ)) (M ᵀ)   ∎
+    where
+      open ≈-Reasoning (Matrixₛ (suc C) A)
+
+opaque
+  unfolding _≋_
+  ᵀ-involutive : (M : Matrix A B) → (M ᵀ) ᵀ ≋ M
+  ᵀ-involutive M = ≋.reflexive (M ᵀᵀ)
+
+opaque
+  unfolding _≋_
+  ≋λᵀ : ([]ᵥ ∥ I) ᵀ ≋ 𝟎 ≑ I {A}
+  ≋λᵀ = begin
+      ([]ᵥ ∥ I) ᵀ ≡⟨ ≡.cong (_ᵀ) ([]ᵥ-∥ I) ⟩
+      I ᵀ         ≡⟨ Iᵀ ⟩
+      I           ≡⟨ []ₕ-≑ I ⟨
+      []ₕ ≑ I     ≡⟨ ≡.cong (_≑ I) ([]ₕ-! 𝟎) ⟨
+      𝟎 ≑ I       ∎
+    where
+      open ≈-Reasoning (Matrixₛ _ _)
+
+opaque
+  unfolding Matrix _∥_ _ᵀ _≑_ _∷ₕ_
+  ∥-ᵀ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) ᵀ ≡ M ᵀ ≑ N ᵀ
+  ∥-ᵀ {A} {zero} {B} [] [] = ≡.sym (replicate-++ A B [])
+  ∥-ᵀ (M₀ ∷ M) (N₀ ∷ N) = begin
+      (M₀ ++ N₀) ∷ₕ ((M ∥ N) ᵀ) ≡⟨ ≡.cong ((M₀ ++ N₀) ∷ₕ_) (∥-ᵀ M N) ⟩
+      (M₀ ++ N₀) ∷ₕ (M ᵀ ≑ N ᵀ) ≡⟨ ∷ₕ-≑ M₀ N₀ (M ᵀ) (N ᵀ) ⟩
+      (M₀ ∷ₕ M ᵀ) ≑ (N₀ ∷ₕ N ᵀ) ∎
+    where
+      open ≡-Reasoning
+
+≑-ᵀ : (M : Matrix A B) (N : Matrix A C) → (M ≑ N) ᵀ ≡ M ᵀ ∥ N ᵀ
+≑-ᵀ M N = begin
+    (M ≑ N) ᵀ           ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ≑ h₂) ᵀ) (M ᵀᵀ) (N ᵀᵀ) ⟨
+    (M ᵀ ᵀ ≑ N ᵀ ᵀ ) ᵀ  ≡⟨ ≡.cong (_ᵀ) (∥-ᵀ (M ᵀ) (N ᵀ)) ⟨
+    (M ᵀ ∥ N ᵀ ) ᵀ ᵀ    ≡⟨ (M ᵀ ∥ N ᵀ ) ᵀᵀ ⟩
+    M ᵀ ∥ N ᵀ           ∎
+  where
+    open ≡-Reasoning
+
+opaque
+  unfolding _≋_
+  ≋ρᵀ : (I ∥ []ᵥ) ᵀ ≋ I {A} ≑ 𝟎
+  ≋ρᵀ {A} = begin
+      (I ∥ []ᵥ) ᵀ ≡⟨ ∥-ᵀ I []ᵥ ⟩
+      I ᵀ ≑ []ᵥ ᵀ ≡⟨ ≡.cong (I ᵀ ≑_) []ᵥ-ᵀ ⟩
+      I ᵀ ≑ []ₕ   ≡⟨ ≡.cong (_≑ []ₕ) Iᵀ ⟩
+      I  ≑ []ₕ    ≡⟨ ≡.cong (I ≑_) ([]ₕ-! 𝟎) ⟨
+      I ≑ 𝟎       ∎
+    where
+      open ≈-Reasoning (Matrixₛ _ _)
+
+opaque
+  unfolding _≋_
+  ≋αᵀ : (((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎)) ∥ (𝟎 {_} {A} ≑ I {B ℕ.+ C}) · (𝟎 ≑ I {C})) ᵀ
+      ≋ (I {A ℕ.+ B} ≑ 𝟎) · (I {A} ≑ 𝟎) ∥ (I {A ℕ.+ B} ≑ 𝟎) · (𝟎 ≑ I {B}) ∥ (𝟎 ≑ I {C})
+  ≋αᵀ {A} {B} {C} = begin
+      (((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ
+          ≡⟨ ∥-ᵀ ((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ⟩
+      ((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ
+          ≡⟨ ≡.cong (_≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ) (∥-ᵀ (I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C}))) ⟩
+      ((I {A} ≑ 𝟎 {A} {B ℕ.+ C}) ᵀ ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ
+          ≡⟨ ≡.cong (λ h → (h ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ) (≑-ᵀ I 𝟎) ⟩
+      (I {A} ᵀ ∥ 𝟎 {A} {B ℕ.+ C} ᵀ ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ
+          ≡⟨ ≡.cong (λ h → (h ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ) (≡.cong₂ _∥_ Iᵀ 𝟎ᵀ) ⟩
+      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (I {B} ≑ 𝟎 {B} {C})) ᵀ) ≑ ((𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) · (𝟎 {C} {B} ≑ I {C})) ᵀ
+          ≈⟨ ≑-cong (≑-cong ≋.refl (·-ᵀ (I ≑ 𝟎) (𝟎 ≑ I))) (·-ᵀ (𝟎 ≑ I) (𝟎 ≑ I)) ⟩
+      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ≑ 𝟎 {B} {C}) ᵀ · (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) ᵀ) ≑ (𝟎 {C} {B} ≑ I {C}) ᵀ · (𝟎 {B ℕ.+ C} {A} ≑ I {B ℕ.+ C}) ᵀ
+          ≡⟨ ≡.cong₂ _≑_ (≡.cong₂ (λ h₁ h₂ → I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ h₁ · h₂) (≑-ᵀ I 𝟎) (≑-ᵀ 𝟎 I)) (≡.cong₂ _·_ (≑-ᵀ 𝟎 I) (≑-ᵀ 𝟎 I)) ⟩
+      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ᵀ ∥ 𝟎 {B} {C} ᵀ) · (𝟎 {B ℕ.+ C} {A} ᵀ ∥ I {B ℕ.+ C} ᵀ)) ≑ (𝟎 {C} {B} ᵀ ∥ I {C} ᵀ) · (𝟎 {B ℕ.+ C} {A} ᵀ ∥ I {B ℕ.+ C} ᵀ)
+          ≡⟨ ≡.cong₂ _≑_ (≡.cong₂ (λ h₁ h₂ → I {A} ∥ 𝟎 ≑ h₁ · h₂) (≡.cong₂ _∥_ Iᵀ 𝟎ᵀ) (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ)) (≡.cong₂ _·_ (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ) (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ)) ⟩
+      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ∥ 𝟎 {C} {B}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})
+          ≡⟨ ≡.cong (λ h → (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ h) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})) (·-∥ (I ∥ 𝟎) 𝟎 I) ⟩
+      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ (I {B} ∥ 𝟎 {C} {B}) · 𝟎 {A} {B ℕ.+ C} ∥ (I {B} ∥ 𝟎 {C} {B}) · I {B ℕ.+ C}) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})
+          ≈⟨ ≑-cong (≑-cong ≋.refl (∥-cong (·-𝟎ʳ (I ∥ 𝟎)) ·-Iʳ)) (≋.refl {x = (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})}) ⟩
+      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C} ∥ I {B ℕ.+ C})
+          ≡⟨ ≡.cong ((I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑_) (·-∥ (𝟎 ∥ I) 𝟎 I) ⟩
+      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ (𝟎 {B} {C} ∥ I {C}) · (𝟎 {A} {B ℕ.+ C}) ∥ (𝟎 {B} {C} ∥ I {C}) · I {B ℕ.+ C}
+          ≈⟨ ≑-cong ≋.refl (∥-cong (·-𝟎ʳ (𝟎 ∥ I)) ·-Iʳ) ⟩
+      (I {A} ∥ 𝟎 {B ℕ.+ C} {A} ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ 𝟎 {A} {C} ∥ 𝟎 {B} {C} ∥ I {C}
+          ≡⟨ ≡.cong (λ h → (I {A} ∥ h ≑ 𝟎 {A} {B} ∥ I {B} ∥ 𝟎 {C} {B}) ≑ 𝟎 {A} {C} ∥ 𝟎 {B} {C} ∥ I {C}) 𝟎∥𝟎 ⟨
+      (I {A} ∥ 𝟎 {B} ∥ 𝟎 {C} ≑ 𝟎 {A} ∥ I {B} ∥ 𝟎 {C}) ≑ 𝟎 {A} ∥ 𝟎 {B} ∥ I {C}
+          ≡⟨ ≑-sym-assoc (I {A} ∥ 𝟎 {B} ∥ 𝟎 {C}) (𝟎 {A} ∥ I {B} ∥ 𝟎 {C}) (𝟎 {A} ∥ 𝟎 {B} ∥ I {C}) ⟨
+      cast₂ _ (I {A} ∥ 𝟎 {B} ∥ 𝟎 {C} ≑ 𝟎 {A} ∥ I {B} ∥ 𝟎 {C} ≑ 𝟎 {A} ∥ 𝟎 {B} ∥ I {C})
+          ≡⟨ ≡.cong (cast₂ _) (∥-≑⁴ I 𝟎 𝟎 𝟎 I 𝟎 𝟎 𝟎 I) ⟩
+      cast₂ (≡.sym assoc) ((I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) ∥ (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})))
+          ≡⟨ cast₂-∥ (≡.sym assoc) ((I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C}))) ((𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})))  ⟨
+      (cast₂ (≡.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C}))) ∥ cast₂ (≡.sym assoc) ((𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})))
+          ≡⟨ ≡.cong (cast₂ (≡.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) ∥_) (cast₂-∥ (≡.sym assoc) (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) (𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})) ⟨
+      cast₂ (≡.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) ∥ cast₂ (≡.sym assoc) (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) ∥ cast₂ (≡.sym assoc) (𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})
+          ≡⟨ ≡.cong₂ _∥_ (≑-sym-assoc I 𝟎 𝟎) (≡.cong₂ _∥_ (≑-sym-assoc 𝟎 I 𝟎) (≑-sym-assoc 𝟎 𝟎 I)) ⟩
+      ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) ∥ ((𝟎 {C} {A} ≑ 𝟎 {C} {B}) ≑ I {C})
+          ≡⟨ ≡.cong (λ h → ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) ∥ (h ≑ I {C})) 𝟎≑𝟎 ⟩
+      ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})
+          ≈⟨ ∥-cong ≋.refl (∥-cong (≑-cong ·-Iˡ (·-𝟎ˡ (𝟎 ≑ I))) ≋.refl) ⟨
+      ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ (((I {A ℕ.+ B} · (𝟎 {B} {A} ≑ I {B})) ≑ (𝟎 {A ℕ.+ B} {C} · (𝟎 {B} {A} ≑ I {B})))) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})
+          ≡⟨ ≡.cong (λ h → ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ h ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})) (≑-· I 𝟎 (𝟎 ≑ I)) ⟨
+      ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})
+          ≈⟨ ∥-cong (≑-cong ·-Iˡ (·-𝟎ˡ (I ≑ 𝟎))) ≋.refl ⟨
+      ((I {A ℕ.+ B} · (I {A} ≑ 𝟎 {A} {B})) ≑ (𝟎 {A ℕ.+ B} {C} · (I {A} ≑ 𝟎 {A} {B}))) ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})
+          ≡⟨ ≡.cong (λ h → h ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C})) (≑-· I 𝟎 (I ≑ 𝟎)) ⟨
+      (I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (I {A} ≑ 𝟎 {A} {B}) ∥ ((I {A ℕ.+ B} ≑ 𝟎 {A ℕ.+ B} {C}) · (𝟎 {B} {A} ≑ I {B})) ∥ (𝟎 {C} {A ℕ.+ B} ≑ I {C}) ∎
+    where
+      assoc : A ℕ.+ B ℕ.+ C ≡ A ℕ.+ (B ℕ.+ C)
+      assoc = ℕ-Props.+-assoc A B C
+      open ≈-Reasoning (Matrixₛ _ _)
+
+≋σᵀ : ((𝟎 ≑ I {A}) ∥ (I {B} ≑ 𝟎)) ᵀ ≋ (𝟎 ≑ I {B}) ∥ (I {A} ≑ 𝟎)
+≋σᵀ {A} {B} = begin
+    ((𝟎 ≑ I) ∥ (I ≑ 𝟎)) ᵀ       ≡⟨ ∥-ᵀ (𝟎 ≑ I) (I ≑ 𝟎) ⟩
+    (𝟎 ≑ I {A}) ᵀ ≑ (I ≑ 𝟎) ᵀ   ≡⟨ ≡.cong₂ _≑_ (≑-ᵀ 𝟎 I) (≑-ᵀ I 𝟎) ⟩
+    𝟎 ᵀ ∥ (I {A}) ᵀ ≑ I ᵀ ∥ 𝟎 ᵀ ≡⟨ ≡.cong₂ _≑_ (≡.cong₂ _∥_ 𝟎ᵀ Iᵀ) (≡.cong₂ _∥_ Iᵀ 𝟎ᵀ) ⟩
+    𝟎 ∥ I {A} ≑ I ∥ 𝟎           ≡⟨ ∥-≑ 𝟎 I I 𝟎 ⟩
+    (𝟎 ≑ I {B}) ∥ (I ≑ 𝟎)       ∎
+  where
+    open ≈-Reasoning (Matrixₛ _ _)
+
+≋⊗  : (M : Matrix A B)
+      (N : Matrix C D)
+    → (I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N
+    ≋ (M ≑ 𝟎) ∥ (𝟎 ≑ N)
+≋⊗ M N = begin
+    (I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N         ≡⟨ ≡.cong₂ _∥_ (≑-· I 𝟎 M) (≑-· 𝟎 I N)  ⟩
+    (I · M ≑ 𝟎 · M) ∥ (𝟎 · N ≑ I · N) ≈⟨ ∥-cong (≑-cong ·-Iˡ (·-𝟎ˡ M)) (≑-cong (·-𝟎ˡ N) ·-Iˡ) ⟩
+    (M ≑ 𝟎) ∥ (𝟎 ≑ N)                 ∎
+  where
+    open ≈-Reasoning (Matrixₛ _ _)
+
+ᵀ-resp-⊗
+    : {M : Matrix A B}
+      {N : Matrix C D}
+    → ((I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N) ᵀ
+    ≋ (I ≑ 𝟎) · M ᵀ ∥ (𝟎 ≑ I) · N ᵀ
+ᵀ-resp-⊗ {M = M} {N = N} = begin
+    ((I ≑ 𝟎) · M ∥ (𝟎 ≑ I) · N) ᵀ ≈⟨ -ᵀ-cong (≋⊗ M N) ⟩
+    ((M ≑ 𝟎) ∥ (𝟎 ≑ N)) ᵀ         ≡⟨ ≡.cong (_ᵀ) (∥-≑ M 𝟎 𝟎 N) ⟨
+    ((M ∥ 𝟎) ≑ (𝟎 ∥ N)) ᵀ         ≡⟨ ≑-ᵀ (M ∥ 𝟎) (𝟎 ∥ N) ⟩
+    (M ∥ 𝟎) ᵀ ∥ (𝟎 ∥ N) ᵀ         ≡⟨ ≡.cong₂ _∥_ (∥-ᵀ M 𝟎) (∥-ᵀ 𝟎 N) ⟩
+    (M ᵀ ≑ 𝟎 ᵀ) ∥ (𝟎 ᵀ ≑ N ᵀ)     ≡⟨ ≡.cong₂ (λ h₁ h₂ → (M ᵀ ≑ h₁) ∥ (h₂ ≑ N ᵀ)) 𝟎ᵀ 𝟎ᵀ ⟩
+    (M ᵀ ≑ 𝟎) ∥ (𝟎 ≑ N ᵀ)         ≈⟨ ≋⊗ (M ᵀ) (N ᵀ) ⟨
+    (I ≑ 𝟎) · M ᵀ ∥ (𝟎 ≑ I) · N ᵀ ∎
+  where
+    open ≈-Reasoning (Matrixₛ _ _)
+
+inj₁ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (I ≑ 𝟎) ≋ M
+inj₁ {A} {C} M N = begin
+    (M ∥ N) · (I ≑ 𝟎)   ≈⟨ ∥-·-≑ M N I 𝟎 ⟩
+    (M · I) [+] (N · 𝟎) ≈⟨ [+]-cong ·-Iʳ (·-𝟎ʳ N) ⟩
+    M [+] 𝟎             ≈⟨ [+]-𝟎ʳ M ⟩
+    M ∎
+  where
+    open ≈-Reasoning (Matrixₛ A C)
+
+inj₂ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (𝟎 ≑ I) ≋ N
+inj₂ {A} {C} {B} M N = begin
+    (M ∥ N) · (𝟎 ≑ I)   ≈⟨ ∥-·-≑ M N 𝟎 I ⟩
+    (M · 𝟎) [+] (N · I) ≈⟨ [+]-cong (·-𝟎ʳ M) ·-Iʳ ⟩
+    𝟎 [+] N             ≈⟨ [+]-𝟎ˡ N ⟩
+    N ∎
+  where
+    open ≈-Reasoning (Matrixₛ B C)
+
+opaque
+  unfolding Matrix
+  split-∥ : (A : ℕ) → (M : Matrix (A ℕ.+ B) C) → Σ[ M₁ ∈ Matrix A C ] Σ[ M₂ ∈ Matrix B C ] M₁ ∥ M₂ ≡ M
+  split-∥ zero M = []ᵥ , M , []ᵥ-∥ M
+  split-∥ (suc A) M′
+    rewrite ≡.sym (head-∷-tailₕ M′)
+    using M₀ ← headₕ M′
+    using M ← tailₕ M′
+    with split-∥ A M
+  ... | M₁ , M₂ , M₁∥M₂≡M = M₀ ∷ₕ M₁ , M₂ , (begin
+      (M₀ ∷ₕ M₁) ∥ M₂ ≡⟨ ∷ₕ-∥ M₀ M₁ M₂ ⟨
+      M₀ ∷ₕ M₁ ∥ M₂   ≡⟨ ≡.cong (M₀ ∷ₕ_) M₁∥M₂≡M ⟩
+      M₀ ∷ₕ M ∎)
+    where
+      open ≡-Reasoning
+
+uniq
+    : (H : Matrix (A ℕ.+ B) C)
+      (M : Matrix A C)
+      (N : Matrix B C)
+    → H · (I ≑ 𝟎) ≋ M
+    → H · (𝟎 ≑ I) ≋ N
+    → M ∥ N ≋ H
+uniq {A} {B} {C} H M N eq₁ eq₂
+  with (H₁ , H₂ , H₁∥H₂≡H) ← split-∥ A H
+  rewrite ≡.sym H₁∥H₂≡H = begin
+    M ∥ N                                         ≈⟨ ∥-cong eq₁ eq₂ ⟨
+    (H₁ ∥ H₂) · (I {A} ≑ 𝟎) ∥ (H₁ ∥ H₂) · (𝟎 ≑ I) ≈⟨ ∥-cong (inj₁ H₁ H₂) (inj₂ H₁ H₂) ⟩
+    (H₁ ∥ H₂) ∎
+  where
+    open ≈-Reasoning (Matrixₛ (A ℕ.+ B) C)
+
+coproduct : Coproduct Mat A B
+coproduct {A} {B} = record
+    { A+B = A ℕ.+ B
+    ; i₁ = I ≑ 𝟎
+    ; i₂ = 𝟎 ≑ I
+    ; [_,_] = _∥_
+    ; inject₁ = λ {a} {b} {c} → inj₁ b c
+    ; inject₂ = λ {a} {b} {c} → inj₂ b c
+    ; unique = λ eq₁ eq₂ → uniq _ _ _ eq₁ eq₂
+    }
+
+opaque
+  unfolding _≋_
+  !-unique : (E : Matrix 0 B) → []ᵥ ≋ E
+  !-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E))
+
+initial : Initial Mat
+initial = record
+    { ⊥ = 0
+    ; ⊥-is-initial = record
+        { ! = []ᵥ
+        ; !-unique = !-unique
+        }
+    }
+
+Mat-Cocartesian : Cocartesian Mat
+Mat-Cocartesian = record
+    { initial = initial
+    ; coproducts = record
+        { coproduct = coproduct
+        }
+    }
+
+Mat-DaggerCocartesian : DaggerCocartesianMonoidal Mat
+Mat-DaggerCocartesian = record
+    { cocartesian = Mat-Cocartesian
+    ; dagger = record
+        { _† = λ M → M ᵀ
+        ; †-identity = ≋.reflexive Iᵀ
+        ; †-homomorphism = λ {f = f} {g} → ·-ᵀ f g
+        ; †-resp-≈ = -ᵀ-cong
+        ; †-involutive = ᵀ-involutive
+        }
+    ; λ≅† = ≋λᵀ
+    ; ρ≅† = ≋ρᵀ
+    ; α≅† = ≋αᵀ
+    ; σ≅† = ≋σᵀ
+    ; †-resp-⊗ = ᵀ-resp-⊗
+    }
+
+p₁-i₁ : (I ≑ 𝟎) ᵀ · (I ≑ 𝟎 {A} {B}) ≋ I
+p₁-i₁ = begin
+    (I ≑ 𝟎) ᵀ · (I ≑ 𝟎)   ≡⟨ ≡.cong (_· (I ≑ 𝟎)) (≑-ᵀ I 𝟎) ⟩
+    (I ᵀ ∥ 𝟎 ᵀ) · (I ≑ 𝟎) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (I ≑ 𝟎)) Iᵀ 𝟎ᵀ ⟩
+    (I ∥ 𝟎) · (I ≑ 𝟎)     ≈⟨ ∥-·-≑ I 𝟎 I 𝟎 ⟩
+    (I · I) [+] (𝟎 · 𝟎)   ≈⟨ [+]-cong ·-Iˡ (·-𝟎ˡ 𝟎) ⟩
+    I [+] 𝟎               ≈⟨ [+]-𝟎ʳ I ⟩
+    I                     ∎
+  where
+    open ≈-Reasoning (Matrixₛ _ _)
+
+p₂-i₂ : (𝟎 {A} {B} ≑ I) ᵀ · (𝟎 ≑ I) ≋ I
+p₂-i₂ = begin
+    (𝟎 ≑ I) ᵀ · (𝟎 ≑ I)   ≡⟨ ≡.cong (_· (𝟎 ≑ I)) (≑-ᵀ 𝟎 I) ⟩
+    (𝟎 ᵀ ∥ I ᵀ) · (𝟎 ≑ I) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (𝟎 ≑ I)) 𝟎ᵀ Iᵀ ⟩
+    (𝟎 ∥ I) · (𝟎 ≑ I)     ≈⟨ ∥-·-≑ 𝟎 I 𝟎 I ⟩
+    (𝟎 · 𝟎) [+] (I · I)   ≈⟨ [+]-cong (·-𝟎ˡ 𝟎) ·-Iˡ ⟩
+    𝟎 [+] I               ≈⟨ [+]-𝟎ˡ I ⟩
+    I                     ∎
+  where
+    open ≈-Reasoning (Matrixₛ _ _)
+
+opaque
+  unfolding 𝟎 ⟨⟩
+  []ᵥ·[]ₕ : []ᵥ · []ₕ ≡ 𝟎 {A} {B}
+  []ᵥ·[]ₕ {A} {B} = begin
+      map ([_] []ₕ) []ᵥ   ≡⟨ map-cong (λ { [] → [⟨⟩]-[]ₕ }) []ᵥ ⟩
+      map (λ _ → ⟨0⟩) []ᵥ ≡⟨ map-const []ᵥ ⟨0⟩ ⟩
+      𝟎                   ∎
+    where
+      open ≡-Reasoning
+
+p₂-i₁ : (𝟎 {A} ≑ I) ᵀ · (I ≑ 𝟎 {B}) ≋ []ᵥ · []ᵥ ᵀ
+p₂-i₁ = begin
+    (𝟎 ≑ I) ᵀ · (I ≑ 𝟎)   ≡⟨ ≡.cong (_· (I ≑ 𝟎)) (≑-ᵀ 𝟎 I) ⟩
+    (𝟎 ᵀ ∥ I ᵀ) · (I ≑ 𝟎) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (I ≑ 𝟎)) 𝟎ᵀ Iᵀ ⟩
+    (𝟎 ∥ I) · (I ≑ 𝟎)     ≈⟨ ∥-·-≑ 𝟎 I I 𝟎 ⟩
+    (𝟎 · I) [+] (I · 𝟎)   ≈⟨ [+]-cong (·-𝟎ˡ I) (·-𝟎ʳ I) ⟩
+    𝟎 [+] 𝟎               ≈⟨ [+]-𝟎ˡ 𝟎 ⟩
+    𝟎                     ≡⟨ []ᵥ·[]ₕ ⟨
+    []ᵥ · []ₕ             ≡⟨ ≡.cong ([]ᵥ ·_) []ᵥ-ᵀ ⟨
+    []ᵥ · []ᵥ ᵀ           ∎
+  where
+    open ≈-Reasoning (Matrixₛ _ _)
+
+p₁-i₂ : (I ≑ 𝟎 {A}) ᵀ · (𝟎 {B} ≑ I) ≋ []ᵥ · []ᵥ ᵀ
+p₁-i₂ = begin
+    (I ≑ 𝟎) ᵀ · (𝟎 ≑ I)   ≡⟨ ≡.cong (_· (𝟎 ≑ I)) (≑-ᵀ I 𝟎) ⟩
+    (I ᵀ ∥ 𝟎 ᵀ) · (𝟎 ≑ I) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (h₁ ∥ h₂) · (𝟎 ≑ I)) Iᵀ 𝟎ᵀ ⟩
+    (I ∥ 𝟎) · (𝟎 ≑ I)     ≈⟨ ∥-·-≑ I 𝟎 𝟎 I ⟩
+    (I · 𝟎) [+] (𝟎 · I)   ≈⟨ [+]-cong (·-𝟎ʳ I) (·-𝟎ˡ I) ⟩
+    𝟎 [+] 𝟎               ≈⟨ [+]-𝟎ˡ 𝟎 ⟩
+    𝟎                     ≡⟨ []ᵥ·[]ₕ ⟨
+    []ᵥ · []ₕ             ≡⟨ ≡.cong ([]ᵥ ·_) []ᵥ-ᵀ ⟨
+    []ᵥ · []ᵥ ᵀ           ∎
+  where
+    open ≈-Reasoning (Matrixₛ _ _)
+
+Mat-SemiadditiveDagger : SemiadditiveDagger Mat
+Mat-SemiadditiveDagger = record
+    { daggerCocartesianMonoidal = Mat-DaggerCocartesian
+    ; p₁-i₁ = p₁-i₁
+    ; p₂-i₂ = p₂-i₂
+    ; p₂-i₁ = p₂-i₁
+    ; p₁-i₂ = p₁-i₂
+    }
diff --git a/Data/Matrix/Transform.agda b/Data/Matrix/Transform.agda
new file mode 100644
index 0000000..671725f
--- /dev/null
+++ b/Data/Matrix/Transform.agda
@@ -0,0 +1,298 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; 0ℓ; _⊔_)
+open import Relation.Binary using (Setoid; Rel; IsEquivalence)
+open import Algebra using (Semiring)
+
+module Data.Matrix.Transform {c ℓ : Level} (R : Semiring c ℓ) where
+
+module R = Semiring R
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec; map; replicate; zipWith)
+open import Data.Vec.Properties using (map-id; map-const; map-∘; zipWith-replicate; zipWith-replicate₁; map-replicate; map-cong)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≗_; _≡_; module ≡-Reasoning)
+open import Function using (id; _∘_)
+
+open import Data.Matrix.Core R.setoid
+  using
+    ( Matrix; Matrixₛ; _≋_; ≋-isEquiv; _ᵀ; _∷ₕ_; []ᵥ; []ₕ; []ᵥ-ᵀ; mapRows
+    ; _ᵀᵀ; []ᵥ-!; ∷ₕ-ᵀ; ∷ₕ-cong; module ≋; -ᵀ-cong; _∥_; []ᵥ-∥; headₕ; tailₕ; head-∷-tailₕ; ∷ₕ-∥
+    ; _≑_; []ᵥ-≑; ∷ₕ-≑
+    )
+open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; _[+]_)
+open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; ⟨⟩; module ≊; _≊_; _++_; ⟨⟩-++)
+open import Data.Vector.Vec using (zipWith-map; map-zipWith; zipWith-map-map)
+open import Data.Vector.Monoid R.+-monoid using (_⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ) renaming (⟨ε⟩ to ⟨0⟩)
+open import Data.Vector.Bisemimodule R using (_∙_; ∙-cong; ∙-zeroˡ; ∙-zeroʳ; _⟨_⟩; *-∙ˡ; ∙-distribʳ)
+
+open Vec
+open ℕ
+open R
+
+private
+  variable
+    n m p : ℕ
+    A B C D : ℕ
+
+opaque
+
+  unfolding Matrix
+
+  opaque
+
+    unfolding Vector
+
+    _[_] : Matrix n m → Vector n → Vector m
+    _[_] M V = map (_∙ V) M
+
+    [_]_ : Vector m → Matrix n m → Vector n
+    [_]_ V M = map (V ∙_) (M ᵀ)
+
+    -[-]-cong : {x y : Vector n} (A : Matrix n m) → x ≊ y → A [ x ] ≊ A [ y ]
+    -[-]-cong {x = x} {y} A ≋V = PW.map⁺ (λ ≋w → ∙-cong ≋w ≋V) {xs = A} ≋.refl
+
+    [-]--cong : {x y : Vector m} {A B : Matrix n m} → x ≊ y → A ≋ B → [ x ] A ≊ [ y ] B
+    [-]--cong ≋V A≋B = PW.map⁺ (∙-cong ≋V) (-ᵀ-cong A≋B)
+
+    opaque
+
+      unfolding _ᵀ []ᵥ
+
+      [-]-[]ᵥ : (V : Vector A) → [ V ] []ᵥ ≡ ⟨⟩
+      [-]-[]ᵥ [] = ≡.refl
+      [-]-[]ᵥ (x ∷ V) = ≡.cong (map ((x ∷ V) ∙_)) []ᵥ-ᵀ
+
+    opaque
+
+      unfolding []ᵥ _ᵀ ⟨0⟩ _∙_
+
+      [-]-[]ₕ : (V : Vector 0) → [ V ] []ₕ ≡ ⟨0⟩ {n}
+      [-]-[]ₕ {zero} [] = ≡.refl
+      [-]-[]ₕ {suc A} [] = ≡.cong (0# ∷_) ([-]-[]ₕ [])
+
+opaque
+
+  unfolding Matrix Vector
+
+  -- The identity matrix
+  I : Matrix n n
+  I {zero} = []
+  I {suc n} = (1# ∷ ⟨0⟩) ∷ ⟨0⟩ ∷ₕ I
+
+  opaque
+
+    unfolding _ᵀ _∷ₕ_
+
+    Iᵀ : I ᵀ ≡ I {n}
+    Iᵀ {zero} = ≡.sym ([]ᵥ-! [])
+    Iᵀ {suc n} = begin
+        (1# ∷ ⟨0⟩) ∷ₕ ((⟨0⟩ ∷ₕ I) ᵀ)  ≡⟨ ≡.cong ((1# ∷ ⟨0⟩) ∷ₕ_) (∷ₕ-ᵀ ⟨0⟩ I) ⟩
+        (1# ∷ ⟨0⟩) ∷ (⟨0⟩ ∷ₕ (I ᵀ))   ≡⟨ ≡.cong (λ h → (1# ∷ ⟨0⟩) ∷ (⟨0⟩ ∷ₕ h)) Iᵀ ⟩
+        (1# ∷ ⟨0⟩) ∷ (⟨0⟩ ∷ₕ I)       ∎
+      where
+        open ≡-Reasoning
+
+opaque
+  unfolding mapRows _ᵀ _[_] [_]_ []ᵥ
+  -[-]ᵀ : (A : Matrix m p) (B : Matrix n m) → mapRows (A [_]) (B ᵀ) ≡ (mapRows ([_] B) A) ᵀ
+  -[-]ᵀ [] B = map-const (B ᵀ) []
+  -[-]ᵀ (A₀ ∷ A) B = begin
+      map (λ V → A₀ ∙ V ∷ map (_∙ V) A) (B ᵀ) ≡⟨ zipWith-map (A₀ ∙_) (A [_]) _∷_ (B ᵀ) ⟨
+      [ A₀ ] B ∷ₕ (map (A [_]) (B ᵀ))         ≡⟨ ≡.cong ([ A₀ ] B ∷ₕ_) (-[-]ᵀ A B) ⟩
+      [ A₀ ] B ∷ₕ ((map ([_] B) A) ᵀ) ∎
+    where
+      open ≡-Reasoning
+
+opaque
+  unfolding [_]_ _[_] _ᵀ []ₕ _∙_ _∷ₕ_ _⟨_⟩
+
+  []-∙ : (V : Vector m) (M : Matrix n m) (W : Vector n) → [ V ] M ∙ W ≈ V ∙ M [ W ]
+  []-∙ {n = n} [] M@[] W = begin
+      [ [] ] []ₕ ∙ W  ≡⟨ ≡.cong (_∙ W) ([-]-[]ₕ []) ⟩
+      ⟨0⟩ ∙ W         ≈⟨ ∙-zeroˡ W ⟩
+      0#              ∎
+    where
+      open ≈-Reasoning setoid
+  []-∙ (V₀ ∷ V) (M₀ ∷ M) W = begin
+      [ V₀ ∷ V ] (M₀ ∷ M) ∙ W                         ≡⟨ ≡.cong (_∙ W) (map-zipWith ((V₀ ∷ V) ∙_) _∷_ M₀ (M ᵀ)) ⟩
+      (zipWith (λ x y → V₀ * x + V ∙ y) M₀ (M ᵀ)) ∙ W ≡⟨ ≡.cong (_∙ W) (zipWith-map-map (V₀ *_) (V ∙_) _+_ M₀ (M ᵀ)) ⟩
+      (V₀ ⟨ M₀ ⟩ ⊕ [ V ] M) ∙ W                       ≈⟨ ∙-distribʳ (V₀ ⟨ M₀ ⟩) ([ V ] M) W ⟩
+      V₀ ⟨ M₀ ⟩ ∙ W + [ V ] M ∙ W                     ≈⟨ +-congʳ (*-∙ˡ V₀ M₀ W) ⟨
+      V₀ * (M₀ ∙ W) + ([ V ] M) ∙ W                   ≈⟨ +-congˡ ([]-∙ V M W) ⟩
+      (V₀ ∷ V) ∙ (M₀ ∷ M) [ W ]                       ∎
+    where
+      open ≈-Reasoning setoid
+
+opaque
+  unfolding Vector [_]_ I _∙_ ⟨0⟩ mapRows _ᵀ []ᵥ
+  [-]I : {n : ℕ} (V : Vector n) → [ V ] I ≊ V
+  [-]I {zero} [] = ≊.refl
+  [-]I {suc n} (x ∷ V) = begin
+      map ((x ∷ V) ∙_) ((1# ∷ ⟨0⟩) ∷ₕ (⟨0⟩ ∷ₕ I) ᵀ)     ≡⟨ ≡.cong (λ h → map ((x ∷ V) ∙_) ((1# ∷ ⟨0⟩) ∷ₕ h)) (∷ₕ-ᵀ ⟨0⟩ I) ⟩
+      x * 1# + V ∙ ⟨0⟩ ∷ map ((x ∷ V) ∙_) (⟨0⟩ ∷ₕ I ᵀ)  ≈⟨ +-congʳ (*-identityʳ x) PW.∷ ≊.refl ⟩
+      x + V ∙ ⟨0⟩ ∷ map ((x ∷ V) ∙_) (⟨0⟩ ∷ₕ I ᵀ)       ≈⟨ +-congˡ (∙-zeroʳ V) PW.∷ ≊.refl ⟩
+      x + 0# ∷ map ((x ∷ V) ∙_) (⟨0⟩ ∷ₕ I ᵀ)            ≈⟨ +-identityʳ x PW.∷ ≊.refl ⟩
+      x ∷ map ((x ∷ V) ∙_) (⟨0⟩ ∷ₕ I ᵀ)                 ≡⟨ ≡.cong (λ h → x ∷ map ((x ∷ V) ∙_) h) (zipWith-replicate₁ _∷_ 0# (I ᵀ)) ⟩
+      x ∷ map ((x ∷ V) ∙_) (map (0# ∷_) (I ᵀ))          ≡⟨ ≡.cong (x ∷_) (map-∘ ((x ∷ V) ∙_) (0# ∷_) (I ᵀ)) ⟨
+      x ∷ map (λ y → x * 0# + V ∙ y) (I ᵀ)              ≈⟨ refl PW.∷ PW.map⁺ (λ ≊V → trans (+-congʳ (zeroʳ x)) (+-congˡ (∙-cong {v₁ = V} ≊.refl ≊V))) ≋.refl ⟩
+      x ∷ map (λ y → 0# + V ∙ y) (I ᵀ)                  ≈⟨ refl PW.∷ PW.map⁺ (λ ≊V → trans (+-identityˡ (V ∙ _)) (∙-cong {v₁ = V} ≊.refl ≊V)) ≋.refl ⟩
+      x ∷ map (V ∙_) (I ᵀ)                              ≈⟨ refl PW.∷ ([-]I V) ⟩
+      x ∷ V                                             ∎
+    where
+      open ≈-Reasoning (Vectorₛ (suc n))
+
+opaque
+  unfolding _≊_ I _[_] _∙_ _≋_ _∷ₕ_ ⟨0⟩
+  I[-] : {n : ℕ} (V : Vector n) → I [ V ] ≊ V
+  I[-] {zero} [] = PW.[]
+  I[-] {suc n} (x ∷ V) = hd PW.∷ tl
+    where
+      hd : (1# ∷ ⟨0⟩) ∙ (x ∷ V) ≈ x
+      hd = begin
+          1# * x + ⟨0⟩ ∙ V  ≈⟨ +-congʳ (*-identityˡ x) ⟩
+          x + ⟨0⟩ ∙ V       ≈⟨ +-congˡ (∙-zeroˡ V) ⟩
+          x + 0#            ≈⟨ +-identityʳ x ⟩
+          x                 ∎
+        where
+          open ≈-Reasoning setoid
+      tl : map (_∙ (x ∷ V)) (⟨0⟩ ∷ₕ I) ≊ V
+      tl = begin
+          map (_∙ (x ∷ V)) (⟨0⟩ ∷ₕ I)       ≡⟨ ≡.cong (map (_∙ (x ∷ V))) (zipWith-replicate₁ _∷_ 0# I) ⟩
+          map (_∙ (x ∷ V)) (map (0# ∷_) I)  ≡⟨ map-∘ (_∙ (x ∷ V)) (0# ∷_) I ⟨
+          map (λ t → 0# * x + t ∙ V) I      ≈⟨ PW.map⁺ (λ ≋X → trans (+-congʳ (zeroˡ x)) (+-congˡ (∙-cong ≋X ≊.refl))) {xs = I} ≋.refl ⟩
+          map (λ t → 0# + t ∙ V) I          ≈⟨ PW.map⁺ (λ {t} ≋X → trans (+-identityˡ (t ∙ V)) (∙-cong ≋X ≊.refl)) {xs = I} ≋.refl ⟩
+          map (_∙ V) I                      ≈⟨ I[-] V ⟩
+          V                                 ∎
+        where
+          open ≈-Reasoning (Vectorₛ n)
+
+opaque
+  unfolding mapRows _[_] _ᵀ _∷ₕ_ I
+  map--[-]-I : (M : Matrix n m) → mapRows (M [_]) I ≋ M ᵀ
+  map--[-]-I {n} {m} [] = ≋.reflexive (map-const I [])
+  map--[-]-I {n} {suc m} (M₀ ∷ M) = begin
+      map ((M₀ ∷ M) [_]) I              ≡⟨⟩
+      map (λ V → M₀ ∙ V ∷ M [ V ]) I    ≡⟨ zipWith-map (M₀ ∙_) (M [_]) _∷_ I ⟨
+      map (M₀ ∙_) I ∷ₕ (map (M [_]) I)  ≈⟨ ∷ₕ-cong (≊.reflexive (≡.sym (≡.cong (map (M₀ ∙_)) Iᵀ))) (map--[-]-I M) ⟩
+      [ M₀ ] I ∷ₕ (M ᵀ)                 ≈⟨ ∷ₕ-cong ([-]I M₀) ≋.refl ⟩
+      M₀ ∷ₕ (M ᵀ)                       ∎
+    where
+      open ≈-Reasoning (Matrixₛ (suc m) n)
+
+opaque
+
+  unfolding [_]_
+
+  [-]--∥
+      : (V : Vector C)
+        (M : Matrix A C)
+        (N : Matrix B C)
+      → [ V ] (M ∥ N) ≡ ([ V ] M) ++ ([ V ] N)
+  [-]--∥ {C} {zero} V M N rewrite []ᵥ-! M = begin
+      [ V ] ([]ᵥ ∥ N)           ≡⟨ ≡.cong ([ V ]_) ([]ᵥ-∥ N) ⟩
+      [ V ] N                   ≡⟨ ⟨⟩-++ ([ V ] N) ⟨
+      ⟨⟩ ++ ([ V ] N)           ≡⟨ ≡.cong (_++ ([ V ] N)) ([-]-[]ᵥ V) ⟨
+      ([ V ] []ᵥ) ++ ([ V ] N)  ∎
+    where
+      open ≡-Reasoning
+  [-]--∥ {C} {suc A} V M N
+    rewrite ≡.sym (head-∷-tailₕ M)
+    using M₀ ← headₕ M
+    using M ← tailₕ M = begin
+      [ V ] ((M₀ ∷ₕ M) ∥ N)                     ≡⟨ ≡.cong ([ V ]_) (∷ₕ-∥ M₀ M N) ⟨
+      [ V ] (M₀ ∷ₕ (M ∥ N))                     ≡⟨ ≡.cong (map (V ∙_)) (∷ₕ-ᵀ M₀ (M ∥ N)) ⟩
+      V ∙ M₀ ∷ ([ V ] (M ∥ N))                  ≡⟨ ≡.cong (V ∙ M₀ ∷_) ([-]--∥ V M N) ⟩
+      V ∙ M₀ ∷ (([ V ] M) ++ ([ V ] N))         ≡⟨⟩
+      (V ∙ M₀ ∷ map (V ∙_ ) (M ᵀ)) ++ ([ V ] N) ≡⟨ ≡.cong (λ h → map (V ∙_) h ++ ([ V ] N)) (∷ₕ-ᵀ M₀ M) ⟨
+      ([ V ] (M₀ ∷ₕ M)) ++ ([ V ] N)            ∎
+    where
+      open ≡-Reasoning
+
+opaque
+
+  unfolding _++_ _∙_
+
+  ∙-++ : (W Y : Vector A) (X Z : Vector B) → (W ++ X) ∙ (Y ++ Z) ≈ W ∙ Y + X ∙ Z
+  ∙-++ [] [] X Z = sym (+-identityˡ (X ∙ Z))
+  ∙-++ (w ∷ W) (y ∷ Y) X Z = begin
+      w * y + (W ++ X) ∙ (Y ++ Z) ≈⟨ +-congˡ (∙-++ W Y X Z) ⟩
+      w * y + (W ∙ Y + X ∙ Z)     ≈⟨ +-assoc _ _ _ ⟨
+      (w * y + W ∙ Y) + X ∙ Z     ∎
+    where
+      open ≈-Reasoning setoid
+
+opaque
+
+  unfolding _⊕_ ⟨⟩ [_]_
+
+  [++]-≑
+      : (V : Vector B)
+        (W : Vector C)
+        (M : Matrix A B)
+        (N : Matrix A C)
+      → [ V ++ W ] (M ≑ N)
+      ≊ [ V ] M ⊕ [ W ] N
+  [++]-≑ {B} {C} {zero} V W M N
+    rewrite []ᵥ-! M
+    rewrite []ᵥ-! N = begin
+      [ V ++ W ] ([]ᵥ {B} ≑ []ᵥ)  ≡⟨ ≡.cong ([ V ++ W ]_) []ᵥ-≑ ⟩
+      [ V ++ W ] []ᵥ              ≡⟨ [-]-[]ᵥ (V ++ W) ⟩
+      ⟨⟩ ⊕ ⟨⟩                     ≡⟨ ≡.cong₂ _⊕_ ([-]-[]ᵥ V) ([-]-[]ᵥ W) ⟨
+      [ V ] []ᵥ ⊕ [ W ] []ᵥ       ∎
+    where
+      open ≈-Reasoning (Vectorₛ 0)
+  [++]-≑ {B} {C} {suc A} V W M N
+    rewrite ≡.sym (head-∷-tailₕ M)
+    rewrite ≡.sym (head-∷-tailₕ N)
+    using M₀ ← headₕ M
+    using M ← tailₕ M
+    using N₀ ← headₕ N
+    using N ← tailₕ N = begin
+      [ V ++ W ] ((M₀ ∷ₕ M) ≑ (N₀ ∷ₕ N))            ≡⟨ ≡.cong ([ V ++ W ]_) (∷ₕ-≑ M₀ N₀ M N) ⟨
+      [ V ++ W ] ((M₀ ++ N₀) ∷ₕ (M ≑ N))            ≡⟨ ≡.cong (map ((V ++ W) ∙_)) (∷ₕ-ᵀ (M₀ ++ N₀) (M ≑ N)) ⟩
+      (V ++ W) ∙ (M₀ ++ N₀) ∷ ([ V ++ W ] (M ≑ N))  ≈⟨ ∙-++ V M₀ W N₀ PW.∷ [++]-≑ V W M N ⟩
+      (V ∙ M₀ ∷ [ V ] M) ⊕ (W ∙ N₀ ∷ [ W ] N)       ≡⟨ ≡.cong₂ (λ h₁ h₂ → map (V ∙_) h₁ ⊕ map (W ∙_) h₂) (∷ₕ-ᵀ M₀ M) (∷ₕ-ᵀ N₀ N) ⟨
+      ([ V ] (M₀ ∷ₕ M)) ⊕ ([ W ] (N₀ ∷ₕ N))         ∎
+    where
+      open ≈-Reasoning (Vectorₛ (suc A))
+opaque
+
+  unfolding []ₕ []ᵥ [_]_ ⟨0⟩ _∙_ _ᵀ
+
+  [⟨⟩]-[]ₕ : [ ⟨⟩ ] ([]ₕ {A}) ≡ ⟨0⟩ {A}
+  [⟨⟩]-[]ₕ {zero} = ≡.refl
+  [⟨⟩]-[]ₕ {suc A} = ≡.cong (0# ∷_) [⟨⟩]-[]ₕ
+
+opaque
+
+  unfolding Vector ⟨⟩ ⟨0⟩ []ᵥ [_]_ _ᵀ _∷ₕ_ 𝟎 _≊_
+
+  [-]-𝟎 : (V : Vector A) →  [ V ] (𝟎 {B}) ≊ ⟨0⟩
+  [-]-𝟎 {A} {zero} V = ≊.reflexive (≡.cong (map (V ∙_)) 𝟎ᵀ)
+  [-]-𝟎 {A} {suc B} V = begin
+      map (V ∙_) (𝟎 ᵀ)        ≡⟨ ≡.cong (map (V ∙_)) 𝟎ᵀ ⟩
+      V ∙ ⟨0⟩ ∷ map (V ∙_) 𝟎  ≡⟨ ≡.cong ((V ∙ ⟨0⟩ ∷_) ∘ map (V ∙_)) 𝟎ᵀ ⟨
+      V ∙ ⟨0⟩ ∷ [ V ] 𝟎       ≈⟨ ∙-zeroʳ V PW.∷ ([-]-𝟎 V) ⟩
+      0# ∷ ⟨0⟩                ∎
+    where
+      open ≈-Reasoning (Vectorₛ (suc B))
+
+opaque
+
+  unfolding ⟨0⟩ ⟨⟩ [_]_
+
+  [⟨0⟩]- : (M : Matrix A B) → [ ⟨0⟩ ] M ≊ ⟨0⟩
+  [⟨0⟩]- {zero} M rewrite []ᵥ-! M = ≊.reflexive ([-]-[]ᵥ ⟨0⟩)
+  [⟨0⟩]- {suc A} M
+    rewrite ≡.sym (head-∷-tailₕ M)
+    using M₀ ← headₕ M
+    using M ← tailₕ M = begin
+      [ ⟨0⟩ ] (M₀ ∷ₕ M)     ≡⟨ ≡.cong (map (⟨0⟩ ∙_)) (∷ₕ-ᵀ M₀ M) ⟩
+      ⟨0⟩ ∙ M₀ ∷ [ ⟨0⟩ ] M  ≈⟨ ∙-zeroˡ M₀ PW.∷ [⟨0⟩]- M ⟩
+      0# ∷ ⟨0⟩              ∎
+    where
+      open ≈-Reasoning (Vectorₛ _)
diff --git a/Data/Matrix/Vec.agda b/Data/Matrix/Vec.agda
new file mode 100644
index 0000000..e0312d4
--- /dev/null
+++ b/Data/Matrix/Vec.agda
@@ -0,0 +1,20 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Matrix.Vec where
+
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Level using (Level)
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec; replicate; zipWith)
+
+private
+  variable
+    a : Level
+    A : Set a
+    n m : ℕ
+
+open Vec
+
+transpose : Vec (Vec A n) m → Vec (Vec A m) n
+transpose [] = replicate _ []
+transpose (row ∷ mat) = zipWith _∷_ row (transpose mat)
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#                ∎
 
diff --git a/Data/Vector/Core.agda b/Data/Vector/Core.agda
index 974f672..a430f12 100644
--- a/Data/Vector/Core.agda
+++ b/Data/Vector/Core.agda
@@ -13,18 +13,18 @@ open import Categories.Category.Instance.Nat using (Natop)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor)
 open import Data.Fin using (Fin)
-open import Data.Nat using (ℕ)
+open import Data.Nat using (ℕ; _+_)
 open import Data.Setoid using (∣_∣)
-open import Data.Vec using (Vec; lookup; tabulate)
+open import Data.Vec as Vec using (Vec; lookup; tabulate)
 open import Data.Vec.Properties using (tabulate∘lookup; lookup∘tabulate; tabulate-cong)
 open import Data.Vec.Relation.Binary.Equality.Setoid S using (_≋_; ≋-isEquivalence)
 open import Function using (Func; _⟶ₛ_; id; _⟨$⟩_; _∘_)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
 
 open Func
 open Setoid S
-open Vec
 open Fin
+open Vec.Vec
 
 private
   variable
@@ -44,6 +44,18 @@ opaque
   ≊-isEquiv : IsEquivalence (_≊_ {n})
   ≊-isEquiv {n} = ≋-isEquivalence n
 
+  _++_ : Vector A → Vector B → Vector (A + B)
+  _++_ = Vec._++_
+
+  ⟨⟩ : Vector 0
+  ⟨⟩ = []
+
+  ⟨⟩-! : (V : Vector 0) → V ≡ ⟨⟩
+  ⟨⟩-! [] = ≡.refl
+
+  ⟨⟩-++ : (V : Vector A) → ⟨⟩ ++ V ≡ V
+  ⟨⟩-++ V = ≡.refl
+
 -- A setoid of vectors for every natural number
 Vectorₛ : ℕ → Setoid c (c ⊔ ℓ)
 Vectorₛ n = record
diff --git a/Data/Vector/Vec.agda b/Data/Vector/Vec.agda
index ae87737..868571a 100644
--- a/Data/Vector/Vec.agda
+++ b/Data/Vector/Vec.agda
@@ -3,8 +3,8 @@
 module Data.Vector.Vec where
 
 open import Data.Fin using (Fin)
-open import Data.Nat using (ℕ)
-open import Data.Vec using (Vec; tabulate; zipWith; replicate)
+open import Data.Nat using (ℕ; _+_)
+open import Data.Vec using (Vec; tabulate; zipWith; replicate; map; _++_)
 open import Function using (_∘_)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
@@ -13,10 +13,18 @@ open Vec
 open ℕ
 open Fin
 
+private
+  variable
+    a b c d e : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    D : Set d
+    E : Set e
+    n : ℕ
+
 zipWith-tabulate
-    : {a : Level}
-      {A : Set a}
-      {n : ℕ}
+    : {n : ℕ}
       (_⊕_ : A → A → A)
       (f g : Fin n → A)
     → zipWith _⊕_ (tabulate f) (tabulate g) ≡ tabulate (λ i → f i ⊕ g i)
@@ -24,10 +32,42 @@ zipWith-tabulate {n = zero} _⊕_ f g = ≡.refl
 zipWith-tabulate {n = suc n} _⊕_ f g = ≡.cong (f zero ⊕ g zero ∷_) (zipWith-tabulate _⊕_ (f ∘ suc) (g ∘ suc))
 
 replicate-tabulate
-    : {a : Level}
-      {A : Set a}
-      {n : ℕ}
+    : {n : ℕ}
       (x : A)
     → replicate n x ≡ tabulate (λ _ → x)
 replicate-tabulate {n = zero} x = ≡.refl
 replicate-tabulate {n = suc n} x = ≡.cong (x ∷_) (replicate-tabulate x)
+
+zipWith-map
+    : {n : ℕ}
+      (f : A → B)
+      (g : A → C)
+      (_⊕_ : B → C → D)
+      (v : Vec A n)
+    → zipWith _⊕_ (map f v) (map g v) ≡ map (λ x → f x ⊕ g x) v
+zipWith-map f g _⊕_ [] = ≡.refl
+zipWith-map f g _⊕_ (x ∷ v) = ≡.cong (f x ⊕ g x ∷_) (zipWith-map f g _⊕_ v)
+
+replicate-++ : (n m : ℕ) (x : A) → replicate n x ++ replicate m x ≡ replicate (n + m) x
+replicate-++ zero _ x = ≡.refl
+replicate-++ (suc n) m x = ≡.cong (x ∷_) (replicate-++ n m x)
+
+map-zipWith
+    : (f : C → D)
+      (_⊕_ : A → B → C)
+      {n : ℕ}
+      (v : Vec A n)
+      (w : Vec B n)
+    → map f (zipWith _⊕_ v w) ≡ zipWith (λ x y → f (x ⊕ y)) v w
+map-zipWith f _⊕_ [] [] = ≡.refl
+map-zipWith f _⊕_ (x ∷ v) (y ∷ w) = ≡.cong (f (x ⊕ y) ∷_) (map-zipWith f _⊕_ v w)
+
+zipWith-map-map
+    : (f : A → C)
+      (g : B → D)
+      (_⊕_ : C → D → E)
+      (v : Vec A n)
+      (w : Vec B n)
+    → zipWith (λ x y → f x ⊕ g y) v w ≡ zipWith _⊕_ (map f v) (map g w)
+zipWith-map-map f g _⊕_ [] [] = ≡.refl
+zipWith-map-map f g _⊕_ (x ∷ v) (y ∷ w) = ≡.cong (f x ⊕ g y ∷_) (zipWith-map-map f g _⊕_ v w)