Karoubi completion is an idempotent completion (#253)

In the sense that it is a completion that *is* idempotent (as well as a
completion that *splits* idempotents).

src/Cat/Diagram/Idempotent.lagda.md

@@ -56,6 +56,20 @@ is-split→is-idempotent {f = f} spl =
   where open is-split spl renaming (inject to s ; project to r)
 ```
 
+Identities are always trivially (split) idempotent:
+
+```agda
+id-is-idempotent : ∀ {A} → is-idempotent {A = A} id
+id-is-idempotent = idr _
+
+id-is-split : ∀ {A} → is-split {A = A} id
+id-is-split {A} .is-split.F = A
+id-is-split .is-split.project = id
+id-is-split .is-split.inject = id
+id-is-split .is-split.p∘i = idr _
+id-is-split .is-split.i∘p = idr _
+```
+
 It's not the case that idempotents are split in every category. Those
 where this is the case are called **idempotent-complete**. Every
 category can be embedded, by a [[fully faithful]] functor, into an

src/Cat/Functor/Equivalence.lagda.md

@@ -23,7 +23,7 @@ open _=>_ hiding (op)
 ```
 -->
 
-# Equivalences
+# Equivalences {defines="equivalence-of-categories"}
 
 A functor $F : \cC \to \cD$ is an **equivalence of categories**
 when it has a [[right adjoint]] $G : \cD \to \cD$, with the unit and

src/Cat/Instances/Karoubi.lagda.md

@@ -1,6 +1,8 @@
 <!--
 ```agda
+open import Cat.Functor.Equivalence
 open import Cat.Functor.Properties
+open import Cat.Morphism
 open import Cat.Prelude
 
 import Cat.Diagram.Idempotent as CI
@@ -84,10 +86,10 @@ which absorbs $\id$ on either side; But this is just $f$ again.
 
 ```agda
 Embed : Functor C Karoubi
-Embed .F₀ x = x , C.id , C.idr _
+Embed .F₀ x = x , C.id , id-is-idempotent
 Embed .F₁ f = f , C.idr _ , C.idl _
-Embed .F-id = KH≡ {ai = C.idl _} {bi = C.idl _} refl
-Embed .F-∘ f g = KH≡ {ai = C.idl _} {bi = C.idl _} refl
+Embed .F-id = KH≡ {ai = id-is-idempotent} {bi = id-is-idempotent} refl
+Embed .F-∘ f g = KH≡ {ai = id-is-idempotent} {bi = id-is-idempotent} refl
 ```
 
 An elementary argument shows that the morphism part of `Embed`{.Agda}
@@ -143,3 +145,24 @@ assumption!
 
 Hence $\~\cC$ is an idempotent-complete category which admits $C$ as
 a full subcategory.
+
+If $\cC$ was already idempotent-complete, then `Embed`{.Agda} is an
+[[equivalence of categories]] between $\cC$ and $~\cC$:
+
+```agda
+Karoubi-is-completion : is-idempotent-complete → is-equivalence Embed
+Karoubi-is-completion complete = ff+split-eso→is-equivalence Embed-is-fully-faithful eso where
+  eso : is-split-eso Embed
+  eso (c , e , ie) = c′ , same where
+    open is-split (complete e ie) renaming (F to c′; inject to i; project to p)
+    module Karoubi = Cat.Morphism Karoubi
+    open Inverses
+    same : (c′ , C.id , _) Karoubi.≅ (c , e , ie)
+    same .to = i , C.idr _ , C.rswizzle (sym i∘p) p∘i
+    same .from = p , C.lswizzle (sym i∘p) p∘i , C.idl _
+    same .inverses .invl = KH≡ {ai = ie} {bi = ie} i∘p
+    same .inverses .invr = KH≡ {ai = id-is-idempotent} {bi = id-is-idempotent} p∘i
+```
+
+This makes the Karoubi envelope an "idempotent completion" in two *different* technical
+senses^[it is a completion that *adds* splittings of idempotents, and a completion that *is* idempotent]!

src/Cat/Morphism.lagda.md

@@ -257,7 +257,7 @@ instance
 A morphism $r : A \to B$ is a retract of another morphism $s : B \to A$
 when $r \cdot s = id$. Note that this is the same equation involved
 in the definition of a section; retracts and sections always come in
-pairs. If sections solve a sort of "curration problem" where we are
+pairs. If sections solve a sort of "curation problem" where we are
 asked to pick out canonical representatives, then retracts solve a
 sort of "classification problem".
 

src/Cat/Reasoning.lagda.md

@@ -161,15 +161,21 @@ module _ (inv : h ∘ i ≡ id) where abstract
   deletel = pulll cancell
 ```
 
-We also have a combinator which combines expanding on the right with a
-cancellation on the left:
+We also have combinators which combine expanding on one side with a
+cancellation on the other side:
 
 ```agda
 lswizzle : g ≡ h ∘ i → f ∘ h ≡ id → f ∘ g ≡ i
 lswizzle {g = g} {h = h} {i = i} {f = f} p q =
   f ∘ g     ≡⟨ ap₂ _∘_ refl p ⟩
   f ∘ h ∘ i ≡⟨ cancell q ⟩
   i         ∎
+
+rswizzle : g ≡ i ∘ h → h ∘ f ≡ id → g ∘ f ≡ i
+rswizzle {g = g} {i = i} {h = h} {f = f} p q =
+  g ∘ f       ≡⟨ ap₂ _∘_ p refl ⟩
+  (i ∘ h) ∘ f ≡⟨ cancelr q ⟩
+  i           ∎
 ```
 
 ## Isomorphisms

support/web/template.html

@@ -125,7 +125,7 @@ <h3 class="Agda" style="margin-top: 0; margin-bottom: 0; white-space: pre;">
         <a href="all-pages.html">view all pages</a> <br />
         <a href="https://github.com/plt-amy/1lab/blob/$source$">link to source</a> <br />
         $if(authors)$
-        <hr /> <div class="author-list">Written by $authors$</div> <br />
+        <hr /> <div class="author-list">This page was written by $authors$</div> <br />
         $endif$
       </div>
     </div>