Show free semimodule functor is cartesian

1 files changed, 61 insertions, 3 deletions

diff --git a/Data/Matrix/Transform.agda b/Data/Matrix/Transform.agda
index 9c9fb23..f536aaf 100644
--- a/Data/Matrix/Transform.agda
+++ b/Data/Matrix/Transform.agda
@@ -21,18 +21,19 @@ open import Data.Matrix.Raw
   using
     ( _ᵀ; _∷ₕ_; []ᵥ; []ₕ; []ᵥ-ᵀ; mapRows
     ; _ᵀᵀ; []ᵥ-!; ∷ₕ-ᵀ; _∥_; []ᵥ-∥; headₕ; tailₕ; head-∷-tailₕ; ∷ₕ-∥
-    ; _≑_; []ᵥ-≑; ∷ₕ-≑
+    ; _≑_; []ᵥ-≑; ∷ₕ-≑; []ₕ-≑; []ₕ-!; ∷ᵥ-∥
     )
 open import Data.Matrix.Core R.setoid
   using
     ( Matrix; Matrixₛ; _≋_; ≋-isEquiv
     ; ∷ₕ-cong; module ≋; ᵀ-cong
     )
-open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; _[+]_)
+open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; _[+]_) renaming (⟨ε⟩∷ᵥ𝟎 to ⟨0⟩∷ᵥ𝟎; ⟨ε⟩∷ₕ𝟎 to ⟨0⟩∷ₕ𝟎)
+open import Data.Matrix.Cast R.setoid using (∥-≑)
 open import Data.Vector.Raw using (⟨⟩; ⟨⟩-++)
 open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; module ≊; _≊_)
 open import Data.Vector.Vec using (zipWith-map; map-zipWith; zipWith-map-map)
-open import Data.Vector.Monoid R.+-monoid using (_⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ) renaming (⟨ε⟩ to ⟨0⟩)
+open import Data.Vector.Monoid R.+-monoid using (_⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ) renaming (⟨ε⟩ to ⟨0⟩; ⟨ε⟩-++ to ⟨0⟩-++)
 open import Data.Vector.Bisemimodule R using (_∙_; ∙-cong; ∙-zeroˡ; ∙-zeroʳ; _⟨_⟩; *-∙ˡ; *-∙ʳ; ∙-distribˡ; ∙-distribʳ)
 
 open Vec
@@ -112,6 +113,34 @@ opaque
         open ≡-Reasoning
 
 opaque
+  unfolding I
+  I-∥-≑ : I {A} ∥ 𝟎 ≑ 𝟎 ∥ I {B} ≡ I
+  I-∥-≑ {zero} {B} = begin
+      I {ℕ.zero} ∥ 𝟎 ≑ 𝟎 ∥ I  ≡⟨ ≡.cong (_≑ 𝟎 ∥ I) ([]ₕ-! (I ∥ 𝟎)) ⟩
+      []ₕ ≑ 𝟎 ∥ I             ≡⟨ []ₕ-≑ (𝟎 ∥ I) ⟩
+      𝟎 ∥ I                   ≡⟨ ≡.cong (_∥ I) ([]ᵥ-! 𝟎) ⟩
+      []ᵥ ∥ I                 ≡⟨ []ᵥ-∥ I ⟩
+      I                       ∎
+    where
+      open ≡-Reasoning
+  I-∥-≑ {suc A} {B} = begin
+      ((1# ∷ ⟨0⟩) ∷ ⟨0⟩ ∷ₕ I) ∥ 𝟎 ≑ 𝟎 ∥ I                           ≡⟨ ≡.cong (λ h → ((1# ∷ ⟨0⟩) ∷ ⟨0⟩ ∷ₕ I {A}) ∥ h ≑ 𝟎 ∥ I) ⟨0⟩∷ᵥ𝟎 ⟨
+      ((1# ∷ ⟨0⟩) ∷ ⟨0⟩ ∷ₕ I {A}) ∥ (⟨0⟩ ∷ 𝟎) ≑ 𝟎 ∥ I               ≡⟨ ≡.cong (λ h → h ≑ 𝟎 ∥ I {B}) (∷ᵥ-∥ (1# ∷ ⟨0⟩) ⟨0⟩ (⟨0⟩ ∷ₕ I) 𝟎) ⟨
+      ((1# ∷ ⟨0⟩ {A}) ++ ⟨0⟩) ∷ ((⟨0⟩ ∷ₕ I {A}) ∥ 𝟎) ≑ 𝟎 ∥ I        ≡⟨ ≡.cong (λ h → ((1# ∷ ⟨0⟩ {A}) ++ ⟨0⟩ {B}) ∷ h ≑ 𝟎 ∥ (I {B})) (∷ₕ-∥ ⟨0⟩ I 𝟎) ⟨
+      (1# ∷ ⟨0⟩ {A} ++ ⟨0⟩) ∷ (⟨0⟩ ∷ₕ (I {A} ∥ 𝟎)) ≑ 𝟎 ∥ I          ≡⟨ ≡.cong (λ h → (1# ∷ h) ∷ (⟨0⟩ ∷ₕ (I {A} ∥ 𝟎)) ≑ 𝟎 ∥ I) ⟨0⟩-++ ⟩
+      (1# ∷ ⟨0⟩) ∷ (⟨0⟩ ∷ₕ (I {A} ∥ 𝟎)) ≑ 𝟎 ∥ I {B}                 ≡⟨ ≡.cong (λ h → (1# ∷ ⟨0⟩) ∷ (⟨0⟩ ∷ₕ (I {A} ∥ 𝟎)) ≑ h ∥ I {B}) ⟨0⟩∷ₕ𝟎 ⟨
+      (1# ∷ ⟨0⟩) ∷ (⟨0⟩ ∷ₕ (I {A} ∥ 𝟎)) ≑ (⟨0⟩ ∷ₕ 𝟎) ∥ I {B}        ≡⟨ ≡.cong (λ h → (1# ∷ ⟨0⟩) ∷ h ≑ (⟨0⟩ ∷ₕ 𝟎) ∥ I {B}) (∷ₕ-∥ ⟨0⟩ I 𝟎) ⟩
+      (1# ∷ ⟨0⟩) ∷ ((⟨0⟩ ∷ₕ I {A}) ∥ 𝟎) ≑ (⟨0⟩ ∷ₕ 𝟎) ∥ I {B}        ≡⟨ ≡.cong ((1# ∷ ⟨0⟩) ∷_) (∥-≑ (⟨0⟩ ∷ₕ I) 𝟎 (⟨0⟩ ∷ₕ 𝟎) I) ⟩
+      (1# ∷ ⟨0⟩) ∷ ((⟨0⟩ ∷ₕ I {A}) ≑ (⟨0⟩ ∷ₕ 𝟎)) ∥ (𝟎 ≑ I {B})      ≡⟨ ≡.cong (λ h → (1# ∷ ⟨0⟩) ∷ (h ∥ (𝟎 ≑ I {B}))) (∷ₕ-≑ ⟨0⟩ ⟨0⟩ I 𝟎) ⟨
+      (1# ∷ ⟨0⟩) ∷ ((⟨0⟩ {A} ++ ⟨0⟩) ∷ₕ (I {A} ≑ 𝟎)) ∥ (𝟎 ≑ I {B})  ≡⟨ ≡.cong (λ h → (1# ∷ ⟨0⟩) ∷ (h ∷ₕ (I {A} ≑ 𝟎)) ∥ (𝟎 ≑ I)) ⟨0⟩-++ ⟩
+      (1# ∷ ⟨0⟩) ∷ (⟨0⟩ ∷ₕ (I {A} ≑ 𝟎)) ∥ (𝟎 ≑ I {B})               ≡⟨ ≡.cong ((1# ∷ ⟨0⟩) ∷_) (∷ₕ-∥ ⟨0⟩ (I ≑ 𝟎) (𝟎 ≑ I)) ⟨
+      (1# ∷ ⟨0⟩) ∷ ⟨0⟩ ∷ₕ ((I {A} ≑ 𝟎) ∥ (𝟎 ≑ I {B}))               ≡⟨ ≡.cong (λ h → (1# ∷ ⟨0⟩) ∷ ⟨0⟩ ∷ₕ h) (∥-≑ I 𝟎 𝟎 I) ⟨
+      (1# ∷ ⟨0⟩) ∷ ⟨0⟩ ∷ₕ (I {A} ∥ 𝟎 ≑ 𝟎 ∥ I {B})                   ≡⟨ ≡.cong (λ h → (1# ∷ ⟨0⟩) ∷ ⟨0⟩ ∷ₕ h) I-∥-≑ ⟩
+      (1# ∷ ⟨0⟩) ∷ ⟨0⟩ ∷ₕ I                                         ∎
+    where
+      open ≡-Reasoning
+
+opaque
   unfolding mapRows _ᵀ _[_] [_]_ []ᵥ
   -[-]ᵀ : (A : Matrix m p) (B : Matrix n m) → mapRows (A [_]) (B ᵀ) ≡ (mapRows ([_] B) A) ᵀ
   -[-]ᵀ [] B = map-const (B ᵀ) []
@@ -228,6 +257,16 @@ opaque
       open ≡-Reasoning
 
 opaque
+  unfolding Matrix _[_]
+  ≑--[-]
+      : (V : Vector A)
+        (M : Matrix A B)
+        (N : Matrix A C)
+      → (M ≑ N) [ V ] ≡ M [ V ] ++ N [ V ]
+  ≑--[-] {A} {zero} {C} V [] N = ≡.refl
+  ≑--[-] {A} {suc B} {C} V (M₀ ∷ M) N = ≡.cong (M₀ ∙ V ∷_) (≑--[-] V M N)
+
+opaque
 
   unfolding _∙_
 
@@ -274,6 +313,19 @@ opaque
       ([ V ] (M₀ ∷ₕ M)) ⊕ ([ W ] (N₀ ∷ₕ N))         ∎
     where
       open ≈-Reasoning (Vectorₛ (suc A))
+
+opaque
+  unfolding Matrix _[_] _⊕_
+  ∥-[++]
+      : (V : Vector A)
+        (W : Vector B)
+        (M : Matrix A C)
+        (N : Matrix B C)
+      → (M ∥ N) [ V ++ W ]
+      ≊ M [ V ] ⊕ N [ W ]
+  ∥-[++] {A} {B} {zero} V W [] [] = PW.[]
+  ∥-[++] {A} {B} {suc C} V W (M₀ ∷ M) (N₀ ∷ N) = ∙-++ M₀ V N₀ W PW.∷ ∥-[++] V W M N
+
 opaque
 
   unfolding []ₕ []ᵥ [_]_ ⟨0⟩ _∙_ _ᵀ
@@ -297,6 +349,12 @@ opaque
       open ≈-Reasoning (Vectorₛ (suc B))
 
 opaque
+  unfolding Matrix _[_] ⟨0⟩ 𝟎
+  𝟎-[-] : (V : Vector A) → (𝟎 {A} {B}) [ V ] ≊ ⟨0⟩
+  𝟎-[-] {A} {zero} V = PW.[]
+  𝟎-[-] {A} {suc B} V = ∙-zeroˡ V PW.∷ 𝟎-[-] V
+
+opaque
 
   unfolding ⟨0⟩ [_]_