From d9ede0379448f50a553af4b91ce835836e712bc3 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 18 Jul 2026 16:20:00 -0700 Subject: Simplify semiadditive dagger definition --- Category/BinaryBiproducts.agda | 6 + Category/Dagger/Semiadditive.agda | 507 +++++------------------------------- Category/Semiadditive.agda | 20 +- Data/Matrix/Dagger-2-Poset.agda | 34 ++- Data/Matrix/SemiadditiveDagger.agda | 430 +++++++++++++++--------------- 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 @@ -30,6 +30,20 @@ record Semiadditive : Set (levelOfTerm π’ž) where open HomReasoning open β‡’-Reasoning + 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 @@ -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) @@ -87,18 +92,6 @@ opaque α΅€-involutive : (M : Matrix A B) β†’ (M α΅€) α΅€ ≋ M α΅€-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 α΅€ @@ -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) } -- cgit v1.2.3