diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-07 13:09:11 -0700 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-07 13:09:11 -0700 |
| commit | 61549e3d703bdc5a017833a01febb9c46d95ec17 (patch) | |
| tree | 7b3aabbe8ddb5d2316cb24368edde212e27d8c1a /Data/Matrix/Dagger-2-Poset.agda | |
| parent | be685059304423e5a5cbb176b44aef1a4a76325b (diff) | |
Update matrices and vectors
Diffstat (limited to 'Data/Matrix/Dagger-2-Poset.agda')
| -rw-r--r-- | Data/Matrix/Dagger-2-Poset.agda | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/Data/Matrix/Dagger-2-Poset.agda b/Data/Matrix/Dagger-2-Poset.agda index cddf183..0cda1ee 100644 --- a/Data/Matrix/Dagger-2-Poset.agda +++ b/Data/Matrix/Dagger-2-Poset.agda @@ -16,10 +16,11 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Category.Dagger.2-Poset using (dagger-2-poset; Dagger-2-Poset) open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) open import Data.Matrix.Category R.semiring using (Mat; _·_; ·-Iˡ; ·-Iʳ; ·-resp-≋; ·-assoc; ∥-·-≑; ·-∥; ·-𝟎ˡ; ≑-·) -open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; _∥_; _≑_; _ᵀ; module ≋; ∥-cong; ≑-cong) +open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; module ≋; ∥-cong; ≑-cong) open import Data.Matrix.Monoid R.+-monoid using (𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ) -open import Data.Matrix.Transform R.semiring using (I; Iᵀ) +open import Data.Matrix.Raw using (_∥_; _≑_; _ᵀ) open import Data.Matrix.SemiadditiveDagger R using (∥-ᵀ; Mat-SemiadditiveDagger) +open import Data.Matrix.Transform R.semiring using (I; Iᵀ) open import Data.Nat using (ℕ) open import Data.Vec using (Vec) open import Data.Vector.Core R.setoid using (Vector; _≊_) @@ -33,7 +34,7 @@ private A B : ℕ opaque - unfolding _≊_ _⊕_ + unfolding _⊕_ ⊕-idem : (V : Vector A) → V ⊕ V ≊ V ⊕-idem [] = PW.[] ⊕-idem (v ∷ V) = +-idem v PW.∷ ⊕-idem V |