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/Vector/Monoid.agda | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'Data/Vector')

diff --git a/Data/Vector/Monoid.agda b/Data/Vector/Monoid.agda
index da09de9..7205800 100644
--- a/Data/Vector/Monoid.agda
+++ b/Data/Vector/Monoid.agda
@@ -12,15 +12,17 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 open import Data.Nat using (ℕ)
 open import Data.Product using (_,_)
-open import Data.Vec using (Vec; foldr′; zipWith; replicate)
+open import Data.Vec using (Vec; foldr′; zipWith; replicate; _++_)
 open import Data.Vector.Core M.setoid as S using (Vector; _≊_; module ≊; pull; Vectorₛ)
+open import Data.Vector.Vec using (replicate-++)
+open import Relation.Binary.PropositionalEquality using (_≡_)
 
 open M
 open Vec
 
 private
   variable
-    n A B C : ℕ
+    n m A B C : ℕ
 
 opaque
 
@@ -54,6 +56,9 @@ opaque
   ⟨ε⟩ : Vector n
   ⟨ε⟩ {n} = replicate n ε
 
+  ⟨ε⟩-++ : ⟨ε⟩ {n} ++ ⟨ε⟩ {m} ≡ ⟨ε⟩
+  ⟨ε⟩-++ {n} {m} = replicate-++ n m ε
+
 opaque
 
   unfolding _⊕_ ⟨ε⟩
@@ -95,9 +100,9 @@ open import Categories.Object.Monoid Setoids-×.monoidal as Obj using (Monoid⇒
 open import Data.Fin using (Fin)
 open import Data.Monoid using (module FromMonoid)
 open import Data.Monoid {c} {c ⊔ ℓ} using (fromMonoid)
-open import Data.Vec using (tabulate; lookup)
+open import Data.Vec using (tabulate; lookup; _++_)
 open import Data.Vec.Properties using (tabulate-cong; lookup-zipWith; lookup-replicate)
-open import Data.Vector.Vec using (zipWith-tabulate; replicate-tabulate)
+open import Data.Vector.Vec using (zipWith-tabulate; replicate-tabulate; replicate-++)
 open import Function using (Func; _⟨$⟩_; _∘_; id)
 open import Relation.Binary.PropositionalEquality as ≡ using (module ≡-Reasoning; _≡_; _≗_)
 
-- 
cgit v1.2.3