From 1528b2a49c0f006bdeff25a46f8f7ab6c23c73fd Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sun, 19 Jul 2026 12:31:03 -0700 Subject: Simplify wiring diagrams using semiadditive dagger --- Category/BinaryBiproducts.agda | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'Category/BinaryBiproducts.agda') diff --git a/Category/BinaryBiproducts.agda b/Category/BinaryBiproducts.agda index 790c73a..c975d18 100644 --- a/Category/BinaryBiproducts.agda +++ b/Category/BinaryBiproducts.agda @@ -224,6 +224,13 @@ record BinaryBiproducts : Set (levelOfTerm π’ž) where [ id , βˆ‡ ] ∘ +-assocΛ‘ β‰ˆβŸ¨ pushΛ‘ (Equiv.sym βˆ‡βˆ˜+₁) ⟩ βˆ‡ ∘ id +₁ βˆ‡ ∘ +-assocΛ‘ ∎ + βˆ‡-assoc-×₁ : {A : Obj} β†’ βˆ‡ {A} ∘ βˆ‡ ×₁ id β‰ˆ βˆ‡ ∘ id ×₁ βˆ‡ ∘ assocΛ‘ + βˆ‡-assoc-×₁ = begin + βˆ‡ ∘ βˆ‡ ×₁ id β‰ˆβŸ¨ refl⟩∘⟨ ×₁-+₁ βˆ‡ id ⟩ + βˆ‡ ∘ βˆ‡ +₁ id β‰ˆβŸ¨ βˆ‡-assoc ⟩ + βˆ‡ ∘ id +₁ βˆ‡ ∘ +-assocΛ‘ β‰ˆβŸ¨ refl⟩∘⟨ ×₁-+₁ id βˆ‡ ⟩∘⟨ assocΛ‘β‰ˆ+-assocΛ‘ ⟨ + βˆ‡ ∘ id ×₁ βˆ‡ ∘ assocΛ‘ ∎ + Ξ”-assoc : {A : Obj} β†’ id ×₁ Ξ” ∘ Ξ” {A} β‰ˆ assocΛ‘ ∘ Ξ” ×₁ id ∘ Ξ” Ξ”-assoc = begin id ×₁ Ξ” ∘ Ξ” β‰ˆβŸ¨ Γ—β‚βˆ˜Ξ” ⟩ @@ -262,3 +269,15 @@ record BinaryBiproducts : Set (levelOfTerm π’ž) where Ξ” ∘ f β‰ˆβŸ¨ Ξ”βˆ˜Β βŸ© ⟨ f , f ⟩ β‰ˆβŸ¨ Γ—β‚βˆ˜Ξ” ⟨ f ×₁ f ∘ Ξ” ∎ + + β‡’βˆ‡-×₁ : {A B : Obj} {f : A β‡’ B} β†’ f ∘ βˆ‡ β‰ˆ βˆ‡ ∘ f ×₁ f + β‡’βˆ‡-×₁ {f = f} = begin + f ∘ βˆ‡ β‰ˆβŸ¨ β‡’βˆ‡ ⟩ + βˆ‡ ∘ f +₁ f β‰ˆβŸ¨ refl⟩∘⟨ ×₁-+₁ f f ⟨ + βˆ‡ ∘ f ×₁ f ∎ + + Γ—β‚βˆ˜first : {A B C D E : Obj} {f : B β‡’ C} {g : D β‡’ E} {h : A β‡’ B} β†’ (f ×₁ g) ∘ first h β‰ˆ (f ∘ h) ×₁ g + Γ—β‚βˆ˜first = Γ—β‚βˆ˜Γ—β‚ β—‹ ×₁-congβ‚‚ Equiv.refl identityΚ³ + + Γ—β‚βˆ˜second : {A B C D E : Obj} {f : A β‡’ B} {g : D β‡’ E} {h : C β‡’ D} β†’ (f ×₁ g) ∘ second h β‰ˆ f ×₁ (g ∘ h) + Γ—β‚βˆ˜second = Γ—β‚βˆ˜Γ—β‚ β—‹ ×₁-congβ‚‚ identityΚ³ Equiv.refl -- cgit v1.2.3