diff options
Diffstat (limited to 'Category/Dagger/Semiadditive.agda')
| -rw-r--r-- | Category/Dagger/Semiadditive.agda | 24 |
1 files changed, 6 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 + } |