aboutsummaryrefslogtreecommitdiff
path: root/Data/Matrix
diff options
context:
space:
mode:
Diffstat (limited to 'Data/Matrix')
-rw-r--r--Data/Matrix/FreeSemimodule.agda193
-rw-r--r--Data/Matrix/Monoid.agda21
-rw-r--r--Data/Matrix/Raw.agda3
-rw-r--r--Data/Matrix/Semiadditive.agda8
-rw-r--r--Data/Matrix/Transform.agda64
5 files changed, 274 insertions, 15 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⟩ [_]_
generated by cgit v1.2.3 (git 2.39.1) at 2026-09-04 08:33:54 +0000