diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-13 00:57:08 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-13 00:57:08 -0500 |
| commit | 154ad08032f9719b0ad32aa357742fe12ff4899a (patch) | |
| tree | eca96e985fd493c93165b188c07f5b9af884babc /Data/Matrix/Semiadditive.agda | |
| parent | 1e73f2658f6d8d1559649b2cd97040f494dc1c96 (diff) | |
Show free semimodule functor is cartesian
Diffstat (limited to 'Data/Matrix/Semiadditive.agda')
| -rw-r--r-- | Data/Matrix/Semiadditive.agda | 8 |
1 files changed, 6 insertions, 2 deletions
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 |