diff options
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 aff22d7..1b7b07f 100644 --- a/Data/Matrix/Dagger-2-Poset.agda +++ b/Data/Matrix/Dagger-2-Poset.agda @@ -13,7 +13,7 @@ module Data.Matrix.Dagger-2-Poset import Data.Vec.Relation.Binary.Pointwise.Inductive as PW import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -open import Category.Dagger.2-Poset using (dagger-2-poset; Dagger-2-Poset) +open import Category.Dagger.2-Poset using (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) @@ -59,7 +59,6 @@ opaque where open ≈-Reasoning (Matrixₛ _ _) - idem : (M : Matrix A B) → (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (M · (𝟎 ∥ I))) · (I ≑ I) ≋ M idem M = begin (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (M · (𝟎 ∥ I))) · (I ≑ I) ≈⟨ +-[+] M M ⟩ @@ -74,5 +73,7 @@ Mat-IdempotentSemiadditiveDagger = record ; idempotent = idem _ } +open IdempotentSemiadditiveDagger Mat-IdempotentSemiadditiveDagger + Mat-Dagger-2-Poset : Dagger-2-Poset -Mat-Dagger-2-Poset = dagger-2-poset Mat-IdempotentSemiadditiveDagger +Mat-Dagger-2-Poset = dagger-2-poset |