diff options
Diffstat (limited to 'Data/Matrix/Semiadditive.agda')
| -rw-r--r-- | Data/Matrix/Semiadditive.agda | 108 |
1 files changed, 52 insertions, 56 deletions
diff --git a/Data/Matrix/Semiadditive.agda b/Data/Matrix/Semiadditive.agda index f91dfd7..babbdfa 100644 --- a/Data/Matrix/Semiadditive.agda +++ b/Data/Matrix/Semiadditive.agda @@ -24,7 +24,7 @@ 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.Raw using (_ᵀ; _ᵀᵀ; mapₕ; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; 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) @@ -66,7 +66,7 @@ inj₂ {A} {C} {B} M N = begin opaque - unfolding Matrix _∷ᵥ_ + unfolding _∷ᵥ_ split-∥ : (A : ℕ) (M : Matrix (A ℕ.+ B) C) → Σ[ M₁ ∈ Matrix A C ] Σ[ M₂ ∈ Matrix B C ] M₁ ∥ M₂ ≡ M split-∥ zero M = []ᵥ , M , []ᵥ-∥ M @@ -158,61 +158,57 @@ isProduct {A} {B} = record ; 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) - π₁∘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)) +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 |