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/Semiadditive.agda | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

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

diff --git a/Data/Matrix/Semiadditive.agda b/Data/Matrix/Semiadditive.agda
index c6926b0..f91dfd7 100644
--- a/Data/Matrix/Semiadditive.agda
+++ b/Data/Matrix/Semiadditive.agda
@@ -269,10 +269,14 @@ Mat-Semiadditive = record
         }
     }
 
-open Semiadditive Mat-Semiadditive using (cartesian)
+open Semiadditive Mat-Semiadditive
+  using ()
+  renaming (cartesian to Mat-Cartesian) public
 
 Mat-CC : CartesianCategory 0ℓ c (c ⊔ ℓ)
 Mat-CC = record
     { U = Mat
-    ; cartesian = cartesian
+    ; cartesian = Mat-Cartesian
     }
+
+module Mat-CC = CartesianCategory Mat-CC
-- 
cgit v1.2.3