Construct monoidal merge functor

1 files changed, 18 insertions, 0 deletions

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