Show matrix change of base functor is cartesianmain

3 files changed, 361 insertions, 229 deletions

diff --git a/Data/Matrix/BaseChange.agda b/Data/Matrix/BaseChange.agda
index 4791efa..2135c13 100644
--- a/Data/Matrix/BaseChange.agda
+++ b/Data/Matrix/BaseChange.agda
@@ -18,6 +18,7 @@ import Data.Matrix.Core as MC
 import Data.Matrix.Endofunctor as Endo
 import Data.Matrix.Monoid as MM
 import Data.Matrix.Raw as MR
+import Data.Matrix.Semiadditive as MS
 import Data.Matrix.Transform as MT
 import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
 import Data.Vector.Bisemimodule as VB
@@ -25,14 +26,14 @@ import Data.Vector.Core as VC
 import Data.Vector.Endofunctor.Monoid as MonEndo
 import Data.Vector.Endofunctor.Setoid as VecEndo
 import Data.Vector.Monoid as VM
-import Relation.Binary.PropositionalEquality as ≡
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 open import Categories.Functor using (Functor)
 open import Category.Instance.Monoids using (MonoidHomomorphism; mk-⇒)
 open import Data.Matrix.Category using (Mat)
+open import Data.Matrix.Semiadditive using (Mat-CC)
 open import Data.Matrix.Transform using (I)
-open import Data.Nat using (ℕ)
+open import Data.Nat using (ℕ; _+_)
 open import Data.Vec using (map; []; _∷_; zipWith; replicate)
 open import Data.Vec.Properties using (map-∘; map-replicate)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺)
@@ -42,6 +43,7 @@ open import Data.Vector.Monoid using (⟨ε⟩)
 open import Data.Vector.Raw using (module Relation)
 open import Function using (id; Func; _⟶ₛ_; _⟨$⟩_; _∘_)
 open import Level using (0ℓ)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 
 open Func
 open Functor
@@ -56,12 +58,14 @@ module MatR where
   open MC R.setoid public
   open MM R.+-monoid public
   open MT R public
+  open MS R public using (Mat-CC; proj₁; proj₂)
   open MCat R using (_·_) public
 
 module MatS where
   open MC S.setoid public
   open MM S.+-monoid public
   open MT S public
+  open MS S public using (Mat-CC; isTerminal; isProduct)
   open MCat S using (_·_) public
 
 module VecR where
@@ -87,14 +91,15 @@ resp
     → change M MatS.≋ change M′
 resp = cong (Mat.₁ func)
 
+⟨ε⟩-homo : {A : ℕ} → (map ⟦_⟧) VecR.⟨ε⟩ ≊ VecS.⟨ε⟩ {A}
+⟨ε⟩-homo {A} = MonoidHomomorphism.ε-homo (MonEndo.mapₘ A (mk-⇒ +-monoidHomomorphism))
+
 opaque
   unfolding I _ᵀ _∷ₕ_ Endo.mapₛ
   ident : {A : ℕ} → change (I R) MatS.≋ I S {A}
   ident {zero} = PW.[]
   ident {suc A} = (1#-homo PW.∷ ⟨ε⟩-homo) PW.∷ map-⟨ε⟩∷ₕI
     where
-      ⟨ε⟩-homo : (map ⟦_⟧) VecR.⟨ε⟩ ≊ VecS.⟨ε⟩ {A}
-      ⟨ε⟩-homo = MonoidHomomorphism.ε-homo (MonEndo.mapₘ A (mk-⇒ +-monoidHomomorphism))
       map-⟨ε⟩∷ₕI : map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ MatR.I) MatS.≋ VecS.⟨ε⟩ ∷ₕ MatS.I {A}
       map-⟨ε⟩∷ₕI = begin
           map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ MatR.I)            ≡⟨ ≡.cong (λ h → map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ h)) MatR.Iᵀ ⟨
@@ -110,6 +115,16 @@ opaque
           open ≈-Reasoning (MatS.Matrixₛ (suc A) A)
 
 opaque
+  unfolding MatS.𝟎 Endo.mapₛ
+  change-𝟎 : {A B : ℕ} → change MatR.𝟎 MatS.≋ MatS.𝟎 {A} {B}
+  change-𝟎 {A} {B} = begin
+      map (map ⟦_⟧) (replicate B VecR.⟨ε⟩)  ≡⟨ map-replicate (map ⟦_⟧) VecR.⟨ε⟩ B ⟩
+      replicate B (map (to func) VecR.⟨ε⟩)  ≈⟨ Relation.R-replicate ⟨ε⟩-homo ⟩
+      replicate B VecS.⟨ε⟩                  ∎
+    where
+      open ≈-Reasoning (MatS.Matrixₛ A B)
+
+opaque
   unfolding VecR._∙_
   ⟦⟧-∙ : {n : ℕ} (V W : VecR.Vector n) → ⟦ V VecR.∙ W ⟧ S.≈ map ⟦_⟧ V VecS.∙ map ⟦_⟧ W
   ⟦⟧-∙ {zero} [] [] = 0#-homo
@@ -164,3 +179,64 @@ ChangeBase = record
     ; homomorphism = homo
     ; F-resp-≈ = resp
     }
+
+open import Categories.Functor.Cartesian using (IsCartesianF; CartesianF)
+
+open import Categories.Object.Product using (IsProduct)
+
+open import Categories.Category using (Category)
+module _ {o ℓ e : Level} {𝒞 : Category o ℓ e} where
+
+  open Category 𝒞
+  open HomReasoning
+  open Equiv
+
+  IsProduct-cong
+      : {P A B : Obj} {f f′ : P ⇒ A} {g g′ : P ⇒ B}
+      → f ≈ f′
+      → g ≈ g′
+      → IsProduct 𝒞 f g
+      → IsProduct 𝒞 f′ g′
+  IsProduct-cong ≈f ≈g isProduct = let open IsProduct 𝒞 isProduct in record
+      { ⟨_,_⟩ = ⟨_,_⟩
+      ; project₁ = sym ≈f ⟩∘⟨refl ○ project₁
+      ; project₂ = sym ≈g ⟩∘⟨refl ○ project₂
+      ; unique = λ eq₁ eq₂ → unique (≈f ⟩∘⟨refl ○ eq₁) (≈g ⟩∘⟨refl ○ eq₂)
+      }
+
+opaque
+  unfolding Endo.mapₛ
+  change-∥ : {A B C : ℕ} {M : Matrix R.setoid A C} {N : Matrix R.setoid B C} → change (M ∥ N) ≡ change M ∥ change N
+  change-∥ {M = M} {N} = Natural.α-∥ ⟦_⟧ M N
+
+ChangeBase-resp-×
+    : {A B : ℕ}
+    → IsProduct (Mat S) (change (MatR.I {A} ∥ MatR.𝟎)) (change (MatR.𝟎 ∥ MatR.I {B}))
+ChangeBase-resp-× {A} {B} = IsProduct-cong eq₁ eq₂ MatS.isProduct
+  where
+    eq₁ : MatS.I ∥ MatS.𝟎 MatS.≋ change (MatR.I ∥ MatR.𝟎)
+    eq₁ = begin
+        MatS.I ∥ MatS.𝟎               ≈⟨ MatS.∥-cong ident change-𝟎 ⟨
+        change MatR.I ∥ change MatR.𝟎 ≡⟨ change-∥ ⟨
+        change (MatR.I ∥ MatR.𝟎)      ∎
+      where
+        open ≈-Reasoning (MatS.Matrixₛ (A + B) A)
+    eq₂ : MatS.𝟎 ∥ MatS.I MatS.≋ change (MatR.𝟎 ∥ MatR.I)
+    eq₂ = begin
+        MatS.𝟎 ∥ MatS.I               ≈⟨ MatS.∥-cong change-𝟎 ident ⟨
+        change MatR.𝟎 ∥ change MatR.I ≡⟨ change-∥ ⟨
+        change (MatR.𝟎 ∥ MatR.I)      ∎
+      where
+        open ≈-Reasoning (MatS.Matrixₛ (A + B) B)
+
+ChangeBase-IsCF : IsCartesianF (Mat-CC R) (Mat-CC S) ChangeBase
+ChangeBase-IsCF = record
+    { F-resp-⊤ = MatS.isTerminal
+    ; F-resp-× = ChangeBase-resp-×
+    }
+
+ChangeBase-CF : CartesianF (Mat-CC R) (Mat-CC S)
+ChangeBase-CF = record
+    { F = ChangeBase
+    ; isCartesian = ChangeBase-IsCF
+    }
diff --git a/Data/Matrix/Semiadditive.agda b/Data/Matrix/Semiadditive.agda
new file mode 100644
index 0000000..c6926b0
--- /dev/null
+++ b/Data/Matrix/Semiadditive.agda
@@ -0,0 +1,278 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (Semiring)
+open import Level using (Level; 0ℓ; _⊔_)
+
+module Data.Matrix.Semiadditive {c ℓ : Level} (R : Semiring c ℓ) where
+
+module R = Semiring R
+
+import Data.Nat as ℕ
+import Data.Nat.Properties as ℕ-Props
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Object.Biproduct using (Biproduct)
+open import Categories.Object.Coproduct using (IsCoproduct)
+open import Categories.Object.Initial using (IsInitial)
+open import Categories.Object.Product using (IsProduct)
+open import Categories.Object.Terminal using (IsTerminal)
+open import Categories.Object.Zero using (Zero)
+open import Category.Semiadditive using (Semiadditive)
+open import Data.Matrix.Category R using (Mat; _·_; ≑-·; ·-Iˡ; ·-Iʳ; ·-𝟎ˡ; ·-𝟎ʳ; ·-∥; ∥-·-≑; ·-resp-≋; ·-assoc)
+open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; module ≋; ∥-cong; ≑-cong; ᵀ-cong)
+open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; 𝟎≑𝟎; 𝟎∥𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ)
+open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; mapRows; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!)
+open import Data.Matrix.Transform R using (I; Iᵀ; [_]_; _[_]; -[-]ᵀ; [-]--cong; [-]-[]ᵥ; [⟨⟩]-[]ₕ)
+open import Data.Nat using (ℕ)
+open import Data.Product using (_,_; Σ-syntax)
+open import Data.Vec using (Vec; map; replicate; _++_)
+open import Data.Vec.Properties using (map-cong; map-const)
+open import Data.Vector.Bisemimodule R using (_∙_ ; ∙-cong)
+open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; module ≊; _≊_)
+open import Data.Vector.Monoid R.+-monoid using () renaming (⟨ε⟩ to ⟨0⟩)
+open import Data.Vector.Raw using (⟨⟩)
+open import Data.Vector.Vec using (replicate-++)
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
+
+open R
+open Vec
+open ℕ.ℕ
+
+private
+  variable
+    A B C D E F : ℕ
+
+inj₁ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (I ≑ 𝟎) ≋ M
+inj₁ {A} {C} M N = begin
+    (M ∥ N) · (I ≑ 𝟎)   ≈⟨ ∥-·-≑ M N I 𝟎 ⟩
+    (M · I) [+] (N · 𝟎) ≈⟨ [+]-cong ·-Iʳ (·-𝟎ʳ N) ⟩
+    M [+] 𝟎             ≈⟨ [+]-𝟎ʳ M ⟩
+    M ∎
+  where
+    open ≈-Reasoning (Matrixₛ A C)
+
+inj₂ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (𝟎 ≑ I) ≋ N
+inj₂ {A} {C} {B} M N = begin
+    (M ∥ N) · (𝟎 ≑ I)   ≈⟨ ∥-·-≑ M N 𝟎 I ⟩
+    (M · 𝟎) [+] (N · I) ≈⟨ [+]-cong (·-𝟎ʳ M) ·-Iʳ ⟩
+    𝟎 [+] N             ≈⟨ [+]-𝟎ˡ N ⟩
+    N ∎
+  where
+    open ≈-Reasoning (Matrixₛ B C)
+
+opaque
+
+  unfolding Matrix _∷ᵥ_
+
+  split-∥ : (A : ℕ) (M : Matrix (A ℕ.+ B) C) → Σ[ M₁ ∈ Matrix A C ] Σ[ M₂ ∈ Matrix B C ] M₁ ∥ M₂ ≡ M
+  split-∥ zero M = []ᵥ , M , []ᵥ-∥ M
+  split-∥ (suc A) M′
+    rewrite ≡.sym (head-∷-tailₕ M′)
+    using M₀ ← headₕ M′
+    using M ← tailₕ M′
+    with split-∥ A M
+  ... | M₁ , M₂ , M₁∥M₂≡M = M₀ ∷ₕ M₁ , M₂ , (begin
+      (M₀ ∷ₕ M₁) ∥ M₂ ≡⟨ ∷ₕ-∥ M₀ M₁ M₂ ⟨
+      M₀ ∷ₕ M₁ ∥ M₂   ≡⟨ ≡.cong (M₀ ∷ₕ_) M₁∥M₂≡M ⟩
+      M₀ ∷ₕ M ∎)
+    where
+      open ≡-Reasoning
+
+  split-≑ : (B : ℕ) (M : Matrix A (B ℕ.+ C)) → Σ[ M₁ ∈ Matrix A B ] Σ[ M₂ ∈ Matrix A C ] M₁ ≑ M₂ ≡ M
+  split-≑ zero M = []ₕ , M , []ₕ-≑ M
+  split-≑ (suc B) (M₀ ∷ M) with split-≑ B M
+  ... | M₁ , M₂ , M₁≑M₂≡M = M₀ ∷ᵥ M₁ , M₂ , (begin
+      (M₀ ∷ᵥ M₁) ≑ M₂ ≡⟨ ∷ᵥ-≑ M₀ M₁ M₂ ⟨
+      M₀ ∷ᵥ M₁ ≑ M₂   ≡⟨ ≡.cong (M₀ ∷ᵥ_) M₁≑M₂≡M ⟩
+      M₀ ∷ᵥ M ∎)
+    where
+      open ≡-Reasoning
+
+∥-uniq
+    : (H : Matrix (A ℕ.+ B) C)
+      (M : Matrix A C)
+      (N : Matrix B C)
+    → H · (I ≑ 𝟎) ≋ M
+    → H · (𝟎 ≑ I) ≋ N
+    → M ∥ N ≋ H
+∥-uniq {A} {B} {C} H M N eq₁ eq₂
+  with (H₁ , H₂ , H₁∥H₂≡H) ← split-∥ A H
+  rewrite ≡.sym H₁∥H₂≡H = begin
+    M ∥ N                                         ≈⟨ ∥-cong eq₁ eq₂ ⟨
+    (H₁ ∥ H₂) · (I {A} ≑ 𝟎) ∥ (H₁ ∥ H₂) · (𝟎 ≑ I) ≈⟨ ∥-cong (inj₁ H₁ H₂) (inj₂ H₁ H₂) ⟩
+    (H₁ ∥ H₂) ∎
+  where
+    open ≈-Reasoning (Matrixₛ (A ℕ.+ B) C)
+
+proj₁ : (M : Matrix A B) (N : Matrix A C) → (I ∥ 𝟎) · (M ≑ N) ≋ M
+proj₁ {A} {B} M N = begin
+    (I ∥ 𝟎) · (M ≑ N)   ≈⟨ ∥-·-≑ I 𝟎 M N ⟩
+    (I · M) [+] (𝟎 · N) ≈⟨ [+]-cong ·-Iˡ (·-𝟎ˡ N) ⟩
+    M [+] 𝟎             ≈⟨ [+]-𝟎ʳ M ⟩
+    M ∎
+  where
+    open ≈-Reasoning (Matrixₛ A B)
+
+proj₂ : (M : Matrix A B) (N : Matrix A C) → (𝟎 ∥ I) · (M ≑ N) ≋ N
+proj₂ {A} {_} {C} M N = begin
+    (𝟎 ∥ I) · (M ≑ N)   ≈⟨ ∥-·-≑ 𝟎 I M N ⟩
+    (𝟎 · M) [+] (I · N) ≈⟨ [+]-cong (·-𝟎ˡ M) ·-Iˡ ⟩
+    𝟎 [+] N             ≈⟨ [+]-𝟎ˡ N ⟩
+    N ∎
+  where
+    open ≈-Reasoning (Matrixₛ A C)
+
+≑-uniq
+    : (H : Matrix A (B ℕ.+ C))
+      (M : Matrix A B)
+      (N : Matrix A C)
+    → (I ∥ 𝟎) · H ≋ M
+    → (𝟎 ∥ I) · H ≋ N
+    → M ≑ N ≋ H
+≑-uniq {A} {B} {C} H M N eq₁ eq₂
+  with (H₁ , H₂ , H₁≑H₂≡H) ← split-≑ B H
+  rewrite ≡.sym H₁≑H₂≡H = begin
+      M ≑ N                                         ≈⟨ ≑-cong eq₁ eq₂ ⟨
+      (I {B} ∥ 𝟎) · (H₁ ≑ H₂) ≑ (𝟎 ∥ I) · (H₁ ≑ H₂) ≈⟨ ≑-cong (proj₁ H₁ H₂) (proj₂ H₁ H₂) ⟩
+      H₁ ≑ H₂                                       ∎
+  where
+    open ≈-Reasoning (Matrixₛ A (B ℕ.+ C))
+
+isCoproduct : IsCoproduct Mat (I {A} ≑ 𝟎) (𝟎 ≑ I {B})
+isCoproduct {A} {B} = record
+    { [_,_] = _∥_
+    ; inject₁ = λ {a} {b} {c} → inj₁ b c
+    ; inject₂ = λ {a} {b} {c} → inj₂ b c
+    ; unique = λ eq₁ eq₂ → ∥-uniq _ _ _ eq₁ eq₂
+    }
+
+isProduct : IsProduct Mat (I {A} ∥ 𝟎) (𝟎 ∥ I {B})
+isProduct {A} {B} = record
+    { ⟨_,_⟩ = _≑_
+    ; project₁ = λ {a} {b} {c} → proj₁ b c
+    ; project₂ = λ {a} {b} {c} → proj₂ b c
+    ; unique = λ eq₁ eq₂ → ≑-uniq _ _ _ eq₁ eq₂
+    }
+
+opaque
+
+  unfolding Matrix
+
+  π₁∘i₁ : (I {A} ∥ 𝟎 {B}) · (I ≑ 𝟎) ≋ I
+  π₁∘i₁ {A} = begin
+      (I ∥ 𝟎) · (I ≑ 𝟎)   ≈⟨ ∥-·-≑ I 𝟎 I 𝟎 ⟩
+      (I · I) [+] (𝟎 · 𝟎) ≈⟨ [+]-cong ·-Iˡ (·-𝟎ˡ 𝟎) ⟩
+      I [+] 𝟎             ≈⟨ [+]-𝟎ʳ I ⟩
+      I                   ∎
+    where
+      open ≈-Reasoning (Matrixₛ A A)
+
+  π₂∘i₂ : (𝟎 {A} {B} ∥ I) · (𝟎 ≑ I) ≋ I
+  π₂∘i₂ {A} {B} = begin
+      (𝟎 ∥ I) · (𝟎 ≑ I)   ≈⟨ ∥-·-≑ 𝟎 I 𝟎 I ⟩
+      (𝟎 · 𝟎) [+] (I · I) ≈⟨ [+]-cong (·-𝟎ˡ 𝟎) ·-Iˡ  ⟩
+      𝟎 [+] I             ≈⟨ [+]-𝟎ˡ I ⟩
+      I                   ∎
+    where
+      open ≈-Reasoning (Matrixₛ B B)
+
+  π₁∘i₂ : (I {A} ∥ 𝟎 {B}) · (𝟎 ≑ I) ≋ 𝟎 {B} {A}
+  π₁∘i₂ {A} {B} = begin
+      (I ∥ 𝟎) · (𝟎 ≑ I)   ≈⟨ ∥-·-≑ I 𝟎 𝟎 I ⟩
+      (I · 𝟎) [+] (𝟎 · I) ≈⟨ [+]-cong (·-𝟎ʳ I) (·-𝟎ˡ I) ⟩
+      𝟎 [+] 𝟎             ≈⟨ [+]-𝟎ʳ 𝟎 ⟩
+      𝟎                   ∎
+    where
+      open ≈-Reasoning (Matrixₛ B A)
+
+  π₂∘i₁ : (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎) ≋ 𝟎 {A} {B}
+  π₂∘i₁ {A} {B} = begin
+      (𝟎 ∥ I) · (I ≑ 𝟎)   ≈⟨ ∥-·-≑ 𝟎 I I 𝟎 ⟩
+      (𝟎 · I) [+] (I · 𝟎) ≈⟨ [+]-cong (·-𝟎ˡ I) (·-𝟎ʳ I) ⟩
+      𝟎 [+] 𝟎             ≈⟨ [+]-𝟎ʳ 𝟎 ⟩
+      𝟎                   ∎
+    where
+      open ≈-Reasoning (Matrixₛ A B)
+
+  permute
+      : (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I)
+      ≋ (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎 {B} {A})
+  permute {A} {B} = begin
+      (I ≑ 𝟎) · (I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I)   ≈⟨ ·-resp-≋ ≋.refl ·-assoc ⟨
+      (I ≑ 𝟎) · ((I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I)) · (𝟎 {A} {B} ∥ I) ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ π₁∘i₂ ≋.refl) ⟩
+      (I ≑ 𝟎) · 𝟎 {B} {A} · (𝟎 {A} {B} ∥ I)                           ≈⟨ ·-resp-≋ ≋.refl (·-𝟎ˡ (𝟎 ∥ I)) ⟩
+      (I ≑ 𝟎 {A} {B}) · 𝟎                                             ≈⟨ ·-𝟎ʳ (I ≑ 𝟎) ⟩
+      𝟎                                                               ≈⟨ ·-𝟎ʳ (𝟎 ≑ I) ⟨
+      (𝟎 {B} {A} ≑ I) · 𝟎                                             ≈⟨ ·-resp-≋ ≋.refl (·-𝟎ˡ (I ∥ 𝟎)) ⟨
+      (𝟎 ≑ I) · 𝟎 {A} {B} · (I ∥ 𝟎 {B} {A})                           ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ π₂∘i₁ ≋.refl) ⟨
+      (𝟎 {B} {A} ≑ I) · ((𝟎 ∥ I) · (I ≑ 𝟎 {A} {B})) · (I ∥ 𝟎 {B} {A}) ≈⟨ ·-resp-≋ ≋.refl ·-assoc ⟩
+      (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎)   ∎
+    where
+      open ≈-Reasoning (Matrixₛ (A ℕ.+ B) (A ℕ.+ B))
+
+biproduct : Biproduct Mat A B
+biproduct {A} {B} = record
+    { A⊕B = A ℕ.+ B
+    ; π₁ = I ∥ 𝟎
+    ; π₂ = 𝟎 ∥ I
+    ; i₁ = I ≑ 𝟎
+    ; i₂ = 𝟎 ≑ I
+    ; isBiproduct = record
+        { isCoproduct = isCoproduct
+        ; isProduct = isProduct
+        ; π₁∘i₁≈id = π₁∘i₁
+        ; π₂∘i₂≈id = π₂∘i₂
+        ; permute = permute
+        }
+    }
+
+opaque
+
+  unfolding _≋_
+
+  ¡-unique : (E : Matrix 0 B) → []ᵥ ≋ E
+  ¡-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E))
+
+  !-unique : (E : Matrix A 0) → []ₕ ≋ E
+  !-unique E = ≋.reflexive (≡.sym ([]ₕ-! E))
+
+isInitial : IsInitial Mat 0
+isInitial = record
+    { ¡ = []ᵥ
+    ; ¡-unique = ¡-unique
+    }
+
+isTerminal : IsTerminal Mat 0
+isTerminal = record
+    { ! = []ₕ
+    ; !-unique = !-unique
+    }
+
+zeroObj : Zero Mat
+zeroObj = record
+    { 𝟘 = 0
+    ; isZero = record
+        { isInitial = isInitial
+        ; isTerminal = isTerminal
+        }
+    }
+
+Mat-Semiadditive : Semiadditive Mat
+Mat-Semiadditive = record
+    { zero = zeroObj
+    ; biproducts = record
+        { biproduct = biproduct
+        }
+    }
+
+open Semiadditive Mat-Semiadditive using (cartesian)
+
+Mat-CC : CartesianCategory 0ℓ c (c ⊔ ℓ)
+Mat-CC = record
+    { U = Mat
+    ; cartesian = cartesian
+    }
diff --git a/Data/Matrix/SemiadditiveDagger.agda b/Data/Matrix/SemiadditiveDagger.agda
index 3e13383..017f05f 100644
--- a/Data/Matrix/SemiadditiveDagger.agda
+++ b/Data/Matrix/SemiadditiveDagger.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Algebra.Bundles using (CommutativeSemiring)
-open import Level using (Level)
+open import Level using (Level; 0ℓ; _⊔_)
 
 module Data.Matrix.SemiadditiveDagger {c ℓ : Level} (R : CommutativeSemiring c ℓ) where
 
@@ -12,6 +12,7 @@ import Data.Nat.Properties as ℕ-Props
 import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
 open import Categories.Category.Cocartesian using (Cocartesian)
 open import Categories.Category.Dagger using (HasDagger)
 open import Categories.Object.Biproduct using (Biproduct)
@@ -26,6 +27,7 @@ open import Data.Matrix.Category R.semiring using (Mat; _·_; ≑-·; ·-Iˡ; ·
 open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; module ≋; ∥-cong; ≑-cong; ᵀ-cong)
 open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; 𝟎≑𝟎; 𝟎∥𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ)
 open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; mapRows; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!)
+open import Data.Matrix.Semiadditive R.semiring using (Mat-Semiadditive)
 open import Data.Matrix.Transform R.semiring using (I; Iᵀ; [_]_; _[_]; -[-]ᵀ; [-]--cong; [-]-[]ᵥ; [⟨⟩]-[]ₕ)
 open import Data.Nat using (ℕ)
 open import Data.Product using (_,_; Σ-syntax)
@@ -112,191 +114,6 @@ opaque
   where
     open ≡-Reasoning
 
-inj₁ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (I ≑ 𝟎) ≋ M
-inj₁ {A} {C} M N = begin
-    (M ∥ N) · (I ≑ 𝟎)   ≈⟨ ∥-·-≑ M N I 𝟎 ⟩
-    (M · I) [+] (N · 𝟎) ≈⟨ [+]-cong ·-Iʳ (·-𝟎ʳ N) ⟩
-    M [+] 𝟎             ≈⟨ [+]-𝟎ʳ M ⟩
-    M ∎
-  where
-    open ≈-Reasoning (Matrixₛ A C)
-
-inj₂ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) · (𝟎 ≑ I) ≋ N
-inj₂ {A} {C} {B} M N = begin
-    (M ∥ N) · (𝟎 ≑ I)   ≈⟨ ∥-·-≑ M N 𝟎 I ⟩
-    (M · 𝟎) [+] (N · I) ≈⟨ [+]-cong (·-𝟎ʳ M) ·-Iʳ ⟩
-    𝟎 [+] N             ≈⟨ [+]-𝟎ˡ N ⟩
-    N ∎
-  where
-    open ≈-Reasoning (Matrixₛ B C)
-
-opaque
-
-  unfolding Matrix _∷ᵥ_
-
-  split-∥ : (A : ℕ) (M : Matrix (A ℕ.+ B) C) → Σ[ M₁ ∈ Matrix A C ] Σ[ M₂ ∈ Matrix B C ] M₁ ∥ M₂ ≡ M
-  split-∥ zero M = []ᵥ , M , []ᵥ-∥ M
-  split-∥ (suc A) M′
-    rewrite ≡.sym (head-∷-tailₕ M′)
-    using M₀ ← headₕ M′
-    using M ← tailₕ M′
-    with split-∥ A M
-  ... | M₁ , M₂ , M₁∥M₂≡M = M₀ ∷ₕ M₁ , M₂ , (begin
-      (M₀ ∷ₕ M₁) ∥ M₂ ≡⟨ ∷ₕ-∥ M₀ M₁ M₂ ⟨
-      M₀ ∷ₕ M₁ ∥ M₂   ≡⟨ ≡.cong (M₀ ∷ₕ_) M₁∥M₂≡M ⟩
-      M₀ ∷ₕ M ∎)
-    where
-      open ≡-Reasoning
-
-  split-≑ : (B : ℕ) (M : Matrix A (B ℕ.+ C)) → Σ[ M₁ ∈ Matrix A B ] Σ[ M₂ ∈ Matrix A C ] M₁ ≑ M₂ ≡ M
-  split-≑ zero M = []ₕ , M , []ₕ-≑ M
-  split-≑ (suc B) (M₀ ∷ M) with split-≑ B M
-  ... | M₁ , M₂ , M₁≑M₂≡M = M₀ ∷ᵥ M₁ , M₂ , (begin
-      (M₀ ∷ᵥ M₁) ≑ M₂ ≡⟨ ∷ᵥ-≑ M₀ M₁ M₂ ⟨
-      M₀ ∷ᵥ M₁ ≑ M₂   ≡⟨ ≡.cong (M₀ ∷ᵥ_) M₁≑M₂≡M ⟩
-      M₀ ∷ᵥ M ∎)
-    where
-      open ≡-Reasoning
-
-∥-uniq
-    : (H : Matrix (A ℕ.+ B) C)
-      (M : Matrix A C)
-      (N : Matrix B C)
-    → H · (I ≑ 𝟎) ≋ M
-    → H · (𝟎 ≑ I) ≋ N
-    → M ∥ N ≋ H
-∥-uniq {A} {B} {C} H M N eq₁ eq₂
-  with (H₁ , H₂ , H₁∥H₂≡H) ← split-∥ A H
-  rewrite ≡.sym H₁∥H₂≡H = begin
-    M ∥ N                                         ≈⟨ ∥-cong eq₁ eq₂ ⟨
-    (H₁ ∥ H₂) · (I {A} ≑ 𝟎) ∥ (H₁ ∥ H₂) · (𝟎 ≑ I) ≈⟨ ∥-cong (inj₁ H₁ H₂) (inj₂ H₁ H₂) ⟩
-    (H₁ ∥ H₂) ∎
-  where
-    open ≈-Reasoning (Matrixₛ (A ℕ.+ B) C)
-
-proj₁ : (M : Matrix A B) (N : Matrix A C) → (I ∥ 𝟎) · (M ≑ N) ≋ M
-proj₁ {A} {B} M N = begin
-    (I ∥ 𝟎) · (M ≑ N)   ≈⟨ ∥-·-≑ I 𝟎 M N ⟩
-    (I · M) [+] (𝟎 · N) ≈⟨ [+]-cong ·-Iˡ (·-𝟎ˡ N) ⟩
-    M [+] 𝟎             ≈⟨ [+]-𝟎ʳ M ⟩
-    M ∎
-  where
-    open ≈-Reasoning (Matrixₛ A B)
-
-proj₂ : (M : Matrix A B) (N : Matrix A C) → (𝟎 ∥ I) · (M ≑ N) ≋ N
-proj₂ {A} {_} {C} M N = begin
-    (𝟎 ∥ I) · (M ≑ N)   ≈⟨ ∥-·-≑ 𝟎 I M N ⟩
-    (𝟎 · M) [+] (I · N) ≈⟨ [+]-cong (·-𝟎ˡ M) ·-Iˡ ⟩
-    𝟎 [+] N             ≈⟨ [+]-𝟎ˡ N ⟩
-    N ∎
-  where
-    open ≈-Reasoning (Matrixₛ A C)
-
-≑-uniq
-    : (H : Matrix A (B ℕ.+ C))
-      (M : Matrix A B)
-      (N : Matrix A C)
-    → (I ∥ 𝟎) · H ≋ M
-    → (𝟎 ∥ I) · H ≋ N
-    → M ≑ N ≋ H
-≑-uniq {A} {B} {C} H M N eq₁ eq₂
-  with (H₁ , H₂ , H₁≑H₂≡H) ← split-≑ B H
-  rewrite ≡.sym H₁≑H₂≡H = begin
-      M ≑ N                                         ≈⟨ ≑-cong eq₁ eq₂ ⟨
-      (I {B} ∥ 𝟎) · (H₁ ≑ H₂) ≑ (𝟎 ∥ I) · (H₁ ≑ H₂) ≈⟨ ≑-cong (proj₁ H₁ H₂) (proj₂ H₁ H₂) ⟩
-      H₁ ≑ H₂                                       ∎
-  where
-    open ≈-Reasoning (Matrixₛ A (B ℕ.+ C))
-
-
-isCoproduct : IsCoproduct Mat (I {A} ≑ 𝟎) (𝟎 ≑ I {B})
-isCoproduct {A} {B} = record
-    { [_,_] = _∥_
-    ; inject₁ = λ {a} {b} {c} → inj₁ b c
-    ; inject₂ = λ {a} {b} {c} → inj₂ b c
-    ; unique = λ eq₁ eq₂ → ∥-uniq _ _ _ eq₁ eq₂
-    }
-
-isProduct : IsProduct Mat (I {A} ∥ 𝟎) (𝟎 ∥ I {B})
-isProduct {A} {B} = record
-    { ⟨_,_⟩ = _≑_
-    ; project₁ = λ {a} {b} {c} → proj₁ b c
-    ; project₂ = λ {a} {b} {c} → proj₂ b c
-    ; unique = λ eq₁ eq₂ → ≑-uniq _ _ _ eq₁ eq₂
-    }
-
-opaque
-
-  unfolding Matrix
-
-  π₁∘i₁ : (I {A} ∥ 𝟎 {B}) · (I ≑ 𝟎) ≋ I
-  π₁∘i₁ {A} = begin
-      (I ∥ 𝟎) · (I ≑ 𝟎)   ≈⟨ ∥-·-≑ I 𝟎 I 𝟎 ⟩
-      (I · I) [+] (𝟎 · 𝟎) ≈⟨ [+]-cong ·-Iˡ (·-𝟎ˡ 𝟎) ⟩
-      I [+] 𝟎             ≈⟨ [+]-𝟎ʳ I ⟩
-      I                   ∎
-    where
-      open ≈-Reasoning (Matrixₛ A A)
-
-  π₂∘i₂ : (𝟎 {A} {B} ∥ I) · (𝟎 ≑ I) ≋ I
-  π₂∘i₂ {A} {B} = begin
-      (𝟎 ∥ I) · (𝟎 ≑ I)   ≈⟨ ∥-·-≑ 𝟎 I 𝟎 I ⟩
-      (𝟎 · 𝟎) [+] (I · I) ≈⟨ [+]-cong (·-𝟎ˡ 𝟎) ·-Iˡ  ⟩
-      𝟎 [+] I             ≈⟨ [+]-𝟎ˡ I ⟩
-      I                   ∎
-    where
-      open ≈-Reasoning (Matrixₛ B B)
-
-  π₁∘i₂ : (I {A} ∥ 𝟎 {B}) · (𝟎 ≑ I) ≋ 𝟎 {B} {A}
-  π₁∘i₂ {A} {B} = begin
-      (I ∥ 𝟎) · (𝟎 ≑ I)   ≈⟨ ∥-·-≑ I 𝟎 𝟎 I ⟩
-      (I · 𝟎) [+] (𝟎 · I) ≈⟨ [+]-cong (·-𝟎ʳ I) (·-𝟎ˡ I) ⟩
-      𝟎 [+] 𝟎             ≈⟨ [+]-𝟎ʳ 𝟎 ⟩
-      𝟎                   ∎
-    where
-      open ≈-Reasoning (Matrixₛ B A)
-
-  π₂∘i₁ : (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎) ≋ 𝟎 {A} {B}
-  π₂∘i₁ {A} {B} = begin
-      (𝟎 ∥ I) · (I ≑ 𝟎)   ≈⟨ ∥-·-≑ 𝟎 I I 𝟎 ⟩
-      (𝟎 · I) [+] (I · 𝟎) ≈⟨ [+]-cong (·-𝟎ˡ I) (·-𝟎ʳ I) ⟩
-      𝟎 [+] 𝟎             ≈⟨ [+]-𝟎ʳ 𝟎 ⟩
-      𝟎                   ∎
-    where
-      open ≈-Reasoning (Matrixₛ A B)
-
-  permute
-      : (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I)
-      ≋ (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎 {B} {A})
-  permute {A} {B} = begin
-      (I ≑ 𝟎) · (I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I)   ≈⟨ ·-resp-≋ ≋.refl ·-assoc ⟨
-      (I ≑ 𝟎) · ((I ∥ 𝟎 {B} {A}) · (𝟎 {B} {A} ≑ I)) · (𝟎 {A} {B} ∥ I) ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ π₁∘i₂ ≋.refl) ⟩
-      (I ≑ 𝟎) · 𝟎 {B} {A} · (𝟎 {A} {B} ∥ I)                           ≈⟨ ·-resp-≋ ≋.refl (·-𝟎ˡ (𝟎 ∥ I)) ⟩
-      (I ≑ 𝟎 {A} {B}) · 𝟎                                             ≈⟨ ·-𝟎ʳ (I ≑ 𝟎) ⟩
-      𝟎                                                               ≈⟨ ·-𝟎ʳ (𝟎 ≑ I) ⟨
-      (𝟎 {B} {A} ≑ I) · 𝟎                                             ≈⟨ ·-resp-≋ ≋.refl (·-𝟎ˡ (I ∥ 𝟎)) ⟨
-      (𝟎 ≑ I) · 𝟎 {A} {B} · (I ∥ 𝟎 {B} {A})                           ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ π₂∘i₁ ≋.refl) ⟨
-      (𝟎 {B} {A} ≑ I) · ((𝟎 ∥ I) · (I ≑ 𝟎 {A} {B})) · (I ∥ 𝟎 {B} {A}) ≈⟨ ·-resp-≋ ≋.refl ·-assoc ⟩
-      (𝟎 {B} {A} ≑ I) · (𝟎 {A} {B} ∥ I) · (I ≑ 𝟎 {A} {B}) · (I ∥ 𝟎)   ∎
-    where
-      open ≈-Reasoning (Matrixₛ (A ℕ.+ B) (A ℕ.+ B))
-
-biproduct : Biproduct Mat A B
-biproduct {A} {B} = record
-    { A⊕B = A ℕ.+ B
-    ; π₁ = I ∥ 𝟎
-    ; π₂ = 𝟎 ∥ I
-    ; i₁ = I ≑ 𝟎
-    ; i₂ = 𝟎 ≑ I
-    ; isBiproduct = record
-        { isCoproduct = isCoproduct
-        ; isProduct = isProduct
-        ; π₁∘i₁≈id = π₁∘i₁
-        ; π₂∘i₂≈id = π₂∘i₂
-        ; permute = permute
-        }
-    }
-
 [I∥𝟎]ᵀ : (I ∥ 𝟎 {B} {A}) ᵀ ≋ I ≑ 𝟎
 [I∥𝟎]ᵀ {B} {A} = begin
     (I ∥ 𝟎) ᵀ ≡⟨ ∥-ᵀ I 𝟎 ⟩
@@ -313,45 +130,6 @@ biproduct {A} {B} = record
   where
     open ≈-Reasoning (Matrixₛ B (A ℕ.+ B))
 
-opaque
-
-  unfolding _≋_
-
-  ¡-unique : (E : Matrix 0 B) → []ᵥ ≋ E
-  ¡-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E))
-
-  !-unique : (E : Matrix A 0) → []ₕ ≋ E
-  !-unique E = ≋.reflexive (≡.sym ([]ₕ-! E))
-
-isInitial : IsInitial Mat 0
-isInitial = record
-    { ¡ = []ᵥ
-    ; ¡-unique = ¡-unique
-    }
-
-isTerminal : IsTerminal Mat 0
-isTerminal = record
-    { ! = []ₕ
-    ; !-unique = !-unique
-    }
-
-zeroObj : Zero Mat
-zeroObj = record
-    { 𝟘 = 0
-    ; isZero = record
-        { isInitial = isInitial
-        ; isTerminal = isTerminal
-        }
-    }
-
-Mat-Semiadditive : Semiadditive Mat
-Mat-Semiadditive = record
-    { zero = zeroObj
-    ; biproducts = record
-        { biproduct = biproduct
-        }
-    }
-
 Mat-HasDagger : HasDagger Mat
 Mat-HasDagger = record
     { _† = λ M → M ᵀ