From 154ad08032f9719b0ad32aa357742fe12ff4899a Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 13 Aug 2026 00:57:08 -0500
Subject: Show free semimodule functor is cartesian

---
 Data/Matrix/Raw.agda | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'Data/Matrix/Raw.agda')

diff --git a/Data/Matrix/Raw.agda b/Data/Matrix/Raw.agda
index f2ad431..ecd5e9f 100644
--- a/Data/Matrix/Raw.agda
+++ b/Data/Matrix/Raw.agda
@@ -104,6 +104,9 @@ opaque
   ∷ₕ-≑ [] W [] N = ≡.refl
   ∷ₕ-≑ (x ∷ V) W (M₀ ∷ M) N = ≡.cong ((x ∷ M₀) ∷_) (∷ₕ-≑ V W M N)
 
+  ∷ᵥ-∥ : (V : Vec A n) (W : Vec A m) (M : Matrix A n p) (N : Matrix A m p) → (V ++ W) ∷ᵥ (M ∥ N) ≡ (V ∷ᵥ M) ∥ (W ∷ᵥ N)
+  ∷ᵥ-∥ {_} {A} {n} {m} {p} V W M N = ≡.refl
+
   headᵥ : Matrix A n (suc m) → Vec A n
   headᵥ = head
 
-- 
cgit v1.2.3