From 1e73f2658f6d8d1559649b2cd97040f494dc1c96 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 5 Aug 2026 17:50:02 -0500 Subject: Show matrix change of base functor is cartesian --- Data/Matrix/BaseChange.agda | 84 ++++++++++- Data/Matrix/Semiadditive.agda | 278 ++++++++++++++++++++++++++++++++++++ Data/Matrix/SemiadditiveDagger.agda | 228 +---------------------------- 3 files changed, 361 insertions(+), 229 deletions(-) create mode 100644 Data/Matrix/Semiadditive.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 + } 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 ᵀ -- cgit v1.2.3