diff options
Diffstat (limited to 'Category')
| -rw-r--r-- | Category/BinaryBiproducts.agda | 12 | ||||
| -rw-r--r-- | Category/Dagger/Semiadditive.agda | 37 | ||||
| -rw-r--r-- | Category/Semiadditive.agda | 256 |
3 files changed, 217 insertions, 88 deletions
diff --git a/Category/BinaryBiproducts.agda b/Category/BinaryBiproducts.agda index 3ded5a7..bc0fac8 100644 --- a/Category/BinaryBiproducts.agda +++ b/Category/BinaryBiproducts.agda @@ -329,3 +329,15 @@ record BinaryBiproducts : Set (levelOfTerm 𝒞) where ⟨ π₁ ×₁ π₁ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ , π₂ ×₁ π₂ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩ ⟨ ⟨ π₁ ∘ ⟨ f , g ⟩ , π₁ ∘ ⟨ h , i ⟩ ⟩ , ⟨ π₂ ∘ ⟨ f , g ⟩ , π₂ ∘ ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ project₁ project₁) (⟨⟩-cong₂ project₂ project₂) ⟩ ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩ ∎ + + σ₂₃-⟨⟩-×₁ + : {X Y A B : Obj} + {f : X ⇒ A} + {g : Y ⇒ B} + {h : X ⇒ A} + {i : Y ⇒ B} + → σ₂₃ ∘ ⟨ f ×₁ g , h ×₁ i ⟩ ≈ ⟨ f , h ⟩ ×₁ ⟨ g , i ⟩ + σ₂₃-⟨⟩-×₁ {f = f} {g} {h} {i} = begin + σ₂₃ ∘ ⟨ f ×₁ g , h ×₁ i ⟩ ≈⟨ σ₂₃-⟨⟩ ⟩ + ⟨ ⟨ f ∘ π₁ , h ∘ π₁ ⟩ , ⟨ g ∘ π₂ , i ∘ π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ ⟨⟩∘ ⟨⟩∘ ⟨ + ⟨ ⟨ f , h ⟩ ∘ π₁ , ⟨ g , i ⟩ ∘ π₂ ⟩ ∎ diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda index 41be19e..8c46e14 100644 --- a/Category/Dagger/Semiadditive.agda +++ b/Category/Dagger/Semiadditive.agda @@ -106,10 +106,14 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where +-† : {A B : Obj} {f g : A ⇒ B} → (f + g) † ≈ (f †) + (g †) +-† {f = f} {g} = begin - (∇ ∘ f ×₁ g ∘ Δ) † ≈⟨ †-homomorphism ⟩ - (f ×₁ g ∘ Δ) † ∘ ∇ † ≈⟨ pushˡ †-homomorphism ⟩ - Δ † ∘ (f ×₁ g) † ∘ ∇ † ≈⟨ Δ† ⟩∘⟨ †-resp-×₁ ⟩∘⟨ ∇† ⟩ - ∇ ∘ (f †) ×₁ (g †) ∘ Δ ∎ + (f + g) † ≈⟨ ⟨ +-∇∘⟨⟩ ⟩† ⟩ + (∇ ∘ ⟨ f , g ⟩) † ≈⟨ †-homomorphism ⟩ + ⟨ f , g ⟩ † ∘ ∇ † ≈⟨ refl⟩∘⟨ ∇† ⟩ + ⟨ f , g ⟩ † ∘ Δ ≈⟨ ⟨⟩-† ⟩∘⟨refl ⟩ + [ f † , g † ] ∘ Δ ≈⟨ pushˡ (Equiv.sym ∇∘×₁) ⟩ + ∇ ∘ (f †) ×₁ (g †) ∘ Δ ≈⟨ refl⟩∘⟨ ×₁∘Δ ⟩ + ∇ ∘ ⟨ f † , g † ⟩ ≈⟨ +-∇∘⟨⟩ ⟨ + (f †) + (g †) ∎ -- bilinearity of composition ∘-distribˡ : {A B C : Obj} {f : B ⇒ C} {g h : A ⇒ B} → f ∘ (g + h) ≈ f ∘ g + f ∘ h @@ -170,9 +174,9 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where ≤-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⟩∘⟨ ×₁-congˡ g≤h ⟩∘⟨refl ⟨ + f + h ≈⟨ +-congˡ g≤h ⟨ f + (g + h) ≈⟨ +-assoc f g h ⟨ - (f + g) + h ≈⟨ refl⟩∘⟨ ×₁-congʳ f≤g ⟩∘⟨refl ⟩ + (f + g) + h ≈⟨ +-congʳ f≤g ⟩ g + h ≈⟨ g≤h ⟩ h ∎ @@ -199,14 +203,13 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where → g ≤ i → (f ×₁ g) ≤ (h ×₁ i) ≤-resp-×₁ {f = f} {h} {g} {i} f≤h g≤i = begin - ∇ ∘ (f ×₁ g) ×₁ (h ×₁ i) ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ Δ-⊕ ⟩ - ∇ ∘ (f ×₁ g) ×₁ (h ×₁ i) ∘ σ₂₃ ∘ Δ ×₁ Δ ≈⟨ refl⟩∘⟨ extendʳ σ₂₃-×₁ ⟩ - ∇ ∘ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ ≈⟨ pushˡ ∇-⊕ ⟩ - ∇ ×₁ ∇ ∘ σ₂₃ ∘ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ ≈⟨ refl⟩∘⟨ cancelˡ σ₂₃-σ₂₃ ⟩ - ∇ ×₁ ∇ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ ≈⟨ refl⟩∘⟨ ×₁∘×₁ ⟩ - ∇ ×₁ ∇ ∘ (f ×₁ h ∘ Δ) ×₁ (g ×₁ i ∘ Δ) ≈⟨ ×₁∘×₁ ⟩ - (∇ ∘ f ×₁ h ∘ Δ) ×₁ (∇ ∘ g ×₁ i ∘ Δ) ≈⟨ ×₁-cong₂ f≤h g≤i ⟩ - h ×₁ i ∎ + f ×₁ g + h ×₁ i ≈⟨ +-∇∘⟨⟩ ⟩ + ∇ ∘ ⟨ f ×₁ g , h ×₁ i ⟩ ≈⟨ pushˡ ∇-⊕ ⟩ + ∇ ×₁ ∇ ∘ σ₂₃ ∘ ⟨ f ×₁ g , h ×₁ i ⟩ ≈⟨ refl⟩∘⟨ σ₂₃-⟨⟩-×₁ ⟩ + ∇ ×₁ ∇ ∘ ⟨ f , h ⟩ ×₁ ⟨ g , i ⟩ ≈⟨ ×₁∘×₁ ⟩ + (∇ ∘ ⟨ f , h ⟩) ×₁ (∇ ∘ ⟨ g , i ⟩) ≈⟨ ×₁-cong₂ +-∇∘⟨⟩ +-∇∘⟨⟩ ⟨ + (f + h) ×₁ (g + i) ≈⟨ ×₁-cong₂ f≤h g≤i ⟩ + h ×₁ i ∎ ≤-resp-∘ : {A B C : Obj} @@ -234,9 +237,9 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where -- special law ∇∘Δ : {A : Obj} → ∇ ∘ Δ ≈ id {A} ∇∘Δ = begin - ∇ ∘ Δ ≈⟨ refl⟩∘⟨ introˡ id×₁id ⟩ - ∇ ∘ id ×₁ id ∘ Δ ≈⟨ idempotent ⟩ - id ∎ + ∇ ∘ Δ ≈⟨ +-∇∘⟨⟩ ⟨ + id + id ≈⟨ idempotent ⟩ + id ∎ dagger-2-poset : Dagger-2-Poset dagger-2-poset = record diff --git a/Category/Semiadditive.agda b/Category/Semiadditive.agda index 7d34fbf..30f84e6 100644 --- a/Category/Semiadditive.agda +++ b/Category/Semiadditive.agda @@ -18,7 +18,10 @@ open import Categories.Object.Zero 𝒞 using (Zero) open import Category.BinaryBiproducts 𝒞 using (BinaryBiproducts) open import Data.Product using (_,_) -private module 𝒞 = Category 𝒞 +private + module 𝒞 = Category 𝒞 + variable + A B C D : 𝒞.Obj -- A semiadditive category has all finite biproducts record Semiadditive : Set (levelOfTerm 𝒞) where @@ -32,9 +35,43 @@ record Semiadditive : Set (levelOfTerm 𝒞) where open 𝒞 + infix 8 _+_ + + field + 𝟎 : A ⇒ B + 𝟎-resp-∘ : {h : A ⇒ B} {k : C ⇒ D} → k ∘ 𝟎 ∘ h ≈ 𝟎 + _+_ : A ⇒ B → A ⇒ B → A ⇒ B + +-resp-≈ : {x y u v : A ⇒ B} → x ≈ y → u ≈ v → x + u ≈ y + v + +-resp-∘ : {f g : B ⇒ C} {h : A ⇒ B} {k : C ⇒ D} → k ∘ (f + g) ∘ h ≈ k ∘ f ∘ h + k ∘ g ∘ h + +-identityˡ : (f : A ⇒ B) → 𝟎 + f ≈ f + +-identityʳ : (f : A ⇒ B) → f + 𝟎 ≈ f + open HomReasoning open ⇒-Reasoning + +-cong : {x y u v : A ⇒ B} → x ≈ y → u ≈ v → x + u ≈ y + v + +-cong = +-resp-≈ + + +-resp-∘ˡ + : {A B C : Obj} + {f g : A ⇒ B} + {k : B ⇒ C} + → k ∘ (f + g) ≈ k ∘ f + k ∘ g + +-resp-∘ˡ {f = f} {g} {h} = begin + h ∘ (f + g) ≈⟨ refl⟩∘⟨ identityʳ ⟨ + h ∘ (f + g) ∘ id ≈⟨ +-resp-∘ ⟩ + h ∘ f ∘ id + h ∘ g ∘ id ≈⟨ +-resp-≈ (refl⟩∘⟨ identityʳ) (refl⟩∘⟨ identityʳ) ⟩ + h ∘ f + h ∘ g ∎ + + 𝟎-resp-∘ˡ + : {A B C : Obj} + {f : B ⇒ C} + → f ∘ 𝟎 {A} {B} ≈ 𝟎 + 𝟎-resp-∘ˡ {f = f} = begin + f ∘ 𝟎 ≈⟨ refl⟩∘⟨ identityʳ ⟨ + f ∘ 𝟎 ∘ id ≈⟨ 𝟎-resp-∘ ⟩ + 𝟎 ∎ + module _ {A B : Obj} where π₁∘i₂≈0 : π₁ {A} {B} ∘ i₂ ≈ zero⇒ @@ -49,6 +86,38 @@ record Semiadditive : Set (levelOfTerm 𝒞) where zero⇒ {A} ∘ π₂ ∘ i₁ ≈⟨ zero-∘ʳ (π₂ ∘ i₁) ⟩ zero⇒ ∎ + 𝟎≈zero⇒ : 𝟎 {A} {B} ≈ zero⇒ + 𝟎≈zero⇒ = begin + 𝟎 ≈⟨ 𝟎-resp-∘ˡ ⟨ + zero⇒ ∘ 𝟎 ≈⟨ zero-∘ʳ {A} {B} 𝟎 ⟩ + zero⇒ ∎ + + module _ {A B : Obj} where + + +-∇∘⟨⟩ : {f g : A ⇒ B} → f + g ≈ ∇ ∘ ⟨ f , g ⟩ + +-∇∘⟨⟩ {f} {g} = begin + f + g ≈⟨ +-resp-≈ (insertˡ inject₁) (insertˡ inject₂) ⟩ + ∇ ∘ i₁ ∘ f + ∇ ∘ i₂ ∘ g ≈⟨ +-resp-∘ˡ ⟨ + ∇ ∘ (i₁ ∘ f + i₂ ∘ g) ≈⟨ refl⟩∘⟨ ⟨⟩-unique left right ⟨ + ∇ ∘ ⟨ f , g ⟩ ∎ + where + left : π₁ ∘ (i₁ ∘ f + i₂ ∘ g) ≈ f + left = begin + π₁ ∘ (i₁ ∘ f + i₂ ∘ g) ≈⟨ +-resp-∘ˡ ⟩ + π₁ ∘ i₁ ∘ f + π₁ ∘ i₂ ∘ g ≈⟨ +-resp-≈ (cancelˡ π₁∘i₁≈id) (pullˡ π₁∘i₂≈0) ⟩ + f + zero⇒ ∘ g ≈⟨ +-resp-≈ Equiv.refl (zero-∘ʳ g) ⟩ + f + zero⇒ ≈⟨ +-resp-≈ Equiv.refl 𝟎≈zero⇒ ⟨ + f + 𝟎 ≈⟨ +-identityʳ f ⟩ + f ∎ + right : π₂ ∘ (i₁ ∘ f + i₂ ∘ g) ≈ g + right = begin + π₂ ∘ (i₁ ∘ f + i₂ ∘ g) ≈⟨ +-resp-∘ˡ ⟩ + π₂ ∘ i₁ ∘ f + π₂ ∘ i₂ ∘ g ≈⟨ +-resp-≈ (pullˡ π₂∘i₁≈0) (cancelˡ π₂∘i₂≈id) ⟩ + zero⇒ ∘ f + g ≈⟨ +-resp-≈ (zero-∘ʳ f) Equiv.refl ⟩ + zero⇒ + g ≈⟨ +-resp-≈ 𝟎≈zero⇒ Equiv.refl ⟨ + 𝟎 + g ≈⟨ +-identityˡ g ⟩ + g ∎ + Δ-⊕ : {X Y : Obj} → Δ {X ⊕ Y} ≈ σ₂₃ ∘ Δ ×₁ Δ Δ-⊕ {X} {Y} = begin ⟨ id , id ⟩ ≈⟨ ⟨⟩-cong₂ id×₁id id×₁id ⟨ @@ -69,45 +138,17 @@ record Semiadditive : Set (levelOfTerm 𝒞) where module _ {A B : Obj} where - _+_ _+′_ : A ⇒ B → A ⇒ B → A ⇒ B - f + g = ∇ ∘ f ×₁ g ∘ Δ - f +′ g = ∇ ∘ f +₁ g ∘ Δ - - infix 8 _+_ - - +-cong : {x y u v : A ⇒ B} → x ≈ y → u ≈ v → x + u ≈ y + v - +-cong eq₁ eq₂ = refl⟩∘⟨ ×₁-cong₂ eq₁ eq₂ ⟩∘⟨refl - +-assoc : (x y z : A ⇒ B) → (x + y) + z ≈ x + (y + z) +-assoc x y z = begin - ∇ ∘ (∇ ∘ x ×₁ y ∘ Δ) ×₁ z ∘ Δ ≈⟨ refl⟩∘⟨ pushˡ (Equiv.sym first∘×₁) ⟩ - ∇ ∘ ∇ ×₁ id ∘ (x ×₁ y ∘ Δ) ×₁ z ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym ×₁∘first) ⟩ - ∇ ∘ ∇ ×₁ id ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ ≈⟨ extendʳ ∇-assoc-×₁ ⟩ - ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ ≈⟨ refl⟩∘⟨ pullʳ (extendʳ assocˡ∘×₁) ⟩ - ∇ ∘ id ×₁ ∇ ∘ x ×₁ y ×₁ z ∘ assocˡ ∘ Δ ×₁ id ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ Δ-assoc ⟨ - ∇ ∘ id ×₁ ∇ ∘ x ×₁ y ×₁ z ∘ id ×₁ Δ ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ ×₁∘second ⟩ - ∇ ∘ id ×₁ ∇ ∘ x ×₁ (y ×₁ z ∘ Δ) ∘ Δ ≈⟨ refl⟩∘⟨ pullˡ second∘×₁ ⟩ - ∇ ∘ x ×₁ (∇ ∘ y ×₁ z ∘ Δ) ∘ Δ ∎ - - +-identityˡ : (x : A ⇒ B) → zero⇒ + x ≈ x - +-identityˡ x = begin - ∇ ∘ zero⇒ ×₁ x ∘ Δ ≈⟨ refl⟩∘⟨ ×₁∘Δ ⟩ - ∇ ∘ ⟨ zero⇒ , x ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (zero-∘ʳ x) identityˡ ⟨ - ∇ ∘ ⟨ zero⇒ ∘ x , id ∘ x ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨ - ∇ ∘ ⟨ zero⇒ , id ⟩ ∘ x ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₁∘i₂≈0 π₂∘i₂≈id ⟩∘⟨refl ⟨ - ∇ ∘ ⟨ π₁ ∘ i₂ , π₂ ∘ i₂ ⟩ ∘ x ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩ - ∇ ∘ i₂ ∘ x ≈⟨ cancelˡ ∇-identityˡ ⟩ - x ∎ - - +-identityʳ : (x : A ⇒ B) → x + zero⇒ ≈ x - +-identityʳ x = begin - ∇ ∘ x ×₁ zero⇒ ∘ Δ ≈⟨ refl⟩∘⟨ ×₁∘Δ ⟩ - ∇ ∘ ⟨ x , zero⇒ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ (zero-∘ʳ x) ⟨ - ∇ ∘ ⟨ id ∘ x , zero⇒ ∘ x ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨ - ∇ ∘ ⟨ id , zero⇒ ⟩ ∘ x ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₁∘i₁≈id π₂∘i₁≈0 ⟩∘⟨refl ⟨ - ∇ ∘ ⟨ π₁ ∘ i₁ , π₂ ∘ i₁ ⟩ ∘ x ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩ - ∇ ∘ i₁ ∘ x ≈⟨ cancelˡ ∇-identityʳ ⟩ - x ∎ + (x + y) + z ≈⟨ +-∇∘⟨⟩ ⟩ + ∇ ∘ ⟨ x + y , z ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ +-∇∘⟨⟩ ⟩ + ∇ ∘ ⟨ ∇ ∘ ⟨ x , y ⟩ , z ⟩ ≈⟨ refl⟩∘⟨ first∘⟨⟩ ⟨ + ∇ ∘ ∇ ×₁ id ∘ ⟨ ⟨ x , y ⟩ , z ⟩ ≈⟨ extendʳ ∇-assoc-×₁ ⟩ + ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ x , y ⟩ , z ⟩ ≈⟨ refl⟩∘⟨ pullʳ assocˡ∘⟨⟩ ⟩ + ∇ ∘ id ×₁ ∇ ∘ ⟨ x , ⟨ y , z ⟩ ⟩ ≈⟨ refl⟩∘⟨ second∘⟨⟩ ⟩ + ∇ ∘ ⟨ x , ∇ ∘ ⟨ y , z ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ +-∇∘⟨⟩ ⟨ + ∇ ∘ ⟨ x , y + z ⟩ ≈⟨ +-∇∘⟨⟩ ⟨ + x + (y + z) ∎ ∇∘+-swap : {A : Obj} → ∇ ∘ +-swap {A} ≈ ∇ ∇∘+-swap = begin @@ -123,19 +164,20 @@ record Semiadditive : Set (levelOfTerm 𝒞) where +-comm : (x y : A ⇒ B) → x + y ≈ y + x +-comm x y = begin - ∇ ∘ x ×₁ y ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ swap∘Δ ⟨ - ∇ ∘ x ×₁ y ∘ swap ∘ Δ ≈⟨ refl⟩∘⟨ extendʳ swap∘×₁ ⟨ - ∇ ∘ swap ∘ y ×₁ x ∘ Δ ≈⟨ refl⟩∘⟨ swap≈+-swap ⟩∘⟨refl ⟩ - ∇ ∘ +-swap ∘ y ×₁ x ∘ Δ ≈⟨ pullˡ ∇∘+-swap ⟩ - ∇ ∘ y ×₁ x ∘ Δ ∎ - - isCM : IsCommutativeMonoid (_≈_ {A} {B}) _+_ zero⇒ + x + y ≈⟨ +-∇∘⟨⟩ ⟩ + ∇ ∘ ⟨ x , y ⟩ ≈⟨ refl⟩∘⟨ swap∘⟨⟩ ⟨ + ∇ ∘ swap ∘ ⟨ y , x ⟩ ≈⟨ refl⟩∘⟨ swap≈+-swap ⟩∘⟨refl ⟩ + ∇ ∘ +-swap ∘ ⟨ y , x ⟩ ≈⟨ pullˡ ∇∘+-swap ⟩ + ∇ ∘ ⟨ y , x ⟩ ≈⟨ +-∇∘⟨⟩ ⟨ + y + x ∎ + + isCM : IsCommutativeMonoid (_≈_ {A} {B}) _+_ 𝟎 isCM = record { isMonoid = record { isSemigroup = record { isMagma = record { isEquivalence = equiv - ; ∙-cong = +-cong + ; ∙-cong = +-resp-≈ } ; assoc = +-assoc } @@ -149,39 +191,16 @@ record Semiadditive : Set (levelOfTerm 𝒞) where { Carrier = A ⇒ B ; _≈_ = _≈_ ; _∙_ = _+_ - ; ε = zero⇒ + ; ε = 𝟎 ; isCommutativeMonoid = isCM } - +-resp-∘ - : {A B C D : Obj} - {f g : B ⇒ C} - {h : A ⇒ B} - {k : C ⇒ D} - → k ∘ (f + g) ∘ h ≈ k ∘ f ∘ h + k ∘ g ∘ h - +-resp-∘ {f = f} {g} {h} {k} = begin - k ∘ (∇ ∘ f ×₁ g ∘ Δ) ∘ h ≈⟨ extendʳ (extendʳ ⇒∇-×₁) ⟩ - ∇ ∘ (k ×₁ k ∘ f ×₁ g ∘ Δ) ∘ h ≈⟨ refl⟩∘⟨ pullʳ (pullʳ ⇒Δ) ⟩ - ∇ ∘ k ×₁ k ∘ f ×₁ g ∘ h ×₁ h ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ ×₁∘×₁ ⟩ - ∇ ∘ k ×₁ k ∘ (f ∘ h) ×₁ (g ∘ h) ∘ Δ ≈⟨ refl⟩∘⟨ pullˡ ×₁∘×₁ ⟩ - ∇ ∘ (k ∘ f ∘ h) ×₁ (k ∘ g ∘ h) ∘ Δ ∎ - - 0-resp-∘ - : {A C D : Obj} - {h : A ⇒ C} - {k : C ⇒ D} - → k ∘ zero⇒ ∘ h ≈ zero⇒ - 0-resp-∘ {h = h} {k} = begin - k ∘ zero⇒ ∘ h ≈⟨ pullˡ (zero-∘ˡ k) ⟩ - zero⇒ ∘ h ≈⟨ zero-∘ʳ h ⟩ - zero⇒ ∎ - cm-category : CM-Category o ℓ e cm-category = record { 𝒞 ; Hom = hom ; +-resp-∘ = +-resp-∘ - ; 0-resp-∘ = 0-resp-∘ + ; 0-resp-∘ = 𝟎-resp-∘ } cartesian : Cartesian @@ -195,3 +214,98 @@ record Semiadditive : Set (levelOfTerm 𝒞) where { initial = initial ; coproducts = binaryCoproducts } + +record SemiadditiveHelper : Set (levelOfTerm 𝒞) where + + field + zero : Zero + biproducts : BinaryBiproducts + + open Zero zero + open BinaryBiproducts biproducts + open 𝒞 + 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⇒ ∎ + +-- Construct hom-set addition from biproduct +semiadditveHelper : SemiadditiveHelper → Semiadditive +semiadditveHelper sh = record + { zero = zero + ; biproducts = biproducts + ; 𝟎 = zero⇒ + ; 𝟎-resp-∘ = 𝟎-resp-∘ + ; _+_ = _+_ + ; +-resp-≈ = +-cong + ; +-resp-∘ = +-resp-∘ + ; +-identityˡ = +-identityˡ + ; +-identityʳ = +-identityʳ + } + where + open SemiadditiveHelper sh + open Zero zero + open BinaryBiproducts biproducts + open 𝒞 + open HomReasoning + open ⇒-Reasoning + + 𝟎-resp-∘ + : {A B C D : Obj} + {h : A ⇒ B} + {k : C ⇒ D} + → k ∘ zero⇒ ∘ h ≈ zero⇒ + 𝟎-resp-∘ {h = h} {k} = begin + k ∘ zero⇒ ∘ h ≈⟨ pullˡ (zero-∘ˡ k) ⟩ + zero⇒ ∘ h ≈⟨ zero-∘ʳ h ⟩ + zero⇒ ∎ + + infix 8 _+_ + + _+_ : A ⇒ B → A ⇒ B → A ⇒ B + f + g = ∇ ∘ ⟨ f , g ⟩ + + +-cong : {x y u v : A ⇒ B} → x ≈ y → u ≈ v → x + u ≈ y + v + +-cong eq₁ eq₂ = refl⟩∘⟨ ⟨⟩-cong₂ eq₁ eq₂ + + +-resp-∘ + : {A B C D : Obj} + {f g : B ⇒ C} + {h : A ⇒ B} + {k : C ⇒ D} + → k ∘ (f + g) ∘ h ≈ k ∘ f ∘ h + k ∘ g ∘ h + +-resp-∘ {f = f} {g} {h} {k} = begin + k ∘ (∇ ∘ ⟨ f , g ⟩) ∘ h ≈⟨ refl⟩∘⟨ pullʳ ⟨⟩∘ ⟩ + k ∘ ∇ ∘ ⟨ f ∘ h , g ∘ h ⟩ ≈⟨ extendʳ ⇒∇-×₁ ⟩ + ∇ ∘ k ×₁ k ∘ ⟨ f ∘ h , g ∘ h ⟩ ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟩ + ∇ ∘ ⟨ k ∘ f ∘ h , k ∘ g ∘ h ⟩ ∎ + + +-identityˡ : (x : A ⇒ B) → zero⇒ + x ≈ x + +-identityˡ x = begin + ∇ ∘ ⟨ zero⇒ , x ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (zero-∘ʳ x) identityˡ ⟨ + ∇ ∘ ⟨ zero⇒ ∘ x , id ∘ x ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨ + ∇ ∘ ⟨ zero⇒ , id ⟩ ∘ x ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₁∘i₂≈0 π₂∘i₂≈id ⟩∘⟨refl ⟨ + ∇ ∘ ⟨ π₁ ∘ i₂ , π₂ ∘ i₂ ⟩ ∘ x ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩ + ∇ ∘ i₂ ∘ x ≈⟨ cancelˡ ∇-identityˡ ⟩ + x ∎ + + +-identityʳ : (x : A ⇒ B) → x + zero⇒ ≈ x + +-identityʳ x = begin + ∇ ∘ ⟨ x , zero⇒ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ (zero-∘ʳ x) ⟨ + ∇ ∘ ⟨ id ∘ x , zero⇒ ∘ x ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨ + ∇ ∘ ⟨ id , zero⇒ ⟩ ∘ x ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₁∘i₁≈id π₂∘i₁≈0 ⟩∘⟨refl ⟨ + ∇ ∘ ⟨ π₁ ∘ i₁ , π₂ ∘ i₁ ⟩ ∘ x ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩ + ∇ ∘ i₁ ∘ x ≈⟨ cancelˡ ∇-identityʳ ⟩ + x ∎ |