diff --git a/src/Cat/Diagram/Coequaliser/Split.lagda.md b/src/Cat/Diagram/Coequaliser/Split.lagda.md
new file mode 100644
index 000000000..ee0dc0506
--- /dev/null
+++ b/src/Cat/Diagram/Coequaliser/Split.lagda.md
@@ -0,0 +1,203 @@
+```agda
+open import Cat.Prelude
+
+module Cat.Diagram.Coequaliser.Split {o ℓ} (C : Precategory o ℓ) where
+open import Cat.Diagram.Coequaliser C
+```
+
+<!--
+```agda
+open import Cat.Reasoning C
+private variable
+  A B E : Ob
+  f g h e s t : Hom A B
+```
+-->
+
+# Split Coequalizers
+
+Split Coequalizers are one of those definitions that seem utterly opaque when first
+presented, but are actually quite natural when viewed through the correct lens.
+With this in mind, we are going to provide the motivation _first_, and then
+define the general construct.
+
+To start, let $R \subseteq B \times B$ be some equivalence relation. A natural thing
+to consider is the quotient $B/R$, which gives us the following diagram:
+~~~{.quiver}
+\[\begin{tikzcd}
+	R & {B \times B} & B & {B/R}
+	\arrow[hook, from=1-1, to=1-2]
+	\arrow["{p_1}", shift left=2, from=1-2, to=1-3]
+	\arrow["{p_2}"', shift right=2, from=1-2, to=1-3]
+	\arrow["q", from=1-3, to=1-4]
+\end{tikzcd}\]
+~~~
+
+Now, when one has a quotient, it's useful to have a means of picking representatives
+for each equivalence class. This is essentially what normalization algorithms do,
+which we can both agree are very useful indeed. This ends up defining a map
+$s : B/R \to B$ that is a section of $q$ (i.e: $q \circ s = id$).
+
+This gives us the following diagram (We've omited the injection of $R$ into
+$B \times B$ for clarity).
+~~~{.quiver}
+\[\begin{tikzcd}
+	R & B & {B/R}
+	\arrow["q", shift left=2, from=1-2, to=1-3]
+	\arrow["s", shift left=2, from=1-3, to=1-2]
+	\arrow["{p_1}", shift left=2, from=1-1, to=1-2]
+	\arrow["{p_2}"', shift right=2, from=1-1, to=1-2]
+\end{tikzcd}\]
+~~~
+
+This lets us define yet another map $r : B \to R$, which will witness the fact that
+any $b : B$ is related to its representative $s(q(b))$. We can define this map explicitly
+as so:
+$$
+  r(b) = (b, s(q(b)))
+$$
+
+Now, how do we encode this diagramatically? To start, $p_1 \circ r = id$ by the
+$\beta$ law for products. Furthermore, $p_2 \circ r = s \circ q$, also by the
+$\beta$ law for products. This gives us a diagram that captures the essence of having
+a quotient by an equivalence relation, along with a means of picking representatives.
+
+~~~{.quiver}
+\[\begin{tikzcd}
+	R & B & {B/R}
+	\arrow["q", shift left=2, from=1-2, to=1-3]
+	\arrow["s", shift left=2, from=1-3, to=1-2]
+	\arrow["{p_1}", shift left=5, from=1-1, to=1-2]
+	\arrow["{p_2}"', shift right=5, from=1-1, to=1-2]
+	\arrow["r"', from=1-2, to=1-1]
+\end{tikzcd}\]
+~~~
+
+Such a situation is called a **split coequaliser**.
+
+```agda
+record is-split-coequaliser (f g : Hom A B) (e : Hom B E)
+                            (s : Hom E B) (t : Hom B A) : Type (o ⊔ ℓ) where
+  field
+    coequal : e ∘ f ≡ e ∘ g
+    rep-section : e ∘ s ≡ id
+    witness-section : f ∘ t ≡ id
+    commute : s ∘ e ≡ g ∘ t
+```
+
+Now, let's show that this thing actually deserves the name Coequaliser.
+```agda
+is-split-coequaliser→is-coequalizer :
+  is-split-coequaliser f g e s t → is-coequaliser f g e
+is-split-coequaliser→is-coequalizer
+  {f = f} {g = g} {e = e} {s = s} {t = t} split-coeq =
+  coequalizes
+  where
+    open is-split-coequaliser split-coeq
+```
+
+The proof here is mostly a diagram shuffle. We construct the universal
+map by going back along $s$, and then following $e'$ to our destination,
+like so:
+
+~~~{.quiver}
+\[\begin{tikzcd}
+	A && B && E \\
+	\\
+	&&&& X
+	\arrow["q", shift left=2, from=1-3, to=1-5]
+	\arrow["s", shift left=2, from=1-5, to=1-3]
+	\arrow["{p_1}", shift left=5, from=1-1, to=1-3]
+	\arrow["{p_2}"', shift right=5, from=1-1, to=1-3]
+	\arrow["r"', from=1-3, to=1-1]
+	\arrow["{e'}", from=1-3, to=3-5]
+	\arrow["{e' \circ s}", color={rgb,255:red,214;green,92;blue,92}, from=1-5, to=3-5]
+\end{tikzcd}\]
+~~~
+
+```agda
+    coequalizes : is-coequaliser f g e
+    coequalizes .is-coequaliser.coequal = coequal
+    coequalizes .is-coequaliser.coequalise {e′ = e′} _ = e′ ∘ s
+    coequalizes .is-coequaliser.universal {e′ = e′} {p = p} =
+      (e′ ∘ s) ∘ e ≡⟨ extendr commute ⟩
+      (e′ ∘ g) ∘ t ≡˘⟨ p ⟩∘⟨refl ⟩
+      (e′ ∘ f) ∘ t ≡⟨ cancelr witness-section ⟩
+      e′           ∎
+    coequalizes .is-coequaliser.unique {e′ = e′} {p} {colim′} q =
+      colim′         ≡⟨ intror rep-section ⟩
+      colim′ ∘ e ∘ s ≡⟨ pulll (sym q) ⟩
+      e′ ∘ s         ∎
+```
+
+Intuitively, we can think of this as constructing a map out of the quotient $B/R$
+from a map out of $B$ by picking a representative, and then applying the map out
+of $B$. Universality follows by the fact that the representative is related to
+the original element of $B$, and uniqueness by the fact that $s$ is a section.
+
+```agda
+record Split-coequaliser (f g : Hom A B) : Type (o ⊔ ℓ) where
+  field
+    {coapex}  : Ob
+    coeq      : Hom B coapex
+    rep       : Hom coapex B
+    witness   : Hom B A
+    has-is-split-coeq : is-split-coequaliser f g coeq rep witness
+
+  open is-split-coequaliser has-is-split-coeq public
+```
+
+## Split coequalizers and split epimorphisms
+
+Much like the situation with coequalizers, the coequalizing map of a
+split coequalizer is a split epimorphism. This follows directly from the fact
+that $s$ is a section of $e$.
+
+```agda
+is-split-coequaliser→is-split-epic
+  : is-split-coequaliser f g e s t → is-split-epic e
+is-split-coequaliser→is-split-epic {e = e} {s = s} split-coeq =
+  split-epic
+  where
+    open is-split-epic
+    open is-split-coequaliser split-coeq
+
+    split-epic : is-split-epic e
+    split-epic .split = s
+    split-epic .section = rep-section
+```
+
+Also of note, if $e$ is a split epimorphism with splitting $s$, then
+the following diagram is a split coequalizer.
+~~~{.quiver}
+\[\begin{tikzcd}
+	A & A & B
+	\arrow["id", shift left=3, from=1-1, to=1-2]
+	\arrow["{s \circ e}"', shift right=3, from=1-1, to=1-2]
+	\arrow["id"{description}, from=1-2, to=1-1]
+	\arrow["e", shift left=1, from=1-2, to=1-3]
+	\arrow["s", shift left=2, from=1-3, to=1-2]
+\end{tikzcd}\]
+~~~
+
+Using the intuition that split coequalizers are quotients of equivalence relations
+equipped with a choice of representatives, we can decode this diagram as constructing
+an equivalence relation on $A$ out of a section of $e$, where $a ~ b$ if and only
+if they get taken to the same cross section of $A$ via $s \circ e$.
+
+```agda
+is-split-epic→is-split-coequalizer
+  : s is-section-of e → is-split-coequaliser id (s ∘ e) e s id
+is-split-epic→is-split-coequalizer {s = s} {e = e} section = split-coeq
+  where
+    open is-split-coequaliser
+
+    split-coeq : is-split-coequaliser id (s ∘ e) e s id
+    split-coeq .coequal =
+      e ∘ id    ≡⟨ idr e ⟩
+      e         ≡⟨ insertl section ⟩
+      e ∘ s ∘ e ∎
+    split-coeq .rep-section = section
+    split-coeq .witness-section = id₂
+    split-coeq .commute = sym (idr (s ∘ e))
+```
diff --git a/src/Cat/Diagram/Coequaliser/Split/Properties.lagda.md b/src/Cat/Diagram/Coequaliser/Split/Properties.lagda.md
new file mode 100644
index 000000000..a7ec76349
--- /dev/null
+++ b/src/Cat/Diagram/Coequaliser/Split/Properties.lagda.md
@@ -0,0 +1,263 @@
+```agda
+open import Cat.Prelude
+
+open import Cat.Diagram.Limit.Finite
+
+import Cat.Diagram.Coequaliser.Split as SplitCoeq
+import Cat.Diagram.Pullback
+import Cat.Diagram.Congruence
+import Cat.Reasoning
+import Cat.Functor.Reasoning
+
+module Cat.Diagram.Coequaliser.Split.Properties where
+```
+
+# Properties of split coequalizers
+
+This module proves some general properties of [split coequalisers].
+
+[split coequalisers]: Cat.Diagram.Coequaliser.Split.html
+
+## Absoluteness
+
+The property of being a split coequaliser is a purely diagrammatic one, which has
+the lovely property of being preserved by _all_ functors. We call such colimits
+**absolute**.
+
+```agda
+module _ {o o′ ℓ ℓ′}
+         {C : Precategory o ℓ} {D : Precategory o′ ℓ′}
+         (F : Functor C D) where
+```
+<!--
+```agda
+  private
+    module C = Cat.Reasoning C
+    module D = Cat.Reasoning D
+    open Cat.Functor.Reasoning F
+    open SplitCoeq
+    variable
+      A B E : C.Ob 
+      f g e s t : C.Hom A B
+```
+-->
+
+The proof follows the fact that functors preserve diagrams, and reduces to a bit
+of symbol shuffling.
+
+```agda
+  is-split-coequaliser-absolute
+    : is-split-coequaliser C f g e s t
+    → is-split-coequaliser D (F₁ f) (F₁ g) (F₁ e) (F₁ s) (F₁ t)
+  is-split-coequaliser-absolute
+    {f = f} {g = g} {e = e} {s = s} {t = t} split-coeq = F-split-coeq
+    where
+      open is-split-coequaliser split-coeq
+
+      F-split-coeq : is-split-coequaliser D _ _ _ _ _
+      F-split-coeq .coequal = weave coequal
+      F-split-coeq .rep-section = annihilate rep-section
+      F-split-coeq .witness-section = annihilate witness-section
+      F-split-coeq .commute = weave commute
+```
+
+## Split Epis and Kernel Pairs
+
+We've already seen one way to construct a split coequalizer from a split epimorphism,
+via `is-split-epic→is-split-coequalizer`{.Agda}. However, this is not the only way!
+A somewhat more intuitive construction can be used which involves taking the kernel
+pair of some split epimorphism $e : B \to C$.
+
+```agda
+module _ {o ℓ} {C : Precategory o ℓ} where
+  open Cat.Reasoning C
+  open Cat.Diagram.Pullback C
+  open SplitCoeq C
+```
+
+First, some preliminaries. We can construct a morphism from $B$ into the kernel
+pair of $e$ by like so:
+
+~~~{.quiver}
+\[\begin{tikzcd}
+	B \\
+	& A & B \\
+	& B & C
+	\arrow[from=2-2, to=3-2]
+	\arrow[from=2-2, to=2-3]
+	\arrow["e"', from=2-3, to=3-3]
+	\arrow["e", from=3-2, to=3-3]
+	\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3]
+	\arrow[color={rgb,255:red,214;green,92;blue,92}, dashed, from=1-1, to=2-2]
+	\arrow["id"', curve={height=12pt}, from=1-1, to=3-2]
+	\arrow["{s \circ e}", curve={height=-12pt}, from=1-1, to=2-3]
+\end{tikzcd}\]
+~~~
+
+Using our intuition of split coequalisers as quotients with representatives,
+this map will pair up an element of $b$ with it's representative.
+
+```agda
+  private
+    represent
+      : ∀ {A B C} {p₁ p₂ : Hom A B} {e : Hom B C} {s : Hom C B}
+      → (kp : is-pullback p₁ e p₂ e)
+      → (section : s is-section-of e)
+      → Hom B A
+    represent {e = e} {s = s} kp section = limiting commutes where
+        open is-pullback kp
+        abstract
+          commutes : e ∘ id ≡ e ∘ s ∘ e
+          commutes = 
+            e ∘ id    ≡⟨ id-comm ⟩
+            id ∘ e    ≡⟨ pushl (sym section) ⟩
+            e ∘ s ∘ e ∎
+```
+
+This map lets us construct the following split coequaliser:
+~~~{.quiver}
+\[\begin{tikzcd}
+	A & B & C
+	\arrow["{p_1}", shift left=3, from=1-1, to=1-2]
+	\arrow["{p_2}"', shift right=3, from=1-1, to=1-2]
+	\arrow["r"{description}, from=1-2, to=1-1]
+	\arrow["e", shift left=2, from=1-2, to=1-3]
+	\arrow["s", shift left=2, from=1-3, to=1-2]
+\end{tikzcd}\]
+~~~
+
+All of the required commuting squares exist due to our clever choice
+of map into the kernel pair.
+
+```agda
+  is-split-epic→is-split-coequalizer-of-kernel-pair
+    : ∀ {A B C} {p₁ p₂ : Hom A B} {e : Hom B C} {s : Hom C B}
+    → (kp : is-pullback p₁ e p₂ e)
+    → (section : s is-section-of e)
+    → is-split-coequaliser p₁ p₂ e s (represent kp section)
+  is-split-epic→is-split-coequalizer-of-kernel-pair
+    {p₁ = p₁} {p₂ = p₂} {e = e} {s = s} kp section = split-coeq where
+      open is-pullback kp
+      open is-split-coequaliser
+
+      split-coeq : is-split-coequaliser _ _ _ _ _
+      split-coeq .coequal = square
+      split-coeq .rep-section = section
+      split-coeq .witness-section = p₁∘limiting
+      split-coeq .commute = sym p₂∘limiting
+```
+
+We also provide a bundled form of this lemma.
+
+```agda
+  split-epic→split-coequalizer-of-kernel-pair
+    : ∀ {B C} {e : Hom B C}
+    → (kp : Pullback e e)
+    → is-split-epic e
+    → Split-coequaliser (Pullback.p₁ kp) (Pullback.p₂ kp)
+  split-epic→split-coequalizer-of-kernel-pair
+    {e = e} kp split-epic = split-coeq where
+      open Pullback kp
+      open is-split-epic split-epic
+      open Split-coequaliser
+   
+      split-coeq : Split-coequaliser _ _
+      split-coeq .coapex = _
+      split-coeq .coeq = e
+      split-coeq .rep = split
+      split-coeq .witness = represent has-is-pb section
+      split-coeq .has-is-split-coeq =
+        is-split-epic→is-split-coequalizer-of-kernel-pair has-is-pb section
+```
+
+
+## Congruences and Quotients
+
+When motivating split coequalisers, we discussed how they arise naturally from
+quotients equipped with a choice of representatives of equivalence classes.
+Let's go the other direction, and show that split coequalizers induce [quotients].
+The rough idea of the construction is that we can construct an idempotent $A \to A$
+that takes every $a : A$ to it's canonical representative, and then to take
+the kernel pair of that morphism to construct a congruence.
+
+[quotients]: Cat.Diagram.Congruence.html#quotient-objects
+[kernel pair]: Cat.Diagram.Congruence.html#quotient-objects
+
+```agda
+module _ {o ℓ}
+         {C : Precategory o ℓ}
+         (fc : Finitely-complete C)
+         where
+```
+
+<!--
+```agda
+  open Cat.Reasoning C
+  open Cat.Diagram.Pullback C
+  open Cat.Diagram.Congruence fc
+  open SplitCoeq C
+  open Finitely-complete fc
+  open Cart
+```
+-->
+
+```agda
+  split-coequaliser→is-quotient-of 
+    : ∀ {R A A/R} {i r : Hom R A} {q : Hom A A/R}
+        {rep : Hom A/R A} {witness : Hom A R}
+      → is-split-coequaliser i r q rep witness
+      → is-quotient-of (Kernel-pair (r ∘ witness)) q
+  split-coequaliser→is-quotient-of
+    {i = i} {r = r} {q = q} {rep = rep} {witness = witness} split-coeq =
+    is-split-coequaliser→is-coequalizer quotient-split
+      where
+        open is-split-coequaliser split-coeq
+        module R′ = Pullback (pullbacks (r ∘ witness) (r ∘ witness))
+```
+
+We will need to do a bit of symbol munging to get the right split coequaliser here,
+as the morphisms don't precisely line up due to the fact that we want to be working
+with the kernel pair, not `R`.
+
+However, we first prove a small helper lemma. If we use the intuition of `R`
+as a set of pairs of elements and their canonical representatives, then this
+lemma states that the representative of $a : A$ is the same as the representative _of_
+the representative of $a$.
+
+```agda
+        same-rep : (r ∘ witness) ∘ i ≡ (r ∘ witness) ∘ r
+        same-rep =
+          (r ∘ witness) ∘ i ≡˘⟨ commute ⟩∘⟨refl ⟩
+          (rep ∘ q) ∘ i     ≡⟨ extendr coequal ⟩
+          (rep ∘ q) ∘ r     ≡⟨ commute ⟩∘⟨refl ⟩
+          (r ∘ witness) ∘ r ∎
+```
+
+Now, onto the meat of the proof. This is mostly mindless algebraic manipulation
+to get things to line up correctly.
+
+```agda
+        quotient-split :
+          is-split-coequaliser
+            (π₁ ∘ ⟨ R′.p₁ , R′.p₂ ⟩) (π₂ ∘ ⟨ R′.p₁ , R′.p₂ ⟩)
+            q rep (R′.limiting same-rep ∘ witness)
+        quotient-split .coequal = retract→is-monic rep-section _ _ $
+          rep ∘ q ∘ π₁ ∘ ⟨ R′.p₁ , R′.p₂ ⟩ ≡⟨ refl⟩∘⟨ refl⟩∘⟨ π₁∘⟨⟩ ⟩
+          rep ∘ q ∘ R′.p₁                  ≡⟨ pulll commute ⟩
+          (r ∘ witness) ∘ R′.p₁            ≡⟨ R′.square ⟩
+          (r ∘ witness) ∘ R′.p₂            ≡⟨ pushl (sym commute) ⟩
+          rep ∘ q ∘ R′.p₂                  ≡˘⟨ refl⟩∘⟨ refl⟩∘⟨ π₂∘⟨⟩ ⟩
+          rep ∘ q ∘ π₂ ∘ ⟨ R′.p₁ , R′.p₂ ⟩ ∎
+        quotient-split .rep-section = rep-section
+        quotient-split .witness-section =
+          (π₁ ∘ ⟨ R′.p₁ , R′.p₂ ⟩) ∘ R′.limiting same-rep ∘ witness ≡⟨ π₁∘⟨⟩ ⟩∘⟨refl ⟩
+          R′.p₁ ∘ R′.limiting same-rep ∘ witness                    ≡⟨ pulll R′.p₁∘limiting ⟩
+          i ∘ witness                                               ≡⟨ witness-section ⟩
+          id ∎
+        quotient-split .commute =
+          rep ∘ q                                                   ≡⟨ commute ⟩
+          r ∘ witness                                               ≡⟨ pushl (sym R′.p₂∘limiting) ⟩
+          R′.p₂ ∘ R′.limiting same-rep ∘ witness                    ≡˘⟨ π₂∘⟨⟩ ⟩∘⟨refl ⟩
+          (π₂ ∘ ⟨ R′.p₁ , R′.p₂ ⟩) ∘ R′.limiting same-rep ∘ witness ∎
+```
+
diff --git a/src/Cat/Diagram/Colimit/Base.lagda.md b/src/Cat/Diagram/Colimit/Base.lagda.md
index cae078b9e..3d485ec46 100644
--- a/src/Cat/Diagram/Colimit/Base.lagda.md
+++ b/src/Cat/Diagram/Colimit/Base.lagda.md
@@ -3,7 +3,7 @@ open import Cat.Diagram.Initial
 open import Cat.Prelude
 
 import Cat.Functor.Reasoning as Func
-import Cat.Morphism
+import Cat.Reasoning
 
 module Cat.Diagram.Colimit.Base where
 ```
@@ -64,8 +64,8 @@ We this pair of category and functor a _diagram_ in $C$.
 ```agda
 module _ {J : Precategory o ℓ} {C : Precategory o′ ℓ′} (F : Functor J C) where
   private
-    import Cat.Reasoning J as J
-    import Cat.Reasoning C as C
+    module J = Cat.Reasoning J
+    module C = Cat.Reasoning C
     module F = Functor F
 
   record Cocone : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
@@ -198,8 +198,15 @@ 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})
 ```
 
 
@@ -238,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.
@@ -247,6 +270,74 @@ 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
+cocone "downstairs" implies that we must have a limiting cocone "upstairs".
+
+More concretely, if the image of a cocone $F \circ K$ in $\ca{D}$
+is a colimiting cocone, then $K$ must have already been a
+colimiting cocone in $\ca{C}$
+
+```agda
+  Reflects-colimit : Cocone Dia → Type _
+  Reflects-colimit K = is-colimit (F F∘ Dia) (F-map-cocone K) → is-colimit Dia K
+```
+
+# Uniqueness
+
+<!--
+```agda
+module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory o₂ h₂}
+         (F : Functor J C)
+       where
+  private
+    module J = Precategory J
+    module C = Cat.Reasoning C
+    module F = Functor F
+    module Cocones = Cat.Reasoning (Cocones F)
+```
+-->
+
+If the universal map $L \to K$ between coapexes of some colimit is
+invertible, that means that $K$ is also a colimiting cocone.
+
+```agda
+  coapex-iso→is-colimit
+    : (K : Cocone F)
+      (L : Colimit F)
+      → C.is-invertible (Colimit-universal F L K)
+      → is-colimit F K
+  coapex-iso→is-colimit K L invert K′ = colimits where
+    module K = Cocone K
+    module K′ = Cocone K′
+    module L = Cocone (Initial.bot L)
+    module universal K = Cocone-hom (Initial.¡ L {K})
+    open C.is-invertible invert
+
+    colimits : is-contr (Cocones.Hom K K′)
+    colimits .centre .Cocone-hom.hom = universal.hom K′ C.∘ inv 
+    colimits .centre .Cocone-hom.commutes _ =
+      (universal.hom K′ C.∘ inv) C.∘ K.ψ _                       ≡˘⟨ ap ((universal.hom K′ C.∘ inv) C.∘_) (universal.commutes K _) ⟩
+      (universal.hom K′ C.∘ inv) C.∘ (universal.hom K C.∘ L.ψ _) ≡⟨ C.cancel-inner invr ⟩
+      universal.hom K′ C.∘ L.ψ _                                 ≡⟨ universal.commutes K′ _ ⟩
+      K′.ψ _                                                     ∎
+    colimits .paths f =
+      let module f = Cocone-hom f in
+      Cocone-hom-path F $ C.invertible→epic invert _ _ $
+      (universal.hom K′ C.∘ inv) C.∘ universal.hom K ≡⟨ C.cancelr invr ⟩
+      universal.hom K′                               ≡⟨ ap Cocone-hom.hom (Initial.¡-unique L (f Cocones.∘ Initial.¡ L)) ⟩
+      f.hom C.∘ universal.hom K                      ∎
+```
+
+
 ## Cocompleteness
 
 A category is **cocomplete** if admits for limits of arbitrary shape.
diff --git a/src/Cat/Diagram/Colimit/Coequaliser.lagda.md b/src/Cat/Diagram/Colimit/Coequaliser.lagda.md
new file mode 100644
index 000000000..3cfa3f048
--- /dev/null
+++ b/src/Cat/Diagram/Colimit/Coequaliser.lagda.md
@@ -0,0 +1,94 @@
+```agda
+open import Cat.Instances.Shape.Parallel
+
+open import Cat.Diagram.Colimit.Base
+open import Cat.Diagram.Coequaliser
+open import Cat.Instances.Functor
+open import Cat.Diagram.Initial
+open import Cat.Prelude
+
+open import Data.Bool
+
+module Cat.Diagram.Colimit.Coequaliser
+  {o ℓ} (Cat : Precategory o ℓ) where
+```
+
+<!--
+```agda
+open import Cat.Reasoning Cat
+open import Cat.Univalent Cat
+
+open is-coequaliser
+open Coequaliser
+open Initial
+open Cocone-hom
+open Functor
+open Cocone
+```
+-->
+
+We establish the correspondence between `Coequaliser`{.Agda} and the
+`Colimit`{.Agda} of a [parallel arrows] diagram.
+
+[parallel arrows]: Cat.Instances.Shape.Parallel.html
+
+```agda
+Fork→Cocone
+  : ∀ {E} (F : Functor ·⇉· Cat)
+  → (eq : Hom (F .F₀ true) E)
+  → eq ∘ F .F₁ {false} {true} false ≡ eq ∘ F .F₁ {false} {true} true
+  → Cocone F
+Fork→Cocone F eq p .coapex = _
+Fork→Cocone F eq p .ψ false = eq ∘ F .F₁ false
+Fork→Cocone F eq p .ψ true = eq
+Fork→Cocone F eq p .commutes {false} {false} tt = elimr (F .F-id)
+Fork→Cocone F eq p .commutes {false} {true} false = refl
+Fork→Cocone F eq p .commutes {false} {true} true = sym p
+Fork→Cocone F eq p .commutes {true} {true} tt = elimr (F .F-id)
+
+Coequaliser→Colimit
+  : ∀ {F : Functor ·⇉· Cat}
+  → Coequaliser Cat (F .F₁ false) (F .F₁ true)
+  → Colimit F
+Coequaliser→Colimit {F = F} coeq = colim where
+  module coeq = Coequaliser coeq
+  colim : Colimit _
+  colim .bot = Fork→Cocone F coeq.coeq coeq.coequal
+  colim .has⊥ K .centre .hom =
+    coeq.coequalise $ K .commutes {false} {true} false
+      ∙ sym (K .commutes true)
+  colim .has⊥ K .centre .commutes false =
+    pulll coeq.universal ∙ K .commutes {false} {true} false
+  colim .has⊥ K .centre .commutes true = coeq.universal
+  colim .has⊥ K .paths other = Cocone-hom-path _ (sym (coeq.unique p)) where
+    p : K .ψ true ≡ other .hom ∘ coeq.coeq
+    p = sym (other .commutes _)
+  
+Colimit→Coequaliser
+  : ∀ {F : Functor ·⇉· Cat}
+  → Colimit F
+  → Coequaliser Cat (F .F₁ false) (F .F₁ true)
+Colimit→Coequaliser {F = F} colim = coequ where
+  module colim = Initial colim
+
+  coequ : Coequaliser Cat _ _
+  coequ .coapex = _
+  coequ .coeq = colim.bot .ψ true
+  coequ .has-is-coeq .coequal =
+    colim.bot .commutes {false} {true} false
+    ∙ sym (colim.bot .commutes true)
+  coequ .has-is-coeq .coequalise p =
+    colim.has⊥ (Fork→Cocone _ _ p) .centre .hom
+  coequ .has-is-coeq .universal {p = p} =
+    colim.has⊥ (Fork→Cocone _ _ p) .centre .commutes true
+  coequ .has-is-coeq .unique {e′ = e′} {p = p} {colim = colim'} x =
+    sym (ap hom (colim.has⊥ (Fork→Cocone _ _ p) .paths other))
+    where
+      other : Cocone-hom _ _ _
+      other .hom = colim'
+      other .commutes false =
+        colim' ∘ colim .bot .ψ false               ≡⟨ pushr (sym $ colim.bot .commutes false) ⟩
+        (colim' ∘ colim.bot .ψ true) ∘ F .F₁ false ≡˘⟨ ap (_∘ F .F₁ false) x ⟩
+        e′ ∘ F .F₁ false ∎
+      other .commutes true = sym x
+```
diff --git a/src/Cat/Diagram/Limit/Finite.lagda.md b/src/Cat/Diagram/Limit/Finite.lagda.md
index 9fc0d2d82..9a0fb2535 100644
--- a/src/Cat/Diagram/Limit/Finite.lagda.md
+++ b/src/Cat/Diagram/Limit/Finite.lagda.md
@@ -72,8 +72,8 @@ to give a terminal object and binary products.
     Pb : ∀ {A B C} (f : Hom A C) (g : Hom B C) → Ob
     Pb f g = pullbacks f g .Pullback.apex
 
-    module Cart = Cartesian C products
-    open Cart using (_⊗_) public
+    module Cart = Cartesian C products hiding (_⊗_)
+    open Cartesian C products using (_⊗_) public
 
   open Finitely-complete
 ```
diff --git a/src/Cat/Diagram/Limit/Product.lagda.md b/src/Cat/Diagram/Limit/Product.lagda.md
index 20ce78923..80978f4bb 100644
--- a/src/Cat/Diagram/Limit/Product.lagda.md
+++ b/src/Cat/Diagram/Limit/Product.lagda.md
@@ -7,6 +7,7 @@ description: |
 ```agda
 open import Cat.Diagram.Limit.Base
 open import Cat.Instances.Discrete
+open import Cat.Instances.Shape.Pair
 open import Cat.Instances.Functor
 open import Cat.Diagram.Terminal
 open import Cat.Diagram.Product
@@ -14,13 +15,12 @@ open import Cat.Prelude
 
 open import Data.Bool
 
-module Cat.Diagram.Limit.Product {o h} (C : Precategory o h) where
+module Cat.Diagram.Limit.Product {o h} (Cat : Precategory o h) where
 ```
 
 <!--
 ```agda
-open import Cat.Reasoning C
-open import Cat.Univalent C
+open import Cat.Reasoning Cat
 
 -- Yikes:
 open is-product
@@ -34,89 +34,60 @@ open Cone
 
 # Products are limits
 
-We establish the correspondence between binary products $A \times B$ and
-limits over the functor out of $\id{Disc}(\{0,1\})$ which maps $0$
-to $A$ and $1$ to $B$. We begin by defining the functor (reusing
-existing infrastructure):
+We establishe the correspondence between binary products $A \times B$
+and the `Limit`{.Agda} of a diagram of the [two object category].
 
-```agda
-2-object-diagram : ∀ {iss} → Ob → Ob → Functor (Disc′ (Bool , iss)) C
-2-object-diagram A B = Disc-diagram Discrete-Bool λ where
-  false → A
-  true  → B
-```
-
-With that out of the way, we can establish the claimed equivalence. We
-start by showing that any pair of morphisms $A \ot Q \to B$ defines a
-cone over the discrete diagram consisting of $A$ and $B$. This is
-essentially by _definition_ of what it means to be a cone in this case,
-but they're arranged in very different ways:
+[two object category]: Cat.Instances.Shape.Pair.html
 
 ```agda
 Pair→Cone
-  : ∀ {iss} {Q A B} → Hom Q A → Hom Q B
-  → Cone (2-object-diagram {iss = iss} A B)
-Pair→Cone {Q = Q} _ _ .apex  = Q
-Pair→Cone p1 p2 .ψ false = p1
-Pair→Cone p1 p2 .ψ true  = p2
-Pair→Cone _ _ .commutes {false} {false} f = ap (_∘ _) (transport-refl _) ∙ idl _
-Pair→Cone _ _ .commutes {false} {true}  f = absurd (true≠false (sym f))
-Pair→Cone _ _ .commutes {true}  {false} f = absurd (true≠false f)
-Pair→Cone _ _ .commutes {true}  {true}  f = ap (_∘ _) (transport-refl _) ∙ idl _
+  : ∀ {X} → (F : Functor ·· Cat)
+  → Hom X (F .F₀ false) → Hom X (F .F₀ true)
+  → Cone F
+Pair→Cone F p1 p2 .apex = _
+Pair→Cone F p1 p2 .ψ false = p1
+Pair→Cone F p1 p2 .ψ true = p2
+Pair→Cone F p1 p2 .commutes {false} {false} tt = eliml (F .F-id)
+Pair→Cone F p1 p2 .commutes {true} {true} tt = eliml (F .F-id)
 ```
 
 The two-way correspondence between products and terminal cones is then
 simple enough to establish by appropriately shuffling the data.
 
 ```agda
-Prod→Lim : ∀ {iss} {A B} → Product C A B → Limit (2-object-diagram {iss = iss} A B)
-Prod→Lim prod .top = Pair→Cone (prod .π₁) (prod .π₂)
-Prod→Lim prod .has⊤ x .centre .hom = prod .⟨_,_⟩ (x .ψ false) (x .ψ true)
-Prod→Lim prod .has⊤ x .centre .commutes false = prod .π₁∘factor
-Prod→Lim prod .has⊤ x .centre .commutes true  = prod .π₂∘factor
-Prod→Lim prod .has⊤ x .paths y = Cone-hom-path (2-object-diagram _ _)
-  (sym (prod .unique (y .hom) (y .commutes _) (y .commutes _)))
-
-Lim→Prod : ∀ {iss} {A B} → Limit (2-object-diagram {iss = iss} A B) → Product C A B
-Lim→Prod x .apex = x .top .apex
-Lim→Prod x .π₁   = x .top .ψ false
-Lim→Prod x .π₂   = x .top .ψ true
-Lim→Prod x .has-is-product .⟨_,_⟩ p1 p2 = x .has⊤ (Pair→Cone p1 p2) .centre .hom
-Lim→Prod x .has-is-product .π₁∘factor = x .has⊤ (Pair→Cone _ _) .centre .commutes _
-Lim→Prod x .has-is-product .π₂∘factor = x .has⊤ (Pair→Cone _ _) .centre .commutes _
-Lim→Prod x .has-is-product .unique f p q =
-  sym (ap hom (x .has⊤ (Pair→Cone _ _) .paths other))
-  where
-    other : Cone-hom (2-object-diagram _ _) _ _
-    other .hom = f
-    other .commutes false = p
-    other .commutes true  = q
-```
-
-We note that _any_ functor $F : \id{Disc}(\{0,1\}) \to \ca{C}$ is
-canonically _equal_, not just naturally isomorphic, to the one we
-defined above.
-
-```agda
-canonical-functors
-  : ∀ {iss} (F : Functor (Disc′ (Bool , iss)) C)
-  → F ≡ 2-object-diagram (F₀ F false) (F₀ F true)
-canonical-functors {iss = iss} F = Functor-path p q where
-  p : ∀ x → _
-  p false = refl
-  p true  = refl
-
-  q : ∀ {x y} (f : x ≡ y) → _
-  q {false} {false} p =
-    F₁ F p            ≡⟨ ap (F₁ F) (iss _ _ _ _) ⟩
-    F₁ F refl         ≡⟨ F-id F ⟩
-    id                ≡˘⟨ transport-refl _ ⟩
-    transport refl id ∎
-  q {true} {true} p =
-    F₁ F p            ≡⟨ ap (F₁ F) (iss _ _ _ _) ⟩
-    F₁ F refl         ≡⟨ F-id F ⟩
-    id                ≡˘⟨ transport-refl _ ⟩
-    transport refl id ∎
-  q {false} {true} p = absurd (true≠false (sym p))
-  q {true} {false} p = absurd (true≠false p)
+Prod→Lim : {F : Functor ·· Cat} → Product Cat (F .F₀ false) (F .F₀ true) → Limit F
+Prod→Lim {F = F} prod = lim where
+  module prod = Product prod
+  lim : Limit _
+  lim .top = Pair→Cone F prod.π₁ prod.π₂
+  lim .has⊤ cone .centre .hom = prod.⟨ cone .ψ false , cone .ψ true ⟩
+  lim .has⊤ cone .centre .commutes false = prod.π₁∘factor
+  lim .has⊤ cone .centre .commutes true = prod.π₂∘factor
+  lim .has⊤ cone .paths other = Cone-hom-path F (sym (prod.unique _ p₁ p₂)) where
+    p₁ : prod.π₁ ∘ other .hom ≡ cone .ψ false
+    p₁ = other .commutes false
+
+    p₂ : prod.π₂ ∘ other .hom ≡ cone .ψ true
+    p₂ = other .commutes true
+
+Lim→Prod : {F : Functor ·· Cat} → Limit F → Product Cat (F .F₀ false) (F .F₀ true)
+Lim→Prod {F = F} lim = prod where
+  module lim = Terminal lim
+  prod : Product Cat _ _
+  prod .apex = lim.top .apex
+  prod .π₁ = lim.top .ψ false
+  prod .π₂ = lim.top .ψ true
+  prod .has-is-product .⟨_,_⟩ f g =
+    lim.has⊤ (Pair→Cone _ f g ) .centre .hom 
+  prod .has-is-product .π₁∘factor =
+    lim.has⊤ (Pair→Cone F _ _) .centre .commutes false
+  prod .has-is-product .π₂∘factor =
+    lim.has⊤ (Pair→Cone F _ _) .centre .commutes true
+  prod .has-is-product .unique f p q =
+    sym (ap hom (lim.has⊤ (Pair→Cone _ _ _) .paths other))
+    where
+      other : Cone-hom _ _ _
+      other .hom = _
+      other .commutes false = p
+      other .commutes true = q
 ```
diff --git a/src/Cat/Functor/Adjoint/Continuous.lagda.md b/src/Cat/Functor/Adjoint/Continuous.lagda.md
index 4cbac4c9a..8164128bd 100644
--- a/src/Cat/Functor/Adjoint/Continuous.lagda.md
+++ b/src/Cat/Functor/Adjoint/Continuous.lagda.md
@@ -154,6 +154,7 @@ of shape categories are entirely determined by the "introduction forms"
 `cospan→cospan-diagram`{.Agda} and `par-arrows→par-diagram`{.Agda}.
 
 ```agda
+  open import Cat.Instances.Shape.Pair
   open import Cat.Instances.Shape.Parallel
   open import Cat.Instances.Shape.Cospan
   open import Cat.Diagram.Limit.Equaliser
@@ -166,11 +167,8 @@ of shape categories are entirely determined by the "introduction forms"
   right-adjoint→product
     : ∀ {A B} → Product D A B → Product C (R.₀ A) (R.₀ B)
   right-adjoint→product {A = A} {B} prod =
-    Lim→Prod C (fixup (right-adjoint-limit (Prod→Lim D prod)))
-    where
-      fixup : Limit (R F∘ 2-object-diagram D {iss = Bool-is-set} A B)
-            → Limit (2-object-diagram C {iss = Bool-is-set} (R.₀ A) (R.₀ B))
-      fixup = subst Limit (canonical-functors _ _)
+    Lim→Prod C (right-adjoint-limit
+      (Prod→Lim D {F = 2-objects→pair-diagram A B} prod))
 
   right-adjoint→pullback
     : ∀ {A B c} {f : D.Hom A c} {g : D.Hom B c}
diff --git a/src/Cat/Functor/Conservative.lagda.md b/src/Cat/Functor/Conservative.lagda.md
index 7d8dfe969..ee9c2fd9e 100644
--- a/src/Cat/Functor/Conservative.lagda.md
+++ b/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,15 +48,17 @@ 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
-      $ subst (λ ϕ → is-invertible D ϕ) F-preserves-universal
-      $ Cone-invertible→apex-invertible (F F∘ Dia)
-      $ !-invertible (Cones (F F∘ Dia)) F∘L-lim K-lim
+    apex-iso→is-limit Dia K L-lim $ conservative invert
     where
       F∘L-lim : Limit (F F∘ Dia)
       F∘L-lim .Terminal.top = F-map-cone F (Terminal.top L-lim)
@@ -67,9 +73,93 @@ module _ {F : Functor C D} (conservative : is-conservative F) where
       open Cone-hom
 
       F-preserves-universal
-        : hom F∘L-lim.! ≡ F .F₁ (hom {x = K} L-lim.!)
+        : F∘L-lim.! .hom ≡ F .F₁ (L-lim.! {x = K} .hom)
       F-preserves-universal =
-        hom F∘L-lim.! ≡⟨ ap hom (F∘L-lim.!-unique (F-map-cone-hom F L-lim.!)) ⟩
-        hom (F-map-cone-hom F (Terminal.! L-lim)) ≡⟨⟩
-        F .F₁ (hom L-lim.!) ∎
+        F∘L-lim.! .hom                           ≡⟨ ap hom (F∘L-lim.!-unique (F-map-cone-hom F L-lim.!)) ⟩
+        F-map-cone-hom F (Terminal.! L-lim) .hom ≡⟨⟩
+        F .F₁ (L-lim.! .hom)                     ∎
+
+      open is-invertible
+      open Inverses
+      inverse = !-invertible (Cones (F F∘ Dia)) F∘L-lim K-lim
+
+      invert : D.is-invertible (F .F₁ (L-lim.! .hom))
+      invert .inv = inverse .inv .hom
+      invert .inverses .invl =
+        F .F₁ (L-lim.! .hom) D.∘ invert .inv ≡˘⟨ F-preserves-universal D.⟩∘⟨refl ⟩
+        F∘L-lim.! .hom D.∘ invert .inv       ≡⟨ ap hom (inverse .inverses .invl) ⟩
+        D.id                                 ∎
+      invert .inverses .invr =
+        invert .inv D.∘ F .F₁ (L-lim.! .hom) ≡˘⟨ D.refl⟩∘⟨ F-preserves-universal ⟩
+        invert .inv D.∘ F∘L-lim.! .hom       ≡⟨ ap hom (inverse .inverses .invr) ⟩
+        D.id                                 ∎
+```
+
+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 ∎
 ```
diff --git a/src/Cat/Instances/Shape/Pair.lagda.md b/src/Cat/Instances/Shape/Pair.lagda.md
new file mode 100644
index 000000000..883cba92f
--- /dev/null
+++ b/src/Cat/Instances/Shape/Pair.lagda.md
@@ -0,0 +1,71 @@
+```agda
+open import Cat.Prelude
+
+open import Data.Bool
+
+module Cat.Instances.Shape.Pair where
+```
+
+# The "pair of objects" category
+
+The pair of objects category is the category with 2 objects,
+and only identity morphisms. It is the shape of [product] and
+[coproduct] diagrams.
+
+[product]: Cat.Diagram.Product.html
+[coproduct]: Cat.Diagram.Coproduct.html
+
+```agda
+·· : Precategory lzero lzero
+·· = precat where
+  open Precategory
+  precat : Precategory _ _
+  precat .Ob = Bool
+
+  precat .Hom false false = ⊤
+  precat .Hom false true = ⊥
+  precat .Hom true false = ⊥
+  precat .Hom true true = ⊤
+```
+
+<!--
+````
+  precat .Hom-set false false = hlevel 2
+  precat .Hom-set false true = hlevel 2
+  precat .Hom-set true false = hlevel 2
+  precat .Hom-set true true = hlevel 2
+
+  precat .id {x = false} = tt
+  precat .id {x = true} = tt
+
+  precat ._∘_ {false} {false} {false} _ _ = tt
+  precat ._∘_ {true} {true} {true} _ _ = tt
+
+  precat .idr {false} {false} _ = refl
+  precat .idr {true} {true} _ = refl
+
+  precat .idl {false} {false} _ = refl
+  precat .idl {true} {true} _ = refl
+
+  precat .assoc {false} {false} {false} {false} _ _ _ = refl
+  precat .assoc {true} {true} {true} {true} _ _ _ = refl
+```
+-->
+
+```agda
+module _ {o ℓ} {C : Precategory o ℓ} where
+  open Precategory C
+  open Functor
+   
+  2-objects→pair-diagram : ∀ (a b : Ob) → Functor ·· C
+  2-objects→pair-diagram a b = funct where
+    funct : Functor _ _
+    funct .F₀ false = a
+    funct .F₀ true = b
+    funct .F₁ {false} {false} _ = id
+    funct .F₁ {true} {true} _ = id
+    funct .F-id {false} = refl
+    funct .F-id {true} = refl
+    funct .F-∘ {false} {false} {false} _ _ = sym (idl _)
+    funct .F-∘ {true} {true} {true} _ _ = sym (idl _)
+```
diff --git a/src/Cat/Morphism.lagda.md b/src/Cat/Morphism.lagda.md
index abbbed862..dc236ce58 100644
--- a/src/Cat/Morphism.lagda.md
+++ b/src/Cat/Morphism.lagda.md
@@ -277,3 +277,102 @@ invertible→epic {f = f} invert g h p =
     open is-invertible invert
 ```
 
+## Sections and Retractions
+
+Given 2 maps $e : A \to B$ and $s : B \to A$, we say that $s$ is a section of
+$e$ if $e \circ s = id$. The intuition behind the name is that $s$ we can think of
+$e$ as taking some sort of quotient, and $s$ as picking out representatives
+for each equivalence class formed by $e$.
+In other words, $s$ picks out a cross-*section*.
+
+```agda
+_is-section-of_ : (s : Hom b a) → (e : Hom a b) → Type _
+_is-section-of_ s e = e ∘ s ≡ id
+```
+
+Furthermore, we also that $e$ is a retraction of $s$ when $e \circ s = id$.
+The intuition here is that the act of picking representatives of equivalence
+classes induces an idempotent map $s \circ e : A \to A$, which *retracts* each
+element of $A$ to the representative of the equivalence class formed by $e$.
+
+```agda
+_is-retract-of_ : (e : Hom a b) → (s : Hom b a) → Type _
+_is-retract-of_ e s = e ∘ s ≡ id
+```
+
+It's worth showing that a retraction does indeed induce an idempotent morphism on
+$A$.
+
+```agda
+retract-idempotent : ∀ {e : Hom a b} {s : Hom b a}
+                     → e is-retract-of s → (s ∘ e) ∘ (s ∘ e) ≡ s ∘ e
+retract-idempotent {e = e} {s = s} retract =
+  (s ∘ e) ∘ s ∘ e ≡˘⟨ assoc s e (s ∘ e) ⟩
+  s ∘ (e ∘ s ∘ e) ≡⟨ ap (s ∘_) (assoc e s e) ⟩
+  s ∘ (e ∘ s) ∘ e ≡⟨ ap (λ ϕ → s ∘ ϕ ∘ e) retract ⟩
+  s ∘ id ∘ e      ≡⟨ ap (s ∘_) (idl e) ⟩
+  s ∘ e ∎
+```
+
+Earlier, I claimed that we ought to think of $e$ as taking some sort of quotient.
+This is made precise by the fact that if $e$ has some section $s$, then $e$ must
+be an epimorphism.
+
+```agda
+section→is-epic : ∀ {e : Hom a b} {s : Hom b a}
+                  → s is-section-of e → is-epic e
+section→is-epic {e = e} {s = s} section g h p =
+  g           ≡˘⟨ idr g ⟩
+  g ∘ id      ≡˘⟨ ap (g ∘_) section ⟩
+  g ∘ e ∘ s   ≡⟨ assoc g e s ⟩
+  (g ∘ e) ∘ s ≡⟨ ap (_∘ s) p ⟩
+  (h ∘ e) ∘ s ≡˘⟨ assoc h e s ⟩
+  h ∘ e ∘ s   ≡⟨ ap (h ∘_) section ⟩
+  h ∘ id      ≡⟨ idr h ⟩
+  h ∎
+```
+
+Dually, if $e$ is a retraction of $s$, then $s$ must be a monomorphism.
+```agda
+retract→is-monic : ∀ {e : Hom a b} {s : Hom b a}
+                  → e is-retract-of s → is-monic s
+retract→is-monic {e = e} {s = s} retract g h p =
+  g           ≡˘⟨ idl g ⟩
+  id ∘ g      ≡˘⟨ ap (_∘ g) retract ⟩
+  (e ∘ s) ∘ g ≡˘⟨ assoc e s g ⟩
+  e ∘ s ∘ g   ≡⟨ ap (e ∘_) p ⟩
+  e ∘ s ∘ h   ≡⟨ assoc e s h ⟩
+  (e ∘ s) ∘ h ≡⟨ ap (_∘ h) retract ⟩
+  id ∘ h      ≡⟨ idl h ⟩
+  h ∎
+```
+
+## Split Epi and Monomorphisms
+
+The fact that the existence of a section of $f$ implies that $f$ is epic gives rise
+to the notion of a split epimorphism. We can think of this
+as some sort of quotient equipped with a choice of representatives.
+
+```agda
+record is-split-epic (f : Hom a b) : Type (o ⊔ h) where
+  field
+    split : Hom b a
+    section : split is-section-of f
+
+is-split-epic→is-epic : is-split-epic f → is-epic f
+is-split-epic→is-epic split-epic = section→is-epic section
+  where
+    open is-split-epic split-epic
+```
+
+Again by duality, we also have the notion of a split monomorphism. We can think
+of these as some embedding along with some classifying map. Alternatively, we
+can view a split monomorphisms as some means of selecting normal forms, along
+with an evaluation map.
+
+```agda
+record is-split-monic (f : Hom a b) : Type (o ⊔ h) where
+  field
+    split : Hom b a
+    retract : split is-retract-of f
+```
diff --git a/src/Cat/Reasoning.lagda.md b/src/Cat/Reasoning.lagda.md
index 425a0e21a..8d8cb46c5 100644
--- a/src/Cat/Reasoning.lagda.md
+++ b/src/Cat/Reasoning.lagda.md
@@ -37,6 +37,9 @@ id-comm {f = f} = idr f ∙ sym (idl f)
 id-comm-sym : ∀ {a b} {f : Hom a b} → id ∘ f ≡ f ∘ id
 id-comm-sym {f = f} = idl f ∙ sym (idr f)
 
+id₂ : ∀ {a} → id ∘ id ≡ id {a}
+id₂ = idl id
+
 module _ (a≡id : a ≡ id) where
 
   eliml : a ∘ f ≡ f