diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-13 00:57:08 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-13 00:57:08 -0500 |
| commit | 154ad08032f9719b0ad32aa357742fe12ff4899a (patch) | |
| tree | eca96e985fd493c93165b188c07f5b9af884babc /Data/Matrix/Monoid.agda | |
| parent | 1e73f2658f6d8d1559649b2cd97040f494dc1c96 (diff) | |
Show free semimodule functor is cartesian
Diffstat (limited to 'Data/Matrix/Monoid.agda')
| -rw-r--r-- | Data/Matrix/Monoid.agda | 21 |
1 files changed, 16 insertions, 5 deletions
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}) = []ᵥ-∥ 𝟎 |