diff options
Diffstat (limited to 'Object/Biproduct.agda')
| -rw-r--r-- | Object/Biproduct.agda | 91 |
1 files changed, 91 insertions, 0 deletions
diff --git a/Object/Biproduct.agda b/Object/Biproduct.agda new file mode 100644 index 0000000..b7c3103 --- /dev/null +++ b/Object/Biproduct.agda @@ -0,0 +1,91 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) + +module Object.Biproduct {o ℓ e} (𝒞 : Category o ℓ e) where + +import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning + +open import Categories.Object.Biproduct 𝒞 using () renaming (module Biproduct to Biproduct′) +open import Categories.Object.Biproduct 𝒞 public hiding (module Biproduct) +open import Morphism.Zero 𝒞 using (IsZero⇒) + +open Category 𝒞 + +module Biproduct {A B : Obj} (BP : Biproduct A B) where + + open Biproduct′ BP public + + open ⇒-Reasoning + open HomReasoning + + private + + permute⟩∘⟨refl : {C : Obj} {f : C ⇒ A⊕B} → i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ f ≈ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ f + permute⟩∘⟨refl = refl⟩∘⟨ assoc²εβ ○ extendʳ permute ○ refl⟩∘⟨ assoc²βε + + π₁i₂-constant : {C : Obj} (f g : C ⇒ B) → (π₁ ∘ i₂) ∘ f ≈ (π₁ ∘ i₂) ∘ g + π₁i₂-constant f g = begin + (π₁ ∘ i₂) ∘ f ≈⟨ assoc ⟩ + π₁ ∘ i₂ ∘ f ≈⟨ insertˡ π₁∘i₁≈id ⟩ + π₁ ∘ i₁ ∘ π₁ ∘ i₂ ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ project₂ ⟨ + π₁ ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ ⟨ π₁ ∘ i₂ ∘ g , f ⟩ ≈⟨ refl⟩∘⟨ permute⟩∘⟨refl ⟩ + π₁ ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ ⟨ π₁ ∘ i₂ ∘ g , f ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ project₁ ⟩ + π₁ ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₂ ∘ g ≈⟨ refl⟩∘⟨ permute⟩∘⟨refl ⟨ + π₁ ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₂ ∘ g ≈⟨ cancelˡ π₁∘i₁≈id ⟩ + π₁ ∘ i₂ ∘ π₂ ∘ i₂ ∘ g ≈⟨ refl⟩∘⟨ refl⟩∘⟨ cancelˡ π₂∘i₂≈id ⟩ + π₁ ∘ i₂ ∘ g ≈⟨ sym-assoc ⟩ + (π₁ ∘ i₂) ∘ g ∎ + + π₁i₂-coconstant : {C : Obj} (f g : A ⇒ C) → f ∘ π₁ ∘ i₂ ≈ g ∘ π₁ ∘ i₂ + π₁i₂-coconstant f g = begin + f ∘ π₁ ∘ i₂ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ introʳ π₂∘i₂≈id ⟩ + f ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₂ ≈⟨ pushˡ (Equiv.sym inject₁) ⟩ + [ f , g ∘ π₁ ∘ i₂ ] ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₂ ≈⟨ refl⟩∘⟨ permute⟩∘⟨refl ⟩ + [ f , g ∘ π₁ ∘ i₂ ] ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₂ ≈⟨ extendʳ inject₂ ⟩ + g ∘ (π₁ ∘ i₂) ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₂ ≈⟨ refl⟩∘⟨ pullʳ (Equiv.sym permute⟩∘⟨refl) ⟩ + g ∘ π₁ ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₂ ≈⟨ refl⟩∘⟨ cancelˡ π₁∘i₁≈id ⟩ + g ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₂ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ elimʳ π₂∘i₂≈id ⟩ + g ∘ π₁ ∘ i₂ ∎ + + π₂i₁-coconstant : {C : Obj} (f g : B ⇒ C) → f ∘ π₂ ∘ i₁ ≈ g ∘ π₂ ∘ i₁ + π₂i₁-coconstant f g = begin + f ∘ π₂ ∘ i₁ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ introʳ π₁∘i₁≈id ⟩ + f ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₁ ≈⟨ pushˡ (Equiv.sym inject₂) ⟩ + [ g ∘ π₂ ∘ i₁ , f ] ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₁ ≈⟨ refl⟩∘⟨ permute⟩∘⟨refl ⟨ + [ g ∘ π₂ ∘ i₁ , f ] ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₁ ≈⟨ extendʳ inject₁ ⟩ + g ∘ (π₂ ∘ i₁) ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₁ ≈⟨ refl⟩∘⟨ pullʳ permute⟩∘⟨refl ⟩ + g ∘ π₂ ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₁ ≈⟨ refl⟩∘⟨ cancelˡ π₂∘i₂≈id ⟩ + g ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₁ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ elimʳ π₁∘i₁≈id ⟩ + g ∘ π₂ ∘ i₁ ∎ + + π₂i₁-constant : {C : Obj} (f g : C ⇒ A) → (π₂ ∘ i₁) ∘ f ≈ (π₂ ∘ i₁) ∘ g + π₂i₁-constant f g = begin + (π₂ ∘ i₁) ∘ f ≈⟨ assoc ⟩ + π₂ ∘ i₁ ∘ f ≈⟨ insertˡ π₂∘i₂≈id ⟩ + π₂ ∘ i₂ ∘ π₂ ∘ i₁ ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ project₁ ⟨ + π₂ ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ ⟨ f , π₂ ∘ i₁ ∘ g ⟩ ≈⟨ refl⟩∘⟨ permute⟩∘⟨refl ⟨ + π₂ ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ ⟨ f , π₂ ∘ i₁ ∘ g ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ project₂ ⟩ + π₂ ∘ i₁ ∘ π₁ ∘ i₂ ∘ π₂ ∘ i₁ ∘ g ≈⟨ refl⟩∘⟨ permute⟩∘⟨refl ⟩ + π₂ ∘ i₂ ∘ π₂ ∘ i₁ ∘ π₁ ∘ i₁ ∘ g ≈⟨ cancelˡ π₂∘i₂≈id ⟩ + π₂ ∘ i₁ ∘ π₁ ∘ i₁ ∘ g ≈⟨ refl⟩∘⟨ refl⟩∘⟨ cancelˡ π₁∘i₁≈id ⟩ + π₂ ∘ i₁ ∘ g ≈⟨ sym-assoc ⟩ + (π₂ ∘ i₁) ∘ g ∎ + + 𝟎⇒ : A ⇒ B + 𝟎⇒ = π₂ ∘ i₁ + + 𝟎⇐ : B ⇒ A + 𝟎⇐ = π₁ ∘ i₂ + + π₁∘i₂-isZero : IsZero⇒ (π₁ ∘ i₂) + π₁∘i₂-isZero = record + { constant = π₁i₂-constant + ; coconstant = π₁i₂-coconstant + } + + π₂∘i₁-isZero : IsZero⇒ (π₂ ∘ i₁) + π₂∘i₁-isZero = record + { constant = π₂i₁-constant + ; coconstant = π₂i₁-coconstant + } |