Merge pull request #240 from TOTBWF/monadicity

Crude Monadicity Theorem

src/Categories/Adjoint/Monadic.agda

@@ -0,0 +1,32 @@
+{-# OPTIONS --without-K --safe #-}
+
+-- Monadic Adjunctions
+-- https://ncatlab.org/nlab/show/monadic+adjunction
+module Categories.Adjoint.Monadic where
+
+open import Level
+
+open import Categories.Adjoint
+open import Categories.Adjoint.Properties
+open import Categories.Category
+open import Categories.Category.Equivalence
+open import Categories.Functor
+open import Categories.Monad
+
+open import Categories.Category.Construction.EilenbergMoore
+open import Categories.Category.Construction.Properties.EilenbergMoore
+
+private
+  variable
+    o ℓ e : Level
+    𝒞 𝒟 : Category o ℓ e
+
+-- An adjunction is monadic if the adjunction "comes from" the induced monad in some sense.
+record IsMonadicAdjunction {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) : Set (levelOfTerm 𝒞 ⊔ levelOfTerm 𝒟) where
+  private
+    T : Monad 𝒞
+    T = adjoint⇒monad adjoint
+
+  field
+    Comparison⁻¹ : Functor (EilenbergMoore T) 𝒟
+    comparison-equiv : WeakInverse (ComparisonF adjoint) Comparison⁻¹

src/Categories/Adjoint/Monadic/Crude.agda

@@ -0,0 +1,174 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Adjoint
+open import Categories.Category
+open import Categories.Functor renaming (id to idF)
+
+-- The crude monadicity theorem. This proof is based off of the version
+-- provided in "Sheaves In Geometry and Logic" by Maclane and Moerdijk.
+module Categories.Adjoint.Monadic.Crude {o ℓ e o′ ℓ′ e′} {𝒞 : Category o ℓ e} {𝒟 : Category o′ ℓ′ e′}
+                                        {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) where
+
+open import Level
+open import Function using (_$_)
+open import Data.Product using (Σ-syntax; _,_)
+
+open import Categories.Adjoint.Properties
+open import Categories.Adjoint.Monadic
+open import Categories.Adjoint.Monadic.Properties
+open import Categories.Category.Equivalence using (StrongEquivalence)
+open import Categories.Category.Equivalence.Properties using (pointwise-iso-equivalence)
+open import Categories.Functor.Properties
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
+open import Categories.NaturalTransformation
+open import Categories.Monad
+
+open import Categories.Diagram.Coequalizer
+open import Categories.Diagram.ReflexivePair
+
+open import Categories.Adjoint.Construction.EilenbergMoore
+open import Categories.Category.Construction.EilenbergMoore
+open import Categories.Category.Construction.Properties.EilenbergMoore
+
+open import Categories.Morphism
+open import Categories.Morphism.Notation
+open import Categories.Morphism.Properties
+import Categories.Morphism.Reasoning as MR
+
+private
+  module L = Functor L
+  module R = Functor R
+
+  module 𝒞 = Category 𝒞
+  module 𝒟 = Category 𝒟
+
+  module adjoint = Adjoint adjoint
+
+  T : Monad 𝒞
+  T = adjoint⇒monad adjoint
+
+  𝒞ᵀ : Category _ _ _
+  𝒞ᵀ = EilenbergMoore T
+
+  Comparison : Functor 𝒟 𝒞ᵀ
+  Comparison = ComparisonF adjoint
+
+  module Comparison = Functor Comparison
+
+  open Coequalizer
+
+-- We could do this with limits, but this is far easier.
+PreservesReflexiveCoequalizers : (F : Functor 𝒟 𝒞) → Set _
+PreservesReflexiveCoequalizers F = ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → (coeq : Coequalizer 𝒟 f g) → IsCoequalizer 𝒞 (F.F₁ f) (F.F₁ g) (F.F₁ (arr coeq))
+  where
+    module F = Functor F
+
+module _ {F : Functor 𝒟 𝒞} (preserves-reflexive-coeq : PreservesReflexiveCoequalizers F) where
+  open Functor F
+
+  -- Unfortunately, we need to prove that the 'coequalize' arrows are equal as a lemma
+  preserves-coequalizer-unique : ∀ {A B C} {f g : 𝒟 [ A , B ]} {h : 𝒟 [ B , C ]} {eq : 𝒟 [ 𝒟 [ h ∘ f ] ≈ 𝒟 [ h ∘ g ] ]}
+                                 → (reflexive-pair : ReflexivePair 𝒟 f g) → (coe : Coequalizer 𝒟 f g)
+                                 →  𝒞 [ F₁ (coequalize coe eq) ≈ IsCoequalizer.coequalize (preserves-reflexive-coeq reflexive-pair coe) ([ F ]-resp-square eq) ]
+  preserves-coequalizer-unique reflexive-pair coe = IsCoequalizer.unique (preserves-reflexive-coeq reflexive-pair coe) (F-resp-≈ (universal coe) ○ homomorphism)
+    where
+      open 𝒞.HomReasoning
+
+
+-- If 𝒟 has coequalizers of reflexive pairs, then the comparison functor has a left adjoint.
+module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → Coequalizer 𝒟 f g) where
+
+  private
+    reflexive-pair : (M : Module T) → ReflexivePair 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M)))
+    reflexive-pair M = record
+      { s = L.F₁ (adjoint.unit.η (Module.A M))
+      ; isReflexivePair = record
+        { sectionₗ = begin
+          𝒟 [ L.F₁ (Module.action M) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ≈˘⟨ L.homomorphism ⟩
+          L.F₁ (𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] )       ≈⟨ L.F-resp-≈ (Module.identity M) ⟩
+          L.F₁ 𝒞.id                                                         ≈⟨ L.identity ⟩
+          𝒟.id                                                              ∎
+        ; sectionᵣ = begin
+          𝒟 [ adjoint.counit.η (L.₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ≈⟨ adjoint.zig ⟩
+          𝒟.id ∎
+        }
+      }
+      where
+        open 𝒟.HomReasoning
+
+    -- The key part of the proof. As we have all reflexive coequalizers, we can create the following coequalizer.
+    -- We can think of this as identifying the action of the algebra lifted to a "free" structure
+    -- and the counit of the adjunction, as the unit of the adjunction (also lifted to the "free structure") is a section of both.
+    has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M)))
+    has-coequalizer M = has-reflexive-coequalizers (reflexive-pair M)
+
+    module Comparison⁻¹ = Functor (Comparison⁻¹ adjoint has-coequalizer)
+    module Comparison⁻¹⊣Comparison = Adjoint (Comparison⁻¹⊣Comparison adjoint has-coequalizer)
+
+    -- We have one interesting coequalizer in 𝒞 built out of a T-module's action.
+    coequalizer-action : (M : Module T) → Coequalizer 𝒞 (R.F₁ (L.F₁ (Module.action M))) (R.F₁ (adjoint.counit.η (L.₀ (Module.A M))))
+    coequalizer-action M = record
+      { arr = Module.action M
+      ; isCoequalizer = record
+        { equality = Module.commute M
+        ; coequalize = λ {X} {h} eq → 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ]
+        ; universal = λ {C} {h} {eq} → begin
+          h                                                                                                       ≈⟨ introʳ adjoint.zag ○ 𝒞.sym-assoc ⟩
+          𝒞 [ 𝒞 [ h ∘ R.F₁ (adjoint.counit.η (L.₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ pushˡ (⟺ eq) ⟩
+          𝒞 [ h ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ]              ≈⟨ pushʳ (adjoint.unit.sym-commute (Module.action M)) ⟩
+          𝒞 [ 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ]                                          ∎
+        ; unique = λ {X} {h} {i} {eq} eq′ → begin
+          i ≈⟨ introʳ (Module.identity M) ⟩
+          𝒞 [ i ∘ 𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] ] ≈⟨ pullˡ (⟺ eq′) ⟩
+          𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] ∎
+        }
+      }
+      where
+        open 𝒞.HomReasoning
+        open MR 𝒞
+
+  -- If 'R' preserves reflexive coequalizers, then the unit of the adjunction is a pointwise isomorphism
+  unit-iso : PreservesReflexiveCoequalizers R → (X : Module T) → Σ[ h ∈ 𝒞ᵀ [ Comparison.F₀ (Comparison⁻¹.F₀ X) , X ] ] (Iso 𝒞ᵀ (Comparison⁻¹⊣Comparison.unit.η X) h)
+  unit-iso preserves-reflexive-coeq X =
+    let
+        coequalizerˣ = has-coequalizer X
+        coequalizerᴿˣ = ((IsCoequalizer⇒Coequalizer 𝒞 (preserves-reflexive-coeq (reflexive-pair X) (has-coequalizer X))))
+        coequalizer-iso = up-to-iso 𝒞 (coequalizer-action X) coequalizerᴿˣ
+        module coequalizer-iso = _≅_ coequalizer-iso
+        open 𝒞
+        open 𝒞.HomReasoning
+        open MR 𝒞
+        α = record
+          { arr = coequalizer-iso.to
+          ; commute = begin
+            coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)                                                                                                                ≈⟨ introʳ (R.F-resp-≈ L.identity ○ R.identity) ⟩
+            (coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)) ∘ R.F₁ (L.F₁ 𝒞.id)                                                                                           ≈⟨ pushʳ (R.F-resp-≈ (L.F-resp-≈ (⟺ coequalizer-iso.isoʳ)) ○ R.F-resp-≈ L.homomorphism ○ R.homomorphism) ⟩
+            ((coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)) ∘ R.F₁ (L.F₁ (R.F₁ (arr coequalizerˣ) ∘ adjoint.unit.η _))) ∘ R.F₁ (L.F₁ coequalizer-iso.to)                ≈⟨ (refl⟩∘⟨ (R.F-resp-≈ L.homomorphism ○ R.homomorphism)) ⟩∘⟨refl ⟩
+            ((coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)) ∘  R.F₁ (L.F₁ (R.F₁ (arr coequalizerˣ))) ∘ R.F₁ (L.F₁ (adjoint.unit.η _))) ∘ R.F₁ (L.F₁ coequalizer-iso.to) ≈⟨ center ([ R ]-resp-square (adjoint.counit.commute _)) ⟩∘⟨refl ⟩
+            ((coequalizer-iso.to ∘ (R.F₁ (arr coequalizerˣ) ∘ R.F₁ (adjoint.counit.η (L.F₀ _))) ∘ R.F₁ (L.F₁ (adjoint.unit.η _))) ∘ R.F₁ (L.F₁ coequalizer-iso.to))       ≈⟨ (refl⟩∘⟨ cancelʳ (⟺ R.homomorphism ○ R.F-resp-≈ adjoint.zig ○ R.identity)) ⟩∘⟨refl  ⟩
+            (coequalizer-iso.to ∘ R.F₁ (arr coequalizerˣ)) ∘ R.F₁ (L.F₁ coequalizer-iso.to)                                                                               ≈˘⟨ universal coequalizerᴿˣ ⟩∘⟨refl ⟩
+            Module.action X ∘ R.F₁ (L.F₁ coequalizer-iso.to) ∎
+          }
+    in α , record { isoˡ = coequalizer-iso.isoˡ ; isoʳ = coequalizer-iso.isoʳ }
+
+  -- If 'R' preserves reflexive coequalizers and reflects isomorphisms, then the counit of the adjunction is a pointwise isomorphism.
+  counit-iso : PreservesReflexiveCoequalizers R → Conservative R → (X : 𝒟.Obj) → Σ[ h ∈ 𝒟 [ X , Comparison⁻¹.F₀ (Comparison.F₀ X) ] ] Iso 𝒟 (Comparison⁻¹⊣Comparison.counit.η X) h
+  counit-iso preserves-reflexive-coeq conservative X =
+    let coequalizerᴿᴷˣ = IsCoequalizer⇒Coequalizer 𝒞 (preserves-reflexive-coeq (reflexive-pair (Comparison.F₀ X)) (has-coequalizer (Comparison.F₀ X)))
+        coequalizerᴷˣ = has-coequalizer (Comparison.F₀ X)
+        coequalizer-iso = up-to-iso 𝒞 coequalizerᴿᴷˣ (coequalizer-action (Comparison.F₀ X))
+        module coequalizer-iso = _≅_ coequalizer-iso
+        open 𝒞.HomReasoning
+        open 𝒞.Equiv
+    in conservative (Iso-resp-≈ 𝒞 coequalizer-iso.iso (⟺ (preserves-coequalizer-unique {R} preserves-reflexive-coeq (reflexive-pair (Comparison.F₀ X)) coequalizerᴷˣ)) refl)
+
+  -- Now, for the final result. Both the unit and counit of the adjunction between the comparison functor and it's inverse are isomorphisms,
+  -- so therefore they form natural isomorphism. Therfore, we have an equivalence of categories.
+  crude-monadicity : PreservesReflexiveCoequalizers R → Conservative R → StrongEquivalence 𝒞ᵀ 𝒟
+  crude-monadicity preserves-reflexlive-coeq conservative = record
+    { F = Comparison⁻¹ adjoint has-coequalizer
+    ; G = Comparison
+    ; weak-inverse = pointwise-iso-equivalence (Comparison⁻¹⊣Comparison adjoint has-coequalizer)
+                                               (counit-iso preserves-reflexlive-coeq conservative)
+                                               (unit-iso preserves-reflexlive-coeq)
+    }

src/Categories/Adjoint/Monadic/Properties.agda

@@ -0,0 +1,138 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Adjoint
+open import Categories.Category
+open import Categories.Functor renaming (id to idF)
+
+module Categories.Adjoint.Monadic.Properties {o ℓ e o′ ℓ′ e′} {𝒞 : Category o ℓ e} {𝒟 : Category o′ ℓ′ e′}
+                                             {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) where
+
+
+open import Level
+open import Function using (_$_)
+
+open import Categories.Adjoint.Properties
+open import Categories.Adjoint.Monadic
+open import Categories.NaturalTransformation.NaturalIsomorphism
+open import Categories.NaturalTransformation
+open import Categories.Monad
+
+open import Categories.Diagram.Coequalizer
+
+open import Categories.Category.Construction.EilenbergMoore
+open import Categories.Category.Construction.Properties.EilenbergMoore
+
+open import Categories.Morphism
+import Categories.Morphism.Reasoning as MR
+
+private
+  module L = Functor L
+  module R = Functor R
+
+  module 𝒞 = Category 𝒞
+  module 𝒟 = Category 𝒟
+
+  module adjoint = Adjoint adjoint
+
+  T : Monad 𝒞
+  T = adjoint⇒monad adjoint
+
+  𝒞ᵀ : Category _ _ _
+  𝒞ᵀ = EilenbergMoore T
+
+  Comparison : Functor 𝒟 𝒞ᵀ
+  Comparison = ComparisonF adjoint
+
+  module Comparison = Functor Comparison
+
+
+-- If we have a coequalizer of the following diagram for every T-algabra, then the comparison functor has a left adjoint.
+module _ (has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M)))) where
+
+  open Coequalizer
+
+  Comparison⁻¹ : Functor 𝒞ᵀ 𝒟
+  Comparison⁻¹ = record
+    { F₀ = λ M → obj (has-coequalizer M)
+    ; F₁ = λ {M} {N} α → coequalize (has-coequalizer M) $ begin
+      𝒟 [ 𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (Module⇒.arr α) ] ∘ L.F₁ (Module.action M) ]                             ≈⟨ pullʳ (⟺ L.homomorphism) ⟩
+      𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (𝒞 [ Module⇒.arr α ∘ Module.action M ]) ]                                    ≈⟨ refl⟩∘⟨ L.F-resp-≈ (Module⇒.commute α) ⟩
+      𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (𝒞 [ Module.action N ∘ R.F₁ (L.F₁ (Module⇒.arr α)) ]) ]                      ≈⟨ refl⟩∘⟨ L.homomorphism ⟩
+      𝒟 [ arr (has-coequalizer N) ∘ 𝒟 [ L.F₁ (Module.action N) ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ]               ≈⟨ pullˡ (equality (has-coequalizer N)) ⟩
+      𝒟 [ 𝒟 [ arr (has-coequalizer N) ∘ adjoint.counit.η (L.F₀ (Module.A N)) ] ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ≈⟨ extendˡ (adjoint.counit.commute (L.F₁ (Module⇒.arr α))) ⟩
+      𝒟 [ 𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (Module⇒.arr α) ] ∘ adjoint.counit.η (L.₀ (Module.A M)) ]                ∎
+    ; identity = λ {A} → ⟺ $ unique (has-coequalizer A) $ begin
+      𝒟 [ arr (has-coequalizer A) ∘ L.F₁ 𝒞.id ] ≈⟨ refl⟩∘⟨ L.identity ⟩
+      𝒟 [ arr (has-coequalizer A) ∘ 𝒟.id ]      ≈⟨ id-comm ⟩
+      𝒟 [ 𝒟.id ∘ arr (has-coequalizer A) ]      ∎
+    ; homomorphism = λ {X} {Y} {Z} {f} {g} → ⟺ $ unique (has-coequalizer X) $ begin
+      𝒟 [ arr (has-coequalizer Z) ∘ L.F₁ (𝒞 [ Module⇒.arr g ∘ Module⇒.arr f ]) ]                              ≈⟨ 𝒟.∘-resp-≈ʳ L.homomorphism ○ 𝒟.sym-assoc ⟩
+      𝒟 [ 𝒟 [ arr (has-coequalizer Z) ∘ L.F₁ (Module⇒.arr g) ] ∘ L.F₁ (Module⇒.arr f) ]                       ≈⟨ universal (has-coequalizer Y) ⟩∘⟨refl ⟩
+      𝒟 [ 𝒟 [ coequalize (has-coequalizer Y) _ ∘ arr (has-coequalizer Y) ] ∘ L.F₁ (Module⇒.arr f) ]            ≈⟨ extendˡ (universal (has-coequalizer X)) ⟩
+      𝒟 [ 𝒟 [ coequalize (has-coequalizer Y) _ ∘ coequalize (has-coequalizer X) _ ] ∘ arr (has-coequalizer X) ] ∎
+    ; F-resp-≈ = λ {A} {B} {f} {g} eq → unique (has-coequalizer A) $ begin
+      𝒟 [ arr (has-coequalizer B) ∘ L.F₁ (Module⇒.arr g) ]            ≈⟨ refl⟩∘⟨ L.F-resp-≈ (𝒞.Equiv.sym eq) ⟩
+      𝒟 [ arr (has-coequalizer B) ∘ L.F₁ (Module⇒.arr f) ]            ≈⟨ universal (has-coequalizer A) ⟩
+      𝒟 [ coequalize (has-coequalizer A) _ ∘ arr (has-coequalizer A) ] ∎
+    }
+    where
+      open 𝒟.HomReasoning
+      open MR 𝒟
+
+  private
+    module Comparison⁻¹ = Functor Comparison⁻¹
+
+  Comparison⁻¹⊣Comparison : Comparison⁻¹ ⊣ Comparison
+  Adjoint.unit Comparison⁻¹⊣Comparison = ntHelper record
+    { η = λ M → record
+      { arr = 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ]
+      ; commute = begin
+        𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ]                                                      ≈⟨ pullʳ (adjoint.unit.commute (Module.action M)) ⟩
+        -- It would be nice to have a reasoning combinator doing this "⟺ homomorphism ... homomorphism" pattern
+        𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ]                          ≈⟨ pullˡ (⟺ R.homomorphism) ⟩
+        𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ L.F₁ (Module.action M) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ]                                 ≈⟨ (R.F-resp-≈ (equality (has-coequalizer M)) ⟩∘⟨refl) ⟩
+        𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ adjoint.counit.η (L.F₀ (Module.A M)) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ]                   ≈⟨ (R.homomorphism ⟩∘⟨refl) ⟩
+        𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ R.F₁ (adjoint.counit.η (L.F₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ]            ≈⟨ cancelʳ adjoint.zag ⟩
+        -- FIXME Use something like cancel here
+        R.F₁ (arr (has-coequalizer M))                                                                                                                  ≈˘⟨ R.F-resp-≈ (𝒟.identityʳ) ⟩
+        R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ 𝒟.id ])                                                                                                     ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ adjoint.zig) ⟩
+        R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ 𝒟 [ adjoint.counit.η (L.F₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ])                          ≈⟨ R.F-resp-≈ (MR.extendʳ 𝒟 (adjoint.counit.sym-commute (arr (has-coequalizer M)))) ⟩
+        R.F₁ (𝒟 [ adjoint.counit.η (obj (has-coequalizer M)) ∘ 𝒟 [ L.F₁ (R.F₁ (arr (has-coequalizer M))) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ])      ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ L.homomorphism) ⟩
+        R.F₁ (𝒟 [ adjoint.counit.η (obj (has-coequalizer M)) ∘ L.F₁ (𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M)])])               ≈⟨ R.homomorphism ⟩
+        𝒞 [ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ∘ R.F₁ (L.F₁ (𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M)])) ]       ∎
+      }
+    ; commute = λ {M} {N} f → begin
+      𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer N)) ∘ adjoint.unit.η (Module.A N) ] ∘ Module⇒.arr f ]                           ≈⟨ extendˡ (adjoint.unit.commute (Module⇒.arr f)) ⟩
+      𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer N)) ∘ R.F₁ (L.F₁ (Module⇒.arr f)) ] ∘ adjoint.unit.η (Module.A M) ]             ≈˘⟨ R.homomorphism ⟩∘⟨refl ⟩
+      𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (Module⇒.arr f) ]) ∘ adjoint.unit.η (Module.A M) ]                    ≈⟨ R.F-resp-≈ (universal (has-coequalizer M)) ⟩∘⟨refl ⟩
+      𝒞 [ R.F₁ (𝒟 [ (coequalize (has-coequalizer M) _) ∘ (arr (has-coequalizer M)) ]) ∘ adjoint.unit.η (Module.A M) ]    ≈⟨ pushˡ R.homomorphism ⟩
+      𝒞 [ R.F₁ (coequalize (has-coequalizer M) _) ∘ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ] ∎
+    }
+    where
+      open 𝒞.HomReasoning
+      open MR 𝒞
+  Adjoint.counit Comparison⁻¹⊣Comparison = ntHelper record
+    { η = λ X → coequalize (has-coequalizer (Comparison.F₀ X)) (adjoint.counit.commute (adjoint.counit.η X))
+    ; commute = λ {X} {Y} f → begin
+      𝒟 [ coequalize (has-coequalizer (Comparison.F₀ Y)) _ ∘ coequalize (has-coequalizer (Comparison.F₀ X)) _ ]  ≈⟨ unique (has-coequalizer (Comparison.F₀ X)) (adjoint.counit.sym-commute f ○ pushˡ (universal (has-coequalizer (Comparison.F₀ Y))) ○ pushʳ (universal (has-coequalizer (Comparison.F₀ X)))) ⟩
+      coequalize (has-coequalizer (Comparison.F₀ X)) (extendˡ (adjoint.counit.commute (adjoint.counit.η X)))     ≈˘⟨ unique (has-coequalizer (Comparison.F₀ X)) (pushʳ (universal (has-coequalizer (Comparison.F₀ X)))) ⟩
+      𝒟 [ f ∘ coequalize (has-coequalizer (Comparison.F₀ X)) _ ]                                                 ∎
+    }
+    where
+      open 𝒟.HomReasoning
+      open MR 𝒟
+  Adjoint.zig Comparison⁻¹⊣Comparison {X} = begin
+    𝒟 [ coequalize (has-coequalizer (Comparison.F₀ (Comparison⁻¹.F₀ X))) _ ∘ coequalize (has-coequalizer X) _ ] ≈⟨ unique (has-coequalizer X) (⟺ adjoint.RLadjunct≈id ○ pushˡ (universal (has-coequalizer (Comparison.F₀ (Comparison⁻¹.F₀ X)))) ○ pushʳ (universal (has-coequalizer X))) ⟩
+    coequalize (has-coequalizer X) {h = arr (has-coequalizer X)} (equality (has-coequalizer X))                 ≈˘⟨ unique (has-coequalizer X) (⟺ 𝒟.identityˡ) ⟩
+    𝒟.id                                                                                                        ∎
+    where
+      open 𝒟.HomReasoning
+      open MR 𝒟
+  Adjoint.zag Comparison⁻¹⊣Comparison {A} = begin
+    𝒞 [ R.F₁ (coequalize (has-coequalizer (Comparison.F₀ A)) _) ∘  𝒞 [ R.F₁ (arr (has-coequalizer (Comparison.F₀ A))) ∘ adjoint.unit.η (Module.A (Comparison.F₀ A)) ] ] ≈⟨ pullˡ (⟺ R.homomorphism) ⟩
+    𝒞 [ R.F₁ (𝒟 [ coequalize (has-coequalizer (Comparison.F₀ A)) _ ∘ arr (has-coequalizer (Comparison.F₀ A)) ]) ∘ adjoint.unit.η (Module.A (Comparison.F₀ A)) ]         ≈˘⟨ R.F-resp-≈ (universal (has-coequalizer (Comparison.F₀ A))) ⟩∘⟨refl ⟩
+    𝒞 [ R.F₁ (adjoint.counit.η A) ∘ adjoint.unit.η (R.F₀ A) ]                                                                                                           ≈⟨ adjoint.zag ⟩
+    𝒞.id                                                                                                                                                                ∎
+    where
+      open 𝒞.HomReasoning
+      open MR 𝒞

src/Categories/Diagram/Coequalizer.agda

@@ -7,18 +7,79 @@ module Categories.Diagram.Coequalizer {o ℓ e} (𝒞 : Category o ℓ e) where
 open Category 𝒞
 open HomReasoning
 
+open import Categories.Morphism 𝒞
+open import Categories.Morphism.Reasoning 𝒞
+
 open import Level
+open import Function using (_$_)
 
 private
   variable
     A B C : Obj
+    h i j k : A ⇒ B
+
+record IsCoequalizer {E} (f g : A ⇒ B) (arr : B ⇒ E) : Set (o ⊔ ℓ ⊔ e) where
+  field
+    equality   : arr ∘ f ≈ arr ∘ g
+    coequalize : {h : B ⇒ C} → h ∘ f ≈ h ∘ g → E ⇒ C
+    universal  : {h : B ⇒ C} {eq : h ∘ f ≈ h ∘ g} → h ≈ coequalize eq ∘ arr
+    unique     : {h : B ⇒ C} {i : E ⇒ C} {eq : h ∘ f ≈ h ∘ g} → h ≈ i ∘ arr → i ≈ coequalize eq
+
+  unique′ : (eq eq′ : h ∘ f ≈ h ∘ g) → coequalize eq ≈ coequalize eq′
+  unique′ eq eq′ = unique universal
+
+  id-coequalize : id ≈ coequalize equality
+  id-coequalize = unique (⟺ identityˡ)
+
+  coequalize-resp-≈ : ∀ {eq :  h ∘ f ≈ h ∘ g} {eq′ : i ∘ f ≈ i ∘ g} →
+    h ≈ i → coequalize eq ≈ coequalize eq′
+  coequalize-resp-≈ {h = h} {i = i} {eq = eq} {eq′ = eq′} h≈i = unique $ begin
+    i                   ≈˘⟨ h≈i ⟩
+    h                   ≈⟨ universal ⟩
+    coequalize eq ∘ arr ∎
+
+  coequalize-resp-≈′ : (eq :  h ∘ f ≈ h ∘ g) → (eq′ : i ∘ f ≈ i ∘ g) →
+    h ≈ i → j ≈ coequalize eq → k ≈ coequalize eq′ → j ≈ k
+  coequalize-resp-≈′ {j = j} {k = k} eq eq′ h≈i eqj eqk = begin
+    j              ≈⟨ eqj ⟩
+    coequalize eq  ≈⟨ coequalize-resp-≈ h≈i ⟩
+    coequalize eq′ ≈˘⟨ eqk ⟩
+    k              ∎
 
 record Coequalizer (f g : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
   field
     {obj} : Obj
     arr   : B ⇒ obj
+    isCoequalizer : IsCoequalizer f g arr
 
-    equality   : arr ∘ f ≈ arr ∘ g
-    coequalize : {h : B ⇒ C} → h ∘ f ≈ h ∘ g → obj ⇒ C
-    universal  : {h : B ⇒ C} {eq : h ∘ f ≈ h ∘ g} → h ≈ coequalize eq ∘ arr
-    unique     : {h : B ⇒ C} {i : obj ⇒ C} {eq : h ∘ f ≈ h ∘ g} → h ≈ i ∘ arr → i ≈ coequalize eq
+  open IsCoequalizer isCoequalizer public
+
+
+-- Proving this via duality arguments is kind of annoying, as ≅ does not behave nicely in
+-- concert with op.
+up-to-iso : (coe₁ coe₂ : Coequalizer h i) → Coequalizer.obj coe₁ ≅ Coequalizer.obj coe₂
+up-to-iso coe₁ coe₂ = record
+  { from = repack coe₁ coe₂
+  ; to = repack coe₂ coe₁
+  ; iso = record
+    { isoˡ = repack-cancel coe₂ coe₁
+    ; isoʳ = repack-cancel coe₁ coe₂
+    }
+  }
+  where
+    open Coequalizer
+
+    repack : (coe₁ coe₂ : Coequalizer h i) → obj coe₁ ⇒ obj coe₂
+    repack coe₁ coe₂ = coequalize coe₁ (equality coe₂)
+
+    repack∘ : (coe₁ coe₂ coe₃ : Coequalizer h i) → repack coe₂ coe₃ ∘ repack coe₁ coe₂ ≈ repack coe₁ coe₃
+    repack∘ coe₁ coe₂ coe₃ = unique coe₁ (⟺ (glueTrianglesˡ (⟺ (universal coe₂)) (⟺ (universal coe₁)))) -- unique e₃ (⟺ (glueTrianglesʳ (⟺ (universal e₃)) (⟺ (universal e₂))))
+
+    repack-cancel : (e₁ e₂ : Coequalizer h i) → repack e₁ e₂ ∘ repack e₂ e₁ ≈ id
+    repack-cancel coe₁ coe₂ = repack∘ coe₂ coe₁ coe₂ ○ ⟺ (id-coequalize coe₂)
+
+IsCoequalizer⇒Coequalizer : IsCoequalizer h i k → Coequalizer h i
+IsCoequalizer⇒Coequalizer {k = k} is-coe = record
+  { arr = k
+  ; isCoequalizer = is-coe
+  }

src/Categories/Diagram/Duality.agda

@@ -57,10 +57,12 @@ Coequalizer⇒coEqualizer coe = record
 coEqualizer⇒Coequalizer : Equalizer f g → Coequalizer f g
 coEqualizer⇒Coequalizer e = record
   { arr        = arr
-  ; equality   = equality
-  ; coequalize = equalize
-  ; universal  = universal
-  ; unique     = unique
+  ; isCoequalizer = record
+    { equality   = equality
+    ; coequalize = equalize
+    ; universal  = universal
+    ; unique     = unique
+    }
   }
   where open Equalizer e
 

src/Categories/Diagram/ReflexivePair.agda

@@ -0,0 +1,38 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Core
+
+-- Reflexive pairs and reflexive coequalizers
+-- https://ncatlab.org/nlab/show/reflexive+coequalizer
+module Categories.Diagram.ReflexivePair {o ℓ e} (𝒞 : Category o ℓ e) where
+
+open import Level
+
+open import Categories.Diagram.Coequalizer 𝒞
+
+open Category 𝒞
+open HomReasoning
+open Equiv
+
+private
+  variable
+    A B R : Obj
+
+-- A reflexive pair can be thought of as a vast generalization of a reflexive relation.
+-- To see this, consider the case in 'Set' where 'R ⊆ A × A', and 'f' and 'g' are the projections.
+-- Then, our morphism 's' would have to look something like the diagonal morphism due to the
+-- restriction it is a section of both 'f' and 'g'.
+record IsReflexivePair (f g : R ⇒ A) (s : A ⇒ R) : Set e where
+  field
+    sectionₗ : f ∘ s ≈ id
+    sectionᵣ : g ∘ s ≈ id
+
+  section : f ∘ s ≈ g ∘ s
+  section = sectionₗ ○ ⟺ sectionᵣ
+
+record ReflexivePair (f g : R ⇒ A) : Set (ℓ ⊔ e) where
+  field
+    s : A ⇒ R
+    isReflexivePair : IsReflexivePair f g s
+
+  open IsReflexivePair isReflexivePair public

src/Categories/Functor/Properties.agda

@@ -16,6 +16,7 @@ import Categories.Morphism as Morphism
 import Categories.Morphism.Reasoning as Reas
 open import Categories.Morphism.IsoEquiv as IsoEquiv
 open import Categories.Morphism.Isomorphism
+open import Categories.Morphism.Notation
 
 private
   variable
@@ -49,6 +50,12 @@ EssentiallySurjective {C = C} {D = D} F = (d : Category.Obj D) → Σ C.Obj (λ
   open Morphism D
   module C = Category C
 
+Conservative : Functor C D → Set _
+Conservative {C = C} {D = D} F = ∀ {A B} {f : C [ A , B ]} {g : D [ F₀ B , F₀ A ]} → Iso D (F₁ f) g → Σ (C [ B , A ]) (λ h → Iso C f h)
+  where
+    open Functor F
+    open Morphism
+
 -- a series of [ Functor ]-respects-Thing combinators (with respects -> resp)
 
 module _ (F : Functor C D) where