diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-10-11 22:59:21 -0700 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-10-11 22:59:21 -0700 |
| commit | 7cb4f160835178d06e0c0bf9802c3cad6d48a9d0 (patch) | |
| tree | 824730560ce0c3d1b08267a6b46da9daf23384c1 /Data/Matrix/Dagger-2-Poset.agda | |
| parent | 4e6acbf8b8084bea12327683aceb300a9b64c367 (diff) | |
Add hom-set addition to semiadditive recordmain
Diffstat (limited to 'Data/Matrix/Dagger-2-Poset.agda')
| -rw-r--r-- | Data/Matrix/Dagger-2-Poset.agda | 24 |
1 files changed, 1 insertions, 23 deletions
diff --git a/Data/Matrix/Dagger-2-Poset.agda b/Data/Matrix/Dagger-2-Poset.agda index 1b7b07f..319b4f9 100644 --- a/Data/Matrix/Dagger-2-Poset.agda +++ b/Data/Matrix/Dagger-2-Poset.agda @@ -45,32 +45,10 @@ opaque [+]-idem [] = PW.[] [+]-idem (M₀ ∷ M) = ⊕-idem M₀ PW.∷ [+]-idem M -+-[+] : (M N : Matrix A B) → (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (N · (𝟎 ∥ I))) · (I ≑ I) ≋ M [+] N -+-[+] M N = begin - (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (N · (𝟎 ∥ I))) · (I ≑ I) ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · (h₁ ≑ h₂) · (I ≑ I)) (·-∥ M I 𝟎) (·-∥ N 𝟎 I) ⟩ - (I ∥ I) · ((M · I) ∥ (M · 𝟎) ≑ (N · 𝟎) ∥ (N · I)) · (I ≑ I) ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ (≑-cong (∥-cong ·-Iʳ (·-𝟎ʳ M)) (∥-cong (·-𝟎ʳ N) ·-Iʳ)) ≋.refl) ⟩ - (I ∥ I) · ((M ∥ 𝟎) ≑ (𝟎 ∥ N)) · (I ≑ I) ≡⟨ ≡.cong ((I ∥ I) ·_) (≑-· (M ∥ 𝟎) (𝟎 ∥ N) (I ≑ I)) ⟩ - (I ∥ I) · (((M ∥ 𝟎) · (I ≑ I)) ≑ ((𝟎 ∥ N) · (I ≑ I))) ≈⟨ ∥-·-≑ I I ((M ∥ 𝟎) · (I ≑ I)) ((𝟎 ∥ N) · (I ≑ I)) ⟩ - (I · (M ∥ 𝟎) · (I ≑ I)) [+] (I · (𝟎 ∥ N) · (I ≑ I)) ≈⟨ [+]-cong ·-Iˡ ·-Iˡ ⟩ - ((M ∥ 𝟎) · (I ≑ I)) [+] ((𝟎 ∥ N) · (I ≑ I)) ≈⟨ [+]-cong (∥-·-≑ M 𝟎 I I) (∥-·-≑ 𝟎 N I I) ⟩ - ((M · I) [+] (𝟎 · I)) [+] ((𝟎 · I) [+] (N · I)) ≈⟨ [+]-cong ([+]-cong ·-Iʳ ·-Iʳ) ([+]-cong ·-Iʳ ·-Iʳ) ⟩ - (M [+] 𝟎) [+] (𝟎 [+] N) ≈⟨ [+]-cong ([+]-𝟎ʳ M) ([+]-𝟎ˡ N) ⟩ - M [+] N ∎ - 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 ⟩ - M [+] M ≈⟨ [+]-idem M ⟩ - M ∎ - where - open ≈-Reasoning (Matrixₛ _ _) - Mat-IdempotentSemiadditiveDagger : IdempotentSemiadditiveDagger Mat Mat-IdempotentSemiadditiveDagger = record { semiadditiveDagger = Mat-SemiadditiveDagger - ; idempotent = idem _ + ; idempotent = [+]-idem _ } open IdempotentSemiadditiveDagger Mat-IdempotentSemiadditiveDagger |