Duskin's Monadicity Theorem

src/Cat/Diagram/Colimit/Base.lagda.md

@@ -198,8 +198,12 @@ cocones over that diagram.
   Colimit : Type _
   Colimit = Initial Cocones
 
+  Colimit-cocone : Colimit → Cocone
+  Colimit-cocone = Initial.bot
+
   Colimit-apex : Colimit → C.Ob
-  Colimit-apex x = coapex (Initial.bot x)
+  Colimit-apex x = coapex (Colimit-cocone x)
+
 
   Colimit-universal : (L : Colimit) → (K : Cocone) → C.Hom (Colimit-apex L) (coapex K) 
   Colimit-universal L K = hom (Initial.¡ L {K})
@@ -241,6 +245,22 @@ functors preserve commutative diagrams.
     F.₁ (Cocone.ψ x _)             ∎
 ```
 
+Note that this also lets us map morphisms between cocones into $\ca{D}$.
+
+```agda
+  F-map-cocone-hom
+    : {X Y : Cocone Dia} 
+    → Cocone-hom Dia X Y
+    → Cocone-hom (F F∘ Dia) (F-map-cocone X) (F-map-cocone Y)
+  F-map-cocone-hom {X = X} {Y = Y} f = hom where
+    module f = Cocone-hom f
+
+    hom : Cocone-hom (F F∘ Dia) (F-map-cocone X) (F-map-cocone Y)
+    hom .Cocone-hom.hom = F .F₁ f.hom
+    hom .Cocone-hom.commutes _ = F.collapse (f.commutes _)
+```
+
+
 Though functors must take cocones to cocones, they may not necessarily
 take colimiting cocones to colimiting cocones! When a functor does, we
 say that it _preserves_ colimits.
@@ -250,6 +270,13 @@ say that it _preserves_ colimits.
   Preserves-colimit K = is-colimit Dia K → is-colimit (F F∘ Dia) (F-map-cocone K)
 ```
 
+```agda
+  F-map-colimit : (L : Colimit Dia) → Preserves-colimit (Colimit-cocone Dia L) → Colimit (F F∘ Dia)
+  F-map-colimit L preserves .Initial.bot = F-map-cocone (Initial.bot L)
+  F-map-colimit L preserves .Initial.has⊥ = preserves (Initial.has⊥ L)
+```
+
+
 ## Reflection of colimits
 
 We say a functor __reflects__ colimits if the existence of a colimiting

src/Cat/Functor/Conservative.lagda.md

@@ -1,10 +1,14 @@
 ```agda
 open import Cat.Diagram.Limit.Base
+open import Cat.Diagram.Colimit.Base
 open import Cat.Diagram.Terminal
+open import Cat.Diagram.Initial
 open import Cat.Functor.Base
 open import Cat.Morphism
 open import Cat.Prelude hiding (J)
 
+import Cat.Reasoning
+
 module Cat.Functor.Conservative where
 ```
 
@@ -44,9 +48,15 @@ in $C$ as well (see `apex-iso→is-limit`{.Agda}).
 
 ```agda
 module _ {F : Functor C D} (conservative : is-conservative F) where
-  conservative-reflects-limits : ∀ {Dia : Functor J C} → (L : Limit Dia)
-                               → (∀ (K : Cone Dia) → Preserves-limit F K)
-                               → (∀ (K : Cone Dia) → Reflects-limit F K)
+  private
+    module D = Cat.Reasoning D
+    module C = Cat.Reasoning C
+    module Cocones {o h o′ h′} {J : Precategory o h} {C : Precategory o′ h′} {Dia : Functor J C} = Cat.Reasoning (Cocones Dia)
+
+  conservative-reflects-limits
+    : ∀ {Dia : Functor J C} → (L : Limit Dia)
+    → (∀ (K : Cone Dia) → Preserves-limit F K)
+    → (∀ (K : Cone Dia) → Reflects-limit F K)
   conservative-reflects-limits {Dia = Dia} L-lim preserves K limits =
     apex-iso→is-limit Dia K L-lim
       $ conservative
@@ -73,3 +83,72 @@ module _ {F : Functor C D} (conservative : is-conservative F) where
         hom (F-map-cone-hom F (Terminal.! L-lim)) ≡⟨⟩
         F .F₁ (hom L-lim.!) ∎
 ```
+
+We also have a dual theorem for colimits.
+
+```agda
+  conservative-reflects-colimits
+    : ∀ {Dia : Functor J C} → (L : Colimit Dia)
+    → (∀ (K : Cocone Dia) → Preserves-colimit F K)
+    → (∀ (K : Cocone Dia) → Reflects-colimit F K)
+  conservative-reflects-colimits
+    {Dia = Dia} L-colim preserves K F∘K-colimits =
+    coapex-iso→is-colimit Dia K L-colim
+    $ conservative
+    invert
+    where
+
+      F∘K-colim : Colimit (F F∘ Dia)
+      F∘K-colim .Initial.bot = F-map-cocone F K
+      F∘K-colim .Initial.has⊥ = F∘K-colimits
+
+      F∘L-colim : Colimit (F F∘ Dia)
+      F∘L-colim = F-map-colimit F L-colim (preserves (Colimit-cocone Dia L-colim))
+
+      module L-colim = Initial L-colim
+      module F∘L-colim = Initial F∘L-colim
+      module F∘K-colim = Initial F∘K-colim
+      open Cocone-hom
+
+      L : Cocone Dia
+      L = L-colim.bot
+
+      F∘L : Cocone (F F∘ Dia)
+      F∘L = F-map-cocone F L-colim.bot
+
+      F∘K : Cocone (F F∘ Dia)
+      F∘K = F-map-cocone F K
+
+      L-universal : (K′ : Cocone Dia) → Cocone-hom Dia L K′
+      L-universal K′ = L-colim.¡ {K′}
+
+      F∘L-universal : (K′ : Cocone (F F∘ Dia)) → Cocone-hom (F F∘ Dia) F∘L K′
+      F∘L-universal K′ =  F∘L-colim.¡ {K′}
+
+      F∘K-universal : (K′ : Cocone (F F∘ Dia)) → Cocone-hom (F F∘ Dia) F∘K K′
+      F∘K-universal K′ =  F∘K-colim.¡ {K′}
+
+      module F∘L-universal K′ = Cocone-hom (F∘L-universal K′)
+      module L-universal K′ = Cocone-hom (L-universal K′)
+      module F∘K-universal K′ = Cocone-hom (F∘K-universal K′)
+
+      F-preserves-universal
+        : ∀ {K′} → F∘L-universal.hom (F-map-cocone F K′) ≡ F. F₁ (L-universal.hom K′)
+      F-preserves-universal {K′} =
+        F∘L-universal.hom (F-map-cocone F K′)     ≡⟨ ap hom (F∘L-colim.¡-unique (F-map-cocone-hom F (L-universal K′))) ⟩
+        hom (F-map-cocone-hom F (L-universal K′)) ≡⟨⟩
+        F .F₁ (L-universal.hom K′) ∎
+
+      invert : is-invertible D (F .F₁ (Colimit-universal Dia L-colim K))
+      invert .is-invertible.inv = F∘K-universal.hom F∘L
+      invert .is-invertible.inverses .Inverses.invl =
+        F .F₁ (L-universal.hom K) D.∘ F∘K-universal.hom F∘L ≡˘⟨ ap (D._∘ F∘K-universal.hom F∘L) F-preserves-universal ⟩
+        F∘L-universal.hom F∘K D.∘ F∘K-universal.hom F∘L     ≡⟨⟩
+        hom (F∘L-universal F∘K Cocones.∘ F∘K-universal F∘L) ≡⟨ ap hom (F∘K-colim.¡-unique₂ (F∘L-universal F∘K Cocones.∘ F∘K-universal F∘L) Cocones.id) ⟩
+        D.id ∎
+      invert .is-invertible.inverses .Inverses.invr =
+        F∘K-universal.hom F∘L D.∘ F .F₁ (L-universal.hom K) ≡˘⟨ ap (F∘K-universal.hom F∘L D.∘_) F-preserves-universal ⟩
+        F∘K-universal.hom F∘L D.∘ F∘L-universal.hom F∘K     ≡⟨⟩
+        hom (F∘K-universal F∘L Cocones.∘ F∘L-universal F∘K) ≡⟨ ap hom (F∘L-colim.¡-unique₂ (F∘K-universal F∘L Cocones.∘ F∘L-universal F∘K) Cocones.id) ⟩
+        D.id ∎
+```