From 1e73f2658f6d8d1559649b2cd97040f494dc1c96 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 5 Aug 2026 17:50:02 -0500
Subject: Show matrix change of base functor is cartesian

---
 Data/Matrix/BaseChange.agda | 84 ++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 80 insertions(+), 4 deletions(-)

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

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ᵀ ⟨
@@ -109,6 +114,16 @@ opaque
         where
           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
@@ -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
+    }
-- 
cgit v1.2.3