diff options
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 |