Show free semimodule functor is cartesian

6 files changed, 283 insertions, 19 deletions

diff --git a/Data/Matrix/FreeSemimodule.agda b/Data/Matrix/FreeSemimodule.agda
index 77f2fe3..210d2e4 100644
--- a/Data/Matrix/FreeSemimodule.agda
+++ b/Data/Matrix/FreeSemimodule.agda
@@ -10,20 +10,33 @@ module R = CommutativeSemiring R
 import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
+open import Algebra.Module using (Semimodule)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
 open import Categories.Functor using (Functor)
-open import Category.Instance.Semimodules {c} {ℓ} {c} {c ⊔ ℓ} R using (Semimodules; SemimoduleHomomorphism)
+open import Categories.Functor.Cartesian using (IsCartesianF; CartesianF)
+open import Categories.Object.Product using (IsProduct)
+open import Categories.Object.Terminal using (IsTerminal)
+open import Category.Cartesian.Instance.Semimodules {c} {ℓ} {c} {c ⊔ ℓ} R using (Semimodules-CC)
+open import Category.Instance.Semimodules {c} {ℓ} {c} {c ⊔ ℓ} R using (Semimodules; SemimoduleHomomorphism) renaming (_≈_ to _≈-SM_)
 open import Data.Matrix.Category R.semiring using (Mat; _·_; ·-[])
 open import Data.Matrix.Core R.setoid using (Matrix; module ≋)
-open import Data.Matrix.Transform R.semiring using (I; _[_]; -[-]-cong; -[-]-cong₁; [_]_; -[⟨0⟩]; I[-]; -[⊕])
-open import Data.Nat using (ℕ)
+open import Data.Matrix.Monoid R.+-monoid using (𝟎)
+open import Data.Matrix.Raw using (_∥_; _≑_)
+open import Data.Matrix.Semiadditive R.semiring using (Mat-CC)
+open import Data.Matrix.Transform R.semiring using (I; _[_]; -[-]-cong; -[-]-cong₁; [_]_; -[⟨0⟩]; I[-]; -[⊕]; ∥-[++]; 𝟎-[-]; ≑--[-]; I-∥-≑)
+open import Data.Nat as Nat using (ℕ)
+open import Data.Vec using ([]; _++_)
 open import Data.Vec using (map)
-open import Data.Vec.Properties using (map-∘)
+open import Data.Vec.Properties using (map-∘; map-++; zipWith-++)
 open import Data.Vector.Bisemimodule R.semiring using (_⟨_⟩; ⟨_⟩_; _∙_; *-∙ˡ; *-∙ʳ; ∙-cong)
 open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; _≊_; module ≊)
-open import Data.Vector.Monoid R.+-monoid using (_⊕_; ⊕-cong; ⟨ε⟩)
+open import Data.Vector.Monoid R.+-monoid using (_⊕_; ⊕-cong; ⟨ε⟩; ⊕-identityˡ; ⊕-identityʳ)
 open import Data.Vector.Semimodule R using (Vector-Semimodule; ⟨-⟩-comm)
+open import Data.Vector.Vec using (replicate-++)
+open import Relation.Binary using (Setoid)
 
 open R
+open SemimoduleHomomorphism using (⟦_⟧; ⟦⟧-cong)
 
 opaque
 
@@ -84,3 +97,173 @@ Free = record
     ; homomorphism = λ {f = M} {N} V → ·-[] M N V
     ; F-resp-≈ = -[-]-cong₁
     }
+
+
+module Free-resp-⊤ where
+
+  opaque
+    unfolding _⊕_ ⟨ε⟩ _⟨_⟩
+    ! : {A : Semimodule R c (c ⊔ ℓ)} → SemimoduleHomomorphism A (Vector-Semimodule 0)
+    ! {A} = record
+        { ⟦_⟧ = λ _ → []
+        ; isSemimoduleHomomorphism = record
+            { isBisemimoduleHomomorphism = record
+                { +ᴹ-isMonoidHomomorphism = record
+                    { isMagmaHomomorphism = record
+                        { isRelHomomorphism = record
+                            { cong = λ _ → PW.[]
+                            }
+                        ; homo = λ _ _ → PW.[]
+                        }
+                    ; ε-homo = PW.[]
+                    }
+                ; *ₗ-homo = λ _ _ → PW.[]
+                ; *ᵣ-homo = λ _ _ → PW.[]
+                }
+            }
+        }
+
+    !-unique
+        : {A : Semimodule R c (c ⊔ ℓ)}
+          (f : SemimoduleHomomorphism A (Vector-Semimodule 0))
+        → ! ≈-SM f
+    !-unique f x with [] ← ⟦ f ⟧ x = PW.[]
+
+Free-resp-⊤ : IsTerminal Semimodules (Vector-Semimodule Mat-CC.⊤)
+Free-resp-⊤ = record { Free-resp-⊤ }
+
+⟨_,_⟩
+    : {A B : ℕ}
+      {X : Semimodule R c (c ⊔ ℓ)}
+    → SemimoduleHomomorphism X (Vector-Semimodule A)
+    → SemimoduleHomomorphism X (Vector-Semimodule B)
+    → SemimoduleHomomorphism X (Vector-Semimodule (A Nat.+ B))
+⟨_,_⟩ {A} {B} {X} f g = record
+    { ⟦_⟧ = λ x → ⟦ f ⟧ x ++ ⟦ g ⟧ x
+    ; isSemimoduleHomomorphism = record
+        { isBisemimoduleHomomorphism = record
+            { +ᴹ-isMonoidHomomorphism = record
+                { isMagmaHomomorphism = record
+                    { isRelHomomorphism = record
+                        { cong = λ ≈x → PW.++⁺ (⟦⟧-cong f ≈x) (⟦⟧-cong g ≈x)
+                        }
+                    ; homo = homo
+                    }
+                ; ε-homo = ε-homo
+                }
+            ; *ₗ-homo = *ₗ-homo
+            ; *ᵣ-homo = *ᵣ-homo
+            }
+        }
+    }
+  where
+    open ≈-Reasoning (PW.setoid setoid (A Nat.+ B))
+    module f = SemimoduleHomomorphism f
+    module g = SemimoduleHomomorphism g
+    open Semimodule X
+    opaque
+      unfolding ⟨ε⟩
+      ε-homo : PW.Pointwise {c} {c} {ℓ} {Carrier} {Carrier} _≈_ {A Nat.+ B} {A Nat.+ B} (⟦ f ⟧ 0ᴹ ++ ⟦ g ⟧ 0ᴹ) ⟨ε⟩
+      ε-homo = begin
+        ⟦ f ⟧ 0ᴹ ++ ⟦ g ⟧ 0ᴹ  ≈⟨ PW.++⁺ f.0ᴹ-homo g.0ᴹ-homo ⟩
+        ⟨ε⟩ {A} ++ ⟨ε⟩ {B}    ≡⟨ replicate-++ A B 0# ⟩
+        ⟨ε⟩                   ∎
+    opaque
+      unfolding _⊕_
+      homo : (x y : Carrierᴹ) → PW.Pointwise _≈_ (f.⟦ x +ᴹ y ⟧ ++ g.⟦ x +ᴹ y ⟧) ((f.⟦ x ⟧ ++ g.⟦ x ⟧) ⊕ (f.⟦ y ⟧ ++ g.⟦ y ⟧))
+      homo x y = begin
+          f.⟦ x +ᴹ y ⟧ ++ g.⟦ x +ᴹ y ⟧                ≈⟨ PW.++⁺ (f.+ᴹ-homo x y) (g.+ᴹ-homo x y) ⟩
+          (f.⟦ x ⟧ ⊕ f.⟦ y ⟧) ++ (g.⟦ x ⟧ ⊕ g.⟦ y ⟧)  ≡⟨ zipWith-++ _+_ f.⟦ x ⟧ g.⟦ x ⟧ f.⟦ y ⟧ g.⟦ y ⟧ ⟨
+          (f.⟦ x ⟧ ++ g.⟦ x ⟧) ⊕ (f.⟦ y ⟧ ++ g.⟦ y ⟧) ∎
+    opaque
+      unfolding _⟨_⟩
+      *ₗ-homo : (r : Carrier) (x : Carrierᴹ) → PW.Pointwise _≈_ (f.⟦ r *ₗ x ⟧ ++ g.⟦ r *ₗ x ⟧) (r ⟨ f.⟦ x ⟧ ++ g.⟦ x ⟧ ⟩)
+      *ₗ-homo r x = begin
+          f.⟦ r *ₗ x ⟧ ++ g.⟦ r *ₗ x ⟧    ≈⟨ PW.++⁺ (f.*ₗ-homo r x) (g.*ₗ-homo r x) ⟩
+          r ⟨ f.⟦ x ⟧ ⟩ ++ r ⟨ g.⟦ x ⟧ ⟩  ≡⟨ map-++ (r *_) f.⟦ x ⟧ g.⟦ x ⟧ ⟨
+          r ⟨ f.⟦ x ⟧ ++ g.⟦ x ⟧ ⟩        ∎
+    opaque
+      unfolding ⟨_⟩_
+      *ᵣ-homo : (r : Carrier) (x : Carrierᴹ) → PW.Pointwise _≈_ (f.⟦ x *ᵣ r ⟧ ++ g.⟦ x *ᵣ r ⟧) (⟨ f.⟦ x ⟧ ++ g.⟦ x ⟧ ⟩ r)
+      *ᵣ-homo r x = begin
+          f.⟦ x *ᵣ r ⟧ ++ g.⟦ x *ᵣ r ⟧    ≈⟨ PW.++⁺ (f.*ᵣ-homo r x) (g.*ᵣ-homo r x) ⟩
+          ⟨ f.⟦ x ⟧ ⟩ r ++ ⟨ g.⟦ x ⟧ ⟩ r  ≡⟨ map-++ (_* r) f.⟦ x ⟧ g.⟦ x ⟧ ⟨
+          ⟨ f.⟦ x ⟧ ++ g.⟦ x ⟧ ⟩ r        ∎
+
+module Project
+    {A B : ℕ}
+    {X : Semimodule R c (c ⊔ ℓ)}
+    {f : SemimoduleHomomorphism X (Vector-Semimodule A)}
+    {g : SemimoduleHomomorphism X (Vector-Semimodule B)}
+  where
+
+  module f = SemimoduleHomomorphism f
+  module g = SemimoduleHomomorphism g
+  open Semimodule X
+
+  project₁ : (x : Carrierᴹ) → PW.Pointwise _≈_ ((I {A} ∥ 𝟎 ) [ f.⟦ x ⟧ ++ g.⟦ x ⟧ ]) f.⟦ x ⟧
+  project₁ x = begin
+      (I ∥ 𝟎) [ f.⟦ x ⟧ ++ g.⟦ x ⟧ ]  ≈⟨ ∥-[++] f.⟦ x ⟧ g.⟦ x ⟧ I 𝟎 ⟩
+      I [ f.⟦ x ⟧ ] ⊕ 𝟎 [ g.⟦ x ⟧ ]   ≈⟨ ⊕-cong (I[-] f.⟦ x ⟧) (𝟎-[-] g.⟦ x ⟧) ⟩
+      f.⟦ x ⟧ ⊕ ⟨ε⟩                   ≈⟨ ⊕-identityʳ f.⟦ x ⟧ ⟩
+      f.⟦ x ⟧                         ∎
+    where
+      open ≈-Reasoning (PW.setoid setoid A)
+
+  project₂ : (x : Carrierᴹ) → PW.Pointwise _≈_ ((𝟎 ∥ I {B} ) [ f.⟦ x ⟧ ++ g.⟦ x ⟧ ]) g.⟦ x ⟧
+  project₂ x = begin
+      (𝟎 ∥ I) [ f.⟦ x ⟧ ++ g.⟦ x ⟧ ]  ≈⟨ ∥-[++] f.⟦ x ⟧ g.⟦ x ⟧ 𝟎 I ⟩
+      𝟎 [ f.⟦ x ⟧ ] ⊕ I [ g.⟦ x ⟧ ]   ≈⟨ ⊕-cong (𝟎-[-] f.⟦ x ⟧) (I[-] g.⟦ x ⟧) ⟩
+      ⟨ε⟩ ⊕ g.⟦ x ⟧                   ≈⟨ ⊕-identityˡ g.⟦ x ⟧ ⟩
+      g.⟦ x ⟧                         ∎
+    where
+      open ≈-Reasoning (PW.setoid setoid B)
+
+module Unique
+    {A B : ℕ}
+    {X : Semimodule R c (c ⊔ ℓ)}
+    {f : SemimoduleHomomorphism X (Vector-Semimodule A)}
+    {g : SemimoduleHomomorphism X (Vector-Semimodule B)}
+    {h : SemimoduleHomomorphism X (Vector-Semimodule (A Nat.+ B))}
+  where
+
+  open Semimodule X
+
+  module f = SemimoduleHomomorphism f
+  module g = SemimoduleHomomorphism g
+  module h = SemimoduleHomomorphism h
+
+  unique
+      : (eq₁ : (x : Carrierᴹ) → PW.Pointwise _≈_ ((I {A} ∥ 𝟎) [ h.⟦ x ⟧ ]) (f.⟦ x ⟧))
+      → (eq₂ : (x : Carrierᴹ) → PW.Pointwise _≈_ ((𝟎 ∥ I {B}) [ h.⟦ x ⟧ ]) (g.⟦ x ⟧))
+      → (x : Carrierᴹ)
+      → PW.Pointwise _≈_ (f.⟦ x ⟧ ++ g.⟦ x ⟧) h.⟦ x ⟧
+  unique eq₁ eq₂ x = begin
+      f.⟦ x ⟧ ++ g.⟦ x ⟧                                  ≈⟨ PW.++⁺ (eq₁ x) (eq₂ x) ⟨
+      ((I {A} ∥ 𝟎) [ h.⟦ x ⟧ ]) ++ ((𝟎 ∥ I) [ h.⟦ x ⟧ ])  ≡⟨ ≑--[-] h.⟦ x ⟧ (I ∥ 𝟎) (𝟎 ∥ I) ⟨
+      ((I {A} ∥ 𝟎) ≑ (𝟎 ∥ I)) [ h.⟦ x ⟧ ]                 ≡⟨ ≡.cong (_[ h.⟦ x ⟧ ]) I-∥-≑ ⟩
+      I [ h.⟦ x ⟧ ]                                       ≈⟨ I[-] h.⟦ x ⟧ ⟩
+      h.⟦ x ⟧                                             ∎
+    where
+      open ≈-Reasoning (PW.setoid setoid (A Nat.+ B))
+      open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+Free-resp-× : {A B : ℕ} → IsProduct Semimodules (F₁ (Mat-CC.π₁ {A} {B})) (F₁ (Mat-CC.π₂ {A} {B}))
+Free-resp-× {A} {B} = record
+    { ⟨_,_⟩ = ⟨_,_⟩
+    ; project₁ = λ {X f g} → Project.project₁ {A} {B} {X} {f} {g}
+    ; project₂ = λ {X f g} → Project.project₂ {A} {B} {X} {f} {g}
+    ; unique = λ {X h f g} eq₁ eq₂ x → Unique.unique {A} {B} {X} {f} {g} {h} eq₁ eq₂ x
+    }
+
+Free-IsCartesianF : IsCartesianF Mat-CC Semimodules-CC Free
+Free-IsCartesianF = record
+    { F-resp-⊤ = Free-resp-⊤
+    ; F-resp-× = Free-resp-×
+    }
+
+Free-IsCC : CartesianF Mat-CC Semimodules-CC
+Free-IsCC = record
+    { F = Free
+    ; isCartesian = Free-IsCartesianF
+    }
diff --git a/Data/Matrix/Monoid.agda b/Data/Matrix/Monoid.agda
index 93b449f..f614dc6 100644
--- a/Data/Matrix/Monoid.agda
+++ b/Data/Matrix/Monoid.agda
@@ -10,7 +10,7 @@ module M = Monoid M
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
 
-open import Data.Matrix.Raw using (_ᵀ; _∷ₕ_; []ᵥ; _≑_; _∥_; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥)
+open import Data.Matrix.Raw using (_ᵀ; _∷ₕ_; _∷ᵥ_; []ᵥ; _≑_; _∥_; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥)
 open import Data.Matrix.Core M.setoid using (Matrix; _≋_)
 open import Data.Nat using (ℕ)
 open import Data.Vec using (Vec; replicate; zipWith)
@@ -54,11 +54,22 @@ opaque
 
   opaque
 
-    unfolding _∷ₕ_ ⟨ε⟩
+    unfolding ⟨ε⟩
 
-    ⟨ε⟩∷ₕ𝟎 : ⟨ε⟩ ∷ₕ 𝟎 {A} {B} ≡ 𝟎
-    ⟨ε⟩∷ₕ𝟎 {A} {zero} = ≡.refl
-    ⟨ε⟩∷ₕ𝟎 {A} {suc B} = ≡.cong (⟨ε⟩ ∷_) ⟨ε⟩∷ₕ𝟎
+    opaque
+
+      unfolding _∷ₕ_
+
+      ⟨ε⟩∷ₕ𝟎 : ⟨ε⟩ ∷ₕ 𝟎 {A} {B} ≡ 𝟎
+      ⟨ε⟩∷ₕ𝟎 {A} {zero} = ≡.refl
+      ⟨ε⟩∷ₕ𝟎 {A} {suc B} = ≡.cong (⟨ε⟩ ∷_) ⟨ε⟩∷ₕ𝟎
+
+    opaque
+
+      unfolding _∷ᵥ_
+
+      ⟨ε⟩∷ᵥ𝟎 : ⟨ε⟩ ∷ᵥ 𝟎 {A} {B} ≡ 𝟎
+      ⟨ε⟩∷ᵥ𝟎 {A} {B} = ≡.refl
 
 𝟎∥𝟎 : 𝟎 {A} {C} ∥ 𝟎 {B} {C} ≡ 𝟎
 𝟎∥𝟎 {zero} {C} rewrite []ᵥ-! (𝟎 {0} {C}) = []ᵥ-∥ 𝟎
diff --git a/Data/Matrix/Raw.agda b/Data/Matrix/Raw.agda
index f2ad431..ecd5e9f 100644
--- a/Data/Matrix/Raw.agda
+++ b/Data/Matrix/Raw.agda
@@ -104,6 +104,9 @@ opaque
   ∷ₕ-≑ [] W [] N = ≡.refl
   ∷ₕ-≑ (x ∷ V) W (M₀ ∷ M) N = ≡.cong ((x ∷ M₀) ∷_) (∷ₕ-≑ V W M N)
 
+  ∷ᵥ-∥ : (V : Vec A n) (W : Vec A m) (M : Matrix A n p) (N : Matrix A m p) → (V ++ W) ∷ᵥ (M ∥ N) ≡ (V ∷ᵥ M) ∥ (W ∷ᵥ N)
+  ∷ᵥ-∥ {_} {A} {n} {m} {p} V W M N = ≡.refl
+
   headᵥ : Matrix A n (suc m) → Vec A n
   headᵥ = head
 
diff --git a/Data/Matrix/Semiadditive.agda b/Data/Matrix/Semiadditive.agda
index c6926b0..f91dfd7 100644
--- a/Data/Matrix/Semiadditive.agda
+++ b/Data/Matrix/Semiadditive.agda
@@ -269,10 +269,14 @@ Mat-Semiadditive = record
         }
     }
 
-open Semiadditive Mat-Semiadditive using (cartesian)
+open Semiadditive Mat-Semiadditive
+  using ()
+  renaming (cartesian to Mat-Cartesian) public
 
 Mat-CC : CartesianCategory 0ℓ c (c ⊔ ℓ)
 Mat-CC = record
     { U = Mat
-    ; cartesian = cartesian
+    ; cartesian = Mat-Cartesian
     }
+
+module Mat-CC = CartesianCategory Mat-CC
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⟩ [_]_
 
diff --git a/Data/Vector/Monoid.agda b/Data/Vector/Monoid.agda
index da09de9..7205800 100644
--- a/Data/Vector/Monoid.agda
+++ b/Data/Vector/Monoid.agda
@@ -12,15 +12,17 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 open import Data.Nat using (ℕ)
 open import Data.Product using (_,_)
-open import Data.Vec using (Vec; foldr′; zipWith; replicate)
+open import Data.Vec using (Vec; foldr′; zipWith; replicate; _++_)
 open import Data.Vector.Core M.setoid as S using (Vector; _≊_; module ≊; pull; Vectorₛ)
+open import Data.Vector.Vec using (replicate-++)
+open import Relation.Binary.PropositionalEquality using (_≡_)
 
 open M
 open Vec
 
 private
   variable
-    n A B C : ℕ
+    n m A B C : ℕ
 
 opaque
 
@@ -54,6 +56,9 @@ opaque
   ⟨ε⟩ : Vector n
   ⟨ε⟩ {n} = replicate n ε
 
+  ⟨ε⟩-++ : ⟨ε⟩ {n} ++ ⟨ε⟩ {m} ≡ ⟨ε⟩
+  ⟨ε⟩-++ {n} {m} = replicate-++ n m ε
+
 opaque
 
   unfolding _⊕_ ⟨ε⟩
@@ -95,9 +100,9 @@ open import Categories.Object.Monoid Setoids-×.monoidal as Obj using (Monoid⇒
 open import Data.Fin using (Fin)
 open import Data.Monoid using (module FromMonoid)
 open import Data.Monoid {c} {c ⊔ ℓ} using (fromMonoid)
-open import Data.Vec using (tabulate; lookup)
+open import Data.Vec using (tabulate; lookup; _++_)
 open import Data.Vec.Properties using (tabulate-cong; lookup-zipWith; lookup-replicate)
-open import Data.Vector.Vec using (zipWith-tabulate; replicate-tabulate)
+open import Data.Vector.Vec using (zipWith-tabulate; replicate-tabulate; replicate-++)
 open import Function using (Func; _⟨$⟩_; _∘_; id)
 open import Relation.Binary.PropositionalEquality as ≡ using (module ≡-Reasoning; _≡_; _≗_)