diff options
Diffstat (limited to 'Category')
| -rw-r--r-- | Category/Dagger/Semiadditive.agda | 24 | ||||
| -rw-r--r-- | Category/Semiadditive.agda | 18 |
2 files changed, 24 insertions, 18 deletions
diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda index 424f8df..adcf6ed 100644 --- a/Category/Dagger/Semiadditive.agda +++ b/Category/Dagger/Semiadditive.agda @@ -188,24 +188,6 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where (f + h) + (g + i) ≈⟨ +-cong f≤h g≤i ⟩ h + i ∎ - Δ-⊕ : {X Y : Obj} → Δ {X ⊕ Y} ≈ σ₂₃ ∘ Δ ×₁ Δ - Δ-⊕ {X} {Y} = begin - ⟨ id , id ⟩ ≈⟨ ⟨⟩-cong₂ id×₁id id×₁id ⟨ - ⟨ id ×₁ id , id ×₁ id ⟩ ≈⟨ ⟨⟩-cong₂ (×₁-cong₂ project₁ project₁) (×₁-cong₂ project₂ project₂) ⟨ - ⟨ (π₁ ∘ Δ) ×₁ (π₁ ∘ Δ) , (π₂ ∘ Δ) ×₁ (π₂ ∘ Δ) ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁ ⟨ - ⟨ π₁ ×₁ π₁ ∘ Δ ×₁ Δ , π₂ ×₁ π₂ ∘ Δ ×₁ Δ ⟩ ≈⟨ ⟨⟩∘ ⟨ - σ₂₃ ∘ Δ ×₁ Δ ∎ - - ∇-⊕ : {X Y : Obj} → ∇ {X ⊕ Y} ≈ ∇ ×₁ ∇ ∘ σ₂₃ - ∇-⊕ {X} {Y} = begin - [ id , id ] ≈⟨ []-cong₂ id×₁id id×₁id ⟨ - [ id ×₁ id , id ×₁ id ] ≈⟨ []-cong₂ (×₁-cong₂ inject₁ inject₁) (×₁-cong₂ inject₂ inject₂) ⟨ - [ (∇ ∘ i₁) ×₁ (∇ ∘ i₁) , (∇ ∘ i₂) ×₁ (∇ ∘ i₂) ] ≈⟨ []-cong₂ ×₁∘×₁ ×₁∘×₁ ⟨ - [ ∇ ×₁ ∇ ∘ i₁ ×₁ i₁ , ∇ ×₁ ∇ ∘ i₂ ×₁ i₂ ] ≈⟨ ∘[] ⟨ - ∇ ×₁ ∇ ∘ [ i₁ ×₁ i₁ , i₂ ×₁ i₂ ] ≈⟨ refl⟩∘⟨ ⟨⟩-unique (∘[] ○ []-cong₂ π₁∘×₁ π₁∘×₁) (∘[] ○ []-cong₂ π₂∘×₁ π₂∘×₁) ⟨ - ∇ ×₁ ∇ ∘ ⟨ π₁ +₁ π₁ , π₂ +₁ π₂ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (×₁-+₁ π₁ π₁) (×₁-+₁ π₂ π₂) ⟨ - ∇ ×₁ ∇ ∘ σ₂₃ ∎ - ≤-resp-×₁ : {A B C D : Obj} {f h : A ⇒ B} @@ -409,3 +391,9 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where ; associator = associator ; M } + + maps-MC : MonoidalCategory o (ℓ ⊔ e) e + maps-MC = record + { U = maps + ; monoidal = maps-monoidal + } diff --git a/Category/Semiadditive.agda b/Category/Semiadditive.agda index 86b5585..7d34fbf 100644 --- a/Category/Semiadditive.agda +++ b/Category/Semiadditive.agda @@ -49,6 +49,24 @@ record Semiadditive : Set (levelOfTerm 𝒞) where zero⇒ {A} ∘ π₂ ∘ i₁ ≈⟨ zero-∘ʳ (π₂ ∘ i₁) ⟩ zero⇒ ∎ + Δ-⊕ : {X Y : Obj} → Δ {X ⊕ Y} ≈ σ₂₃ ∘ Δ ×₁ Δ + Δ-⊕ {X} {Y} = begin + ⟨ id , id ⟩ ≈⟨ ⟨⟩-cong₂ id×₁id id×₁id ⟨ + ⟨ id ×₁ id , id ×₁ id ⟩ ≈⟨ ⟨⟩-cong₂ (×₁-cong₂ project₁ project₁) (×₁-cong₂ project₂ project₂) ⟨ + ⟨ (π₁ ∘ Δ) ×₁ (π₁ ∘ Δ) , (π₂ ∘ Δ) ×₁ (π₂ ∘ Δ) ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁ ⟨ + ⟨ π₁ ×₁ π₁ ∘ Δ ×₁ Δ , π₂ ×₁ π₂ ∘ Δ ×₁ Δ ⟩ ≈⟨ ⟨⟩∘ ⟨ + σ₂₃ ∘ Δ ×₁ Δ ∎ + + ∇-⊕ : {X Y : Obj} → ∇ {X ⊕ Y} ≈ ∇ ×₁ ∇ ∘ σ₂₃ + ∇-⊕ {X} {Y} = begin + [ id , id ] ≈⟨ []-cong₂ id×₁id id×₁id ⟨ + [ id ×₁ id , id ×₁ id ] ≈⟨ []-cong₂ (×₁-cong₂ inject₁ inject₁) (×₁-cong₂ inject₂ inject₂) ⟨ + [ (∇ ∘ i₁) ×₁ (∇ ∘ i₁) , (∇ ∘ i₂) ×₁ (∇ ∘ i₂) ] ≈⟨ []-cong₂ ×₁∘×₁ ×₁∘×₁ ⟨ + [ ∇ ×₁ ∇ ∘ i₁ ×₁ i₁ , ∇ ×₁ ∇ ∘ i₂ ×₁ i₂ ] ≈⟨ ∘[] ⟨ + ∇ ×₁ ∇ ∘ [ i₁ ×₁ i₁ , i₂ ×₁ i₂ ] ≈⟨ refl⟩∘⟨ ⟨⟩-unique (∘[] ○ []-cong₂ π₁∘×₁ π₁∘×₁) (∘[] ○ []-cong₂ π₂∘×₁ π₂∘×₁) ⟨ + ∇ ×₁ ∇ ∘ ⟨ π₁ +₁ π₁ , π₂ +₁ π₂ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (×₁-+₁ π₁ π₁) (×₁-+₁ π₂ π₂) ⟨ + ∇ ×₁ ∇ ∘ σ₂₃ ∎ + module _ {A B : Obj} where _+_ _+′_ : A ⇒ B → A ⇒ B → A ⇒ B |