Reorganize matrix code

1 files changed, 0 insertions, 623 deletions

diff --git a/Data/Mat/Cocartesian.agda b/Data/Mat/Cocartesian.agda
deleted file mode 100644
index 5ea92b3..0000000
--- a/Data/Mat/Cocartesian.agda
+++ /dev/null
@@ -1,623 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Algebra.Bundles using (Semiring)
-open import Level using (Level)
-
-module Data.Mat.Cocartesian {c ℓ : Level} (Rig : Semiring c ℓ) where
-
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
-
-open import Data.Mat.Category Rig
-  using
-   ( Mat; Matrix; Vector; zeros; I; _≊_; module ≊; ≊-setoid; _≋_; module ≋; ≋-setoid
-   ; _ᵀ; mapRows; _·_; _∙_; _ᵀᵀ; _⊕_; ·-identityʳ; ∙-zerosʳ; ∙-zerosˡ
-   )
-  renaming ([_]_ to [_]′_)
-
-open import Categories.Category.Cocartesian Mat using (Cocartesian)
-open import Categories.Object.Coproduct Mat using (Coproduct)
-open import Categories.Object.Initial Mat using (Initial)
-open import Data.Mat.Util using (replicate-++; zipWith-map; transpose-zipWith; zipWith-cong)
-open import Data.Nat as ℕ using (ℕ)
-open import Data.Product using (_,_; Σ-syntax)
-open import Data.Vec using (Vec; map; zipWith; replicate; _++_; head; tail)
-open import Data.Vec.Properties using (zipWith-replicate; map-cong; map-const; map-id)
-open import Function using (id; _∘_)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
-
-open Semiring Rig renaming (Carrier to R)
-open Vec
-open ℕ.ℕ
-
-private
-  variable
-    A B C D : ℕ
-    A₁ A₂ B₁ B₂ : ℕ
-
-opaque
-  unfolding Vector
-  _+++_ : Vector A → Vector B → Vector (A ℕ.+ B)
-  _+++_ = _++_
-
-opaque
-  unfolding Matrix Vector
-  _∥_ : Matrix A C → Matrix B C → Matrix (A ℕ.+ B) C
-  _∥_ M N = zipWith _++_ M N
-
-opaque
-  unfolding Matrix
-  [_] : Vector A → Matrix A 1
-  [_] V = V ∷ []
-
-opaque
-  unfolding Matrix Vector
-  ⟦_⟧ : R → Matrix 1 1
-  ⟦_⟧ x = [ x ∷ [] ]
-
-[_]ᵀ : Vector A → Matrix 1 A
-[_]ᵀ V = [ V ] ᵀ
-
-opaque
-  unfolding Vector
-  ⟨⟩ : Vector 0
-  ⟨⟩ = []
-
-opaque
-  unfolding Vector
-  _∷′_ : R → Vector A → Vector (suc A)
-  _∷′_ = _∷_
-
-infixr 5 _∷′_
-
-infixr 7 _∥_
-
-opaque
-  unfolding Matrix
-  _≑_ : Matrix A B → Matrix A C → Matrix A (B ℕ.+ C)
-  _≑_ M N = M ++ N
-
-infixr 6 _≑_
-
-opaque
-  unfolding Matrix
-  _∷ᵥ_ : Vector A → Matrix A B → Matrix A (suc B)
-  _∷ᵥ_ V M = V ∷ M
-
-infixr 5 _∷ᵥ_
-
-opaque
-  unfolding Matrix Vector
-  _∷ₕ_ : Vector B → Matrix A B → Matrix (suc A) B
-  _∷ₕ_ V M = zipWith _∷_ V M
-
-infixr 5 _∷ₕ_
-
-opaque
-  unfolding Matrix
-  headᵥ : Matrix A (suc B) → Vector A
-  headᵥ (V ∷ _) = V
-
-opaque
-  unfolding Matrix
-  tailᵥ : Matrix A (suc B) → Matrix A B
-  tailᵥ (_ ∷ M) = M
-
-opaque
-  unfolding Matrix Vector
-  headₕ : Matrix (suc A) B → Vector B
-  headₕ M = map head M
-
-opaque
-  unfolding Matrix Vector
-  tailₕ : Matrix (suc A) B → Matrix A B
-  tailₕ M = map tail M
-
-opaque
-  unfolding _∷ᵥ_ headᵥ tailᵥ
-  head-∷-tailᵥ : (M : Matrix A (suc B)) → headᵥ M ∷ᵥ tailᵥ M ≡ M
-  head-∷-tailᵥ (_ ∷ _) = ≡.refl
-
-opaque
-  unfolding _∷ₕ_ headₕ tailₕ
-  head-∷-tailₕ : (M : Matrix (suc A) B) → headₕ M ∷ₕ tailₕ M ≡ M
-  head-∷-tailₕ M = begin
-      zipWith _∷_ (map head M) (map tail M) ≡⟨ zipWith-map head tail _∷_ M ⟩
-      map (λ x → head x ∷ tail x) M         ≡⟨ map-cong (λ { (_ ∷ _) → ≡.refl }) M ⟩
-      map id M                              ≡⟨ map-id M ⟩
-      M ∎
-    where
-      open ≡-Reasoning
-
-opaque
-  unfolding Matrix
-  []ₕ : Matrix A 0
-  []ₕ = []
-
-opaque
-  unfolding []ₕ _ᵀ
-  []ᵥ : Matrix 0 B
-  []ᵥ = []ₕ ᵀ
-
-opaque
-  unfolding []ᵥ
-  []ᵥ-ᵀ : []ᵥ ᵀ ≡ []ₕ {A}
-  []ᵥ-ᵀ = []ₕ ᵀᵀ
-
-opaque
-  unfolding []ₕ
-  []ₕ-! : (E : Matrix A 0) → E ≡ []ₕ
-  []ₕ-! [] = ≡.refl
-
-opaque
-  unfolding []ᵥ
-  []ᵥ-! : (E : Matrix 0 B) → E ≡ []ᵥ
-  []ᵥ-! [] = ≡.refl
-  []ᵥ-! ([] ∷ E) = ≡.cong ([] ∷_) ([]ᵥ-! E)
-
-opaque
-  unfolding Matrix Vector
-  _∷[_,_]_ : R → Vector B → Vector A → Matrix A B → Matrix (suc A) (suc B)
-  _∷[_,_]_ v C R M = (v ∷ R) ∷ᵥ (C ∷ₕ M)
-
-opaque
-  unfolding Matrix
-  𝟎 : Matrix A B
-  𝟎 {A} {B} = replicate B zeros
-
-opaque
-  unfolding 𝟎 _ᵀ zeros _∷ₕ_ _∥_
-  𝟎ᵀ : 𝟎 ᵀ ≡ 𝟎 {A} {B}
-  𝟎ᵀ {zero} = ≡.refl
-  𝟎ᵀ {suc A} = begin
-      zeros ∷ₕ (𝟎 ᵀ)  ≡⟨ ≡.cong (zeros ∷ₕ_) 𝟎ᵀ ⟩
-      zeros ∷ₕ 𝟎      ≡⟨ zipWith-replicate _∷_ 0# zeros ⟩
-      𝟎               ∎
-    where
-      open ≡-Reasoning
-
-opaque
-  unfolding _∥_ []ᵥ
-  []ᵥ-∥ : (M : Matrix A B) → []ᵥ ∥ M ≡ M
-  []ᵥ-∥ [] = ≡.refl
-  []ᵥ-∥ (M₀ ∷ M) = ≡.cong (M₀ ∷_) ([]ᵥ-∥ M)
-
-opaque
-  unfolding _≑_ []ₕ
-  []ₕ-≑ : (M : Matrix A B) → []ₕ ≑ M ≡ M
-  []ₕ-≑ _ = ≡.refl
-
-opaque
-  unfolding _∷ₕ_ _ᵀ _∷ᵥ_
-  ∷ₕ-ᵀ : (V : Vector A) (M : Matrix B A) → (V ∷ₕ M) ᵀ ≡ V ∷ᵥ M ᵀ
-  ∷ₕ-ᵀ = transpose-zipWith
-
-opaque
-  unfolding _∷ₕ_ _ᵀ _∷ᵥ_
-  ∷ᵥ-ᵀ : (V : Vector B) (M : Matrix B A) → (V ∷ᵥ M) ᵀ ≡ V ∷ₕ M ᵀ
-  ∷ᵥ-ᵀ V M = ≡.refl
-
-opaque
-  unfolding _∷ₕ_ _∥_
-  ∷ₕ-∥ : (V : Vector C) (M : Matrix A C) (N : Matrix B C) → V ∷ₕ (M ∥ N) ≡ (V ∷ₕ M) ∥ N
-  ∷ₕ-∥ [] [] [] = ≡.refl
-  ∷ₕ-∥ (x ∷ V) (M₀ ∷ M) (N₀ ∷ N) = ≡.cong ((x ∷ M₀ ++ N₀) ∷_) (∷ₕ-∥ V M N)
-
-opaque
-  unfolding _∷ᵥ_ _≑_
-  ∷ᵥ-≑ : (V : Vector A) (M : Matrix A B) (N : Matrix A C) → V ∷ᵥ (M ≑ N) ≡ (V ∷ᵥ M) ≑ N
-  ∷ᵥ-≑ V M N = ≡.refl
-
-opaque
-  unfolding zeros [_]′_ Matrix _∙_
-  [-]- : (V : Vector 0) (E : Matrix A 0) → [ V ]′ E ≡ zeros
-  [-]- {zero} _ [] = ≡.refl
-  [-]- {suc A} [] [] = ≡.cong (0# ∷_) ([-]- [] [])
-
-opaque
-  unfolding ⟨⟩ _+++_
-  ⟨⟩-+++ : (V : Vector A) → ⟨⟩ +++ V ≡ V
-  ⟨⟩-+++ V = ≡.refl
-
-opaque
-  unfolding _∷′_ _+++_
-  ∷-+++ : (x : R) (M : Vector A) (N : Vector B) → (x ∷′ M) +++ N ≡ x ∷′ (M +++ N)
-  ∷-+++ x M N = ≡.refl
-
-opaque
-  unfolding []ₕ [_]′_ _ᵀ []ᵥ ⟨⟩
-  [-]-[]ᵥ : (V : Vector A) → [ V ]′ []ᵥ ≡ ⟨⟩
-  [-]-[]ᵥ [] = ≡.refl
-  [-]-[]ᵥ (x ∷ V) = ≡.cong (map ((x ∷ V) ∙_)) []ᵥ-ᵀ
-
-opaque
-  unfolding [_]′_ _ᵀ _∷ᵥ_ _∷′_
-  [-]-∷ₕ : (V M₀ : Vector B) (M : Matrix A B) → [ V ]′ (M₀ ∷ₕ M) ≡ V ∙ M₀ ∷′ ([ V ]′ M)
-  [-]-∷ₕ V M₀ M = ≡.cong (map (V ∙_)) (∷ₕ-ᵀ M₀ M)
-    where
-      open ≡-Reasoning
-
-[-]--∥
-    : (V : Vector C)
-      (M : Matrix A C)
-      (N : Matrix B C)
-    → [ V ]′ (M ∥ N) ≡ ([ V ]′ M) +++ ([ V ]′ N)
-[-]--∥ {C} {zero} V M N rewrite []ᵥ-! M = begin
-    [ V ]′ ([]ᵥ ∥ N)            ≡⟨ ≡.cong ([ V ]′_) ([]ᵥ-∥ N) ⟩
-    [ V ]′ N                    ≡⟨ ⟨⟩-+++ ([ V ]′ N) ⟨
-    ⟨⟩ +++ ([ V ]′ N)           ≡⟨ ≡.cong (_+++ ([ V ]′ N)) ([-]-[]ᵥ V) ⟨
-    ([ V ]′ []ᵥ) +++ ([ V ]′ N) ∎
-  where
-    open ≡-Reasoning
-[-]--∥ {C} {suc A} V M N
-  rewrite ≡.sym (head-∷-tailₕ M)
-  using M₀ ← headₕ M
-  using M ← tailₕ M = begin
-    [ V ]′ ((M₀ ∷ₕ M) ∥ N)                ≡⟨ ≡.cong ([ V ]′_) (∷ₕ-∥ M₀ M N) ⟨
-    [ V ]′ (M₀ ∷ₕ (M ∥ N))                ≡⟨ [-]-∷ₕ V M₀ (M ∥ N) ⟩
-    V ∙ M₀ ∷′ ([ V ]′ (M ∥ N))            ≡⟨ ≡.cong (V ∙ M₀ ∷′_) ([-]--∥ V M N) ⟩
-    V ∙ M₀ ∷′ (([ V ]′ M) +++ ([ V ]′ N)) ≡⟨ ∷-+++ (V ∙ M₀) ([ V ]′ M) ([ V ]′ N) ⟨
-    (V ∙ M₀ ∷′ [ V ]′ M) +++ ([ V ]′ N)   ≡⟨ ≡.cong (_+++ ([ V ]′ N)) ([-]-∷ₕ V M₀ M) ⟨
-    ([ V ]′ (M₀ ∷ₕ M)) +++ ([ V ]′ N)     ∎
-  where
-    open ≡-Reasoning
-
-opaque
-  unfolding _∥_ mapRows _+++_
-  ·-∥
-      : (M : Matrix C D)
-        (N : Matrix A C)
-        (P : Matrix B C)
-      → M · (N ∥ P) ≡ M · N ∥ M · P
-  ·-∥ {C} {D} {A} {B} [] N P = ≡.refl
-  ·-∥ {C} {D} {A} {B} (M₀ ∷ M) N P = ≡.cong₂ _∷_ ([-]--∥ M₀ N P) (·-∥ M N P)
-
-opaque
-  unfolding _≑_ mapRows
-  ≑-· : (M : Matrix B C)
-        (N : Matrix B D)
-        (P : Matrix A B)
-      → (M ≑ N) · P ≡ (M · P) ≑ (N · P)
-  ≑-· [] N P = ≡.refl
-  ≑-· (M₀ ∷ M) N P = ≡.cong ([ M₀ ]′ P ∷_) (≑-· M N P)
-
-opaque
-  unfolding Matrix
-  _[+]_ : Matrix A B → Matrix A B → Matrix A B
-  _[+]_ = zipWith _⊕_
-
-opaque
-  unfolding _+++_ _≑_ _∷ₕ_
-  ∷ₕ-≑ : (V : Vector A) (W : Vector B) (M : Matrix C A) (N : Matrix C B) → (V +++ W) ∷ₕ (M ≑ N) ≡ (V ∷ₕ M) ≑ (W ∷ₕ N)
-  ∷ₕ-≑ [] W [] N = ≡.refl
-  ∷ₕ-≑ (x ∷ V) W (M₀ ∷ M) N = ≡.cong ((x ∷ M₀) ∷_) (∷ₕ-≑ V W M N)
-
-opaque
-  unfolding _+++_ _∙_
-  ∙-+++ : (W Y : Vector A) (X Z : Vector B) → (W +++ X) ∙ (Y +++ Z) ≈ W ∙ Y + X ∙ Z
-  ∙-+++ [] [] X Z = sym (+-identityˡ (X ∙ Z))
-  ∙-+++ (w ∷ W) (y ∷ Y) X Z = begin
-      w * y + (W ++ X) ∙ (Y ++ Z) ≈⟨ +-congˡ (∙-+++ W Y X Z) ⟩
-      w * y + (W ∙ Y + X ∙ Z)     ≈⟨ +-assoc _ _ _ ⟨
-      (w * y + W ∙ Y) + X ∙ Z     ∎
-    where
-      open ≈-Reasoning setoid
-
-opaque
-  unfolding []ᵥ _≑_
-  []ᵥ-≑ : []ᵥ {A} ≑ []ᵥ {B} ≡ []ᵥ
-  []ᵥ-≑ {A} {B} = replicate-++ A B []
-
-opaque
-  unfolding _⊕_ ⟨⟩
-  ⟨⟩-⊕ : ⟨⟩ ⊕ ⟨⟩ ≡ ⟨⟩
-  ⟨⟩-⊕ = ≡.refl
-
-opaque
-  unfolding ≊-setoid _∷′_ _⊕_
-  [+++]-≑
-      : (V : Vector B)
-        (W : Vector C)
-        (M : Matrix A B)
-        (N : Matrix A C)
-      → [ V +++ W ]′ (M ≑ N)
-      ≊ [ V ]′ M ⊕ [ W ]′ N
-  [+++]-≑ {B} {C} {zero} V W M N
-    rewrite []ᵥ-! M
-    rewrite []ᵥ-! N = begin
-      [ V +++ W ]′ ([]ᵥ {B} ≑ []ᵥ)  ≡⟨ ≡.cong ([ V +++ W ]′_) []ᵥ-≑ ⟩
-      [ V +++ W ]′ []ᵥ              ≡⟨ [-]-[]ᵥ (V +++ W) ⟩
-      ⟨⟩                            ≡⟨ ⟨⟩-⊕ ⟨
-      ⟨⟩ ⊕ ⟨⟩                       ≡⟨ ≡.cong₂ _⊕_ ([-]-[]ᵥ V) ([-]-[]ᵥ W) ⟨
-      [ V ]′ []ᵥ ⊕ [ W ]′ []ᵥ       ∎
-    where
-      open ≈-Reasoning (≊-setoid 0)
-  [+++]-≑ {B} {C} {suc A} V W M N
-    rewrite ≡.sym (head-∷-tailₕ M)
-    rewrite ≡.sym (head-∷-tailₕ N)
-    using M₀ ← headₕ M
-    using M ← tailₕ M
-    using N₀ ← headₕ N
-    using N ← tailₕ N = begin
-      [ V +++ W ]′ ((M₀ ∷ₕ M) ≑ (N₀ ∷ₕ N))              ≡⟨ ≡.cong ([ V +++ W ]′_) (∷ₕ-≑ M₀ N₀ M N) ⟨
-      [ V +++ W ]′ ((M₀ +++ N₀) ∷ₕ (M ≑ N))             ≡⟨ [-]-∷ₕ (V +++ W) (M₀ +++ N₀) (M ≑ N) ⟩
-      (V +++ W) ∙ (M₀ +++ N₀) ∷′ ([ V +++ W ]′ (M ≑ N)) ≈⟨ ∙-+++ V M₀ W N₀ PW.∷ [+++]-≑ V W M N ⟩
-      (V ∙ M₀ ∷′ [ V ]′ M) ⊕ (W ∙ N₀ ∷′ [ W ]′ N)       ≡⟨ ≡.cong₂ _⊕_ ([-]-∷ₕ V M₀ M) ([-]-∷ₕ W N₀ N) ⟨
-      ([ V ]′ (M₀ ∷ₕ M)) ⊕ ([ W ]′ (N₀ ∷ₕ N))           ∎
-    where
-      open ≈-Reasoning (≊-setoid (suc A))
-
-opaque
-  unfolding _∥_ _+++_ mapRows _[+]_ ≋-setoid
-  ∥-·-≑
-      : (W : Matrix A C)
-        (X : Matrix B C)
-        (Y : Matrix D A)
-        (Z : Matrix D B)
-      → (W ∥ X) · (Y ≑ Z) ≋ (W · Y) [+] (X · Z)
-  ∥-·-≑ [] [] Y Z = PW.[]
-  ∥-·-≑ {A} {C} {B} {D} (W₀ ∷ W) (X₀ ∷ X) Y Z = [+++]-≑ W₀ X₀ Y Z PW.∷ ∥-·-≑ W X Y Z
-    where
-      open ≈-Reasoning (≋-setoid A B)
-
-opaque
-  unfolding _⊕_ _≊_
-  ⊕-cong : {V V′ W W′ : Vector A} → V ≊ V′ → W ≊ W′ → V ⊕ W ≊ V′ ⊕ W′
-  ⊕-cong = zipWith-cong +-cong
-
-opaque
-  unfolding _[+]_ _≋_
-  [+]-cong : {M M′ N N′ : Matrix A B} → M ≋ M′ → N ≋ N′ → M [+] N ≋ M′ [+] N′
-  [+]-cong = zipWith-cong ⊕-cong
-
-opaque
-  unfolding ⟨⟩ []ₕ [_]′_ zeros _∙_
-  [⟨⟩]-[]ₕ : [ ⟨⟩ ]′ ([]ₕ {A}) ≡ zeros {A}
-  [⟨⟩]-[]ₕ {zero} = ≡.refl
-  [⟨⟩]-[]ₕ {suc A} = ≡.cong (0# ∷_) [⟨⟩]-[]ₕ
-
-opaque
-  unfolding Vector ⟨⟩ zeros []ᵥ [_]′_ _ᵀ _∷ₕ_ 𝟎 _≊_
-  [-]-𝟎 : (V : Vector A) →  [ V ]′ (𝟎 {B}) ≊ zeros
-  [-]-𝟎 {A} {zero} V = ≊.reflexive (≡.cong (map (V ∙_)) 𝟎ᵀ)
-  [-]-𝟎 {A} {suc B} V = begin
-      map (V ∙_) (𝟎 ᵀ)          ≡⟨ ≡.cong (map (V ∙_)) 𝟎ᵀ ⟩
-      V ∙ zeros ∷ map (V ∙_) 𝟎  ≡⟨ ≡.cong ((V ∙ zeros ∷_) ∘ map (V ∙_)) 𝟎ᵀ ⟨
-      V ∙ zeros ∷ [ V ]′ 𝟎      ≈⟨ ∙-zerosʳ V PW.∷ ([-]-𝟎 V) ⟩
-      0# ∷ zeros                ∎
-    where
-      open ≈-Reasoning (≊-setoid (suc B))
-
-opaque
-  unfolding _⊕_ zeros _≊_
-  ⊕-zerosʳ : (V : Vector A) → V ⊕ zeros ≊ V
-  ⊕-zerosʳ [] = PW.[]
-  ⊕-zerosʳ (x ∷ V) = +-identityʳ x PW.∷ ⊕-zerosʳ V
-
-opaque
-  unfolding _⊕_ zeros _≊_
-  ⊕-zerosˡ : (V : Vector A) → zeros ⊕ V ≊ V
-  ⊕-zerosˡ [] = PW.[]
-  ⊕-zerosˡ (x ∷ V) = +-identityˡ x PW.∷ ⊕-zerosˡ V
-
-opaque
-  unfolding Matrix _[+]_ _≋_ 𝟎
-  [+]-𝟎ʳ : (M : Matrix A B) → M [+] 𝟎 ≋ M
-  [+]-𝟎ʳ [] = PW.[]
-  [+]-𝟎ʳ (M₀ ∷ M) = ⊕-zerosʳ M₀ PW.∷ [+]-𝟎ʳ M
-
-opaque
-  unfolding Matrix _[+]_ _≋_ 𝟎
-  [+]-𝟎ˡ : (M : Matrix A B) → 𝟎 [+] M ≋ M
-  [+]-𝟎ˡ [] = PW.[]
-  [+]-𝟎ˡ (M₀ ∷ M) = ⊕-zerosˡ M₀ PW.∷ [+]-𝟎ˡ M
-
-
-opaque
-  unfolding ≋-setoid mapRows 𝟎
-  ·-𝟎ʳ : (M : Matrix A B) →  M · 𝟎 {C} ≋ 𝟎
-  ·-𝟎ʳ [] = ≋.refl
-  ·-𝟎ʳ (M₀ ∷ M) = begin
-      [ M₀ ]′ 𝟎 ∷ M · 𝟎 ≈⟨ [-]-𝟎 M₀ PW.∷ ·-𝟎ʳ M ⟩
-      zeros ∷ 𝟎         ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-
-opaque
-  unfolding Matrix zeros ≊-setoid _∷′_ ⟨⟩
-  [zeros]- : (M : Matrix A B) → [ zeros ]′ M ≊ zeros
-  [zeros]- {zero} M rewrite []ᵥ-! M = ≊.reflexive ([-]-[]ᵥ zeros)
-  [zeros]- {suc A} M
-    rewrite ≡.sym (head-∷-tailₕ M)
-    using M₀ ← headₕ M
-    using M ← tailₕ M = begin
-      [ zeros ]′ (M₀ ∷ₕ M)      ≡⟨ [-]-∷ₕ zeros M₀ M ⟩
-      zeros ∙ M₀ ∷ [ zeros ]′ M ≈⟨ ∙-zerosˡ M₀ PW.∷ [zeros]- M ⟩
-      0# ∷ zeros                ∎
-    where
-      open ≈-Reasoning (≊-setoid _)
-
-opaque
-  unfolding ≋-setoid mapRows 𝟎 _ᵀ []ᵥ
-  ·-𝟎ˡ : (M : Matrix A B) →  𝟎 {B} {C} · M ≋ 𝟎
-  ·-𝟎ˡ {A} {B} {zero} M = PW.[]
-  ·-𝟎ˡ {A} {B} {suc C} M = [zeros]- M PW.∷ ·-𝟎ˡ M
-
-opaque
-  unfolding ≋-setoid
-  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 ·-identityʳ (·-𝟎ʳ N) ⟩
-      M [+] 𝟎             ≈⟨ [+]-𝟎ʳ M ⟩
-      M ∎
-    where
-      open ≈-Reasoning (≋-setoid A C)
-
-opaque
-  unfolding ≋-setoid
-  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) ·-identityʳ ⟩
-      𝟎 [+] N             ≈⟨ [+]-𝟎ˡ N ⟩
-      N ∎
-    where
-      open ≈-Reasoning (≋-setoid 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
-
-opaque
-  unfolding _≋_ _∷ₕ_
-  ∷ₕ-cong : {V V′ : Vector B} {M M′ : Matrix A B} → V ≊ V′ → M ≋ M′ → V ∷ₕ M ≋ V′ ∷ₕ M′
-  ∷ₕ-cong PW.[] PW.[] = PW.[]
-  ∷ₕ-cong (≈x PW.∷ ≊V) (≊M₀ PW.∷ ≋M) = (≈x PW.∷ ≊M₀) PW.∷ (∷ₕ-cong ≊V ≋M)
-
-opaque
-  unfolding Vector
-  head′ : Vector (suc A) → R
-  head′ = head
-
-opaque
-  unfolding Vector
-  tail′ : Vector (suc A) → Vector A
-  tail′ = tail
-
-opaque
-  unfolding _≊_ head′
-  head-cong : {V V′ : Vector (suc A)} → V ≊ V′ → head′ V ≈ head′ V′
-  head-cong (≈x PW.∷ _) = ≈x
-
-opaque
-  unfolding _≊_ tail′
-  tail-cong : {V V′ : Vector (suc A)} → V ≊ V′ → tail′ V ≊ tail′ V′
-  tail-cong (_ PW.∷ ≊V) = ≊V
-
-opaque
-  unfolding _≋_ headₕ head′
-  ≋headₕ : {M M′ : Matrix (suc A) B} → M ≋ M′ → headₕ M ≊ headₕ M′
-  ≋headₕ M≋M′ = PW.map⁺ head-cong M≋M′
-
-opaque
-  unfolding _≋_ tailₕ tail′
-  ≋tailₕ : {M M′ : Matrix (suc A) B} → M ≋ M′ → tailₕ M ≋ tailₕ M′
-  ≋tailₕ M≋M′ = PW.map⁺ tail-cong M≋M′
-
-opaque
-  unfolding _≋_ _≊_ _∷ₕ_
-  _≋∷ₕ_ : {V V′ : Vector B} → V ≊ V′ → {M M′ : Matrix A B} → M ≋ M′ → V ∷ₕ M ≋ V′ ∷ₕ M′
-  _≋∷ₕ_ PW.[] PW.[] = PW.[]
-  _≋∷ₕ_ (≈x PW.∷ ≊V) (≊M₀ PW.∷ ≋M) = (≈x PW.∷ ≊M₀) PW.∷ (≊V ≋∷ₕ ≋M)
-
-opaque
-  unfolding _≋_ _∥_ []ᵥ _∷ₕ_
-  ∥-cong : {M M′ : Matrix A C} {N N′ : Matrix B C} → M ≋ M′ → N ≋ N′ → M ∥ N ≋ M′ ∥ N′
-  ∥-cong {zero} {C} {B} {M} {M′} {N} {N′} ≋M ≋N
-    rewrite []ᵥ-! M
-    rewrite []ᵥ-! M′ = begin
-      ([]ᵥ ∥ N)   ≡⟨ []ᵥ-∥ N ⟩
-      N           ≈⟨ ≋N ⟩
-      N′          ≡⟨ []ᵥ-∥ N′ ⟨
-      ([]ᵥ ∥ N′)  ∎
-    where
-      open ≈-Reasoning (≋-setoid _ _)
-  ∥-cong {suc A} {C} {B} {M} {M′} {N} {N′} ≋M ≋N
-    rewrite ≡.sym (head-∷-tailₕ M)
-    using M₀ ← headₕ M
-    using M- ← tailₕ M
-    rewrite ≡.sym (head-∷-tailₕ M′)
-    using M₀′ ← headₕ M′
-    using M-′ ← tailₕ M′ = begin
-      (M₀ ∷ₕ M-) ∥ N     ≡⟨ ∷ₕ-∥ M₀ M- N ⟨
-      M₀ ∷ₕ M- ∥ N       ≈⟨ ∷ₕ-cong ≊M₀ (∥-cong ≋M- ≋N) ⟩
-      M₀′ ∷ₕ M-′ ∥ N′    ≡⟨ ∷ₕ-∥ M₀′ M-′ N′ ⟩
-      (M₀′ ∷ₕ M-′) ∥ N′  ∎
-    where
-      ≊M₀ : M₀ ≊ M₀′
-      ≊M₀ = begin
-          headₕ M             ≡⟨ ≡.cong headₕ (head-∷-tailₕ M) ⟨
-          headₕ (M₀ ∷ₕ M-)    ≈⟨ ≋headₕ ≋M ⟩
-          headₕ (M₀′ ∷ₕ M-′)  ≡⟨ ≡.cong headₕ (head-∷-tailₕ M′) ⟩
-          headₕ M′            ∎
-        where
-          open ≈-Reasoning (≊-setoid _)
-      ≋M- : M- ≋ M-′
-      ≋M- = begin
-          tailₕ M             ≡⟨ ≡.cong tailₕ (head-∷-tailₕ M) ⟨
-          tailₕ (M₀ ∷ₕ M-)    ≈⟨ ≋tailₕ ≋M ⟩
-          tailₕ (M₀′ ∷ₕ M-′)  ≡⟨ ≡.cong tailₕ (head-∷-tailₕ M′) ⟩
-          tailₕ M′            ∎
-        where
-          open ≈-Reasoning (≋-setoid _ _)
-      open ≈-Reasoning (≋-setoid _ _)
-
-opaque
-  unfolding _≋_ _≑_
-  ≑-cong : {M M′ : Matrix A B} {N N′ : Matrix A C} → M ≋ M′ → N ≋ N′ → M ≑ N ≋ M′ ≑ N′
-  ≑-cong PW.[] ≋N = ≋N
-  ≑-cong (M₀≊M₀′ PW.∷ ≋M) ≋N = M₀≊M₀′ PW.∷ ≑-cong ≋M ≋N
-
-opaque
-  unfolding ≋-setoid
-  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 (≋-setoid (A ℕ.+ B) C)
-
-coproduct : Coproduct A B
-coproduct {A} {B} = record
-    { A+B = A ℕ.+ B
-    ; i₁ = I ≑ 𝟎
-    ; i₂ = 𝟎 ≑ I
-    ; [_,_] = _∥_
-    ; inject₁ = λ {a} {b} {c} → inj₁ b c
-    ; inject₂ = λ {a} {b} {c} → inj₂ b c
-    ; unique = λ eq₁ eq₂ → uniq _ _ _ eq₁ eq₂
-    }
-
-opaque
-  unfolding _≋_
-  !-unique : (E : Matrix 0 B) → []ᵥ ≋ E
-  !-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E))
-
-initial : Initial
-initial = record
-    { ⊥ = 0
-    ; ⊥-is-initial = record
-        { ! = []ᵥ
-        ; !-unique = !-unique
-        }
-    }
-
-Mat-Cocartesian : Cocartesian
-Mat-Cocartesian = record
-    { initial = initial
-    ; coproducts = record
-        { coproduct = coproduct
-        }
-    }