aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Category/BinaryBiproducts.agda6
-rw-r--r--Category/Dagger/Semiadditive.agda507
-rw-r--r--Category/Semiadditive.agda20
-rw-r--r--Data/Matrix/Dagger-2-Poset.agda34
-rw-r--r--Data/Matrix/SemiadditiveDagger.agda430
5 files changed, 312 insertions, 685 deletions
diff --git a/Category/BinaryBiproducts.agda b/Category/BinaryBiproducts.agda
index 5b59df4..790c73a 100644
--- a/Category/BinaryBiproducts.agda
+++ b/Category/BinaryBiproducts.agda
@@ -54,6 +54,12 @@ record BinaryBiproducts : Set (levelOfTerm π’ž) where
open β‡’-Reasoning π’ž
open HomReasoning
+ ×₁-congΛ‘ : {A B C D : Obj} β†’ {f : A β‡’ B} {g h : C β‡’ D} β†’ g β‰ˆ h β†’ f ×₁ g β‰ˆ f ×₁ h
+ ×₁-congΛ‘ gβ‰ˆh = ×₁-congβ‚‚ Equiv.refl gβ‰ˆh
+
+ ×₁-congΚ³ : {A B C D : Obj} β†’ {f g : A β‡’ B} {h : C β‡’ D} β†’ f β‰ˆ g β†’ f ×₁ h β‰ˆ g ×₁ h
+ ×₁-congΚ³ fβ‰ˆg = ×₁-congβ‚‚ fβ‰ˆg Equiv.refl
+
π₁iβ‚‚β‰ˆΟ€β‚‚i₁ : {A B : Obj} β†’ π₁ ∘ iβ‚‚ β‰ˆ Ο€β‚‚Β {A} {B} ∘ i₁
π₁iβ‚‚β‰ˆΟ€β‚‚i₁ {A} {B} = begin
π₁ ∘ iβ‚‚ β‰ˆβŸ¨ identityΚ³ ⟨
diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda
index e8a9b39..a5b03ab 100644
--- a/Category/Dagger/Semiadditive.agda
+++ b/Category/Dagger/Semiadditive.agda
@@ -5,446 +5,77 @@ open import Categories.Category using (Category)
module Category.Dagger.Semiadditive {o β„“ e : Level} (π’ž : Category o β„“ e) where
-import Categories.Category.Monoidal.Reasoning as βŠ—-Reasoning
-import Categories.Morphism.Reasoning as β‡’-Reasoning
+import Categories.Morphism.Reasoning π’ž as β‡’-Reasoning
-open import Categories.Category.BinaryProducts π’ž using (BinaryProducts)
-open import Categories.Category.Cartesian π’ž using (Cartesian)
-open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
-open import Categories.Category.Cocartesian π’ž using (Cocartesian)
-open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
-open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal)
open import Categories.Category.Dagger using (HasDagger)
-open import Categories.Category.Monoidal using (Monoidal)
-open import Categories.Category.Monoidal.Symmetric using (module Symmetric)
-open import Categories.Category.Monoidal.Symmetric.Properties using () renaming (module Shorthands to Οƒ-Shorthands)
-open import Categories.Category.Monoidal.Utilities using (module Shorthands)
-open import Categories.Functor using (Functor)
-open import Categories.Object.Duality using (Coproduct⇒coProduct)
-open import Categories.Object.Terminal π’ž using (Terminal)
+open import Category.Semiadditive using (Semiadditive)
open import Relation.Binary using (Rel)
-record DaggerCocartesianMonoidal : Set (suc (o βŠ” β„“ βŠ” e)) where
+record SemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where
field
- cocartesian : Cocartesian
+ semiadditive : Semiadditive π’ž
dagger : HasDagger π’ž
- open Cocartesian cocartesian using (i₁; iβ‚‚) renaming (_+₁_ to _βŠ—β‚_)
- open CocartesianMonoidal cocartesian using (+-monoidal)
- open CocartesianSymmetricMonoidal π’ž cocartesian using (+-symmetric)
- open HasDagger dagger using (_†; isUnitary; isSelfAdjoint)
- open Shorthands +-monoidal using (Ξ»β‡’; λ⇐; ρ⇒; ρ⇐; Ξ±β‡’; α⇐)
- open Οƒ-Shorthands +-symmetric using (Οƒβ‡’)
open Category π’ž
-
- -- dagger and cocartesian monoidal structure are compatible
- field
- λ≅† : {A : Obj} β†’ Ξ»β‡’ {A} † β‰ˆ λ⇐
- ρ≅† : {A : Obj} β†’ ρ⇒ {A} † β‰ˆ ρ⇐
- α≅† : {A B C : Obj} β†’ Ξ±β‡’ {A} {B} {C} † β‰ˆ α⇐
- σ≅† : {A B : Obj} β†’ Οƒβ‡’ {A} {B} † β‰ˆ Οƒβ‡’
- †-resp-βŠ— : {A B C D : Obj} {f : A β‡’ B} {g : C β‡’ D} β†’ (f βŠ—β‚ g) † β‰ˆ (f †) βŠ—β‚ (g †)
-
-record SemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where
+ open HasDagger dagger public
+ open Semiadditive semiadditive public
field
- daggerCocartesianMonoidal : DaggerCocartesianMonoidal
-
- open DaggerCocartesianMonoidal daggerCocartesianMonoidal public
- open Cocartesian cocartesian using ([]∘+-assocΚ³; []∘+-swap) renaming (_+_ to _βŠ•β‚€_; _+₁_ to infixr 10 _βŠ•β‚_; -+- to βŠ•) public
- open CocartesianMonoidal cocartesian using (+-monoidal) public
- open Cocartesian cocartesian using (i₁; iβ‚‚; Β‘) public
- open Cocartesian cocartesian using (βŠ₯; [_,_]; ∘[]; []∘+₁; []-congΛ‘; []-congβ‚‚; coproduct; Β‘-unique; inject₁; injectβ‚‚; +-unique; +-Ξ·) renaming (βˆ‡βˆ˜+₁ to β–½βˆ˜+₁)
- open CocartesianSymmetricMonoidal π’ž cocartesian using (+-symmetric)
- open HasDagger dagger using (_†; †-involutive; ⟨_βŸ©β€ ; †-identity; †-homomorphism) public
- open Monoidal +-monoidal using (unitorΛ‘-commute-from; unitorΚ³-commute-from; assoc-commute-from; module unitorΛ‘; module unitorΚ³; module associator)
- open Οƒ-Shorthands +-symmetric using (Οƒβ‡’)
- open Symmetric +-symmetric using (module braiding)
- open Shorthands +-monoidal using (Ξ»β‡’; λ⇐; ρ⇒; ρ⇐; Ξ±β‡’; α⇐)
- open Category π’ž
-
- module βŠ• = Functor βŠ•
-
- -- projection maps
- p₁ : {A B : Obj} β†’ A βŠ•β‚€ B β‡’ A
- p₁ = i₁ †
-
- pβ‚‚ : {A B : Obj} β†’ A βŠ•β‚€ B β‡’ B
- pβ‚‚ = iβ‚‚ †
-
- -- codiagonal
- β–½ : {A : Obj} β†’ A βŠ•β‚€ A β‡’ A
- β–½ = [ id , id ]
-
- -- diagonal
- β–³ : {A : Obj} β†’ A β‡’ A βŠ•β‚€ A
- β–³ = β–½ †
-
- open βŠ—-Reasoning +-monoidal
- open β‡’-Reasoning π’ž
-
- β–½-assoc : {A : Obj} β†’ β–½ {A} ∘ β–½ βŠ•β‚ id β‰ˆ β–½ ∘ id βŠ•β‚ β–½ ∘ Ξ±β‡’
- β–½-assoc = begin
- [ id , id ] ∘ [ id , id ] βŠ•β‚ id β‰ˆβŸ¨ []∘+₁ ⟩
- [ id ∘ [ id , id ] , id ∘ id ] β‰ˆβŸ¨ []-congβ‚‚ identityΛ‘ identityΛ‘ ⟩
- [ [ id , id ] , id ] β‰ˆβŸ¨ []∘+-assocΚ³ ⟨
- [ id , [ id , id ] ] ∘ Ξ±β‡’ β‰ˆβŸ¨ []-congβ‚‚ identityΛ‘ identityΛ‘ ⟩∘⟨refl ⟨
- [ id ∘ id , id ∘ [ id , id ] ] ∘ Ξ±β‡’ β‰ˆβŸ¨ pushΛ‘ (Equiv.sym []∘+₁) ⟩
- [ id , id ] ∘ id βŠ•β‚ [ id , id ] ∘ Ξ±β‡’ ∎
-
- β–³-assoc : {A : Obj} β†’ id βŠ•β‚ β–³ ∘ β–³ {A} β‰ˆ Ξ±β‡’ ∘ β–³ βŠ•β‚ id ∘ β–³
- β–³-assoc = begin
- id βŠ•β‚ β–³ ∘ β–³ β‰ˆβŸ¨ †-involutive (id βŠ•β‚ β–³ ∘ β–³) ⟨
- (id βŠ•β‚ β–³ ∘ β–³) † † β‰ˆβŸ¨ ⟨ †-homomorphism βŸ©β€  ⟩
- (β–³ † ∘ (id βŠ•β‚ β–³) †) † β‰ˆβŸ¨ ⟨ (†-involutive β–½ ⟩∘⟨ †-resp-βŠ—) βŸ©β€  ⟩
- (β–½ ∘ (id †) βŠ•β‚ (β–³ †)) † β‰ˆβŸ¨ ⟨ refl⟩∘⟨ †-identity βŸ©βŠ—βŸ¨ †-involutive β–½ βŸ©β€  ⟩
- (β–½ ∘ id βŠ•β‚ β–½) † β‰ˆβŸ¨ ⟨ refl⟩∘⟨ introΚ³ associator.isoΚ³ βŸ©β€  ⟩
- (β–½ ∘ id βŠ•β‚ β–½ ∘ Ξ±β‡’ ∘ α⇐) † β‰ˆβŸ¨ ⟨ refl⟩∘⟨ assoc βŸ©β€  ⟨
- (β–½ ∘ (id βŠ•β‚ β–½ ∘ Ξ±β‡’) ∘ α⇐) † β‰ˆβŸ¨ ⟨ extendΚ³ β–½-assoc βŸ©β€  ⟨
- (β–½ ∘ β–½ βŠ•β‚ id ∘ α⇐) † β‰ˆβŸ¨ †-homomorphism ⟩
- (β–½ βŠ•β‚ id ∘ α⇐) † ∘ β–½ † β‰ˆβŸ¨ pushΛ‘ †-homomorphism ⟩
- α⇐ † ∘ (β–½ βŠ•β‚ id) † ∘ β–³ β‰ˆβŸ¨ ⟨ α≅† βŸ©β€  ⟩∘⟨refl ⟨
- Ξ±β‡’ † † ∘ (β–½ βŠ•β‚ id) † ∘ β–³ β‰ˆβŸ¨ †-involutive Ξ±β‡’ ⟩∘⟨refl ⟩
- Ξ±β‡’ ∘ (β–½ βŠ•β‚ id) † ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ †-resp-βŠ— ⟩∘⟨refl ⟩
- Ξ±β‡’ ∘ (β–½ †) βŠ•β‚ (id †) ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ reflβŸ©βŠ—βŸ¨ †-identity ⟩∘⟨refl ⟩
- Ξ±β‡’ ∘ β–³ βŠ•β‚ id ∘ β–³ ∎
-
- ! : {A : Obj} β†’ A β‡’ βŠ₯
- ! = Β‘ †
-
- β–½-identityΛ‘ : {A : Obj} β†’ β–½ {A} ∘ Β‘ βŠ•β‚ id β‰ˆ Ξ»β‡’
- β–½-identityΛ‘ = begin
- [ id , id ] ∘ Β‘ βŠ•β‚ id β‰ˆβŸ¨ []∘+₁ ⟩
- [ id ∘ Β‘ , id ∘ id ] β‰ˆβŸ¨ []-congβ‚‚ identityΛ‘ identityΒ² ⟩
- [ ‘ , id ] ∎
-
- β–³-identityΛ‘ : {A : Obj} β†’ ! {A} βŠ•β‚ id ∘ β–³ β‰ˆ λ⇐
- β–³-identityΛ‘ = begin
- ! βŠ•β‚ id ∘ β–³ β‰ˆβŸ¨ reflβŸ©βŠ—βŸ¨ †-identity ⟩∘⟨refl ⟨
- (Β‘ †) βŠ•β‚ (id †) ∘ β–½ † β‰ˆβŸ¨ †-resp-βŠ— ⟩∘⟨refl ⟨
- (Β‘ βŠ•β‚ id) † ∘ β–½ † β‰ˆβŸ¨ †-homomorphism ⟨
- (β–½ ∘ Β‘ βŠ•β‚ id) † β‰ˆβŸ¨ ⟨ β–½-identityΛ‘ βŸ©β€  ⟩
- Ξ»β‡’ † β‰ˆβŸ¨ λ≅† ⟩
- λ⇐ ∎
-
- β–½-identityΚ³ : {A : Obj} β†’ β–½ {A} ∘ id βŠ•β‚ Β‘ β‰ˆ ρ⇒
- β–½-identityΚ³ = begin
- [ id , id ] ∘ id βŠ•β‚ Β‘ β‰ˆβŸ¨ []∘+₁ ⟩
- [ id ∘ id , id ∘ Β‘ ] β‰ˆβŸ¨ []-congβ‚‚ identityΒ² identityΛ‘ ⟩
- [ id , ‘ ] ∎
-
- β–³-identityΚ³ : {A : Obj} β†’ id {A} βŠ•β‚ ! ∘ β–³ β‰ˆ ρ⇐
- β–³-identityΚ³ = begin
- id βŠ•β‚ (Β‘ †) ∘ β–½ † β‰ˆβŸ¨ †-identity βŸ©βŠ—βŸ¨refl ⟩∘⟨refl ⟨
- (id †) βŠ•β‚ (Β‘ †) ∘ β–½ † β‰ˆβŸ¨ †-resp-βŠ— ⟩∘⟨refl ⟨
- (id βŠ•β‚ Β‘) † ∘ β–½ † β‰ˆβŸ¨ †-homomorphism ⟨
- (β–½ ∘ id βŠ•β‚ Β‘) † β‰ˆβŸ¨ ⟨ β–½-identityΚ³ βŸ©β€  ⟩
- ρ⇒ † β‰ˆβŸ¨ ρ≅† ⟩
- ρ⇐  ∎
-
- β–½-comm : {A : Obj} β†’ β–½ {A} ∘ Οƒβ‡’ β‰ˆ β–½
- β–½-comm = []∘+-swap
-
- β–³-comm : {A : Obj} β†’ Οƒβ‡’ ∘ β–³ {A} β‰ˆ β–³
- β–³-comm = begin
- Οƒβ‡’ ∘ β–½ † β‰ˆβŸ¨ σ≅† ⟩∘⟨refl ⟨
- Οƒβ‡’ † ∘ β–½ † β‰ˆβŸ¨ †-homomorphism ⟨
- (β–½ ∘ Οƒβ‡’) † β‰ˆβŸ¨ ⟨ β–½-comm βŸ©β€  ⟩
- β–½ † ∎
-
- β‡’β–½ : {A B : Obj} {f : A β‡’ B} β†’ f ∘ β–½ β‰ˆ β–½ ∘ f βŠ•β‚ f
- β‡’β–½ {A} {B} {f} = begin
- f ∘ [ id , id ] β‰ˆβŸ¨ ∘[] ⟩
- [ f ∘ id , f ∘ id ] β‰ˆβŸ¨ []-congβ‚‚ identityΚ³ identityΚ³ ⟩
- [ f , f ] β‰ˆβŸ¨ []-congβ‚‚ identityΛ‘ identityΛ‘ ⟨
- [ id ∘ f , id ∘ f ] β‰ˆβŸ¨ []∘+₁ ⟨
- [ id , id ] ∘ f βŠ•β‚ f ∎
-
- β‡’β–³ : {A B : Obj} {f : A β‡’ B} β†’ β–³ ∘ f β‰ˆ f βŠ•β‚ f ∘ β–³
- β‡’β–³ {A} {B} {f} = begin
- β–½ † ∘ f β‰ˆβŸ¨ refl⟩∘⟨ †-involutive f ⟨
- β–½ † ∘ f † † β‰ˆβŸ¨ †-homomorphism ⟨
- (f † ∘ β–½) † β‰ˆβŸ¨ ⟨ β‡’β–½ βŸ©β€  ⟩
- (β–½ ∘ (f †) βŠ•β‚ (f †)) † β‰ˆβŸ¨ †-homomorphism ⟩
- ((f †) βŠ•β‚ (f †)) † ∘ β–½ † β‰ˆβŸ¨ †-resp-βŠ— ⟩∘⟨refl ⟩
- (f † †) βŠ•β‚ (f † †) ∘ β–½ † β‰ˆβŸ¨ †-involutive f βŸ©βŠ—βŸ¨ †-involutive f ⟩∘⟨refl ⟩
- f βŠ•β‚ f ∘ β–½ † ∎
-
- β‡’Β‘ : {A B : Obj} {f : A β‡’ B} β†’ f ∘ Β‘ β‰ˆ Β‘
- β‡’Β‘ {A} {B} {f} = Equiv.sym (Β‘-unique (f ∘ Β‘))
-
- β‡’! : {A B : Obj} {f : A β‡’ B} β†’ ! ∘ f β‰ˆ !
- β‡’! {A} {B} {f} = begin
- Β‘ † ∘ f β‰ˆβŸ¨ refl⟩∘⟨ †-involutive f ⟨
- Β‘ † ∘ f † † β‰ˆβŸ¨ †-homomorphism ⟨
- (f † ∘ Β‘) † β‰ˆβŸ¨ ⟨ β‡’Β‘ βŸ©β€  ⟩
- Β‘ † ∎
-
- Οβ‡β‰ˆi₁ : {A : Obj} β†’ ρ⇐ {A} β‰ˆ i₁
- Οβ‡β‰ˆi₁ = Equiv.refl
-
- Ξ»β‡β‰ˆiβ‚‚ : {A : Obj} β†’ λ⇐ {A} β‰ˆ iβ‚‚
- Ξ»β‡β‰ˆiβ‚‚ = Equiv.refl
-
- Ξ»β‡’β‰ˆpβ‚‚ : {A : Obj} β†’ Ξ»β‡’ {A} β‰ˆ pβ‚‚
- Ξ»β‡’β‰ˆpβ‚‚ = begin
- Ξ»β‡’ β‰ˆβŸ¨ †-involutive Ξ»β‡’ ⟨
- Ξ»β‡’ † † β‰ˆβŸ¨ ⟨ λ≅† βŸ©β€  ⟩
- λ⇐ † β‰ˆβŸ¨ ⟨ Ξ»β‡β‰ˆiβ‚‚ βŸ©β€  ⟩
- iβ‚‚ † ∎
-
- Οβ‡’β‰ˆp₁ : {A : Obj} β†’ ρ⇒ {A} β‰ˆ p₁
- Οβ‡’β‰ˆp₁ = begin
- ρ⇒ β‰ˆβŸ¨ †-involutive ρ⇒ ⟨
- ρ⇒ † † β‰ˆβŸ¨ ⟨ ρ≅† βŸ©β€  ⟩
- ρ⇐ † β‰ˆβŸ¨ ⟨ Οβ‡β‰ˆi₁ βŸ©β€  ⟩
- i₁ † ∎
-
- i₁-βŠ• : {A B : Obj} β†’ i₁ {A} {B} β‰ˆ id βŠ•β‚ Β‘ ∘ ρ⇐
- i₁-βŠ• = begin
- i₁ β‰ˆβŸ¨ identityʳ ⟨
- i₁ ∘ id β‰ˆβŸ¨ inject₁ ⟨
- id βŠ•β‚ Β‘ ∘ i₁ β‰ˆβŸ¨ refl⟩∘⟨ Οβ‡β‰ˆi₁ ⟨
- id βŠ•β‚ Β‘ ∘ ρ⇐ ∎
-
- iβ‚‚-βŠ• : {A B : Obj} β†’ iβ‚‚ {A} {B} β‰ˆ Β‘ βŠ•β‚ id ∘ λ⇐
- iβ‚‚-βŠ• = begin
- iβ‚‚ β‰ˆβŸ¨ identityΚ³ ⟨
- iβ‚‚ ∘ id β‰ˆβŸ¨ injectβ‚‚ ⟨
- Β‘ βŠ•β‚ id ∘ iβ‚‚ β‰ˆβŸ¨ refl⟩∘⟨ Ξ»β‡β‰ˆiβ‚‚ ⟨
- Β‘ βŠ•β‚ id ∘ λ⇐ ∎
-
- p₁-βŠ• : {A B : Obj} β†’ p₁ {A} {B} β‰ˆ ρ⇒ ∘ id βŠ•β‚ !
- p₁-βŠ• {A} {B} = begin
- i₁ † β‰ˆβŸ¨ ⟨ i₁-βŠ• βŸ©β€  ⟩
- (id βŠ•β‚ Β‘ ∘ ρ⇐) † β‰ˆβŸ¨ †-homomorphism ⟩
- ρ⇐ † ∘ (id βŠ•β‚ Β‘) † β‰ˆβŸ¨ refl⟩∘⟨ †-resp-βŠ— ⟩
- ρ⇐ † ∘ (id †) βŠ•β‚ (Β‘ †) β‰ˆβŸ¨ ⟨ ρ≅† βŸ©β€  ⟩∘⟨refl ⟨
- ρ⇒ † † ∘ (id †) βŠ•β‚ (Β‘ †) β‰ˆβŸ¨ †-involutive ρ⇒ ⟩∘⟨ †-identity βŸ©βŠ—βŸ¨refl ⟩
- ρ⇒ ∘ id βŠ•β‚ (Β‘ †) ∎
-
- pβ‚‚-βŠ• : {A B : Obj} β†’ pβ‚‚ {A} {B} β‰ˆ Ξ»β‡’ ∘ ! βŠ•β‚ id
- pβ‚‚-βŠ• {A} {B} = begin
- iβ‚‚ † β‰ˆβŸ¨ ⟨ iβ‚‚-βŠ• βŸ©β€  ⟩
- (Β‘ βŠ•β‚ id ∘ λ⇐) † β‰ˆβŸ¨ †-homomorphism ⟩
- λ⇐ † ∘ (Β‘ βŠ•β‚ id) † β‰ˆβŸ¨ refl⟩∘⟨ †-resp-βŠ— ⟩
- λ⇐ † ∘ (Β‘ †) βŠ•β‚ (id †) β‰ˆβŸ¨ ⟨ λ≅† βŸ©β€  ⟩∘⟨refl ⟨
- Ξ»β‡’ † † ∘ (Β‘ †) βŠ•β‚ (id †) β‰ˆβŸ¨ †-involutive Ξ»β‡’ ⟩∘⟨ reflβŸ©βŠ—βŸ¨ †-identity ⟩
- Ξ»β‡’ ∘ (Β‘ †) βŠ•β‚ id ∎
-
- β–½βˆ˜i₁ : {A : Obj} β†’ β–½ ∘ i₁ β‰ˆ id {A}
- β–½βˆ˜i₁ = begin
- β–½ ∘ i₁ β‰ˆβŸ¨ refl⟩∘⟨ i₁-βŠ• ⟩
- β–½ ∘ id βŠ•β‚ Β‘ ∘ ρ⇐ β‰ˆβŸ¨ pullΛ‘ β–½-identityΚ³ ⟩
- ρ⇒ ∘ ρ⇐ β‰ˆβŸ¨ unitorΚ³.isoΚ³ ⟩
- id ∎
-
- β–½βˆ˜iβ‚‚ : {A : Obj} β†’ β–½ ∘ iβ‚‚ β‰ˆ id {A}
- β–½βˆ˜iβ‚‚ = begin
- β–½ ∘ iβ‚‚ β‰ˆβŸ¨ refl⟩∘⟨ iβ‚‚-βŠ• ⟩
- β–½ ∘ Β‘ βŠ•β‚ id ∘ λ⇐ β‰ˆβŸ¨ pullΛ‘ β–½-identityΛ‘ ⟩
- Ξ»β‡’ ∘ λ⇐ β‰ˆβŸ¨ unitorΛ‘.isoΚ³ ⟩
- id ∎
-
- pβ‚βˆ˜β–³ : {A : Obj} β†’ p₁ ∘ β–³ β‰ˆ id {A}
- pβ‚βˆ˜β–³ = begin
- p₁ ∘ β–³ β‰ˆβŸ¨ pushΛ‘ p₁-βŠ• ⟩
- ρ⇒ ∘ id βŠ•β‚ ! ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ β–³-identityΚ³ ⟩
- ρ⇒ ∘ ρ⇐ β‰ˆβŸ¨ unitorΚ³.isoΚ³ ⟩
- id ∎
-
- pβ‚‚βˆ˜β–³ : {A : Obj} β†’ pβ‚‚ ∘ β–³ β‰ˆ id {A}
- pβ‚‚βˆ˜β–³ = begin
- pβ‚‚ ∘ β–³ β‰ˆβŸ¨ pushΛ‘ pβ‚‚-βŠ• ⟩
- Β  Ξ»β‡’ ∘ ! βŠ•β‚ id ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ β–³-identityΛ‘ ⟩
- Β  Ξ»β‡’ βˆ˜Β Ξ»β‡ β‰ˆβŸ¨ unitorΛ‘.isoΚ³ ⟩
- id ∎
-
- -- zero arrows
- z : {A B : Obj} β†’ A β‡’ B
- z = ‘ ∘ !
-
- field
- -- orthogonality conditions: pα΅’iβ±ΌΒ β‰ˆ Ξ΄α΅’β±Ό
- p₁-i₁ : {A B : Obj} β†’ p₁ {A} {B} ∘ i₁ β‰ˆ id {A}
- pβ‚‚-iβ‚‚ : {A B : Obj} β†’ pβ‚‚ {A} {B} ∘ iβ‚‚ β‰ˆ id {B}
- pβ‚‚-i₁ : {A B : Obj} β†’ pβ‚‚ {A} {B} ∘ i₁ β‰ˆ z {A} {B}
- p₁-iβ‚‚ : {A B : Obj} β†’ p₁ {A} {B} ∘ iβ‚‚ β‰ˆ z {B} {A}
-
- -- commutative monoid structure on homs
- module _ {A B : Obj} where
-
- _+_ : A β‡’ B β†’ A β‡’ B β†’ A β‡’ B
- _+_ f g = β–½ ∘ f βŠ•β‚ g ∘ β–³
-
- infixl 6 _+_
-
- +-associative : {f g h : A β‡’ B} β†’ (f + g) + h β‰ˆ f + (g + h)
- +-associative {f} {g} {h} = begin
- β–½ ∘ (β–½ ∘ f βŠ•β‚ g ∘ β–³) βŠ•β‚ h ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pushΛ‘ split₁ˑ ⟩
- β–½ ∘ β–½ βŠ•β‚ id ∘ (f βŠ•β‚ g ∘ β–³) βŠ•β‚ h ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ pushΛ‘ split₁ʳ ⟩
- β–½ ∘ β–½ βŠ•β‚ id ∘ (f βŠ•β‚ g) βŠ•β‚ h ∘ β–³ βŠ•β‚ id ∘ β–³ β‰ˆβŸ¨ extendΚ³ β–½-assoc ⟩
- β–½ ∘ (id βŠ•β‚ β–½ ∘ Ξ±β‡’) ∘ (f βŠ•β‚ g) βŠ•β‚ h ∘ β–³ βŠ•β‚ id ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pullΚ³ (extendΚ³ assoc-commute-from) ⟩
- β–½ ∘ id βŠ•β‚ β–½ ∘ f βŠ•β‚ g βŠ•β‚ h ∘ Ξ±β‡’ ∘ β–³ βŠ•β‚ id ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ β–³-assoc ⟨
- β–½ ∘ id βŠ•β‚ β–½ ∘ f βŠ•β‚ g βŠ•β‚ h ∘ id βŠ•β‚ β–³ ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ pullΛ‘ mergeβ‚‚Κ³ ⟩
- β–½ ∘ id βŠ•β‚ β–½ ∘ f βŠ•β‚ (g βŠ•β‚ h ∘ β–³) ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pullΛ‘ mergeβ‚‚Λ‘ ⟩
- β–½ ∘ f βŠ•β‚ (β–½ ∘ g βŠ•β‚ h ∘ β–³) ∘ β–³ ∎
-
- +-identityΛ‘ : {f : A β‡’ B} β†’ z + f β‰ˆ f
- +-identityΛ‘ {f} = begin
- β–½ ∘ (Β‘ ∘ !) βŠ•β‚ f ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pushΛ‘ split₁ˑ ⟩
- β–½ ∘ Β‘ βŠ•β‚ id ∘ ! βŠ•β‚ f ∘ β–³ β‰ˆβŸ¨ pullΛ‘ β–½-identityΛ‘ ⟩
- Ξ»β‡’ ∘ ! βŠ•β‚ f ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pushΛ‘ serialize₂₁ ⟩
- Ξ»β‡’ ∘ id βŠ•β‚ f ∘ ! βŠ•β‚ id ∘ β–³ β‰ˆβŸ¨ extendΚ³ unitorΛ‘-commute-from ⟩
- f ∘ Ξ»β‡’ ∘ ! βŠ•β‚ id ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ reflβŸ©βˆ˜βŸ¨Β β–³-identityΛ‘ ⟩
- f ∘ Ξ»β‡’ ∘ λ⇐ β‰ˆβŸ¨ elimΚ³ unitorΛ‘.isoΚ³ ⟩
- f ∎
-
- +-identityΚ³ : {f : A β‡’ B} β†’ f + z β‰ˆ f
- +-identityΚ³ {f} = begin
- β–½ ∘ f βŠ•β‚ (Β‘ ∘ !) ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pushΛ‘ splitβ‚‚Λ‘ ⟩
- β–½ ∘ id βŠ•β‚ Β‘ ∘ (f βŠ•β‚ !) ∘ β–³ β‰ˆβŸ¨ pullΛ‘ β–½-identityΚ³ ⟩
- ρ⇒ ∘ f βŠ•β‚ ! ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pushΛ‘ serialize₁₂ ⟩
- ρ⇒ ∘ f βŠ•β‚ id ∘ id βŠ•β‚ ! ∘ β–³ β‰ˆβŸ¨ extendΚ³ unitorΚ³-commute-from ⟩
- f ∘ ρ⇒ ∘ id βŠ•β‚ ! ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ β–³-identityΚ³ ⟩
- f ∘ ρ⇒ ∘ ρ⇐ β‰ˆβŸ¨ elimΚ³ unitorΚ³.isoΚ³ ⟩
- f ∎
-
- +-commutative : {f g : A β‡’ B} β†’ f + g β‰ˆ g + f
- +-commutative {f} {g} = begin
- β–½ ∘ f βŠ•β‚ g ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ β–³-comm ⟨
- β–½ ∘ f βŠ•β‚ g ∘ Οƒβ‡’ ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ extendΚ³ (braiding.β‡’.sym-commute _) ⟩
- β–½ ∘ Οƒβ‡’ ∘ g βŠ•β‚ f ∘ β–³ β‰ˆβŸ¨ pullΛ‘ β–½-comm ⟩
- β–½ ∘ g βŠ•β‚ f ∘ β–³ ∎
-
- +-cong : {f g h i : A β‡’ B} β†’ f β‰ˆ h β†’ g β‰ˆ i β†’ f + g β‰ˆ h + i
- +-cong fβ‰ˆh gβ‰ˆi = refl⟩∘⟨ fβ‰ˆh βŸ©βŠ—βŸ¨ gβ‰ˆi ⟩∘⟨refl
-
- +-congΛ‘ : {f g i : A β‡’ B} β†’ g β‰ˆ i β†’ f + g β‰ˆ f + i
- +-congΛ‘ gβ‰ˆi = +-cong Equiv.refl gβ‰ˆi
-
- +-congΚ³ : {f g h : A β‡’ B} β†’ f β‰ˆ h β†’ f + g β‰ˆ h + g
- +-congΚ³ fβ‰ˆh = +-cong fβ‰ˆh Equiv.refl
+ π₁† : {A B : Obj} β†’ π₁ {A} {B} † β‰ˆ i₁
+ π₂† : {A B : Obj} β†’ Ο€β‚‚ {A} {B} † β‰ˆ iβ‚‚
+ ⟨⟩-† : {A B C : Obj} {f : A β‡’ B} {g : A β‡’ C} β†’ ⟨ f , g ⟩ † β‰ˆ [ f † , g † ]
+
+ open HomReasoning
+ open β‡’-Reasoning
+
+ Δ† : {A : Obj} β†’ Ξ” {A} † β‰ˆ βˆ‡
+ Δ† = begin
+ ⟨ id , id ⟩ † β‰ˆβŸ¨ ⟨⟩-† ⟩
+ [ id † , id † ] β‰ˆβŸ¨ []-congβ‚‚ †-identity †-identity ⟩
+ [ id , id ] ∎
+
+ βˆ‡β€  : {A : Obj} β†’ βˆ‡ {A} † β‰ˆ Ξ”
+ βˆ‡β€  = begin
+ βˆ‡ † β‰ˆβŸ¨ ⟨ Δ† βŸ©β€  ⟨
+ Ξ” † † β‰ˆβŸ¨ †-involutive Ξ” ⟩
+ Ξ” ∎
+
+ †-resp-×₁ : {A B C D : Obj} {f : A β‡’ B} {g : C β‡’ D} β†’ (f ×₁ g) † β‰ˆ (f †) ×₁ (g †)
+ †-resp-×₁ {f = f} {g} = begin
+ ⟨ f ∘ π₁ , g ∘ Ο€β‚‚ ⟩ † β‰ˆβŸ¨ ⟨⟩-† ⟩
+ [ (f ∘ π₁) † , (g ∘ Ο€β‚‚) † ] β‰ˆβŸ¨ []-congβ‚‚ †-homomorphism †-homomorphism ⟩
+ [ π₁ † ∘ f † , Ο€β‚‚ † ∘ g † ] β‰ˆβŸ¨ []-congβ‚‚ (π₁† ⟩∘⟨refl) (π₂† ⟩∘⟨refl) ⟩
+ [ i₁ ∘ f † , iβ‚‚ ∘ g † ] β‰ˆβŸ¨ ×₁-+₁ (f †) (g †) ⟨
+ ⟨ f † ∘ π₁ , g † ∘ Ο€β‚‚ ⟩ ∎
+
+ +-congΛ‘ : {A B : Obj} {f g h : A β‡’ B} β†’ g β‰ˆ h β†’ f + g β‰ˆ f + h
+ +-congΛ‘ gβ‰ˆh = +-cong Equiv.refl gβ‰ˆh
+
+ +-congΚ³ : {A B : Obj} {f g h : A β‡’ B} β†’ f β‰ˆ g β†’ f + h β‰ˆ g + h
+ +-congΚ³ fβ‰ˆg = +-cong fβ‰ˆg Equiv.refl
+-† : {A B : Obj} {f g : A β‡’ B} β†’ (f + g) † β‰ˆ (f †) + (g †)
+-† {f = f} {g} = begin
- (β–½ ∘ f βŠ•β‚ g ∘ β–³) † β‰ˆβŸ¨ †-homomorphism ⟩
- (f βŠ•β‚ g ∘ β–³) † ∘ β–½ † β‰ˆβŸ¨ pushΛ‘ †-homomorphism ⟩
- β–³ † ∘ (f βŠ•β‚ g) † ∘ β–½ † β‰ˆβŸ¨ †-involutive β–½ ⟩∘⟨refl ⟩
- β–½ ∘ (f βŠ•β‚ g) † ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ †-resp-βŠ— ⟩∘⟨refl ⟩
- β–½ ∘ (f †) βŠ•β‚ (g †) ∘ β–³ ∎
+ (βˆ‡ ∘ f ×₁ g ∘ Ξ”) † β‰ˆβŸ¨ †-homomorphism ⟩
+ (f ×₁ g ∘ Ξ”) † ∘ βˆ‡ † β‰ˆβŸ¨ pushΛ‘ †-homomorphism ⟩
+ Ξ” † ∘ (f ×₁ g) † ∘ βˆ‡ † β‰ˆβŸ¨ Δ† ⟩∘⟨ †-resp-×₁ ⟩∘⟨ βˆ‡β€  ⟩
+ βˆ‡ ∘ (f †) ×₁ (g †) ∘ Ξ” ∎
-- bilinearity of composition
∘-distribΛ‘ : {A B C : Obj} {f : B β‡’ C} {g h : A β‡’ B} β†’ f ∘ (g + h) β‰ˆ f ∘ g + f ∘ h
∘-distribˑ {f = f} {g} {h} = begin
- f ∘ β–½ ∘ g βŠ•β‚ h ∘ β–³ β‰ˆβŸ¨ extendΚ³ β‡’β–½ ⟩
- β–½ ∘ f βŠ•β‚ f ∘ g βŠ•β‚ h ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pullΛ‘ (Equiv.sym βŠ—-distrib-over-∘) ⟩
- β–½ ∘ (f ∘ g) βŠ•β‚ (f ∘ h) ∘ β–³ ∎
+ f ∘ (g + h) β‰ˆβŸ¨ refl⟩∘⟨ identityΚ³ ⟨
+ f ∘ (g + h) ∘ id β‰ˆβŸ¨ +-resp-∘ ⟩
+ f ∘ g ∘ id + f ∘ h ∘ id β‰ˆβŸ¨ +-cong (refl⟩∘⟨ identityΚ³) (refl⟩∘⟨ identityΚ³) ⟩
+ f ∘ g + f ∘ h ∎
∘-distribΚ³ : {A B C : Obj} {f g : B β‡’ C} {h : A β‡’ B} β†’ (f + g) ∘ h β‰ˆ f ∘ h + g ∘ h
∘-distribʳ {f = f} {g} {h} = begin
- (β–½ ∘ f βŠ•β‚ g ∘ β–³) ∘ h β‰ˆβŸ¨ pullΚ³ (pullΚ³ β‡’β–³) ⟩
- β–½ ∘ f βŠ•β‚ g ∘ h βŠ•β‚ h ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pullΛ‘ (Equiv.sym βŠ—-distrib-over-∘) ⟩
- β–½ ∘ (f ∘ h) βŠ•β‚ (g ∘ h) ∘ β–³ ∎
-
- terminal : Terminal
- terminal = record
- { ⊀ = βŠ₯
- ; ⊀-is-terminal = record
- { ! = !
- ; !-unique = Ξ» f β†’ ⟨ Β‘-unique (f †) βŸ©β€  β—‹ †-involutive f
- }
- }
-
- β–½βˆ˜iβ‚βŠ•iβ‚‚ : {A B : Obj} β†’ β–½ ∘ i₁ βŠ•β‚ iβ‚‚ β‰ˆ id {A βŠ•β‚€ B}
- β–½βˆ˜iβ‚βŠ•iβ‚‚ = begin
- β–½ ∘ i₁ βŠ•β‚ iβ‚‚ β‰ˆβŸ¨ []∘+₁ ⟩
- [ id ∘ i₁ , id ∘ iβ‚‚ ] β‰ˆβŸ¨ []-congβ‚‚ identityΛ‘ identityΛ‘ ⟩
- [ i₁ , iβ‚‚ ] β‰ˆβŸ¨ +-Ξ· ⟩
- id ∎
-
- pβ‚βŠ•pβ‚‚βˆ˜β–³ : {A B : Obj} β†’ p₁ βŠ•β‚ pβ‚‚ ∘ β–³ β‰ˆ id {A βŠ•β‚€ B}
- pβ‚βŠ•pβ‚‚βˆ˜β–³ = begin
- (i₁ †) βŠ•β‚ (iβ‚‚ †) ∘ β–½ † β‰ˆβŸ¨ †-resp-βŠ— ⟩∘⟨refl ⟨
- (i₁ βŠ•β‚ iβ‚‚) † ∘ β–½ † β‰ˆβŸ¨ †-homomorphism ⟨
- (β–½ ∘ i₁ βŠ•β‚ iβ‚‚) † β‰ˆβŸ¨ ⟨ β–½βˆ˜iβ‚βŠ•iβ‚‚ βŸ©β€  ⟩
- id † β‰ˆβŸ¨ †-identity ⟩
- id ∎
-
- products : BinaryProducts
- products = record
- { product = Ξ» {A B} β†’ record
- { AΓ—B = A βŠ•β‚€ B
- ; π₁ = p₁
- ; Ο€β‚‚ = pβ‚‚
- ; ⟨_,_⟩ = Ξ» f g β†’ f βŠ•β‚ g ∘ β–³
- ; project₁ = proj₁
- ; projectβ‚‚ = projβ‚‚
- ; unique = uniq
- }
- }
- where
- module _ {A B X : Obj} where
- module _ {h : X β‡’ A} {i : X β‡’ B} where
- proj₁ : p₁ ∘ h βŠ•β‚ i ∘ β–³ β‰ˆ h
- proj₁ = begin
- p₁ ∘ h βŠ•β‚ i ∘ β–³ β‰ˆβŸ¨ pushΛ‘ p₁-βŠ• ⟩
- ρ⇒ ∘ id βŠ•β‚ ! ∘ h βŠ•β‚ i ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pullΛ‘ mergeβ‚‚Λ‘ ⟩
- ρ⇒ ∘ h βŠ•β‚ (! ∘ i) ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ reflβŸ©βŠ—βŸ¨ β‡’! ⟩∘⟨refl ⟩
- ρ⇒ ∘ h βŠ•β‚ ! ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pushΛ‘ serialize₁₂ ⟩
- ρ⇒ ∘ h βŠ•β‚ id ∘ id βŠ•β‚ ! ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ β–³-identityΚ³ ⟩
- ρ⇒ ∘ h βŠ•β‚ id ∘ ρ⇐ β‰ˆβŸ¨ extendΚ³ unitorΚ³-commute-from ⟩
- h ∘ ρ⇒ ∘ ρ⇐ β‰ˆβŸ¨ elimΚ³ unitorΚ³.isoΚ³ ⟩
- h ∎
- projβ‚‚ : pβ‚‚ ∘ h βŠ•β‚ i ∘ β–³ β‰ˆ i
- projβ‚‚ = begin
- pβ‚‚ ∘ h βŠ•β‚ i ∘ β–³ β‰ˆβŸ¨ pushΛ‘ pβ‚‚-βŠ• ⟩
- Ξ»β‡’ ∘ ! βŠ•β‚ id ∘ h βŠ•β‚ i ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pullΛ‘ merge₁ˑ ⟩
- Ξ»β‡’ ∘ (! ∘ h) βŠ•β‚ i ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ β‡’! βŸ©βŠ—βŸ¨refl ⟩∘⟨refl ⟩
- Ξ»β‡’ ∘ ! βŠ•β‚ i ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ pushΛ‘ serialize₂₁ ⟩
- Ξ»β‡’ ∘ id βŠ•β‚ i ∘ ! βŠ•β‚ id ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ β–³-identityΛ‘ ⟩
- Ξ»β‡’ ∘ id βŠ•β‚ i ∘ λ⇐ β‰ˆβŸ¨ extendΚ³ unitorΛ‘-commute-from ⟩
- i ∘ Ξ»β‡’ ∘ λ⇐ β‰ˆβŸ¨ elimΚ³ unitorΛ‘.isoΚ³ ⟩
- i ∎
- module _ {h : X β‡’ A βŠ•β‚€ B} {i : X β‡’ A} {j : X β‡’ B} where
- uniq : p₁ ∘ h β‰ˆ i β†’ pβ‚‚ ∘ h β‰ˆ j β†’ i βŠ•β‚ j ∘ β–³ β‰ˆ h
- uniq pβ‚βˆ˜hβ‰ˆi pβ‚‚βˆ˜hβ‰ˆj = begin
- i βŠ•β‚ j ∘ β–³ β‰ˆβŸ¨ pβ‚βˆ˜hβ‰ˆi βŸ©βŠ—βŸ¨ pβ‚‚βˆ˜hβ‰ˆj ⟩∘⟨refl ⟨
- (p₁ ∘ h) βŠ•β‚ (pβ‚‚ ∘ h) ∘ β–³ β‰ˆβŸ¨ pushΛ‘ βŠ—-distrib-over-∘ ⟩
- p₁ βŠ•β‚ pβ‚‚ ∘ h βŠ•β‚ h ∘ β–³ β‰ˆβŸ¨ pushΚ³ (Equiv.sym β‡’β–³) ⟩
- (p₁ βŠ•β‚ pβ‚‚ ∘ β–³) ∘ h β‰ˆβŸ¨ elimΛ‘ pβ‚βŠ•pβ‚‚βˆ˜β–³ ⟩
- h ∎
-
- cartesian : Cartesian
- cartesian = record
- { terminal = terminal
- ; products = products
- }
-
- open Cartesian cartesian using (_×₁_)
- open CartesianMonoidal cartesian using (monoidal)
- open Shorthands monoidal using () renaming (Ξ±β‡’ to Ξ±β‡’β€²)
-
- ×₁-βŠ•β‚ : {A B C D : Obj} (f : A β‡’ B) (g : C β‡’ D) β†’ f ×₁ g β‰ˆ f βŠ•β‚ g
- ×₁-βŠ•β‚ f g = begin
- (f ∘ p₁) βŠ•β‚ (g ∘ pβ‚‚) ∘ β–³ β‰ˆβŸ¨ pushΛ‘ βŠ—-distrib-over-∘ ⟩
- f βŠ•β‚ g ∘ p₁ βŠ•β‚ pβ‚‚ ∘ β–³ β‰ˆβŸ¨ elimΚ³ pβ‚βŠ•pβ‚‚βˆ˜β–³ ⟩
- f βŠ•β‚ g ∎
-
- β‰ˆΞ±β‡’ : {A B C : Obj} β†’ Ξ±β‡’β€² {A} {B} {C} β‰ˆ Ξ±β‡’ {A} {B} {C}
- β‰ˆΞ±β‡’ {A} {B} {C} = begin
- (p₁ ∘ p₁) βŠ•β‚ ((pβ‚‚ ∘ p₁) βŠ•β‚ pβ‚‚ ∘ β–³) ∘ β–³ β‰ˆβŸ¨ reflβŸ©βŠ—βŸ¨ pushΛ‘ split₁ˑ ⟩∘⟨refl ⟩
- (p₁ ∘ p₁) βŠ•β‚ ((pβ‚‚ βŠ•β‚ id) ∘ (p₁ βŠ•β‚ pβ‚‚) ∘ β–³) ∘ β–³ β‰ˆβŸ¨ reflβŸ©βŠ—βŸ¨ elimΚ³ pβ‚βŠ•pβ‚‚βˆ˜β–³ ⟩∘⟨refl ⟩
- (p₁ ∘ p₁) βŠ•β‚ (pβ‚‚ βŠ•β‚ id) ∘ β–³ β‰ˆβŸ¨ †-homomorphism βŸ©βŠ—βŸ¨ (reflβŸ©βŠ—βŸ¨ †-identity ) ⟩∘⟨refl ⟨
- ((i₁ ∘ i₁) †) βŠ•β‚ (pβ‚‚ βŠ•β‚ (id †)) ∘ β–³ β‰ˆβŸ¨ reflβŸ©βŠ—βŸ¨ †-resp-βŠ— ⟩∘⟨refl ⟨
- ((i₁ ∘ i₁) †) βŠ•β‚ ((iβ‚‚ βŠ•β‚ id) †) ∘ β–³ β‰ˆβŸ¨ †-resp-βŠ— ⟩∘⟨refl ⟨
- ((i₁ ∘ i₁) βŠ•β‚ (iβ‚‚ βŠ•β‚ id)) † ∘ β–³ β‰ˆβŸ¨ †-homomorphism ⟨
- (β–½ ∘ ((i₁ ∘ i₁) βŠ•β‚ (iβ‚‚ βŠ•β‚ id))) † β‰ˆβŸ¨ ⟨ β–½βˆ˜+₁ βŸ©β€  ⟩
- [ i₁ ∘ i₁ , iβ‚‚ βŠ•β‚ id ] † β‰ˆβŸ¨ ⟨ []-congΛ‘ ([]-congΛ‘ identityΚ³) βŸ©β€  ⟩
- α⇐ † β‰ˆβŸ¨ ⟨ α≅† βŸ©β€  ⟨
- Ξ±β‡’ † † β‰ˆβŸ¨ †-involutive Ξ±β‡’ ⟩
- Ξ±β‡’ ∎
+ (f + g) ∘ h β‰ˆβŸ¨ pushΛ‘ (Equiv.sym identityΛ‘) ⟩
+ id ∘ (f + g) ∘ h β‰ˆβŸ¨ +-resp-∘ ⟩
+ id ∘ f ∘ h + id ∘ g ∘ h β‰ˆβŸ¨ +-cong (pullΛ‘ identityΛ‘) (pullΛ‘ identityΛ‘) ⟩
+ f ∘ h + g ∘ h ∎
record IdempotentSemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where
@@ -452,10 +83,10 @@ record IdempotentSemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where
semiadditiveDagger : SemiadditiveDagger
open SemiadditiveDagger semiadditiveDagger public
- open Category π’ž
- open βŠ—-Reasoning +-monoidal
- open β‡’-Reasoning π’ž
+ open Category π’ž
+ open HomReasoning
+ open β‡’-Reasoning
field
idempotent : {A B : Obj} {f : AΒ β‡’ B} β†’ f + f β‰ˆ f
@@ -469,15 +100,15 @@ record IdempotentSemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where
≀-antisym : {A B : Obj} {f g : A β‡’ B} β†’ f ≀ g β†’ g ≀ f β†’ f β‰ˆ g
≀-antisym {A} {B} {f} {g} f≀g g≀f = begin
f β‰ˆβŸ¨ g≀f ⟨
- g + f β‰ˆβŸ¨ +-commutative ⟩
+ g + f β‰ˆβŸ¨ +-comm g f ⟩
f + g β‰ˆβŸ¨ f≀g ⟩
g ∎
≀-trans : {A B : Obj} {f g h : A β‡’ B} β†’ f ≀ g β†’ g ≀ h β†’ f ≀ h
≀-trans {A} {B} {f} {g} {h} f≀g g≀h = begin
- f + h β‰ˆβŸ¨ refl⟩∘⟨ reflβŸ©βŠ—βŸ¨ g≀h ⟩∘⟨refl ⟨
- f + (g + h) β‰ˆβŸ¨ +-associative ⟨
- (f + g) + h β‰ˆβŸ¨ refl⟩∘⟨ f≀g βŸ©βŠ—βŸ¨refl ⟩∘⟨refl ⟩
+ f + h β‰ˆβŸ¨ refl⟩∘⟨ ×₁-congΛ‘ g≀h ⟩∘⟨refl ⟨
+ f + (g + h) β‰ˆβŸ¨ +-assoc f g h ⟨
+ (f + g) + h β‰ˆβŸ¨ refl⟩∘⟨ ×₁-congΚ³ f≀g ⟩∘⟨refl ⟩
g + h β‰ˆβŸ¨ g≀h ⟩
h ∎
@@ -488,12 +119,12 @@ record IdempotentSemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where
β†’ g ≀ i
β†’ (f + g) ≀ (h + i)
≀-resp-+ {f = f} {g} {h} {i} f≀h g≀i = begin
- f + g + (h + i) β‰ˆβŸ¨ +-associative ⟩
- f + (g + (h + i)) β‰ˆβŸ¨ +-congΛ‘ +-associative ⟨
- f + (g + h + i) β‰ˆβŸ¨ +-congΛ‘ (+-congΚ³ +-commutative) ⟩
- f + (h + g + i) β‰ˆβŸ¨ +-congΛ‘ +-associative ⟩
- f + (h + (g + i)) β‰ˆβŸ¨ +-associative ⟨
- f + h + (g + i) β‰ˆβŸ¨ +-cong f≀h g≀i ⟩
+ (f + g) + (h + i) β‰ˆβŸ¨ +-assoc f g (h + i) ⟩
+ f + (g + (h + i)) β‰ˆβŸ¨ +-congΛ‘ (+-assoc g h i) ⟨
+ f + ((g + h) + i) β‰ˆβŸ¨ +-congΛ‘ (+-congΚ³ (+-comm g h)) ⟩
+ f + ((h + g) + i) β‰ˆβŸ¨ +-congΛ‘ (+-assoc h g i) ⟩
+ f + (h + (g + i)) β‰ˆβŸ¨ +-assoc f h (g + i) ⟨
+ (f + h) + (g + i) β‰ˆβŸ¨ +-cong f≀h g≀i ⟩
h + i ∎
≀-resp-∘
@@ -506,8 +137,8 @@ record IdempotentSemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where
≀-resp-∘ {f = f} {h} {g} {i} f≀h g≀i = begin
f ∘ g + (h ∘ i) β‰ˆβŸ¨ +-congΛ‘ (f≀h ⟩∘⟨refl) ⟨
f ∘ g + ((f + h) ∘ i) β‰ˆβŸ¨ +-congΛ‘ ∘-distribΚ³ ⟩
- f ∘ g + (f ∘ i + h ∘ i) β‰ˆβŸ¨ +-associative ⟨
- f ∘ g + f ∘ i + h ∘ i β‰ˆβŸ¨ +-congΚ³ ∘-distribΛ‘ ⟨
+ f ∘ g + (f ∘ i + h ∘ i) β‰ˆβŸ¨ +-assoc (f ∘ g) (f ∘ i) (h ∘ i) ⟨
+ (f ∘ g + f ∘ i) + h ∘ i β‰ˆβŸ¨ +-congΚ³ ∘-distribΛ‘ ⟨
f ∘ (g + i) + h ∘ i β‰ˆβŸ¨ +-congΚ³ (refl⟩∘⟨ g≀i) ⟩
f ∘ i + h ∘ i β‰ˆβŸ¨ ∘-distribΚ³ ⟨
(f + h) ∘ i β‰ˆβŸ¨ f≀h ⟩∘⟨refl ⟩
@@ -520,8 +151,8 @@ record IdempotentSemiadditiveDagger : Set (suc (o βŠ” β„“ βŠ” e)) where
g † ∎
-- special law
- β–½βˆ˜β–³ : {A : Obj} β†’ β–½ ∘ β–³ β‰ˆ id {A}
- β–½βˆ˜β–³ = begin
- β–½ ∘ β–³ β‰ˆβŸ¨ refl⟩∘⟨ introΛ‘ βŠ•.identity ⟩
- β–½ ∘ id βŠ•β‚ id ∘ β–³ β‰ˆβŸ¨ idempotent ⟩
+ βˆ‡βˆ˜Ξ” : {A : Obj} β†’ βˆ‡ ∘ Ξ” β‰ˆ id {A}
+ βˆ‡βˆ˜Ξ” = begin
+ βˆ‡ ∘ Ξ” β‰ˆβŸ¨ refl⟩∘⟨ introΛ‘ id×₁id ⟩
+ βˆ‡ ∘ id ×₁ id ∘ Ξ” β‰ˆβŸ¨ idempotent ⟩
id ∎
diff --git a/Category/Semiadditive.agda b/Category/Semiadditive.agda
index e7afc0e..3e8dbc4 100644
--- a/Category/Semiadditive.agda
+++ b/Category/Semiadditive.agda
@@ -32,6 +32,20 @@ record Semiadditive : Set (levelOfTerm π’ž) where
module _ {A B : Obj} where
+ Ο€β‚βˆ˜iβ‚‚β‰ˆ0 : π₁ {A} {B} ∘ iβ‚‚ β‰ˆ zeroβ‡’
+ Ο€β‚βˆ˜iβ‚‚β‰ˆ0 = begin
+ π₁ ∘ iβ‚‚ β‰ˆβŸ¨ π₁iβ‚‚-absorbΛ‘ zeroβ‡’ ⟨
+ zeroβ‡’ {A} ∘ π₁ ∘ iβ‚‚ β‰ˆβŸ¨ zero-∘ʳ (π₁ ∘ iβ‚‚) ⟩
+ zeroβ‡’ ∎
+
+ Ο€β‚‚βˆ˜iβ‚β‰ˆ0 : Ο€β‚‚ {A} {B} ∘ i₁ β‰ˆ zeroβ‡’
+ Ο€β‚‚βˆ˜iβ‚β‰ˆ0 = begin
+ Ο€β‚‚ ∘ i₁ β‰ˆβŸ¨ Ο€β‚‚i₁-absorbΛ‘ zeroβ‡’ ⟨
+ zeroβ‡’ {A} ∘ Ο€β‚‚ ∘ i₁ β‰ˆβŸ¨ zero-∘ʳ (Ο€β‚‚ ∘ i₁) ⟩
+ zeroβ‡’ ∎
+
+ module _ {A B : Obj} where
+
_+_ _+β€²_Β : A β‡’ B β†’ A β‡’ B β†’ A β‡’ B
f + g = βˆ‡ ∘ f ×₁ g ∘ Ξ”
f +β€² g = βˆ‡ ∘ f +₁ g ∘ Ξ”
@@ -61,8 +75,7 @@ record Semiadditive : Set (levelOfTerm π’ž) where
βˆ‡ ∘ zeroβ‡’ ×₁ x ∘ Ξ” β‰ˆβŸ¨ refl⟩∘⟨ Γ—β‚βˆ˜Ξ” ⟩
βˆ‡ ∘ ⟨ zeroβ‡’ , x ⟩ β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congβ‚‚ (zero-∘ʳ x) identityΛ‘ ⟨
βˆ‡ ∘ ⟨ zeroβ‡’ ∘ x , id ∘ x ⟩ β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩∘ ⟨
- βˆ‡ ∘ ⟨ zeroβ‡’ , id ⟩ ∘ x β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congΚ³ (zero-∘ʳ πŸŽβ‡) ⟩∘⟨refl ⟨
- βˆ‡ ∘ ⟨ zeroβ‡’ {A} ∘ πŸŽβ‡ , id ⟩ ∘ x β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congβ‚‚ (π₁iβ‚‚-absorbΛ‘ zeroβ‡’) (Equiv.sym Ο€β‚‚βˆ˜iβ‚‚β‰ˆid) ⟩∘⟨refl ⟩
+ βˆ‡ ∘ ⟨ zeroβ‡’ , id ⟩ ∘ x β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congβ‚‚ Ο€β‚βˆ˜iβ‚‚β‰ˆ0 Ο€β‚‚βˆ˜iβ‚‚β‰ˆid ⟩∘⟨refl ⟨
βˆ‡ ∘ ⟨ π₁ ∘ iβ‚‚ , Ο€β‚‚ ∘ iβ‚‚ ⟩ ∘ x β‰ˆβŸ¨ refl⟩∘⟨ g-Ξ· ⟩∘⟨refl ⟩
βˆ‡ ∘ iβ‚‚ ∘ x β‰ˆβŸ¨ cancelΛ‘ βˆ‡-identityΛ‘ ⟩
x ∎
@@ -72,8 +85,7 @@ record Semiadditive : Set (levelOfTerm π’ž) where
βˆ‡ ∘ x ×₁ zeroβ‡’ ∘ Ξ” β‰ˆβŸ¨ refl⟩∘⟨ Γ—β‚βˆ˜Ξ” ⟩
βˆ‡ ∘ ⟨ x , zeroβ‡’ ⟩ β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congβ‚‚ identityΛ‘ (zero-∘ʳ x) ⟨
βˆ‡ ∘ ⟨ id ∘ x , zeroβ‡’ ∘ x ⟩ β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩∘ ⟨
- βˆ‡ ∘ ⟨ id , zeroβ‡’ ⟩ ∘ x β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congΛ‘ (zero-∘ʳ πŸŽβ‡’) ⟩∘⟨refl ⟨
- βˆ‡ ∘ ⟨ id , zeroβ‡’ {A} ∘ πŸŽβ‡’ ⟩ ∘ x β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congβ‚‚ (Equiv.sym Ο€β‚βˆ˜iβ‚β‰ˆid) (Ο€β‚‚i₁-absorbΛ‘ zeroβ‡’) ⟩∘⟨refl ⟩
+ βˆ‡ ∘ ⟨ id , zeroβ‡’ ⟩ ∘ x β‰ˆβŸ¨ refl⟩∘⟨ ⟨⟩-congβ‚‚ Ο€β‚βˆ˜iβ‚β‰ˆid Ο€β‚‚βˆ˜iβ‚β‰ˆ0 ⟩∘⟨refl ⟨
βˆ‡ ∘ ⟨ π₁ ∘ i₁ , Ο€β‚‚ ∘ i₁ ⟩ ∘ x β‰ˆβŸ¨ refl⟩∘⟨ g-Ξ· ⟩∘⟨refl ⟩
βˆ‡ ∘ i₁ ∘ x β‰ˆβŸ¨ cancelΛ‘ βˆ‡-identityΚ³ ⟩
x ∎
diff --git a/Data/Matrix/Dagger-2-Poset.agda b/Data/Matrix/Dagger-2-Poset.agda
index 400be2e..aff22d7 100644
--- a/Data/Matrix/Dagger-2-Poset.agda
+++ b/Data/Matrix/Dagger-2-Poset.agda
@@ -15,7 +15,7 @@ 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.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.Monoid R.+-monoid using (𝟎; _[+]_; [+]-cong; [+]-𝟎ˑ; [+]-𝟎ʳ)
open import Data.Matrix.Raw using (_βˆ₯_; _≑_; _α΅€)
@@ -45,28 +45,26 @@ opaque
[+]-idem [] = PW.[]
[+]-idem (Mβ‚€ ∷ M) = βŠ•-idem Mβ‚€ PW.∷ [+]-idem M
-+-[+] : (M N : Matrix A B) β†’ (I βˆ₯ I) Β· (((I ≑ 𝟎) Β· M) βˆ₯ ((𝟎 ≑ I) Β· N)) Β· (I βˆ₯ I) α΅€ ≋ M [+] N
++-[+] : (M N : Matrix A B) β†’ (I βˆ₯ I) Β· ((M Β· (I βˆ₯ 𝟎)) ≑ (N Β· (𝟎 βˆ₯ I))) Β· (I ≑ I) ≋ M [+] N
+-[+] M N = begin
- (I βˆ₯ I) Β· (((I ≑ 𝟎) Β· M) βˆ₯ ((𝟎 ≑ I) Β· N)) Β· (I βˆ₯ I) α΅€ β‰‘βŸ¨ ≑.congβ‚‚ (Ξ» h₁ hβ‚‚ β†’ (I βˆ₯ I) Β· (h₁ βˆ₯ hβ‚‚) Β· (I βˆ₯ I) α΅€) (≑-Β· I 𝟎 M) (≑-Β· 𝟎 I N) ⟩
- (I βˆ₯ I) Β· ((I Β· M ≑ 𝟎 Β· M) βˆ₯ (𝟎 Β· N ≑ I Β· N)) Β· (I βˆ₯ I) α΅€ β‰ˆβŸ¨ Β·-resp-≋ ≋.refl (Β·-resp-≋ (βˆ₯-cong (≑-cong Β·-IΛ‘ (Β·-𝟎ˑ M)) (≑-cong (Β·-𝟎ˑ N) Β·-IΛ‘)) ≋.refl) ⟩
- (I βˆ₯ I) Β· ((M ≑ 𝟎) βˆ₯ (𝟎 ≑ N)) Β· (I βˆ₯ I) α΅€ β‰‘βŸ¨ ≑.cong (Ξ» h β†’ (I βˆ₯ I) Β· ((M ≑ 𝟎) βˆ₯ (𝟎 ≑ N)) Β· h) (βˆ₯-α΅€ I I) ⟩
- (I βˆ₯ I) Β· ((M ≑ 𝟎) βˆ₯ (𝟎 ≑ N)) Β· (I α΅€ ≑ I α΅€) β‰‘βŸ¨ ≑.congβ‚‚ (Ξ» h₁ hβ‚‚ β†’ (I βˆ₯ I) Β· ((M ≑ 𝟎) βˆ₯ (𝟎 ≑ N)) Β· (h₁ ≑ hβ‚‚)) Iα΅€ Iα΅€ ⟩
- (I βˆ₯ I) Β· ((M ≑ 𝟎) βˆ₯ (𝟎 ≑ N)) Β· (I ≑ I) β‰ˆβŸ¨ Β·-assoc ⟨
- ((I βˆ₯ I) Β· ((M ≑ 𝟎) βˆ₯ (𝟎 ≑ N))) Β· (I ≑ I) β‰‘βŸ¨ ≑.cong (_Β· (I ≑ I)) (Β·-βˆ₯ (I βˆ₯ I) (M ≑ 𝟎) (𝟎 ≑ N)) ⟩
- (((I βˆ₯ I) Β· (M ≑ 𝟎)) βˆ₯ ((I βˆ₯ I) Β· (𝟎 ≑ N))) Β· (I ≑ I) β‰ˆβŸ¨ βˆ₯-Β·-≑ ((I βˆ₯ I) Β· (M ≑ 𝟎)) ((I βˆ₯ I) Β· (𝟎 ≑ N)) I I ⟩
- (((I βˆ₯ I) Β· (M ≑ 𝟎)) Β· I) [+] (((I βˆ₯ I) Β· (𝟎 ≑ N)) Β· I) β‰ˆβŸ¨ [+]-cong Β·-IΚ³ Β·-IΚ³ ⟩
- ((I βˆ₯ I) Β· (M ≑ 𝟎)) [+] ((I βˆ₯ I) Β· (𝟎 ≑ N)) β‰ˆβŸ¨ [+]-cong (βˆ₯-Β·-≑ I I M 𝟎) (βˆ₯-Β·-≑ I I 𝟎 N) ⟩
- ((I Β· M) [+] (I Β· 𝟎)) [+] ((I Β· 𝟎) [+] (I Β· N)) β‰ˆβŸ¨ [+]-cong ([+]-cong Β·-IΛ‘ Β·-IΛ‘) ([+]-cong Β·-IΛ‘ Β·-IΛ‘) ⟩
- (M [+] 𝟎) [+] (𝟎 [+] N) β‰ˆβŸ¨ [+]-cong ([+]-𝟎ʳ M) ([+]-𝟎ˑ N) ⟩
- M [+] N ∎
+ (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) Β· (((I ≑ 𝟎) Β· M) βˆ₯ ((𝟎 ≑ I) Β· M)) Β· (I βˆ₯ I) α΅€ ≋ M
+
+idem : (M : Matrix A B) β†’ (I βˆ₯ I) Β· ((M Β· (I βˆ₯ 𝟎)) ≑ (M Β· (𝟎 βˆ₯ I))) Β· (I ≑ I) ≋ M
idem M = begin
- (I βˆ₯ I) Β· (((I ≑ 𝟎) Β· M) βˆ₯ ((𝟎 ≑ I) Β· M)) Β· (I βˆ₯ I) α΅€ β‰ˆβŸ¨ +-[+] M M ⟩
- M [+] M β‰ˆβŸ¨ [+]-idem M ⟩
- M ∎
+ (I βˆ₯ I) Β· ((M Β· (I βˆ₯ 𝟎)) ≑ (M Β· (𝟎 βˆ₯ I))) Β· (I ≑ I) β‰ˆβŸ¨ +-[+] M M ⟩
+ M [+] M β‰ˆβŸ¨ [+]-idem M ⟩
+ M ∎
where
open β‰ˆ-Reasoning (Matrixβ‚› _ _)
diff --git a/Data/Matrix/SemiadditiveDagger.agda b/Data/Matrix/SemiadditiveDagger.agda
index 1415c7e..3e13383 100644
--- a/Data/Matrix/SemiadditiveDagger.agda
+++ b/Data/Matrix/SemiadditiveDagger.agda
@@ -7,29 +7,34 @@ module Data.Matrix.SemiadditiveDagger {c β„“ : Level} (R : CommutativeSemiring c
module R = CommutativeSemiring R
-import Relation.Binary.Reasoning.Setoid as β‰ˆ-Reasoning
-import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
-import Data.Nat.Properties as β„•-Props
import Data.Nat as β„•
+import Data.Nat.Properties as β„•-Props
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+import Relation.Binary.Reasoning.Setoid as β‰ˆ-Reasoning
open import Categories.Category.Cocartesian using (Cocartesian)
-open import Categories.Object.Coproduct using (Coproduct)
-open import Categories.Object.Initial using (Initial)
-open import Category.Dagger.Semiadditive using (DaggerCocartesianMonoidal; SemiadditiveDagger)
-open import Data.Matrix.Cast R.setoid using (castβ‚‚; castβ‚‚-βˆ₯; βˆ₯-≑; βˆ₯-≑⁴; ≑-sym-assoc)
-open import Data.Matrix.Category R.semiring using (Mat; _Β·_; ≑-Β·; Β·-IΛ‘; Β·-IΚ³; Β·-𝟎ˑ; Β·-𝟎ʳ; Β·-βˆ₯; βˆ₯-Β·-≑)
-open import Data.Matrix.Raw using (_α΅€; _α΅€α΅€; mapRows; []α΅₯; []α΅₯-βˆ₯; []β‚•; []β‚•-!; []β‚•-≑; _∷α΅₯_; _βˆ·β‚•_; ∷α΅₯-α΅€; _βˆ₯_; _≑_; βˆ·β‚•-α΅€; βˆ·β‚•-≑; []α΅₯-α΅€; head-∷-tailβ‚•; headβ‚•; tailβ‚•; βˆ·β‚•-βˆ₯; []α΅₯-!)
+open import Categories.Category.Dagger using (HasDagger)
+open import Categories.Object.Biproduct using (Biproduct)
+open import Categories.Object.Coproduct using (IsCoproduct)
+open import Categories.Object.Initial using (IsInitial)
+open import Categories.Object.Product using (IsProduct)
+open import Categories.Object.Terminal using (IsTerminal)
+open import Categories.Object.Zero using (Zero)
+open import Category.Dagger.Semiadditive using (SemiadditiveDagger)
+open import Category.Semiadditive using (Semiadditive)
+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; α΅€-cong)
open import Data.Matrix.Monoid R.+-monoid using (𝟎; πŸŽα΅€; πŸŽβ‰‘πŸŽ; 𝟎βˆ₯𝟎; _[+]_; [+]-cong; [+]-𝟎ˑ; [+]-𝟎ʳ)
+open import Data.Matrix.Raw using (_α΅€; _α΅€α΅€; mapRows; []α΅₯; []α΅₯-βˆ₯; []β‚•; []β‚•-!; []β‚•-≑; _∷α΅₯_; _βˆ·β‚•_; ∷α΅₯-α΅€; _βˆ₯_; _≑_; βˆ·β‚•-α΅€; βˆ·β‚•-≑; []α΅₯-α΅€; head-∷-tailβ‚•; headβ‚•; tailβ‚•; βˆ·β‚•-βˆ₯; ∷α΅₯-≑; []α΅₯-!)
open import Data.Matrix.Transform R.semiring using (I; Iα΅€; [_]_; _[_]; -[-]α΅€; [-]--cong; [-]-[]α΅₯; [⟨⟩]-[]β‚•)
open import Data.Nat using (β„•)
open import Data.Product using (_,_; Ξ£-syntax)
open import Data.Vec using (Vec; map; replicate; _++_)
open import Data.Vec.Properties using (map-cong; map-const)
open import Data.Vector.Bisemimodule R.semiring using (_βˆ™_ ; βˆ™-cong)
-open import Data.Vector.Raw using (⟨⟩)
open import Data.Vector.Core R.setoid using (Vector; Vectorβ‚›; module β‰Š; _β‰Š_)
open import Data.Vector.Monoid R.+-monoid using () renaming (⟨Ρ⟩ to ⟨0⟩)
+open import Data.Vector.Raw using (⟨⟩)
open import Data.Vector.Vec using (replicate-++)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality as ≑ using (_≑_; module ≑-Reasoning)
@@ -88,18 +93,6 @@ opaque
α΅€-involutive M = ≋.reflexive (M α΅€α΅€)
opaque
- unfolding _≋_
- ≋λᡀ : ([]α΅₯ βˆ₯ I) α΅€ ≋ 𝟎 ≑ I {A}
- ≋λᡀ = begin
- ([]α΅₯ βˆ₯ I) α΅€ β‰‘βŸ¨ ≑.cong (_α΅€) ([]α΅₯-βˆ₯ I) ⟩
- I α΅€ β‰‘βŸ¨ Iα΅€ ⟩
- I β‰‘βŸ¨ []β‚•-≑ I ⟨
- []β‚• ≑ I β‰‘βŸ¨ ≑.cong (_≑ I) ([]β‚•-! 𝟎) ⟨
- 𝟎 ≑ I ∎
- where
- open β‰ˆ-Reasoning (Matrixβ‚› _ _)
-
-opaque
unfolding Matrix _βˆ₯_ _α΅€ _≑_ _βˆ·β‚•_
βˆ₯-α΅€ : (M : Matrix A C) (N : Matrix B C) β†’ (M βˆ₯ N) α΅€ ≑ M α΅€ ≑ N α΅€
βˆ₯-α΅€ {A} {zero} {B} [] [] = ≑.sym (replicate-++ A B [])
@@ -119,110 +112,6 @@ opaque
where
open ≑-Reasoning
-opaque
- unfolding _≋_
- ≋ρᡀ : (I βˆ₯ []α΅₯) α΅€ ≋ I {A} ≑ 𝟎
- ≋ρᡀ {A} = begin
- (I βˆ₯ []α΅₯) α΅€ β‰‘βŸ¨ βˆ₯-α΅€ I []α΅₯ ⟩
- I α΅€ ≑ []α΅₯ α΅€ β‰‘βŸ¨ ≑.cong (I α΅€ ≑_) []α΅₯-α΅€ ⟩
- I α΅€ ≑ []β‚• β‰‘βŸ¨ ≑.cong (_≑ []β‚•) Iα΅€ ⟩
- I ≑ []β‚• β‰‘βŸ¨ ≑.cong (I ≑_) ([]β‚•-! 𝟎) ⟨
- I ≑ 𝟎 ∎
- where
- open β‰ˆ-Reasoning (Matrixβ‚› _ _)
-
-opaque
- unfolding _≋_
- ≋αᡀ : (((I {A} ≑ 𝟎 {A} {B β„•.+ C}) βˆ₯ (𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (I {B} ≑ 𝟎)) βˆ₯ (𝟎 {_} {A} ≑ I {B β„•.+ C}) Β· (𝟎 ≑ I {C})) α΅€
- ≋ (I {A β„•.+ B} ≑ 𝟎) Β· (I {A} ≑ 𝟎) βˆ₯ (I {A β„•.+ B} ≑ 𝟎) Β· (𝟎 ≑ I {B}) βˆ₯ (𝟎 ≑ I {C})
- ≋αᡀ {A} {B} {C} = begin
- (((I {A} ≑ 𝟎 {A} {B β„•.+ C}) βˆ₯ (𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (I {B} ≑ 𝟎 {B} {C})) βˆ₯ (𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (𝟎 {C} {B} ≑ I {C})) α΅€
- β‰‘βŸ¨ βˆ₯-α΅€ ((I {A} ≑ 𝟎 {A} {B β„•.+ C}) βˆ₯ (𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (I {B} ≑ 𝟎 {B} {C})) ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (𝟎 {C} {B} ≑ I {C})) ⟩
- ((I {A} ≑ 𝟎 {A} {B β„•.+ C}) βˆ₯ (𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (I {B} ≑ 𝟎 {B} {C})) α΅€ ≑ ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (𝟎 {C} {B} ≑ I {C})) α΅€
- β‰‘βŸ¨ ≑.cong (_≑ ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (𝟎 {C} {B} ≑ I {C})) α΅€) (βˆ₯-α΅€ (I {A} ≑ 𝟎 {A} {B β„•.+ C}) ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (I {B} ≑ 𝟎 {B} {C}))) ⟩
- ((I {A} ≑ 𝟎 {A} {B β„•.+ C}) α΅€ ≑ ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (I {B} ≑ 𝟎 {B} {C})) α΅€) ≑ ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (𝟎 {C} {B} ≑ I {C})) α΅€
- β‰‘βŸ¨ ≑.cong (Ξ» h β†’ (h ≑ ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (I {B} ≑ 𝟎 {B} {C})) α΅€) ≑ ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (𝟎 {C} {B} ≑ I {C})) α΅€) (≑-α΅€ I 𝟎) ⟩
- (I {A} α΅€ βˆ₯ 𝟎 {A} {B β„•.+ C} α΅€ ≑ ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (I {B} ≑ 𝟎 {B} {C})) α΅€) ≑ ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (𝟎 {C} {B} ≑ I {C})) α΅€
- β‰‘βŸ¨ ≑.cong (Ξ» h β†’ (h ≑ ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (I {B} ≑ 𝟎 {B} {C})) α΅€) ≑ ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (𝟎 {C} {B} ≑ I {C})) α΅€) (≑.congβ‚‚ _βˆ₯_ Iα΅€ πŸŽα΅€) ⟩
- (I {A} βˆ₯ 𝟎 {B β„•.+ C} {A} ≑ ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (I {B} ≑ 𝟎 {B} {C})) α΅€) ≑ ((𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) Β· (𝟎 {C} {B} ≑ I {C})) α΅€
- β‰ˆβŸ¨ ≑-cong (≑-cong ≋.refl (Β·-α΅€ (I ≑ 𝟎) (𝟎 ≑ I))) (Β·-α΅€ (𝟎 ≑ I) (𝟎 ≑ I)) ⟩
- (I {A} βˆ₯ 𝟎 {B β„•.+ C} {A} ≑ (I {B} ≑ 𝟎 {B} {C}) α΅€ Β· (𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) α΅€) ≑ (𝟎 {C} {B} ≑ I {C}) α΅€ Β· (𝟎 {B β„•.+ C} {A} ≑ I {B β„•.+ C}) α΅€
- β‰‘βŸ¨ ≑.congβ‚‚ _≑_ (≑.congβ‚‚ (Ξ» h₁ hβ‚‚ β†’ I {A} βˆ₯ 𝟎 {B β„•.+ C} {A} ≑ h₁ Β· hβ‚‚) (≑-α΅€ I 𝟎) (≑-α΅€ 𝟎 I)) (≑.congβ‚‚ _Β·_ (≑-α΅€ 𝟎 I) (≑-α΅€ 𝟎 I)) ⟩
- (I {A} βˆ₯ 𝟎 {B β„•.+ C} {A} ≑ (I {B} α΅€ βˆ₯ 𝟎 {B} {C} α΅€) Β· (𝟎 {B β„•.+ C} {A} α΅€ βˆ₯ I {B β„•.+ C} α΅€)) ≑ (𝟎 {C} {B} α΅€ βˆ₯ I {C} α΅€) Β· (𝟎 {B β„•.+ C} {A} α΅€ βˆ₯ I {B β„•.+ C} α΅€)
- β‰‘βŸ¨ ≑.congβ‚‚ _≑_ (≑.congβ‚‚ (Ξ» h₁ hβ‚‚ β†’ I {A} βˆ₯ 𝟎 ≑ h₁ Β· hβ‚‚) (≑.congβ‚‚ _βˆ₯_ Iα΅€ πŸŽα΅€) (≑.congβ‚‚ _βˆ₯_ πŸŽα΅€ Iα΅€)) (≑.congβ‚‚ _Β·_ (≑.congβ‚‚ _βˆ₯_ πŸŽα΅€ Iα΅€) (≑.congβ‚‚ _βˆ₯_ πŸŽα΅€ Iα΅€)) ⟩
- (I {A} βˆ₯ 𝟎 {B β„•.+ C} {A} ≑ (I {B} βˆ₯ 𝟎 {C} {B}) Β· (𝟎 {A} {B β„•.+ C} βˆ₯ I {B β„•.+ C})) ≑ (𝟎 {B} {C} βˆ₯ I {C}) Β· (𝟎 {A} {B β„•.+ C} βˆ₯ I {B β„•.+ C})
- β‰‘βŸ¨ ≑.congΒ (Ξ» h β†’ (I {A} βˆ₯ 𝟎 {B β„•.+ C} {A} ≑ h) ≑ (𝟎 {B} {C} βˆ₯ I {C}) Β· (𝟎 {A} {B β„•.+ C} βˆ₯ I {B β„•.+ C})) (Β·-βˆ₯ (I βˆ₯ 𝟎) 𝟎 I) ⟩
- (I {A} βˆ₯ 𝟎 {B β„•.+ C} {A} ≑ (I {B} βˆ₯ 𝟎 {C} {B}) Β· 𝟎 {A} {B β„•.+ C} βˆ₯ (I {B} βˆ₯ 𝟎 {C} {B}) Β· I {B β„•.+ C}) ≑ (𝟎 {B} {C} βˆ₯ I {C}) Β· (𝟎 {A} {B β„•.+ C} βˆ₯ I {B β„•.+ C})
- β‰ˆβŸ¨ ≑-cong (≑-cong ≋.refl (βˆ₯-cong (Β·-𝟎ʳ (I βˆ₯ 𝟎)) Β·-IΚ³)) (≋.refl {x = (𝟎 {B} {C} βˆ₯ I {C}) Β· (𝟎 {A} {B β„•.+ C} βˆ₯ I {B β„•.+ C})}) ⟩
- (I {A} βˆ₯ 𝟎 {B β„•.+ C} {A} ≑ 𝟎 {A} {B} βˆ₯ I {B} βˆ₯ 𝟎 {C} {B}) ≑ (𝟎 {B} {C} βˆ₯ I {C}) Β· (𝟎 {A} {B β„•.+ C} βˆ₯ I {B β„•.+ C})
- β‰‘βŸ¨ ≑.congΒ ((I {A} βˆ₯ 𝟎 {B β„•.+ C} {A} ≑ 𝟎 {A} {B} βˆ₯ I {B} βˆ₯ 𝟎 {C} {B}) ≑_) (Β·-βˆ₯ (𝟎 βˆ₯ I) 𝟎 I) ⟩
- (I {A} βˆ₯ 𝟎 {B β„•.+ C} {A} ≑ 𝟎 {A} {B} βˆ₯ I {B} βˆ₯ 𝟎 {C} {B}) ≑ (𝟎 {B} {C} βˆ₯ I {C}) Β· (𝟎 {A} {B β„•.+ C}) βˆ₯ (𝟎 {B} {C} βˆ₯ I {C}) Β· I {B β„•.+ C}
- β‰ˆβŸ¨ ≑-cong ≋.refl (βˆ₯-cong (Β·-𝟎ʳ (𝟎 βˆ₯ I)) Β·-IΚ³) ⟩
- (I {A} βˆ₯ 𝟎 {B β„•.+ C} {A} ≑ 𝟎 {A} {B} βˆ₯ I {B} βˆ₯ 𝟎 {C} {B}) ≑ 𝟎 {A} {C} βˆ₯ 𝟎 {B} {C} βˆ₯ I {C}
- β‰‘βŸ¨ ≑.cong (Ξ» h β†’ (I {A} βˆ₯ h ≑ 𝟎 {A} {B} βˆ₯ I {B} βˆ₯ 𝟎 {C} {B}) ≑ 𝟎 {A} {C} βˆ₯ 𝟎 {B} {C} βˆ₯ I {C}) 𝟎βˆ₯𝟎 ⟨
- (I {A} βˆ₯ 𝟎 {B} βˆ₯ 𝟎 {C} ≑ 𝟎 {A} βˆ₯ I {B} βˆ₯ 𝟎 {C}) ≑ 𝟎 {A} βˆ₯ 𝟎 {B} βˆ₯ I {C}
- β‰‘βŸ¨ ≑-sym-assoc (I {A} βˆ₯ 𝟎 {B} βˆ₯ 𝟎 {C}) (𝟎 {A} βˆ₯ I {B} βˆ₯ 𝟎 {C}) (𝟎 {A} βˆ₯ 𝟎 {B} βˆ₯ I {C}) ⟨
- castβ‚‚ _ (I {A} βˆ₯ 𝟎 {B} βˆ₯ 𝟎 {C} ≑ 𝟎 {A} βˆ₯ I {B} βˆ₯ 𝟎 {C} ≑ 𝟎 {A} βˆ₯ 𝟎 {B} βˆ₯ I {C})
- β‰‘βŸ¨ ≑.cong (castβ‚‚ _) (βˆ₯-≑⁴ I 𝟎 𝟎 𝟎 I 𝟎 𝟎 𝟎 I) ⟩
- castβ‚‚ (≑.sym assoc) ((I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) βˆ₯ (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) βˆ₯ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})))
- β‰‘βŸ¨ castβ‚‚-βˆ₯ (≑.sym assoc) ((I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C}))) ((𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) βˆ₯ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C}))) ⟨
- (castβ‚‚ (≑.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C}))) βˆ₯ castβ‚‚ (≑.sym assoc) ((𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) βˆ₯ ((𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})))
- β‰‘βŸ¨ ≑.cong (castβ‚‚ (≑.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) βˆ₯_) (castβ‚‚-βˆ₯ (≑.sym assoc) (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) (𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})) ⟨
- castβ‚‚ (≑.sym assoc) (I {A} ≑ 𝟎 {A} {B} ≑ (𝟎 {A} {C})) βˆ₯ castβ‚‚ (≑.sym assoc) (𝟎 {B} {A} ≑ I {B} ≑ 𝟎 {B} {C}) βˆ₯ castβ‚‚ (≑.sym assoc) (𝟎 {C} {A} ≑ 𝟎 {C} {B} ≑ I {C})
- β‰‘βŸ¨ ≑.congβ‚‚ _βˆ₯_ (≑-sym-assoc I 𝟎 𝟎) (≑.congβ‚‚ _βˆ₯_ (≑-sym-assoc 𝟎 I 𝟎) (≑-sym-assoc 𝟎 𝟎 I)) ⟩
- ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) βˆ₯ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) βˆ₯ ((𝟎 {C} {A} ≑ 𝟎 {C} {B}) ≑ I {C})
- β‰‘βŸ¨ ≑.cong (Ξ» h β†’ ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) βˆ₯ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) βˆ₯ (h ≑ I {C})) πŸŽβ‰‘πŸŽ ⟩
- ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) βˆ₯ ((𝟎 {B} {A} ≑ I {B}) ≑ 𝟎 {B} {C}) βˆ₯ (𝟎 {C} {A β„•.+ B} ≑ I {C})
- β‰ˆβŸ¨ βˆ₯-cong ≋.refl (βˆ₯-cong (≑-cong Β·-IΛ‘ (Β·-𝟎ˑ (𝟎 ≑ I))) ≋.refl) ⟨
- ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) βˆ₯ (((I {A β„•.+ B} Β· (𝟎 {B} {A} ≑ I {B})) ≑ (𝟎 {A β„•.+ B} {C} Β· (𝟎 {B} {A} ≑ I {B})))) βˆ₯ (𝟎 {C} {A β„•.+ B} ≑ I {C})
- β‰‘βŸ¨ ≑.cong (Ξ» h β†’ ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) βˆ₯ h βˆ₯ (𝟎 {C} {A β„•.+ B} ≑ I {C})) (≑-Β· I 𝟎 (𝟎 ≑ I)) ⟨
- ((I {A} ≑ 𝟎 {A} {B}) ≑ (𝟎 {A} {C})) βˆ₯ ((I {A β„•.+ B} ≑ 𝟎 {A β„•.+ B} {C}) Β· (𝟎 {B} {A} ≑ I {B})) βˆ₯ (𝟎 {C} {A β„•.+ B} ≑ I {C})
- β‰ˆβŸ¨ βˆ₯-cong (≑-cong Β·-IΛ‘ (Β·-𝟎ˑ (I ≑ 𝟎))) ≋.refl ⟨
- ((I {A β„•.+ B} Β· (I {A} ≑ 𝟎 {A} {B})) ≑ (𝟎 {A β„•.+ B} {C} Β· (I {A} ≑ 𝟎 {A} {B}))) βˆ₯ ((I {A β„•.+ B} ≑ 𝟎 {A β„•.+ B} {C}) Β· (𝟎 {B} {A} ≑ I {B})) βˆ₯ (𝟎 {C} {A β„•.+ B} ≑ I {C})
- β‰‘βŸ¨ ≑.cong (Ξ» h β†’ h βˆ₯ ((I {A β„•.+ B} ≑ 𝟎 {A β„•.+ B} {C}) Β· (𝟎 {B} {A} ≑ I {B})) βˆ₯ (𝟎 {C} {A β„•.+ B} ≑ I {C})) (≑-Β· I 𝟎 (I ≑ 𝟎)) ⟨
- (I {A β„•.+ B} ≑ 𝟎 {A β„•.+ B} {C}) Β· (I {A} ≑ 𝟎 {A} {B}) βˆ₯ ((I {A β„•.+ B} ≑ 𝟎 {A β„•.+ B} {C}) Β· (𝟎 {B} {A} ≑ I {B})) βˆ₯ (𝟎 {C} {A β„•.+ B} ≑ I {C}) ∎
- where
- assoc : A β„•.+ B β„•.+ C ≑ A β„•.+ (B β„•.+ C)
- assoc = β„•-Props.+-assoc A B C
- open β‰ˆ-Reasoning (Matrixβ‚› _ _)
-
-≋σᡀ : ((𝟎 ≑ I {A}) βˆ₯ (I {B} ≑ 𝟎)) α΅€ ≋ (𝟎 ≑ I {B}) βˆ₯ (I {A} ≑ 𝟎)
-≋σᡀ {A} {B} = begin
- ((𝟎 ≑ I) βˆ₯ (I ≑ 𝟎)) α΅€ β‰‘βŸ¨ βˆ₯-α΅€ (𝟎 ≑ I) (I ≑ 𝟎) ⟩
- (𝟎 ≑ I {A}) α΅€ ≑ (I ≑ 𝟎) α΅€ β‰‘βŸ¨ ≑.congβ‚‚ _≑_ (≑-α΅€ 𝟎 I) (≑-α΅€ I 𝟎) ⟩
- 𝟎 α΅€ βˆ₯ (I {A}) α΅€ ≑ I α΅€ βˆ₯ 𝟎 α΅€ β‰‘βŸ¨ ≑.congβ‚‚ _≑_ (≑.congβ‚‚ _βˆ₯_ πŸŽα΅€ Iα΅€) (≑.congβ‚‚ _βˆ₯_ Iα΅€ πŸŽα΅€) ⟩
- 𝟎 βˆ₯ I {A} ≑ I βˆ₯ 𝟎 β‰‘βŸ¨ βˆ₯-≑ 𝟎 I I 𝟎 ⟩
- (𝟎 ≑ I {B}) βˆ₯ (I ≑ 𝟎) ∎
- where
- open β‰ˆ-Reasoning (Matrixβ‚› _ _)
-
-β‰‹βŠ— : (M : Matrix A B)
- (N : Matrix C D)
- β†’ (I ≑ 𝟎) Β· M βˆ₯ (𝟎 ≑ I) Β· N
- ≋ (M ≑ 𝟎) βˆ₯ (𝟎 ≑ N)
-β‰‹βŠ— M N = begin
- (I ≑ 𝟎) Β· M βˆ₯ (𝟎 ≑ I) Β· N β‰‘βŸ¨ ≑.congβ‚‚ _βˆ₯_ (≑-Β· I 𝟎 M) (≑-Β· 𝟎 I N) ⟩
- (I Β· M ≑ 𝟎 Β· M) βˆ₯ (𝟎 Β· N ≑ I Β· N) β‰ˆβŸ¨ βˆ₯-cong (≑-cong Β·-IΛ‘ (Β·-𝟎ˑ M)) (≑-cong (Β·-𝟎ˑ N) Β·-IΛ‘) ⟩
- (M ≑ 𝟎) βˆ₯ (𝟎 ≑ N) ∎
- where
- open β‰ˆ-Reasoning (Matrixβ‚› _ _)
-
-α΅€-resp-βŠ—
- : {M : Matrix A B}
- {N : Matrix C D}
- β†’ ((I ≑ 𝟎) Β· M βˆ₯ (𝟎 ≑ I) Β· N) α΅€
- ≋ (I ≑ 𝟎) Β· M α΅€ βˆ₯ (𝟎 ≑ I) Β· N α΅€
-α΅€-resp-βŠ— {M = M} {N = N} = begin
- ((I ≑ 𝟎) Β· M βˆ₯ (𝟎 ≑ I) Β· N) α΅€ β‰ˆβŸ¨ α΅€-cong (β‰‹βŠ— M N) ⟩
- ((M ≑ 𝟎) βˆ₯ (𝟎 ≑ N)) α΅€ β‰‘βŸ¨ ≑.cong (_α΅€) (βˆ₯-≑ M 𝟎 𝟎 N) ⟨
- ((M βˆ₯ 𝟎) ≑ (𝟎 βˆ₯ N)) α΅€ β‰‘βŸ¨ ≑-α΅€ (M βˆ₯ 𝟎) (𝟎 βˆ₯ N) ⟩
- (M βˆ₯ 𝟎) α΅€ βˆ₯ (𝟎 βˆ₯ N) α΅€ β‰‘βŸ¨ ≑.congβ‚‚ _βˆ₯_ (βˆ₯-α΅€ M 𝟎) (βˆ₯-α΅€ 𝟎 N) ⟩
- (M α΅€ ≑ 𝟎 α΅€) βˆ₯ (𝟎 α΅€ ≑ N α΅€) β‰‘βŸ¨ ≑.congβ‚‚ (Ξ» h₁ hβ‚‚ β†’ (M α΅€ ≑ h₁) βˆ₯ (hβ‚‚ ≑ N α΅€)) πŸŽα΅€ πŸŽα΅€ ⟩
- (M α΅€ ≑ 𝟎) βˆ₯ (𝟎 ≑ N α΅€) β‰ˆβŸ¨ β‰‹βŠ— (M α΅€) (N α΅€) ⟨
- (I ≑ 𝟎) Β· M α΅€ βˆ₯ (𝟎 ≑ I) Β· N α΅€ ∎
- where
- open β‰ˆ-Reasoning (Matrixβ‚› _ _)
-
inj₁ : (M : Matrix A C) (N : Matrix B C) β†’ (M βˆ₯ N) Β· (I ≑ 𝟎) ≋ M
inj₁ {A} {C} M N = begin
(M βˆ₯ N) Β· (I ≑ 𝟎) β‰ˆβŸ¨ βˆ₯-Β·-≑ M N I 𝟎 ⟩
@@ -242,8 +131,10 @@ injβ‚‚ {A} {C} {B} M N = begin
open β‰ˆ-Reasoning (Matrixβ‚› B C)
opaque
- unfolding Matrix
- split-βˆ₯ : (A : β„•) β†’ (M : Matrix (A β„•.+ B) C) β†’ Ξ£[ M₁ ∈ Matrix A C ] Ξ£[ Mβ‚‚ ∈ Matrix B C ] M₁ βˆ₯ Mβ‚‚ ≑ M
+
+ unfolding Matrix _∷α΅₯_
+
+ split-βˆ₯ : (A : β„•) (M : Matrix (A β„•.+ B) C) β†’ Ξ£[ M₁ ∈ Matrix A C ] Ξ£[ Mβ‚‚ ∈ Matrix B C ] M₁ βˆ₯ Mβ‚‚ ≑ M
split-βˆ₯ zero M = []α΅₯ , M , []α΅₯-βˆ₯ M
split-βˆ₯ (suc A) Mβ€²
rewrite ≑.sym (head-∷-tailβ‚• Mβ€²)
@@ -257,14 +148,24 @@ opaque
where
open ≑-Reasoning
-uniq
+ split-≑ : (B : β„•) (M : Matrix A (B β„•.+ C)) β†’ Ξ£[ M₁ ∈ Matrix A B ] Ξ£[ Mβ‚‚ ∈ Matrix A C ] M₁ ≑ Mβ‚‚ ≑ M
+ split-≑ zero M = []β‚• , M , []β‚•-≑ M
+ split-≑ (suc B) (Mβ‚€ ∷ M) with split-≑ B M
+ ... | M₁ , Mβ‚‚ , M₁≑M₂≑M = Mβ‚€ ∷α΅₯ M₁ , Mβ‚‚ , (begin
+ (Mβ‚€ ∷α΅₯ M₁) ≑ Mβ‚‚ β‰‘βŸ¨ ∷α΅₯-≑ Mβ‚€ M₁ Mβ‚‚ ⟨
+ Mβ‚€ ∷α΅₯ M₁ ≑ Mβ‚‚ β‰‘βŸ¨ ≑.cong (Mβ‚€ ∷α΅₯_) M₁≑M₂≑M ⟩
+ Mβ‚€ ∷α΅₯ M ∎)
+ where
+ open ≑-Reasoning
+
+βˆ₯-uniq
: (H : Matrix (A β„•.+ B) C)
(M : Matrix A C)
(N : Matrix B C)
β†’ H Β· (I ≑ 𝟎) ≋ M
β†’ H Β· (𝟎 ≑ I) ≋ N
β†’ M βˆ₯ N ≋ H
-uniq {A} {B} {C} H M N eq₁ eqβ‚‚
+βˆ₯-uniq {A} {B} {C} H M N eq₁ eqβ‚‚
with (H₁ , Hβ‚‚ , H₁βˆ₯H₂≑H) ← split-βˆ₯ A H
rewrite ≑.sym H₁βˆ₯H₂≑H = begin
M βˆ₯ N β‰ˆβŸ¨ βˆ₯-cong eq₁ eqβ‚‚ ⟨
@@ -273,119 +174,198 @@ uniq {A} {B} {C} H M N eq₁ eqβ‚‚
where
open β‰ˆ-Reasoning (Matrixβ‚› (A β„•.+ B) C)
-coproduct : Coproduct Mat A B
-coproduct {A} {B} = record
- { A+B = A β„•.+ B
- ; i₁ = I ≑ 𝟎
- ; iβ‚‚ = 𝟎 ≑ I
- ; [_,_] = _βˆ₯_
+proj₁ : (M : Matrix A B) (N : Matrix A C) β†’ (I βˆ₯ 𝟎) Β· (M ≑ N) ≋ M
+proj₁ {A} {B} M N = begin
+ (I βˆ₯ 𝟎) Β· (M ≑ N) β‰ˆβŸ¨ βˆ₯-Β·-≑ I 𝟎 M N ⟩
+ (I Β· M) [+] (𝟎 Β· N) β‰ˆβŸ¨ [+]-cong Β·-IΛ‘ (Β·-𝟎ˑ N) ⟩
+ M [+] 𝟎 β‰ˆβŸ¨ [+]-𝟎ʳ M ⟩
+ M ∎
+ where
+ open β‰ˆ-Reasoning (Matrixβ‚› A B)
+
+projβ‚‚ : (M : Matrix A B) (N : Matrix A C) β†’ (𝟎 βˆ₯ I) Β· (M ≑ N) ≋ N
+projβ‚‚ {A} {_} {C} M N = begin
+ (𝟎 βˆ₯ I) Β· (M ≑ N) β‰ˆβŸ¨ βˆ₯-Β·-≑ 𝟎 I M N ⟩
+ (𝟎 Β· M) [+] (I Β· N) β‰ˆβŸ¨ [+]-cong (Β·-𝟎ˑ M) Β·-IΛ‘ ⟩
+ 𝟎 [+] N β‰ˆβŸ¨ [+]-𝟎ˑ N ⟩
+ N ∎
+ where
+ open β‰ˆ-Reasoning (Matrixβ‚› A C)
+
+≑-uniq
+ : (H : Matrix A (B β„•.+ C))
+ (M : Matrix A B)
+ (N : Matrix A C)
+ β†’ (I βˆ₯ 𝟎) Β· H ≋ M
+ β†’ (𝟎 βˆ₯ I) Β· H ≋ N
+ β†’ M ≑ N ≋ H
+≑-uniq {A} {B} {C} H M N eq₁ eqβ‚‚
+ with (H₁ , Hβ‚‚ , H₁≑H₂≑H) ← split-≑ B H
+ rewrite ≑.sym H₁≑H₂≑H = begin
+ M ≑ N β‰ˆβŸ¨ ≑-cong eq₁ eqβ‚‚ ⟨
+ (I {B} βˆ₯ 𝟎) Β· (H₁ ≑ Hβ‚‚) ≑ (𝟎 βˆ₯ I) Β· (H₁ ≑ Hβ‚‚) β‰ˆβŸ¨ ≑-cong (proj₁ H₁ Hβ‚‚) (projβ‚‚ H₁ Hβ‚‚) ⟩
+ H₁ ≑ Hβ‚‚ ∎
+ where
+ open β‰ˆ-Reasoning (Matrixβ‚› A (B β„•.+ C))
+
+
+isCoproduct : IsCoproduct Mat (I {A} ≑ 𝟎) (𝟎 ≑ I {B})
+isCoproduct {A} {B} = record
+ { [_,_] = _βˆ₯_
; inject₁ = Ξ» {a} {b} {c} β†’ inj₁ b c
; injectβ‚‚ = Ξ» {a} {b} {c} β†’ injβ‚‚ b c
- ; unique = Ξ» eq₁ eqβ‚‚ β†’ uniq _ _ _ eq₁ eqβ‚‚
+ ; unique = Ξ» eq₁ eqβ‚‚ β†’ βˆ₯-uniq _ _ _ eq₁ eqβ‚‚
}
+isProduct : IsProduct Mat (I {A} βˆ₯ 𝟎) (𝟎 βˆ₯ I {B})
+isProduct {A} {B} = record
+ { ⟨_,_⟩ = _≑_
+ ; project₁ = Ξ» {a} {b} {c} β†’ proj₁ b c
+ ; projectβ‚‚ = Ξ» {a} {b} {c} β†’ projβ‚‚ b c
+ ; unique = Ξ» eq₁ eqβ‚‚ β†’ ≑-uniq _ _ _ eq₁ eqβ‚‚
+ }
+
+opaque
+
+ unfolding Matrix
+
+ Ο€β‚βˆ˜i₁ : (I {A} βˆ₯ 𝟎 {B}) Β· (I ≑ 𝟎) ≋ I
+ Ο€β‚βˆ˜i₁ {A} = begin
+ (I βˆ₯ 𝟎) Β· (I ≑ 𝟎) β‰ˆβŸ¨ βˆ₯-Β·-≑ I 𝟎 I 𝟎 ⟩
+ (I Β· I) [+] (𝟎 Β· 𝟎) β‰ˆβŸ¨ [+]-cong Β·-IΛ‘ (Β·-𝟎ˑ 𝟎) ⟩
+ I [+] 𝟎 β‰ˆβŸ¨ [+]-𝟎ʳ I ⟩
+ I ∎
+ where
+ open β‰ˆ-Reasoning (Matrixβ‚› A A)
+
+ Ο€β‚‚βˆ˜iβ‚‚ : (𝟎 {A} {B} βˆ₯ I) Β· (𝟎 ≑ I) ≋ I
+ Ο€β‚‚βˆ˜iβ‚‚ {A} {B} = begin
+ (𝟎 βˆ₯ I) Β· (𝟎 ≑ I) β‰ˆβŸ¨ βˆ₯-Β·-≑ 𝟎 I 𝟎 I ⟩
+ (𝟎 Β· 𝟎) [+] (I Β· I) β‰ˆβŸ¨ [+]-cong (Β·-𝟎ˑ 𝟎) Β·-IΛ‘ ⟩
+ 𝟎 [+] I β‰ˆβŸ¨ [+]-𝟎ˑ I ⟩
+ I ∎
+ where
+ open β‰ˆ-Reasoning (Matrixβ‚› B B)
+
+ Ο€β‚βˆ˜iβ‚‚ : (I {A} βˆ₯ 𝟎 {B}) Β· (𝟎 ≑ I) ≋ 𝟎 {B} {A}
+ Ο€β‚βˆ˜iβ‚‚ {A} {B} = begin
+ (I βˆ₯ 𝟎) Β· (𝟎 ≑ I) β‰ˆβŸ¨ βˆ₯-Β·-≑ I 𝟎 𝟎 I ⟩
+ (I Β· 𝟎) [+] (𝟎 Β· I) β‰ˆβŸ¨ [+]-cong (Β·-𝟎ʳ I) (Β·-𝟎ˑ I) ⟩
+ 𝟎 [+] 𝟎 β‰ˆβŸ¨ [+]-𝟎ʳ 𝟎 ⟩
+ 𝟎 ∎
+ where
+ open β‰ˆ-Reasoning (Matrixβ‚› B A)
+
+ Ο€β‚‚βˆ˜i₁ : (𝟎 {A} {B} βˆ₯ I) Β· (I ≑ 𝟎) ≋ 𝟎 {A} {B}
+ Ο€β‚‚βˆ˜i₁ {A} {B} = begin
+ (𝟎 βˆ₯ I) Β· (I ≑ 𝟎) β‰ˆβŸ¨ βˆ₯-Β·-≑ 𝟎 I I 𝟎 ⟩
+ (𝟎 Β· I) [+] (I Β· 𝟎) β‰ˆβŸ¨ [+]-cong (Β·-𝟎ˑ I) (Β·-𝟎ʳ I) ⟩
+ 𝟎 [+] 𝟎 β‰ˆβŸ¨ [+]-𝟎ʳ 𝟎 ⟩
+ 𝟎 ∎
+ where
+ open β‰ˆ-Reasoning (Matrixβ‚› A B)
+
+ permute
+ : (I ≑ 𝟎 {A} {B}) Β· (I βˆ₯ 𝟎 {B} {A}) Β· (𝟎 {B} {A} ≑ I) Β· (𝟎 {A} {B} βˆ₯ I)
+ ≋ (𝟎 {B} {A} ≑ I) Β· (𝟎 {A} {B} βˆ₯ I) Β· (I ≑ 𝟎 {A} {B}) Β· (I βˆ₯ 𝟎 {B} {A})
+ permute {A} {B} = begin
+ (I ≑ 𝟎) Β· (I βˆ₯ 𝟎 {B} {A}) Β· (𝟎 {B} {A} ≑ I) Β· (𝟎 {A} {B} βˆ₯ I) β‰ˆβŸ¨ Β·-resp-≋ ≋.refl Β·-assoc ⟨
+ (I ≑ 𝟎) Β· ((I βˆ₯ 𝟎 {B} {A}) Β· (𝟎 {B} {A} ≑ I)) Β· (𝟎 {A} {B} βˆ₯ I) β‰ˆβŸ¨ Β·-resp-≋ ≋.refl (Β·-resp-≋ Ο€β‚βˆ˜iβ‚‚ ≋.refl) ⟩
+ (I ≑ 𝟎) Β· 𝟎 {B} {A} Β· (𝟎 {A} {B} βˆ₯ I) β‰ˆβŸ¨ Β·-resp-≋ ≋.refl (Β·-𝟎ˑ (𝟎 βˆ₯ I)) ⟩
+ (I ≑ 𝟎 {A} {B}) Β· 𝟎 β‰ˆβŸ¨ Β·-𝟎ʳ (I ≑ 𝟎) ⟩
+ 𝟎 β‰ˆβŸ¨ Β·-𝟎ʳ (𝟎 ≑ I) ⟨
+ (𝟎 {B} {A} ≑ I) Β· 𝟎 β‰ˆβŸ¨ Β·-resp-≋ ≋.refl (Β·-𝟎ˑ (I βˆ₯ 𝟎)) ⟨
+ (𝟎 ≑ I) Β· 𝟎 {A} {B} Β· (I βˆ₯ 𝟎 {B} {A}) β‰ˆβŸ¨ Β·-resp-≋ ≋.refl (Β·-resp-≋ Ο€β‚‚βˆ˜i₁ ≋.refl) ⟨
+ (𝟎 {B} {A} ≑ I) Β· ((𝟎 βˆ₯ I) Β· (I ≑ 𝟎 {A} {B})) Β· (I βˆ₯ 𝟎 {B} {A}) β‰ˆβŸ¨ Β·-resp-≋ ≋.refl Β·-assoc ⟩
+ (𝟎 {B} {A} ≑ I) Β· (𝟎 {A} {B} βˆ₯ I) Β· (I ≑ 𝟎 {A} {B}) Β· (I βˆ₯ 𝟎) ∎
+ where
+ open β‰ˆ-Reasoning (Matrixβ‚› (A β„•.+ B) (A β„•.+ B))
+
+biproduct : Biproduct Mat A B
+biproduct {A} {B} = record
+ { AβŠ•B = A β„•.+ B
+ ; π₁ = I βˆ₯ 𝟎
+ ; Ο€β‚‚ = 𝟎 βˆ₯ I
+ ; i₁ = I ≑ 𝟎
+ ; iβ‚‚ = 𝟎 ≑ I
+ ; isBiproduct = record
+ { isCoproduct = isCoproduct
+ ; isProduct = isProduct
+ ; Ο€β‚βˆ˜iβ‚β‰ˆid = Ο€β‚βˆ˜i₁
+ ; Ο€β‚‚βˆ˜iβ‚‚β‰ˆid = Ο€β‚‚βˆ˜iβ‚‚
+ ; permute = permute
+ }
+ }
+
+[Iβˆ₯𝟎]α΅€ : (I βˆ₯ 𝟎 {B} {A}) α΅€ ≋ I ≑ 𝟎
+[Iβˆ₯𝟎]α΅€ {B} {A} = begin
+ (I βˆ₯ 𝟎) α΅€ β‰‘βŸ¨ βˆ₯-α΅€ I 𝟎 ⟩
+ I α΅€ ≑ 𝟎 α΅€ β‰‘βŸ¨ ≑.congβ‚‚ _≑_ Iα΅€ πŸŽα΅€ ⟩
+ I ≑ 𝟎 ∎
+ where
+ open β‰ˆ-Reasoning (Matrixβ‚› A (A β„•.+ B))
+
+[𝟎βˆ₯I]α΅€ : (𝟎 {A} {B} βˆ₯ I) α΅€ ≋ 𝟎 ≑ I
+[𝟎βˆ₯I]α΅€ {A} {B} = begin
+ (𝟎 βˆ₯ I) α΅€ β‰‘βŸ¨ βˆ₯-α΅€ 𝟎 I ⟩
+ 𝟎 α΅€ ≑ I α΅€ β‰‘βŸ¨ ≑.congβ‚‚ _≑_ πŸŽα΅€ Iα΅€ ⟩
+ 𝟎 ≑ I ∎
+ where
+ open β‰ˆ-Reasoning (Matrixβ‚› B (A β„•.+ B))
+
opaque
+
unfolding _≋_
+
Β‘-unique : (E : Matrix 0 B) β†’ []α΅₯ ≋ E
Β‘-unique E = ≋.reflexive (≑.sym ([]α΅₯-! E))
-initial : Initial Mat
-initial = record
- { βŠ₯ = 0
- ; βŠ₯-is-initial = record
- { Β‘ = []α΅₯
- ; Β‘-unique = Β‘-unique
- }
+ !-unique : (E : Matrix A 0) β†’ []β‚• ≋ E
+ !-unique E = ≋.reflexive (≑.sym ([]β‚•-! E))
+
+isInitial : IsInitial Mat 0
+isInitial = record
+ { Β‘ = []α΅₯
+ ; Β‘-unique = Β‘-unique
}
-Mat-Cocartesian : Cocartesian Mat
-Mat-Cocartesian = record
- { initial = initial
- ; coproducts = record
- { coproduct = coproduct
- }
+isTerminal : IsTerminal Mat 0
+isTerminal = record
+ { ! = []β‚•
+ ; !-unique = !-unique
}
-Mat-DaggerCocartesian : DaggerCocartesianMonoidal Mat
-Mat-DaggerCocartesian = record
- { cocartesian = Mat-Cocartesian
- ; dagger = record
- { _† = Ξ» M β†’ M α΅€
- ; †-identity = ≋.reflexive Iα΅€
- ; †-homomorphism = Ξ» {f = f} {g} β†’ Β·-α΅€ f g
- ; †-resp-β‰ˆ = α΅€-cong
- ; †-involutive = α΅€-involutive
+zeroObj : Zero Mat
+zeroObj = record
+ { 𝟘 = 0
+ ; isZero = record
+ { isInitial = isInitial
+ ; isTerminal = isTerminal
}
- ; λ≅† = ≋λᡀ
- ; ρ≅† = ≋ρᡀ
- ; α≅† = ≋αᡀ
- ; σ≅† = ≋σᡀ
- ; †-resp-βŠ— = α΅€-resp-βŠ—
}
-p₁-i₁ : (I ≑ 𝟎) α΅€ Β· (I ≑ 𝟎 {A} {B}) ≋ I
-p₁-i₁ = begin
- (I ≑ 𝟎) α΅€ Β· (I ≑ 𝟎) β‰‘βŸ¨ ≑.cong (_Β· (I ≑ 𝟎)) (≑-α΅€ I 𝟎) ⟩
- (I α΅€ βˆ₯ 𝟎 α΅€) Β· (I ≑ 𝟎) β‰‘βŸ¨ ≑.congβ‚‚ (Ξ» h₁ hβ‚‚ β†’ (h₁ βˆ₯ hβ‚‚) Β· (I ≑ 𝟎)) Iα΅€ πŸŽα΅€ ⟩
- (I βˆ₯ 𝟎) Β· (I ≑ 𝟎) β‰ˆβŸ¨ βˆ₯-Β·-≑ I 𝟎 I 𝟎 ⟩
- (I Β· I) [+] (𝟎 Β· 𝟎) β‰ˆβŸ¨ [+]-cong Β·-IΛ‘ (Β·-𝟎ˑ 𝟎) ⟩
- I [+] 𝟎 β‰ˆβŸ¨ [+]-𝟎ʳ I ⟩
- I ∎
- where
- open β‰ˆ-Reasoning (Matrixβ‚› _ _)
-
-pβ‚‚-iβ‚‚ : (𝟎 {A} {B} ≑ I) α΅€ Β· (𝟎 ≑ I) ≋ I
-pβ‚‚-iβ‚‚ = begin
- (𝟎 ≑ I) α΅€ Β· (𝟎 ≑ I) β‰‘βŸ¨ ≑.cong (_Β· (𝟎 ≑ I)) (≑-α΅€ 𝟎 I) ⟩
- (𝟎 α΅€ βˆ₯ I α΅€) Β· (𝟎 ≑ I) β‰‘βŸ¨ ≑.congβ‚‚ (Ξ» h₁ hβ‚‚ β†’ (h₁ βˆ₯ hβ‚‚) Β· (𝟎 ≑ I)) πŸŽα΅€ Iα΅€ ⟩
- (𝟎 βˆ₯ I) Β· (𝟎 ≑ I) β‰ˆβŸ¨ βˆ₯-Β·-≑ 𝟎 I 𝟎 I ⟩
- (𝟎 Β· 𝟎) [+] (I Β· I) β‰ˆβŸ¨ [+]-cong (Β·-𝟎ˑ 𝟎) Β·-IΛ‘ ⟩
- 𝟎 [+] I β‰ˆβŸ¨ [+]-𝟎ˑ I ⟩
- I ∎
- where
- open β‰ˆ-Reasoning (Matrixβ‚› _ _)
-
-opaque
- unfolding 𝟎 mapRows
- []α΅₯Β·[]β‚• : []α΅₯ Β· []β‚• ≑ 𝟎 {A} {B}
- []α΅₯Β·[]β‚• {A} {B} = begin
- map ([_] []β‚•) []α΅₯ β‰‘βŸ¨ map-cong (Ξ» { [] β†’ [⟨⟩]-[]β‚• }) []α΅₯ ⟩
- map (Ξ» _ β†’ ⟨0⟩) []α΅₯ β‰‘βŸ¨ map-const []α΅₯ ⟨0⟩ ⟩
- 𝟎 ∎
- where
- open ≑-Reasoning
+Mat-Semiadditive : Semiadditive Mat
+Mat-Semiadditive = record
+ { zero = zeroObj
+ ; biproducts = record
+ { biproduct = biproduct
+ }
+ }
-pβ‚‚-i₁ : (𝟎 {A} ≑ I) α΅€ Β· (I ≑ 𝟎 {B}) ≋ []α΅₯ Β· []α΅₯ α΅€
-pβ‚‚-i₁ = begin
- (𝟎 ≑ I) α΅€ Β· (I ≑ 𝟎) β‰‘βŸ¨ ≑.cong (_Β· (I ≑ 𝟎)) (≑-α΅€ 𝟎 I) ⟩
- (𝟎 α΅€ βˆ₯ I α΅€) Β· (I ≑ 𝟎) β‰‘βŸ¨ ≑.congβ‚‚ (Ξ» h₁ hβ‚‚ β†’ (h₁ βˆ₯ hβ‚‚) Β· (I ≑ 𝟎)) πŸŽα΅€ Iα΅€ ⟩
- (𝟎 βˆ₯ I) Β· (I ≑ 𝟎) β‰ˆβŸ¨ βˆ₯-Β·-≑ 𝟎 I I 𝟎 ⟩
- (𝟎 Β· I) [+] (I Β· 𝟎) β‰ˆβŸ¨ [+]-cong (Β·-𝟎ˑ I) (Β·-𝟎ʳ I) ⟩
- 𝟎 [+] 𝟎 β‰ˆβŸ¨ [+]-𝟎ˑ 𝟎 ⟩
- 𝟎 β‰‘βŸ¨ []α΅₯Β·[]β‚• ⟨
- []α΅₯ Β· []β‚• β‰‘βŸ¨ ≑.cong ([]α΅₯ Β·_) []α΅₯-α΅€ ⟨
- []α΅₯ Β· []α΅₯ α΅€ ∎
- where
- open β‰ˆ-Reasoning (Matrixβ‚› _ _)
-
-p₁-iβ‚‚ : (I ≑ 𝟎 {A}) α΅€ Β· (𝟎 {B} ≑ I) ≋ []α΅₯ Β· []α΅₯ α΅€
-p₁-iβ‚‚ = begin
- (I ≑ 𝟎) α΅€ Β· (𝟎 ≑ I) β‰‘βŸ¨ ≑.cong (_Β· (𝟎 ≑ I)) (≑-α΅€ I 𝟎) ⟩
- (I α΅€ βˆ₯ 𝟎 α΅€) Β· (𝟎 ≑ I) β‰‘βŸ¨ ≑.congβ‚‚ (Ξ» h₁ hβ‚‚ β†’ (h₁ βˆ₯ hβ‚‚) Β· (𝟎 ≑ I)) Iα΅€ πŸŽα΅€ ⟩
- (I βˆ₯ 𝟎) Β· (𝟎 ≑ I) β‰ˆβŸ¨ βˆ₯-Β·-≑ I 𝟎 𝟎 I ⟩
- (I Β· 𝟎) [+] (𝟎 Β· I) β‰ˆβŸ¨ [+]-cong (Β·-𝟎ʳ I) (Β·-𝟎ˑ I) ⟩
- 𝟎 [+] 𝟎 β‰ˆβŸ¨ [+]-𝟎ˑ 𝟎 ⟩
- 𝟎 β‰‘βŸ¨ []α΅₯Β·[]β‚• ⟨
- []α΅₯ Β· []β‚• β‰‘βŸ¨ ≑.cong ([]α΅₯ Β·_) []α΅₯-α΅€ ⟨
- []α΅₯ Β· []α΅₯ α΅€ ∎
- where
- open β‰ˆ-Reasoning (Matrixβ‚› _ _)
+Mat-HasDagger : HasDagger Mat
+Mat-HasDagger = record
+ { _† = Ξ» M β†’ M α΅€
+ ; †-identity = ≋.reflexive Iα΅€
+ ; †-homomorphism = Ξ» {f = f} {g} β†’ Β·-α΅€ f g
+ ; †-resp-β‰ˆ = α΅€-cong
+ ; †-involutive = α΅€-involutive
+ }
Mat-SemiadditiveDagger : SemiadditiveDagger Mat
Mat-SemiadditiveDagger = record
- { daggerCocartesianMonoidal = Mat-DaggerCocartesian
- ; p₁-i₁ = p₁-i₁
- ; pβ‚‚-iβ‚‚ = pβ‚‚-iβ‚‚
- ; pβ‚‚-i₁ = pβ‚‚-i₁
- ; p₁-iβ‚‚ = p₁-iβ‚‚
+ { semiadditive = Mat-Semiadditive
+ ; dagger = Mat-HasDagger
+ ; π₁† = [Iβˆ₯𝟎]α΅€
+ ; π₂† = [𝟎βˆ₯I]α΅€
+ ; ⟨⟩-† = Ξ» {f = M} {N} β†’ ≋.reflexive (≑-α΅€ M N)
}
generated by cgit v1.2.3 (git 2.39.1) at 2026-07-21 11:44:38 +0000