Add category of finitely-cocomplete categories

- Objects are categories with all finite colimits
- Morphisms are functors preserving finite colimits (i.e. right exact)

6 files changed, 899 insertions, 5 deletions

diff --git a/Category/Cocomplete/Finitely/Bundle.agda b/Category/Cocomplete/Finitely/Bundle.agda
index af40895..74f434f 100644
--- a/Category/Cocomplete/Finitely/Bundle.agda
+++ b/Category/Cocomplete/Finitely/Bundle.agda
@@ -1,12 +1,12 @@
 {-# OPTIONS --without-K --safe #-}
 module Category.Cocomplete.Finitely.Bundle where
 
-open import Level
+open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
 open import Categories.Category.Core using (Category)
 open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
 open import Category.Cocomplete.Finitely.SymmetricMonoidal using (module FinitelyCocompleteSymmetricMonoidal)
 open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
-
+open import Level using (_⊔_; suc)
 
 record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
 
@@ -17,11 +17,20 @@ record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
   open Category U public
   open FinitelyCocomplete finCo public
 
-  open FinitelyCocompleteSymmetricMonoidal finCo using (+-monoidal; +-symmetric)
+  open FinitelyCocompleteSymmetricMonoidal finCo
+    using ()
+    renaming (+-monoidal to monoidal; +-symmetric to symmetric)
+    public
 
   symmetricMonoidalCategory : SymmetricMonoidalCategory o ℓ e
   symmetricMonoidalCategory = record
       { U = U
-      ; monoidal = +-monoidal
-      ; symmetric = +-symmetric
+      ; monoidal = monoidal
+      ; symmetric = symmetric
+      }
+
+  cocartesianCategory : CocartesianCategory o ℓ e
+  cocartesianCategory = record
+      { U = U
+      ; cocartesian = cocartesian
       }
diff --git a/Category/Cocomplete/Finitely/Product.agda b/Category/Cocomplete/Finitely/Product.agda
new file mode 100644
index 0000000..25dc346
--- /dev/null
+++ b/Category/Cocomplete/Finitely/Product.agda
@@ -0,0 +1,83 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Core using (Category)
+open import Level using (Level)
+
+module Category.Cocomplete.Finitely.Product {o ℓ e : Level} {𝒞 𝒟 : Category o ℓ e} where
+
+open import Categories.Category using (_[_,_])
+open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
+open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts)
+open import Categories.Category.Product using (Product)
+open import Categories.Diagram.Coequalizer using (Coequalizer)
+open import Categories.Object.Coproduct using (Coproduct)
+open import Categories.Object.Initial using (IsInitial; Initial)
+open import Data.Product.Base using (_,_; _×_; dmap; zip; map)
+
+Initial-× : Initial 𝒞 → Initial 𝒟 → Initial (Product 𝒞 𝒟)
+Initial-× initial-𝒞 initial-𝒟 = record
+    { ⊥ = 𝒞.⊥ , 𝒟.⊥
+    ; ⊥-is-initial = record
+        { ! = 𝒞.! , 𝒟.!
+        ; !-unique = dmap 𝒞.!-unique 𝒟.!-unique
+        }
+    }
+  where
+    module 𝒞 = Initial initial-𝒞
+    module 𝒟 = Initial initial-𝒟
+
+Coproducts-× : BinaryCoproducts 𝒞 → BinaryCoproducts 𝒟 → BinaryCoproducts (Product 𝒞 𝒟)
+Coproducts-× coproducts-𝒞 coproducts-𝒟 = record { coproduct = coproduct }
+  where
+    coproduct : ∀ {(A₁ , B₁) (A₂ , B₂) : _ × _} → Coproduct (Product 𝒞 𝒟) (A₁ , B₁) (A₂ , B₂)
+    coproduct = record
+        { A+B = 𝒞.A+B , 𝒟.A+B
+        ; i₁ = 𝒞.i₁ , 𝒟.i₁
+        ; i₂ = 𝒞.i₂ , 𝒟.i₂
+        ; [_,_] = zip 𝒞.[_,_] 𝒟.[_,_]
+        ; inject₁ = 𝒞.inject₁ , 𝒟.inject₁
+        ; inject₂ = 𝒞.inject₂ , 𝒟.inject₂
+        ; unique = zip 𝒞.unique 𝒟.unique
+        }
+      where
+        module Coprod {𝒞} (coprods : BinaryCoproducts 𝒞) where
+          open BinaryCoproducts coprods using (coproduct)
+          open coproduct public
+        module 𝒞 = Coprod coproducts-𝒞
+        module 𝒟 = Coprod coproducts-𝒟
+
+Coequalizer-×
+    : (∀ {A} {B} (f g : 𝒞 [ A , B ]) → Coequalizer 𝒞 f g)
+    → (∀ {A} {B} (f g : 𝒟 [ A , B ]) → Coequalizer 𝒟 f g)
+    → ∀ {A} {B} {C} {D} ((f₁ , g₁) (f₂ , g₂) : 𝒞 [ A , B ] × 𝒟 [ C , D ])
+    → Coequalizer (Product 𝒞 𝒟) (f₁ , g₁) (f₂ , g₂)
+Coequalizer-× coequalizer-𝒞 coequalizer-𝒟 (f₁ , g₁) (f₂ , g₂) = record
+    { arr = 𝒞.arr , 𝒟.arr
+    ; isCoequalizer = record
+        { equality = 𝒞.equality , 𝒟.equality
+        ; coequalize = map 𝒞.coequalize 𝒟.coequalize
+        ; universal = 𝒞.universal , 𝒟.universal
+        ; unique = map 𝒞.unique 𝒟.unique
+        }
+    }
+  where
+    module 𝒞 = Coequalizer (coequalizer-𝒞 f₁ f₂)
+    module 𝒟 = Coequalizer (coequalizer-𝒟 g₁ g₂)
+
+Cocartesian-× : Cocartesian 𝒞 → Cocartesian 𝒟 → Cocartesian (Product 𝒞 𝒟)
+Cocartesian-× cocartesian-𝒞 cocartesian-𝒟 = record
+    { initial = Initial-× 𝒞.initial 𝒟.initial
+    ; coproducts = Coproducts-× 𝒞.coproducts 𝒟.coproducts
+    }
+  where
+    module 𝒞 = Cocartesian cocartesian-𝒞
+    module 𝒟 = Cocartesian cocartesian-𝒟
+
+FinitelyCocomplete-× : FinitelyCocomplete 𝒞 → FinitelyCocomplete 𝒟 → FinitelyCocomplete (Product 𝒞 𝒟)
+FinitelyCocomplete-× finitelyCocomplete-𝒞 finitelyCocomplete-𝒟 = record
+    { cocartesian = Cocartesian-× 𝒞.cocartesian 𝒟.cocartesian
+    ; coequalizer = Coequalizer-× 𝒞.coequalizer 𝒟.coequalizer
+    }
+  where
+    module 𝒞 = FinitelyCocomplete finitelyCocomplete-𝒞
+    module 𝒟 = FinitelyCocomplete finitelyCocomplete-𝒟
diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda
new file mode 100644
index 0000000..0847165
--- /dev/null
+++ b/Category/Instance/FinitelyCocompletes.agda
@@ -0,0 +1,369 @@
+{-# OPTIONS --without-K --safe #-}
+open import Level using (Level)
+module Category.Instance.FinitelyCocompletes {o ℓ e : Level} where
+
+open import Categories.Category using (_[_,_])
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Helper using (categoryHelper)
+open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products)
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Instance.Cats using (Cats)
+open import Categories.Category.Instance.One using (One; One-⊤)
+open import Categories.Category.Product using (πˡ; πʳ; _※_; _⁂_) renaming (Product to ProductCat)
+open import Categories.Diagram.Coequalizer using (IsCoequalizer)
+open import Categories.Functor using (Functor) renaming (id to idF)
+open import Categories.Object.Coproduct using (IsCoproduct)
+open import Categories.Object.Initial using (IsInitial)
+open import Categories.Object.Product.Core using (Product)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+open import Category.Cocomplete.Finitely.Product using (FinitelyCocomplete-×)
+open import Category.Instance.One.Properties using (One-FinitelyCocomplete)
+open import Data.Product.Base using (_,_; proj₁; proj₂; map; dmap; zip′)
+open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact)
+open import Function.Base using (id; flip)
+open import Level using (Level; suc; _⊔_)
+
+FinitelyCocompletes : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
+FinitelyCocompletes = categoryHelper record
+    { Obj = FinitelyCocompleteCategory o ℓ e
+    ; _⇒_ = RightExactFunctor
+    ; _≈_ = λ F G → REF.F F ≃ REF.F G
+    ; id = idREF
+    ; _∘_ = ∘-RightExactFunctor
+    ; assoc = λ {_ _ _ _ F G H} → associator (REF.F F) (REF.F G) (REF.F H)
+    ; identityˡ = unitorˡ
+    ; identityʳ = unitorʳ
+    ; equiv = record
+        { refl = ≃.refl
+        ; sym = ≃.sym
+        ; trans = ≃.trans
+        }
+    ; ∘-resp-≈ = _ⓘₕ_
+    }
+  where
+    module REF = RightExactFunctor
+
+One-FCC : FinitelyCocompleteCategory o ℓ e
+One-FCC = record
+    { U = One
+    ; finCo = One-FinitelyCocomplete
+    }
+
+_×_
+    : FinitelyCocompleteCategory o ℓ e
+    → FinitelyCocompleteCategory o ℓ e
+    → FinitelyCocompleteCategory o ℓ e
+_×_ 𝒞 𝒟 = record
+    { U = ProductCat 𝒞.U 𝒟.U
+    ; finCo = FinitelyCocomplete-× 𝒞.finCo 𝒟.finCo
+    }
+  where
+    module 𝒞 = FinitelyCocompleteCategory 𝒞
+    module 𝒟 = FinitelyCocompleteCategory 𝒟
+
+module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where
+
+  private
+    module 𝒞 = FinitelyCocompleteCategory 𝒞
+    module 𝒟 = FinitelyCocompleteCategory 𝒟
+    module 𝒞×𝒟 = FinitelyCocompleteCategory (𝒞 × 𝒟)
+
+  πˡ-RightExact : IsRightExact (𝒞 × 𝒟) 𝒞 πˡ
+  πˡ-RightExact = record
+      { F-resp-⊥ = F-resp-⊥
+      ; F-resp-+ = F-resp-+
+      ; F-resp-coeq = F-resp-coeq
+      }
+    where
+      F-resp-⊥
+          : {(A , B) : 𝒞×𝒟.Obj}
+          → IsInitial 𝒞×𝒟.U (A , B)
+          → IsInitial 𝒞.U A
+      F-resp-⊥ {A , B} initial = record
+          { ! = λ { {C} → proj₁ (! {C , B}) }
+          ; !-unique = λ { f → proj₁ (!-unique (f , 𝒟.id)) }
+          }
+        where
+          open IsInitial initial
+      F-resp-+
+          : {(C₁ , D₁) (C₂ , D₂) (C₃ , D₃) : 𝒞×𝒟.Obj}
+            {(i₁-c , i₁-d) : 𝒞×𝒟.U [ (C₁ , D₁) , (C₃ , D₃) ]}
+            {(i₂-c , i₂-d) : 𝒞×𝒟.U [ (C₂ , D₂) , (C₃ , D₃) ]}
+          → IsCoproduct (ProductCat 𝒞.U 𝒟.U) (i₁-c , i₁-d) (i₂-c , i₂-d)
+          → IsCoproduct 𝒞.U i₁-c i₂-c
+      F-resp-+ {_} {_} {_} {i₁-c , i₁-d} {i₂-c , i₂-d} isCoproduct = record
+          { [_,_] = λ { h₁ h₂ → proj₁ (copairing (h₁ , i₁-d) (h₂ , i₂-d)) }
+          ; inject₁ = proj₁ inject₁
+          ; inject₂ = proj₁ inject₂
+          ; unique = λ { eq₁ eq₂ → proj₁ (unique (eq₁ , 𝒟.identityˡ) (eq₂ , 𝒟.identityˡ)) }
+          }
+        where
+          open IsCoproduct isCoproduct renaming ([_,_] to copairing)
+      F-resp-coeq
+          : {(C₁ , D₁) (C₂ , D₂) (C₃ , D₃) : 𝒞×𝒟.Obj}
+            {f g : 𝒞×𝒟.U [ (C₁ , D₁) , (C₂ , D₂) ]}
+            {h : 𝒞×𝒟.U [ (C₂ , D₂) , (C₃ , D₃) ]}
+          → IsCoequalizer (ProductCat 𝒞.U 𝒟.U) f g h
+          → IsCoequalizer 𝒞.U (proj₁ f) (proj₁ g) (proj₁ h)
+      F-resp-coeq isCoequalizer = record
+          { equality = proj₁ equality
+          ; coequalize = λ { eq → proj₁ (coequalize (eq , proj₂ equality)) }
+          ; universal = proj₁ universal
+          ; unique = λ { eq → proj₁ (unique (eq , 𝒟.Equiv.sym 𝒟.identityˡ)) }
+          }
+        where
+          open IsCoequalizer isCoequalizer
+
+  πʳ-RightExact : IsRightExact (𝒞 × 𝒟) 𝒟 πʳ
+  πʳ-RightExact = record
+      { F-resp-⊥ = F-resp-⊥
+      ; F-resp-+ = F-resp-+
+      ; F-resp-coeq = F-resp-coeq
+      }
+    where
+      F-resp-⊥
+          : {(A , B) : 𝒞×𝒟.Obj}
+          → IsInitial 𝒞×𝒟.U (A , B)
+          → IsInitial 𝒟.U B
+      F-resp-⊥ {A , B} initial = record
+          { ! = λ { {C} → proj₂ (! {A , C}) }
+          ; !-unique = λ { f → proj₂ (!-unique (𝒞.id , f)) }
+          }
+        where
+          open IsInitial initial
+      F-resp-+
+          : {(C₁ , D₁) (C₂ , D₂) (C₃ , D₃) : 𝒞×𝒟.Obj}
+            {(i₁-c , i₁-d) : 𝒞×𝒟.U [ (C₁ , D₁) , (C₃ , D₃) ]}
+            {(i₂-c , i₂-d) : 𝒞×𝒟.U [ (C₂ , D₂) , (C₃ , D₃) ]}
+          → IsCoproduct 𝒞×𝒟.U (i₁-c , i₁-d) (i₂-c , i₂-d)
+          → IsCoproduct 𝒟.U i₁-d i₂-d
+      F-resp-+ {_} {_} {_} {i₁-c , i₁-d} {i₂-c , i₂-d} isCoproduct = record
+          { [_,_] = λ { h₁ h₂ → proj₂ (copairing (i₁-c , h₁) (i₂-c , h₂)) }
+          ; inject₁ = proj₂ inject₁
+          ; inject₂ = proj₂ inject₂
+          ; unique = λ { eq₁ eq₂ → proj₂ (unique (𝒞.identityˡ , eq₁) (𝒞.identityˡ , eq₂)) }
+          }
+        where
+          open IsCoproduct isCoproduct renaming ([_,_] to copairing)
+      F-resp-coeq
+          : {(C₁ , D₁) (C₂ , D₂) (C₃ , D₃) : 𝒞×𝒟.Obj}
+            {f g : 𝒞×𝒟.U [ (C₁ , D₁) , (C₂ , D₂) ]}
+            {h : 𝒞×𝒟.U [ (C₂ , D₂) , (C₃ , D₃) ]}
+          → IsCoequalizer 𝒞×𝒟.U f g h
+          → IsCoequalizer 𝒟.U (proj₂ f) (proj₂ g) (proj₂ h)
+      F-resp-coeq isCoequalizer = record
+          { equality = proj₂ equality
+          ; coequalize = λ { eq → proj₂ (coequalize (proj₁ equality , eq)) }
+          ; universal = proj₂ universal
+          ; unique = λ { eq → proj₂ (unique (𝒞.Equiv.sym 𝒞.identityˡ , eq)) }
+          }
+        where
+          open IsCoequalizer isCoequalizer
+
+module _ where
+
+  open FinitelyCocompleteCategory using (U)
+
+  IsRightExact-※
+      : {𝒞 𝒟 ℰ : FinitelyCocompleteCategory o ℓ e}
+        (F : Functor (U 𝒞) (U 𝒟))
+        (G : Functor (U 𝒞) (U ℰ))
+      → IsRightExact 𝒞 𝒟 F
+      → IsRightExact 𝒞 ℰ G
+      → IsRightExact 𝒞 (𝒟 × ℰ) (F ※ G)
+  IsRightExact-※ {𝒞} {𝒟} {ℰ} F G isRightExact-F isRightExact-G = record 
+      { F-resp-⊥ = F-resp-⊥′
+      ; F-resp-+ = F-resp-+′
+      ; F-resp-coeq = F-resp-coeq′
+      }
+    where
+      module 𝒞 = FinitelyCocompleteCategory 𝒞
+      module 𝒟 = FinitelyCocompleteCategory 𝒟
+      module ℰ = FinitelyCocompleteCategory ℰ
+      open IsRightExact isRightExact-F
+      open IsRightExact isRightExact-G renaming (F-resp-⊥ to G-resp-⊥; F-resp-+ to G-resp-+; F-resp-coeq to G-resp-coeq)
+      module F = Functor F
+      module G = Functor G
+      F-resp-⊥′
+          : {A : 𝒞.Obj}
+          → IsInitial 𝒞.U A
+          → IsInitial (ProductCat 𝒟.U ℰ.U) (F.₀ A , G.₀ A)
+      F-resp-⊥′ A-isInitial = record
+          { ! = F[A]-isInitial.! , G[A]-isInitial.!
+          ; !-unique = dmap F[A]-isInitial.!-unique G[A]-isInitial.!-unique
+          }
+        where
+          module F[A]-isInitial = IsInitial (F-resp-⊥ A-isInitial)
+          module G[A]-isInitial = IsInitial (G-resp-⊥ A-isInitial)
+      F-resp-+′
+          : {A B C : 𝒞.Obj} {i₁ : 𝒞.U [ A , C ]} {i₂ : 𝒞.U [ B , C ]}
+          → IsCoproduct 𝒞.U i₁ i₂
+          → IsCoproduct (ProductCat 𝒟.U ℰ.U) (F.₁ i₁ , G.₁ i₁) (F.₁ i₂ , G.₁ i₂)
+      F-resp-+′ {A} {B} {A+B} A+B-isCoproduct = record
+          { [_,_] = zip′ F[A+B]-isCoproduct.[_,_] G[A+B]-isCoproduct.[_,_]
+          ; inject₁ = F[A+B]-isCoproduct.inject₁ , G[A+B]-isCoproduct.inject₁
+          ; inject₂ = F[A+B]-isCoproduct.inject₂ , G[A+B]-isCoproduct.inject₂
+          ; unique = zip′ F[A+B]-isCoproduct.unique G[A+B]-isCoproduct.unique
+          }
+        where
+          module F[A+B]-isCoproduct = IsCoproduct (F-resp-+ A+B-isCoproduct)
+          module G[A+B]-isCoproduct = IsCoproduct (G-resp-+ A+B-isCoproduct)
+      F-resp-coeq′
+          : {A B C : 𝒞.Obj} {f g : 𝒞.U [ A , B ]} {h : 𝒞.U [ B , C ]}
+          → IsCoequalizer 𝒞.U f g h
+          → IsCoequalizer (ProductCat 𝒟.U ℰ.U) (F.₁ f , G.₁ f) (F.₁ g , G.₁ g) (F.₁ h , G.₁ h)
+      F-resp-coeq′ h-isCoequalizer = record
+          { equality = F[h]-isCoequalizer.equality , G[h]-isCoequalizer.equality
+          ; coequalize = map F[h]-isCoequalizer.coequalize G[h]-isCoequalizer.coequalize
+          ; universal = F[h]-isCoequalizer.universal , G[h]-isCoequalizer.universal
+          ; unique = map F[h]-isCoequalizer.unique G[h]-isCoequalizer.unique
+          }
+        where
+          module F[h]-isCoequalizer = IsCoequalizer (F-resp-coeq h-isCoequalizer)
+          module G[h]-isCoequalizer = IsCoequalizer (G-resp-coeq h-isCoequalizer)
+
+  IsRightExact-⁂
+      : {𝒜 ℬ 𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e}
+        (F : Functor (U 𝒜) (U 𝒞))
+        (G : Functor (U ℬ) (U 𝒟))
+      → IsRightExact 𝒜 𝒞 F
+      → IsRightExact ℬ 𝒟 G
+      → IsRightExact (𝒜 × ℬ) (𝒞 × 𝒟) (F ⁂ G)
+  IsRightExact-⁂ {𝒜} {ℬ} {𝒞} {𝒟} F G isRightExact-F isRightExact-G = record 
+      { F-resp-⊥ = F-resp-⊥′
+      ; F-resp-+ = F-resp-+′
+      ; F-resp-coeq = F-resp-coeq′
+      }
+    where
+      module 𝒜 = FinitelyCocompleteCategory 𝒜
+      module ℬ = FinitelyCocompleteCategory ℬ
+      module 𝒞 = FinitelyCocompleteCategory 𝒞
+      module 𝒟 = FinitelyCocompleteCategory 𝒟
+      module 𝒜×ℬ = FinitelyCocompleteCategory (𝒜 × ℬ)
+      module 𝒞×𝒟 = FinitelyCocompleteCategory (𝒞 × 𝒟)
+      open IsRightExact isRightExact-F
+      open IsRightExact isRightExact-G renaming (F-resp-⊥ to G-resp-⊥; F-resp-+ to G-resp-+; F-resp-coeq to G-resp-coeq)
+      module F = Functor F
+      module G = Functor G
+      F-resp-⊥′
+          : {(A , B) : 𝒜×ℬ.Obj}
+          → IsInitial 𝒜×ℬ.U (A , B)
+          → IsInitial 𝒞×𝒟.U (F.₀ A , G.₀ B)
+      F-resp-⊥′ {A , B} A,B-isInitial = record
+          { ! = F[A]-isInitial.! , G[B]-isInitial.!
+          ; !-unique = dmap F[A]-isInitial.!-unique G[B]-isInitial.!-unique
+          }
+        where
+          module A,B-isInitial = IsInitial A,B-isInitial
+          A-isInitial : IsInitial 𝒜.U A
+          A-isInitial = record
+              { ! = λ { {X} → proj₁ (A,B-isInitial.! {X , B}) }
+              ; !-unique = λ { f → proj₁ (A,B-isInitial.!-unique (f , ℬ.id)) }
+              }
+          B-isInitial : IsInitial ℬ.U B
+          B-isInitial = record
+              { ! = λ { {X} → proj₂ (A,B-isInitial.! {A , X}) }
+              ; !-unique = λ { f → proj₂ (A,B-isInitial.!-unique (𝒜.id , f)) }
+              }
+          module F[A]-isInitial = IsInitial (F-resp-⊥ A-isInitial)
+          module G[B]-isInitial = IsInitial (G-resp-⊥ B-isInitial)
+      F-resp-+′
+          : {A B C : 𝒜×ℬ.Obj} {(i₁ , i₁′) : 𝒜×ℬ.U [ A , C ]} {(i₂ , i₂′) : 𝒜×ℬ.U [ B , C ]}
+          → IsCoproduct 𝒜×ℬ.U (i₁ , i₁′) (i₂ , i₂′)
+          → IsCoproduct 𝒞×𝒟.U (F.₁ i₁ , G.₁ i₁′) (F.₁ i₂ , G.₁ i₂′)
+      F-resp-+′ {A} {B} {A+B} {i₁ , i₁′} {i₂ , i₂′} A+B,A+B′-isCoproduct = record
+          { [_,_] = zip′ F[A+B]-isCoproduct.[_,_] G[A+B′]-isCoproduct.[_,_]
+          ; inject₁ = F[A+B]-isCoproduct.inject₁ , G[A+B′]-isCoproduct.inject₁
+          ; inject₂ = F[A+B]-isCoproduct.inject₂ , G[A+B′]-isCoproduct.inject₂
+          ; unique = zip′ F[A+B]-isCoproduct.unique G[A+B′]-isCoproduct.unique
+          }
+        where
+          module A+B,A+B′-isCoproduct = IsCoproduct A+B,A+B′-isCoproduct
+          A+B-isCoproduct : IsCoproduct 𝒜.U i₁ i₂
+          A+B-isCoproduct = record
+              { [_,_] = λ { f g → proj₁ (A+B,A+B′-isCoproduct.[ (f , i₁′) , (g , i₂′) ]) }
+              ; inject₁ = proj₁ A+B,A+B′-isCoproduct.inject₁
+              ; inject₂ = proj₁ A+B,A+B′-isCoproduct.inject₂
+              ; unique = λ { ≈f ≈g → proj₁ (A+B,A+B′-isCoproduct.unique (≈f , ℬ.identityˡ) (≈g , ℬ.identityˡ)) }
+              }
+          A+B′-isCoproduct : IsCoproduct ℬ.U i₁′ i₂′
+          A+B′-isCoproduct = record
+              { [_,_] = λ { f g → proj₂ (A+B,A+B′-isCoproduct.[ (i₁ , f) , (i₂ , g) ]) }
+              ; inject₁ = proj₂ A+B,A+B′-isCoproduct.inject₁
+              ; inject₂ = proj₂ A+B,A+B′-isCoproduct.inject₂
+              ; unique = λ { ≈f ≈g → proj₂ (A+B,A+B′-isCoproduct.unique (𝒜.identityˡ , ≈f) (𝒜.identityˡ , ≈g)) }
+              }
+          module F[A+B]-isCoproduct = IsCoproduct (F-resp-+ A+B-isCoproduct)
+          module G[A+B′]-isCoproduct = IsCoproduct (G-resp-+ A+B′-isCoproduct)
+      F-resp-coeq′
+          : {A B C : 𝒜×ℬ.Obj} {(f , f′) (g , g′) : 𝒜×ℬ.U [ A , B ]} {(h , h′) : 𝒜×ℬ.U [ B , C ]}
+          → IsCoequalizer 𝒜×ℬ.U (f , f′) (g , g′) (h , h′)
+          → IsCoequalizer 𝒞×𝒟.U (F.₁ f , G.₁ f′) (F.₁ g , G.₁ g′) (F.₁ h , G.₁ h′)
+      F-resp-coeq′ {_} {_} {_} {f , f′} {g , g′} {h , h′} h,h′-isCoequalizer = record
+          { equality = F[h]-isCoequalizer.equality , G[h′]-isCoequalizer.equality
+          ; coequalize = map F[h]-isCoequalizer.coequalize G[h′]-isCoequalizer.coequalize
+          ; universal = F[h]-isCoequalizer.universal , G[h′]-isCoequalizer.universal
+          ; unique = map F[h]-isCoequalizer.unique G[h′]-isCoequalizer.unique
+          }
+        where
+          module h,h′-isCoequalizer = IsCoequalizer h,h′-isCoequalizer
+          h-isCoequalizer : IsCoequalizer 𝒜.U f g h
+          h-isCoequalizer = record
+              { equality = proj₁ h,h′-isCoequalizer.equality
+              ; coequalize = λ { eq → proj₁ (h,h′-isCoequalizer.coequalize (eq , proj₂ h,h′-isCoequalizer.equality)) }
+              ; universal = proj₁ h,h′-isCoequalizer.universal
+              ; unique = λ { ≈h → proj₁ (h,h′-isCoequalizer.unique (≈h , ℬ.Equiv.sym ℬ.identityˡ)) }
+              }
+          h′-isCoequalizer : IsCoequalizer ℬ.U f′ g′ h′
+          h′-isCoequalizer = record
+              { equality = proj₂ h,h′-isCoequalizer.equality
+              ; coequalize = λ { eq′ → proj₂ (h,h′-isCoequalizer.coequalize (proj₁ h,h′-isCoequalizer.equality , eq′)) }
+              ; universal = proj₂ h,h′-isCoequalizer.universal
+              ; unique = λ { ≈h′ → proj₂ (h,h′-isCoequalizer.unique (𝒜.Equiv.sym 𝒜.identityˡ , ≈h′)) }
+              }
+
+          module F[h]-isCoequalizer = IsCoequalizer (F-resp-coeq h-isCoequalizer)
+          module G[h′]-isCoequalizer = IsCoequalizer (G-resp-coeq h′-isCoequalizer)
+_×₁_
+    : {𝒜 ℬ 𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e}
+    → RightExactFunctor 𝒜 𝒞
+    → RightExactFunctor ℬ 𝒟
+    → RightExactFunctor (𝒜 × ℬ) (𝒞 × 𝒟)
+F ×₁ G = record
+    { F = F.F ⁂ G.F
+    ; isRightExact = IsRightExact-⁂ F.F G.F F.isRightExact G.isRightExact
+    }
+  where
+    module F = RightExactFunctor F
+    module G = RightExactFunctor G
+
+FinitelyCocompletes-Products : {𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e} → Product FinitelyCocompletes 𝒞 𝒟
+FinitelyCocompletes-Products {𝒞} {𝒟} = record
+    { A×B = 𝒞 × 𝒟
+    ; π₁ = rightexact πˡ (πˡ-RightExact 𝒞 𝒟)
+    ; π₂ = rightexact πʳ (πʳ-RightExact 𝒞 𝒟)
+    ; ⟨_,_⟩ = λ { (rightexact F isF) (rightexact G isG) → rightexact (F ※ G) (IsRightExact-※  F G isF isG) }
+    ; project₁ = λ { {_} {rightexact F _} {rightexact G _} → Cats.project₁ {h = F} {i = G} }
+    ; project₂ = λ { {_} {rightexact F _} {rightexact G _} → Cats.project₂ {h = F} {i = G} }
+    ; unique = Cats.unique
+    }
+  where
+    module 𝒞 = FinitelyCocompleteCategory 𝒞
+    module 𝒟 = FinitelyCocompleteCategory 𝒟
+    module Cats = BinaryProducts Products.Cats-has-all
+
+FinitelyCocompletes-BinaryProducts : BinaryProducts FinitelyCocompletes
+FinitelyCocompletes-BinaryProducts = record
+    { product = FinitelyCocompletes-Products
+    }
+
+FinitelyCocompletes-Cartesian : Cartesian FinitelyCocompletes
+FinitelyCocompletes-Cartesian = record 
+    { terminal = record
+        { ⊤ = One-FCC
+        ; ⊤-is-terminal = _
+        }
+    ; products = FinitelyCocompletes-BinaryProducts
+    }
diff --git a/Category/Instance/One/Properties.agda b/Category/Instance/One/Properties.agda
new file mode 100644
index 0000000..1452669
--- /dev/null
+++ b/Category/Instance/One/Properties.agda
@@ -0,0 +1,35 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Category.Instance.One.Properties {o ℓ e : Level} where
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Instance.One using () renaming (One to One′)
+
+One : Category o ℓ e
+One = One′
+
+open import Categories.Category.Cocartesian One using (Cocartesian)
+open import Categories.Category.Cocomplete.Finitely One using (FinitelyCocomplete)
+open import Categories.Object.Initial One using (Initial)
+open import Categories.Category.Cocartesian One using (BinaryCoproducts)
+
+
+One-Initial : Initial
+One-Initial = _
+
+One-BinaryCoproducts : BinaryCoproducts
+One-BinaryCoproducts = _
+
+One-Cocartesian : Cocartesian
+One-Cocartesian = record
+    { initial = One-Initial
+    ; coproducts = One-BinaryCoproducts
+    }
+
+One-FinitelyCocomplete : FinitelyCocomplete
+One-FinitelyCocomplete = record
+    { cocartesian = One-Cocartesian
+    ; coequalizer = _
+    }
diff --git a/Category/Instance/Properties/FinitelyCocompletes.agda b/Category/Instance/Properties/FinitelyCocompletes.agda
new file mode 100644
index 0000000..9f848f4
--- /dev/null
+++ b/Category/Instance/Properties/FinitelyCocompletes.agda
@@ -0,0 +1,208 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+module Category.Instance.Properties.FinitelyCocompletes {o ℓ e : Level} where
+
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+open import Categories.Category.Product using (Product) renaming (_⁂_ to _⁂′_)
+open import Categories.Diagram.Coequalizer using (IsCoequalizer)
+open import Categories.Functor.Core using (Functor)
+open import Categories.Functor using (_∘F_) renaming (id to idF)
+open import Categories.Object.Coproduct using (IsCoproduct; IsCoproduct⇒Coproduct; Coproduct)
+open import Categories.Object.Initial using (IsInitial)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes; FinitelyCocompletes-Cartesian; _×₁_)
+open import Data.Product.Base using (_,_) renaming (_×_ to _×′_)
+open import Functor.Exact using (IsRightExact; RightExactFunctor)
+open import Level using (_⊔_; suc)
+
+FinitelyCocompletes-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
+FinitelyCocompletes-CC = record
+    { U = FinitelyCocompletes
+    ; cartesian = FinitelyCocompletes-Cartesian
+    }
+
+module FinCoCom = CartesianCategory FinitelyCocompletes-CC
+open BinaryProducts (FinCoCom.products) using (_×_; π₁; π₂; _⁂_; assocˡ) --  hiding (unique)
+
+module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where
+
+  private
+    module 𝒞 = FinitelyCocompleteCategory 𝒞
+    module 𝒞×𝒞 = FinitelyCocompleteCategory (𝒞 × 𝒞)
+
+  open 𝒞 using ([_,_]; +-unique; i₁; i₂; _∘_; _+_; module Equiv; _⇒_; _+₁_; -+-)
+  open Equiv
+  module -+- = Functor -+-
+
+  +-resp-⊥
+      : {(A , B) : 𝒞×𝒞.Obj}
+      → IsInitial 𝒞×𝒞.U (A , B)
+      → IsInitial 𝒞.U (A + B)
+  +-resp-⊥ {A , B} A,B-isInitial = record
+      { ! = [ A-isInitial.! , B-isInitial.! ]
+      ; !-unique = λ { f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂))) }
+      }
+    where
+      open IsRightExact
+      open RightExactFunctor
+      module A-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₁ {𝒞} {𝒞})) A,B-isInitial)
+      module B-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₂ {𝒞} {𝒞})) A,B-isInitial)
+
+  +-resp-+
+      : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj}
+        {(i₁-₁ , i₁-₂) : (A₁ ⇒ C₁) ×′ (A₂ ⇒ C₂)}
+        {(i₂-₁ , i₂-₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)}
+      → IsCoproduct 𝒞×𝒞.U (i₁-₁ , i₁-₂) (i₂-₁ , i₂-₂)
+      → IsCoproduct 𝒞.U (i₁-₁ +₁ i₁-₂) (i₂-₁ +₁ i₂-₂)
+  +-resp-+ {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {i₁-₁ , i₁-₂} {i₂-₁ , i₂-₂} isCoproduct = record
+      { [_,_] = λ { h₁ h₂ → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂  , h₂ ∘ i₂ ] ] }
+      ; inject₁ = inject₁
+      ; inject₂ = inject₂
+      ; unique = unique
+      }
+    where
+      open IsRightExact
+      open RightExactFunctor
+      module Coprod₁ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₁ {𝒞} {𝒞})) isCoproduct))
+      module Coprod₂ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₂ {𝒞} {𝒞})) isCoproduct))
+      open 𝒞 using ([]-cong₂; []∘+₁; +-g-η; +₁∘i₁; +₁∘i₂)
+      open 𝒞 using (Obj; _≈_; module HomReasoning; assoc)
+      open HomReasoning
+      open ⇒-Reasoning 𝒞.U
+      inject₁
+          : {X : Obj}
+            {h₁ : A₁ + A₂ ⇒ X}
+            {h₂ : B₁ + B₂ ⇒ X}
+          → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁
+      inject₁ {_} {h₁} {h₂} = begin
+          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂)  ≈⟨ []∘+₁ ⟩
+          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₁-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₁-₂ ]     ≈⟨ []-cong₂ Coprod₁.inject₁ Coprod₂.inject₁ ⟩
+          [ h₁ ∘ i₁ , h₁ ∘ i₂ ]                                                               ≈⟨ +-g-η ⟩
+          h₁                                                                                  ∎
+      inject₂
+          : {X : Obj}
+            {h₁ : A₁ + A₂ ⇒ X}
+            {h₂ : B₁ + B₂ ⇒ X}
+          → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂
+      inject₂ {_} {h₁} {h₂} = begin
+          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂)  ≈⟨ []∘+₁ ⟩
+          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₂-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₂-₂ ]     ≈⟨ []-cong₂ Coprod₁.inject₂ Coprod₂.inject₂ ⟩
+          [ h₂ ∘ i₁ , h₂ ∘ i₂ ]                                                               ≈⟨ +-g-η ⟩
+          h₂                                                                                  ∎
+      unique
+          : {X : Obj}
+            {i : C₁ + C₂ ⇒ X}
+            {h₁ : A₁ + A₂ ⇒ X}
+            {h₂ : B₁ + B₂ ⇒ X}
+            (eq₁ : i ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁)
+            (eq₂ : i ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂)
+          → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈ i
+      unique {X} {i} {h₁} {h₂} eq₁ eq₂ = begin
+          [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈⟨ []-cong₂ (Coprod₁.unique eq₁-₁ eq₂-₁) (Coprod₂.unique eq₁-₂ eq₂-₂) ⟩
+          [ i ∘ i₁ , i ∘ i₂ ]                                               ≈⟨ +-g-η ⟩
+          i                                                                 ∎
+        where
+          eq₁-₁ : (i ∘ i₁) ∘ i₁-₁ ≈ h₁ ∘ i₁
+          eq₁-₁ = begin
+              (i ∘ i₁) ∘ i₁-₁         ≈⟨ pushʳ +₁∘i₁ ⟨
+              i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₁ ≈⟨ pullˡ eq₁ ⟩
+              h₁ ∘ i₁                 ∎
+          eq₂-₁ : (i ∘ i₁) ∘ i₂-₁ ≈ h₂ ∘ i₁
+          eq₂-₁ = begin
+              (i ∘ i₁) ∘ i₂-₁         ≈⟨ pushʳ +₁∘i₁ ⟨
+              i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₁ ≈⟨ pullˡ eq₂ ⟩
+              h₂ ∘ i₁                 ∎
+          eq₁-₂ : (i ∘ i₂) ∘ i₁-₂ ≈ h₁ ∘ i₂
+          eq₁-₂ = begin
+              (i ∘ i₂) ∘ i₁-₂         ≈⟨ pushʳ +₁∘i₂ ⟨
+              i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₂ ≈⟨ pullˡ eq₁ ⟩
+              h₁ ∘ i₂                 ∎
+          eq₂-₂ : (i ∘ i₂) ∘ i₂-₂ ≈ h₂ ∘ i₂
+          eq₂-₂ = begin
+              (i ∘ i₂) ∘ i₂-₂         ≈⟨ pushʳ +₁∘i₂ ⟨
+              i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₂ ≈⟨ pullˡ eq₂ ⟩
+              h₂ ∘ i₂                 ∎
+
+  +-resp-coeq
+      : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj}
+        {(f₁ , f₂) (g₁ , g₂) : (A₁ ⇒ B₁) ×′ (A₂ ⇒ B₂)}
+        {(h₁ , h₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)}
+      → IsCoequalizer 𝒞×𝒞.U (f₁ , f₂) (g₁ , g₂) (h₁ , h₂)
+      → IsCoequalizer 𝒞.U (f₁ +₁ f₂) (g₁ +₁ g₂) (h₁ +₁ h₂)
+  +-resp-coeq {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {f₁ , f₂} {g₁ , g₂} {h₁ , h₂} isCoeq = record
+      { equality = sym -+-.homomorphism ○ []-cong₂ (refl⟩∘⟨ Coeq₁.equality) (refl⟩∘⟨ Coeq₂.equality) ○ -+-.homomorphism
+      ; coequalize = coequalize
+      ; universal = universal _
+      ; unique = uniq _
+      }
+    where
+      open IsRightExact
+      open RightExactFunctor
+      module Coeq₁ = IsCoequalizer (F-resp-coeq (isRightExact (π₁ {𝒞} {𝒞})) isCoeq)
+      module Coeq₂ = IsCoequalizer (F-resp-coeq (isRightExact (π₂ {𝒞} {𝒞})) isCoeq)
+      open 𝒞 using ([]-cong₂; +₁∘i₁; +₁∘i₂; []∘+₁; +-g-η)
+      open 𝒞 using (Obj; _≈_; module HomReasoning; assoc; sym-assoc)
+      open 𝒞.HomReasoning
+      open ⇒-Reasoning 𝒞.U
+
+      module _ {X : Obj} {k : B₁ + B₂ ⇒ X} (eq : k ∘ (f₁ +₁ f₂) ≈ k ∘ (g₁ +₁ g₂)) where
+
+        eq₁ : (k ∘ i₁) ∘ f₁ ≈ (k ∘ i₁) ∘ g₁
+        eq₁ = begin
+            (k ∘ i₁) ∘ f₁       ≈⟨ pushʳ +₁∘i₁ ⟨
+            k ∘ (f₁ +₁ f₂) ∘ i₁ ≈⟨ extendʳ eq ⟩
+            k ∘ (g₁ +₁ g₂) ∘ i₁ ≈⟨ pushʳ +₁∘i₁ ⟩
+            (k ∘ i₁) ∘ g₁       ∎
+
+        eq₂ : (k ∘ i₂) ∘ f₂ ≈ (k ∘ i₂) ∘ g₂
+        eq₂ = begin
+            (k ∘ i₂) ∘ f₂       ≈⟨ pushʳ +₁∘i₂ ⟨
+            k ∘ (f₁ +₁ f₂) ∘ i₂ ≈⟨ extendʳ eq ⟩
+            k ∘ (g₁ +₁ g₂) ∘ i₂ ≈⟨ pushʳ +₁∘i₂ ⟩
+            (k ∘ i₂) ∘ g₂       ∎
+
+        coequalize : C₁ + C₂ ⇒ X
+        coequalize = [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ]
+
+        universal : k ≈ coequalize ∘ (h₁ +₁ h₂)
+        universal = begin
+            k                                                         ≈⟨ +-g-η ⟨
+            [ k ∘ i₁ , k ∘ i₂ ]                                       ≈⟨ []-cong₂ Coeq₁.universal Coeq₂.universal ⟩
+            [ Coeq₁.coequalize eq₁ ∘ h₁ , Coeq₂.coequalize eq₂ ∘ h₂ ] ≈⟨ []∘+₁ ⟨
+            coequalize ∘ (h₁ +₁ h₂)                                   ∎
+
+        uniq : {i : C₁ + C₂ ⇒ X} → k ≈ i ∘ (h₁ +₁ h₂) → i ≈ coequalize
+        uniq {i} eq′ = begin
+            i                   ≈⟨ +-g-η ⟨
+            [ i ∘ i₁ , i ∘ i₂ ] ≈⟨ []-cong₂ (Coeq₁.unique eq₁′) (Coeq₂.unique eq₂′) ⟩
+            [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ] ∎
+          where
+            eq₁′ : k ∘ i₁ ≈ (i ∘ i₁) ∘ h₁
+            eq₁′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₁
+            eq₂′ : k ∘ i₂ ≈ (i ∘ i₂) ∘ h₂
+            eq₂′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₂
+
+module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where
+
+  open FinCoCom using (_⇒_; _∘_; id)
+  module 𝒞 = FinitelyCocompleteCategory 𝒞
+
+  -+- : 𝒞 × 𝒞 ⇒ 𝒞
+  -+- = record
+      { F = 𝒞.-+-
+      ; isRightExact = record
+          { F-resp-⊥ = +-resp-⊥ 𝒞
+          ; F-resp-+ = +-resp-+ 𝒞
+          ; F-resp-coeq = +-resp-coeq 𝒞
+          }
+      }
+
+  [x+y]+z : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞
+  [x+y]+z = -+- ∘ (-+- ×₁ id)
+
+  x+[y+z] : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞
+  x+[y+z] = -+- ∘ (id ×₁ -+-) ∘ assocˡ
diff --git a/Functor/Exact.agda b/Functor/Exact.agda
new file mode 100644
index 0000000..b7ac9da
--- /dev/null
+++ b/Functor/Exact.agda
@@ -0,0 +1,190 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Exact where
+
+import Function.Base as Function
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
+open import Categories.Diagram.Coequalizer using (Coequalizer; IsCoequalizer; IsCoequalizer⇒Coequalizer)
+open import Categories.Diagram.Pushout using (IsPushout; Pushout)
+open import Categories.Diagram.Pushout.Properties using (Coproduct×Coequalizer⇒Pushout; up-to-iso)
+open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
+open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-≅)
+open import Categories.Object.Coproduct using (IsCoproduct; Coproduct; IsCoproduct⇒Coproduct; Coproduct⇒IsCoproduct)
+open import Categories.Object.Initial using (IsInitial)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+open import Function.Base using (id)
+open import Level
+
+module _ {o ℓ e : Level} {𝒞 : Category o ℓ e} where
+
+  open Category 𝒞
+
+  Coequalizer-resp-≈
+      : {A B C : Obj}
+        {f f′ g g′ : A ⇒ B}
+        {arr : B ⇒ C}
+      → f ≈ f′
+      → g ≈ g′
+      → IsCoequalizer 𝒞 f g arr
+      → IsCoequalizer 𝒞 f′ g′ arr
+  Coequalizer-resp-≈ ≈f ≈g ce = record
+      { equality = refl⟩∘⟨ sym ≈f ○ equality ○ refl⟩∘⟨ ≈g
+      ; coequalize = λ { eq → coequalize (refl⟩∘⟨ ≈f ○ eq ○ refl⟩∘⟨ sym ≈g) }
+      ; universal = universal
+      ; unique = unique
+      }
+    where
+      open HomReasoning
+      open Equiv
+      open IsCoequalizer ce
+
+  IsPushout⇒Pushout
+      : {A B C D : Obj}
+        {f : A ⇒ B} {g : A ⇒ C} {i₁ : B ⇒ D} {i₂ : C ⇒ D}
+      → IsPushout 𝒞 f g i₁ i₂
+      → Pushout 𝒞 f g
+  IsPushout⇒Pushout isP = record { i₁ = _ ; i₂ = _ ; isPushout = isP }
+
+module _ {o ℓ e : Level} {𝒞 𝒟 : Category o ℓ e} (F : Functor 𝒞 𝒟) where
+
+  open Functor F
+  open Category 𝒞
+
+  PreservesCoequalizer : Set (o ⊔ ℓ ⊔ e)
+  PreservesCoequalizer = {A B C : Obj} {f g : A ⇒ B} {h : B ⇒ C} → IsCoequalizer 𝒞 f g h → IsCoequalizer 𝒟 (F₁ f) (F₁ g) (F₁ h)
+
+  PreservesCoproduct : Set (o ⊔ ℓ ⊔ e)
+  PreservesCoproduct = {A B C : Obj} {i₁ : A ⇒ C} {i₂ : B ⇒ C} → IsCoproduct 𝒞 i₁ i₂ → IsCoproduct 𝒟 (F₁ i₁) (F₁ i₂)
+
+  PreservesInitial : Set (o ⊔ ℓ ⊔ e)
+  PreservesInitial = {A : Obj} → IsInitial 𝒞 A → IsInitial 𝒟 (F₀ A)
+
+  PreservesPushouts : Set (o ⊔ ℓ ⊔ e)
+  PreservesPushouts = {A B C D : Obj} {f : A ⇒ B} {g : A ⇒ C} {i₁ : B ⇒ D} {i₂ : C ⇒ D} → IsPushout 𝒞 f g i₁ i₂ → IsPushout 𝒟 (F₁ f) (F₁ g) (F₁ i₁) (F₁ i₂)
+
+module _ {o ℓ e : Level} (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where
+
+  open FinitelyCocompleteCategory using (U)
+
+  record IsRightExact (F : Functor (U 𝒞) (U 𝒟)) : Set (o ⊔ ℓ ⊔ e) where
+
+    field
+      F-resp-⊥ : PreservesInitial F
+      F-resp-+ : PreservesCoproduct F
+      F-resp-coeq : PreservesCoequalizer F
+
+    open FinitelyCocompleteCategory 𝒞 hiding (U)
+    open Functor F
+
+    F-resp-pushout : PreservesPushouts F
+    F-resp-pushout {A} {B} {C} {D} {f} {g} {i₁} {i₂} P = record
+        { commute = [ F ]-resp-square P.commute
+        ; universal = λ { eq → F-P′.universal eq ∘′ F-≅D.from }
+        ; universal∘i₁≈h₁ = assoc′ ○′ refl⟩∘⟨′ [ F ]-resp-square P.universal∘i₁≈h₁ ○′ F-P′.universal∘i₁≈h₁
+        ; universal∘i₂≈h₂ = assoc′ ○′ refl⟩∘⟨′ [ F ]-resp-square P.universal∘i₂≈h₂ ○′ F-P′.universal∘i₂≈h₂
+        ; unique-diagram = λ { eq₁ eq₂ →
+            insertʳ′ F-≅D.isoˡ ○′
+            F-P′.unique-diagram
+                (assoc′ ○′
+                  refl⟩∘⟨′ (Equiv′.sym (insertˡ′ F-≅D.isoˡ ○′ (refl⟩∘⟨′ [ F ]-resp-square P.universal∘i₁≈h₁))) ○′
+                  eq₁ ○′
+                  refl⟩∘⟨′ (insertˡ′ F-≅D.isoˡ ○′ (refl⟩∘⟨′ [ F ]-resp-square P.universal∘i₁≈h₁)) ○′
+                  sym-assoc′)
+                (assoc′ ○′
+                  refl⟩∘⟨′ (Equiv′.sym (insertˡ′ F-≅D.isoˡ ○′ (refl⟩∘⟨′ [ F ]-resp-square P.universal∘i₂≈h₂))) ○′
+                  eq₂ ○′
+                  refl⟩∘⟨′ (insertˡ′ F-≅D.isoˡ ○′ (refl⟩∘⟨′ [ F ]-resp-square P.universal∘i₂≈h₂)) ○′
+                  sym-assoc′) ⟩∘⟨refl′ ○′
+            cancelʳ′ F-≅D.isoˡ }
+        }
+      where
+        module P = IsPushout P
+        cp : Coproduct (U 𝒞) B C
+        cp = coproduct
+        open Coproduct cp using (inject₁; inject₂; [_,_]; g-η; []-cong₂) renaming (i₁ to ι₁; i₂ to ι₂; A+B to B+C)
+        ce : Coequalizer (U 𝒞) (ι₁ ∘ f) (ι₂ ∘ g)
+        ce = coequalizer (ι₁ ∘ f) (ι₂ ∘ g)
+        open Coequalizer ce using (equality; coequalize) renaming (arr to i₁-i₂; obj to D′; universal to univ; unique to uniq)
+        open HomReasoning
+        open import Categories.Morphism.Reasoning (U 𝒞)
+        open import Categories.Morphism.Reasoning (U 𝒟) using () renaming (pullʳ to pullʳ′; insertʳ to insertʳ′; cancelʳ to cancelʳ′; insertˡ to insertˡ′; extendˡ to extendˡ′)
+        import Categories.Morphism as Morphism
+        open Morphism (U 𝒞) using (_≅_)
+        open Morphism (U 𝒟) using () renaming (_≅_ to _≅′_)
+        P′ : IsPushout (U 𝒞) f g (i₁-i₂ ∘ ι₁) (i₁-i₂ ∘ ι₂)
+        P′ = Pushout.isPushout (Coproduct×Coequalizer⇒Pushout (U 𝒞) cp ce)
+        open Category (U 𝒟) using () renaming (_∘_ to _∘′_; module HomReasoning to 𝒟-Reasoning; assoc to assoc′; sym-assoc to sym-assoc′; module Equiv to Equiv′)
+        open 𝒟-Reasoning using () renaming (_○_ to _○′_; refl⟩∘⟨_ to refl⟩∘⟨′_; _⟩∘⟨refl to _⟩∘⟨refl′)
+        ≅D : D ≅ D′
+        ≅D = up-to-iso (U 𝒞) (IsPushout⇒Pushout P) (IsPushout⇒Pushout P′)
+        F-≅D : F₀ D ≅′ F₀ D′
+        F-≅D = [ F ]-resp-≅ ≅D
+        module F-≅D = _≅′_ F-≅D
+        F-cp : IsCoproduct (U 𝒟) (F₁ ι₁) (F₁ ι₂)
+        F-cp = F-resp-+ (Coproduct⇒IsCoproduct (U 𝒞) cp)
+        F-ce : IsCoequalizer (U 𝒟) (F₁ ι₁ ∘′ F₁ f) (F₁ ι₂ ∘′ F₁ g) (F₁ i₁-i₂)
+        F-ce = Coequalizer-resp-≈ homomorphism homomorphism (F-resp-coeq (Coequalizer.isCoequalizer ce))
+        F-P′ : IsPushout (U 𝒟) (F₁ f) (F₁ g) (F₁ i₁-i₂ ∘′ F₁ ι₁) (F₁ i₁-i₂ ∘′ F₁ ι₂)
+        F-P′ = Pushout.isPushout (Coproduct×Coequalizer⇒Pushout (U 𝒟) (IsCoproduct⇒Coproduct (U 𝒟) F-cp) (IsCoequalizer⇒Coequalizer (U 𝒟) F-ce))
+        module F-P′ = IsPushout F-P′
+
+  record RightExactFunctor : Set (o ⊔ ℓ ⊔ e) where
+
+    constructor rightexact
+
+    field
+      F : Functor (U 𝒞) (U 𝒟)
+      isRightExact : IsRightExact F
+
+    open Functor F public
+    open IsRightExact isRightExact public
+
+module _ where
+
+  open FinitelyCocompleteCategory using (U)
+
+  ∘-resp-IsRightExact
+      : {o ℓ e : Level}
+        {𝒞 𝒟 ℰ : FinitelyCocompleteCategory o ℓ e}
+        {F : Functor (U 𝒞) (U 𝒟)}
+        {G : Functor (U 𝒟) (U ℰ)}
+      → IsRightExact 𝒞 𝒟 F
+      → IsRightExact 𝒟 ℰ G
+      → IsRightExact 𝒞 ℰ (G ∘F F)
+  ∘-resp-IsRightExact F-isRightExact G-isRightExact = record
+      { F-resp-⊥ = G.F-resp-⊥ ∘ F.F-resp-⊥
+      ; F-resp-+ = G.F-resp-+ ∘ F.F-resp-+
+      ; F-resp-coeq = G.F-resp-coeq ∘ F.F-resp-coeq
+      }
+    where
+      open Function using (_∘_)
+      module F = IsRightExact F-isRightExact
+      module G = IsRightExact G-isRightExact
+
+∘-RightExactFunctor
+    : {o ℓ e : Level}
+    → {A B C : FinitelyCocompleteCategory o ℓ e}
+    → RightExactFunctor B C → RightExactFunctor A B → RightExactFunctor A C
+∘-RightExactFunctor F G = record
+    { F = F.F ∘F G.F
+    ; isRightExact = ∘-resp-IsRightExact G.isRightExact F.isRightExact
+    }
+  where
+    module F = RightExactFunctor F
+    module G = RightExactFunctor G
+
+idF-RightExact : {o ℓ e : Level} → {𝒞 : FinitelyCocompleteCategory o ℓ e} → IsRightExact 𝒞 𝒞 idF
+idF-RightExact = record
+    { F-resp-⊥ = id
+    ; F-resp-+ = id
+    ; F-resp-coeq = id
+    }
+
+idREF : {o ℓ e : Level} → {𝒞 : FinitelyCocompleteCategory o ℓ e} → RightExactFunctor 𝒞 𝒞
+idREF = record
+    { F = idF
+    ; isRightExact = idF-RightExact
+    }