1 files changed, 190 insertions, 0 deletions
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
+    }