Merge branch 'abelian-categories' of github.com:TOTBWF/agda-categorie…

…s into abelian-categories
agda · Apr 3, 2021 · b9128b3 · b9128b3
2 parents 2677bdb + ad98503
commit b9128b3
Show file tree

Hide file tree

Showing 2 changed files with 60 additions and 18 deletions.
diff --git a/src/Categories/Category/Preadditive/Properties.agda b/src/Categories/Category/Preadditive/Properties.agda
@@ -23,30 +23,36 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (preadditive : Preadditive 𝒞) wh
 
   Initial⇒Zero : Initial 𝒞 → Zero 𝒞
   Initial⇒Zero initial = record
-    { zero = ⊥
-    ; ! = ! 
-    ; ¡ = 0H
-    ; !-unique = !-unique
-    ; ¡-unique = λ f → begin
-      0H     ≈˘⟨ 0-resp-∘ˡ ⟩
-      0H ∘ f ≈⟨ !-unique₂ 0H id ⟩∘⟨refl ⟩
-      id ∘ f ≈⟨ identityˡ ⟩
-      f ∎
+    { 𝟘 = ⊥
+    ; isZero = record
+      { isInitial = ⊥-is-initial
+      ; isTerminal = record
+        { ! = 0H
+        ; !-unique = λ f → begin
+          0H     ≈˘⟨ 0-resp-∘ˡ ⟩
+          0H ∘ f ≈⟨ !-unique₂ 0H id ⟩∘⟨refl ⟩
+          id ∘ f ≈⟨ identityˡ ⟩
+          f ∎
+        }
+      }
     }
     where
       open Initial initial
 
   Terminal⇒Zero : Terminal 𝒞 → Zero 𝒞
   Terminal⇒Zero terminal = record
-    { zero = ⊤
-    ; ! = 0H
-    ; ¡ = !
-    ; !-unique = λ f → begin
-      0H     ≈˘⟨ 0-resp-∘ʳ ⟩
-      f ∘ 0H ≈⟨ refl⟩∘⟨ !-unique₂ ⟩
-      f ∘ id ≈⟨ identityʳ ⟩
-      f ∎
-    ; ¡-unique = !-unique
+    { 𝟘 = ⊤
+    ; isZero = record
+      { isInitial = record
+        { ! = 0H
+        ; !-unique = λ f → begin
+          0H     ≈˘⟨ 0-resp-∘ʳ ⟩
+          f ∘ 0H ≈⟨ refl⟩∘⟨ !-unique₂ ⟩
+          f ∘ id ≈⟨ identityʳ ⟩
+          f ∎
+        }
+      ; isTerminal = ⊤-is-terminal
+      }
     }
     where
       open Terminal terminal

diff --git a/src/Categories/Object/Biproduct/Properties.agda b/src/Categories/Object/Biproduct/Properties.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Categories.Object.Biproduct.Properties where
+
+open import Categories.Category
+open import Categories.Object.Biproduct
+open import Categories.Object.Coproduct
+open import Categories.Object.Product
+
+module _ {o ℓ e} (𝒞 : Category o ℓ e) where
+
+  Biproduct⇒Product : ∀ {A B} → Biproduct 𝒞 A B → Product 𝒞 A B
+  Biproduct⇒Product biproduct = record
+    { A×B = A⊕B
+    ; π₁ = π₁
+    ; π₂ = π₂
+    ; ⟨_,_⟩ = ⟨_,_⟩
+    ; project₁ = project₁
+    ; project₂ = project₂
+    ; unique = ⟨⟩-unique
+    }
+    where
+      open Biproduct biproduct
+
+  Biproduct⇒Coproduct : ∀ {A B} → Biproduct 𝒞 A B → Coproduct 𝒞 A B
+  Biproduct⇒Coproduct biproduct = record
+    { A+B = A⊕B
+    ; i₁ = i₁
+    ; i₂ = i₂
+    ; [_,_] = [_,_]
+    ; inject₁ = inject₁
+    ; inject₂ = inject₂
+    ; unique = []-unique
+    }
+    where
+      open Biproduct biproduct