Facts about Adjoints (#439)

# Description

The following PR proves a bunch of random facts about adjoints. The most
notable results are:
- A characterization of when a left/right adjoint is full or faithful
- A characterization of when a right adjoint is conservative
- All of Borceux 3.6

This requires a bit of machinery to set up: in particular, we need a bit
of theory about strong monos. In light of this,
I've factored out a lot of the proofs about strong epis into general
results about orthogonal maps. I've also done a
naming/API standardization pass on `StrongEpi`, and renamed it to
`Strong.Epi` to make `Strong.Mono` a bit more
well organized.

There are also a bunch of misc. reasoning combinator additions,
including `Cat.Natural.Reasoning`.

## Checklist

Before submitting a merge request, please check the items below:

- [x] I've read [the contributing
guidelines](https://github.com/plt-amy/1lab/blob/main/CONTRIBUTING.md).
- [x] The imports of new modules have been sorted with
`support/sort-imports.hs` (or `nix run --experimental-features
nix-command -f . sort-imports`).
- [x] All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content,
and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title
with `chore:`.

---------

Co-authored-by: Amélia Liao <me@amelia.how>

Author: TOTBWF

src/Borceux.lagda.md

@@ -11,6 +11,7 @@ open import Algebra.Group.Free hiding (_◆_)
 open import Algebra.Group.Ab
 
 open import Cat.Diagram.Coequaliser.RegularEpi
+open import Cat.Functor.Adjoint.Epireflective
 open import Cat.Functor.Adjoint.Representable
 open import Cat.Instances.Elements.Covariant renaming (∫ to ∫cov)
 open import Cat.Instances.StrictCat.Cohesive hiding (Disc)
@@ -58,14 +59,14 @@ open import Cat.Functor.Subcategory
 open import Cat.Instances.Delooping
 open import Cat.Instances.StrictCat
 open import Cat.Morphism.Orthogonal
+open import Cat.Morphism.Strong.Epi
 open import Cat.Bi.Instances.Spans
 open import Cat.Diagram.Idempotent
 open import Cat.Diagram.Limit.Base
 open import Cat.Diagram.Limit.Cone
 open import Cat.Functor.Hom.Yoneda
 open import Cat.Functor.Properties
 open import Cat.Instances.Discrete
-open import Cat.Morphism.StrongEpi
 open import Cat.Diagram.Equaliser
 open import Cat.Diagram.Separator
 open import Cat.Instances.Functor
@@ -382,7 +383,7 @@ _ = has-section+monic→invertible
 
 ## 2 Limits
 
-## 2.1 Products
+### 2.1 Products
 
 <!--
 ```agda
@@ -405,7 +406,7 @@ _ = is-indexed-product-assoc
 * Proposition 2.1.5: `Indexed-product-unique`{.Agda}
 * Proposition 2.1.6: `is-indexed-product-assoc`{.Agda}
 
-## 2.2 Coproducts
+### 2.2 Coproducts
 
 <!--
 ```agda
@@ -419,7 +420,7 @@ _ = is-indexed-coproduct-assoc
 * Proposition 2.2.2: `is-indexed-coproduct→iso`{.Agda}
 * Proposition 2.2.3: `is-indexed-coproduct-assoc`{.Agda}
 
-## 2.3 Initial and terminal objects
+### 2.3 Initial and terminal objects
 
 <!--
 ```agda
@@ -438,7 +439,7 @@ _ = Zero-group-is-zero
   * a. `Sets-initial`{.Agda}, `Sets-terminal`{.Agda}
   * b. 🚧 `Zero-group-is-zero`{.Agda}
 
-## 2.4 Equalizers, coequalizers
+### 2.4 Equalizers, coequalizers
 
 <!--
 ```agda
@@ -456,7 +457,7 @@ _ = equaliser+epi→invertible
 * Proposition 2.4.4: `id-is-equaliser`{.Agda}
 * Proposition 2.4.5: `equaliser+epi→invertible`{.Agda}
 
-## 2.5 Pullbacks, pushouts
+### 2.5 Pullbacks, pushouts
 
 <!--
 ```agda
@@ -709,6 +710,26 @@ _ = is-reflective
 
 ### 3.6 Epireflective subcategories
 
+<!--
+```agda
+_ = is-epireflective
+_ = epireflective+strong-mono→unit-invertible
+_ = factor+strong-mono-unit-invertible→epireflective
+_ = is-strong-epireflective
+_ = strong-epireflective+mono→unit-invertible
+_ = factor+mono-unit-invertible→strong-epireflective
+```
+-->
+
+* Definition 3.6.1: `is-epireflective`{.Agda}
+* Proposition 3.6.2:
+  * (1 ⇒ 2): `epireflective+strong-mono→unit-invertible`{.Agda}
+  * (2 ⇒ 1): `factor+strong-mono-unit-invertible→epireflective`{.Agda}
+* Definition 3.6.2: `is-strong-epireflective`{.Agda}
+* Proposition 3.6.4:
+  * (1 ⇒ 2): `strong-epireflective+mono→unit-invertible`{.Agda}
+  * (2 ⇒ 1): `factor+mono-unit-invertible→strong-epireflective`{.Agda}
+
 ### 3.7 Kan extensions
 
 <!--
@@ -765,9 +786,9 @@ _ = Karoubi-is-completion
 ```agda
 _ = is-regular-epi
 _ = is-strong-epi
-_ = strong-epi-compose
-_ = strong-epi-cancell
-_ = strong-epi+mono→is-invertible
+_ = strong-epi-∘
+_ = strong-epi-cancelr
+_ = strong-epi+mono→invertible
 _ = is-regular-epi→is-strong-epi
 _ = is-strong-epi→is-extremal-epi
 _ = equaliser-lifts→is-strong-epi
@@ -778,9 +799,9 @@ _ = is-extremal-epi→is-strong-epi
 * Definition 4.3.1: `is-regular-epi`{.Agda}
 * Definition 4.3.5: `is-strong-epi`{.Agda}
 * Proposition 4.3.6:
-  * 1. `strong-epi-compose`{.Agda}
-  * 2. `strong-epi-cancel-l`{.Agda}
-  * 3. `strong-epi-mono→is-invertible`{.Agda}
+  * 1. `strong-epi-∘`{.Agda}
+  * 2. `strong-epi-cancelr`{.Agda}
+  * 3. `strong-epi-mono→invertible`{.Agda}
   * 4. `is-regular-epi→is-strong-epi`{.Agda}
   * 5. `is-strong-epi→is-extremal-epi`{.Agda}
 * Proposition 4.3.7:

src/Cat/Bi/Instances/Relations.lagda.md

@@ -3,7 +3,7 @@
 {-# OPTIONS --lossy-unification #-}
 open import Cat.Diagram.Pullback.Properties
 open import Cat.Morphism.Factorisation
-open import Cat.Morphism.StrongEpi
+open import Cat.Morphism.Strong.Epi
 open import Cat.Instances.Functor
 open import Cat.Instances.Product
 open import Cat.Diagram.Pullback
@@ -168,7 +168,7 @@ point of view informed by parametricity, one might argue that this is
 not only the correct move, but the _only possible_ way of turning a map
 into a subobject.]
 
-[strong epimorphism]: Cat.Morphism.StrongEpi.html
+[strong epimorphism]: Cat.Morphism.Strong.Epi.html
 
 ```agda
   it : Hom (inter .apex) (a ⊗₀ c)

src/Cat/Diagram/Projective/Strong.lagda.md

@@ -16,8 +16,8 @@ open import Data.Set.Surjection
 open import Data.Dec
 
 import Cat.Diagram.Separator.Strong
+import Cat.Morphism.Strong.Epi
 import Cat.Diagram.Projective
-import Cat.Morphism.StrongEpi
 import Cat.Reasoning
 ```
 -->
@@ -31,7 +31,7 @@ module Cat.Diagram.Projective.Strong
 <!--
 ```agda
 open Cat.Diagram.Projective C
-open Cat.Morphism.StrongEpi C
+open Cat.Morphism.Strong.Epi C
 open Cat.Reasoning C
 ```
 -->

src/Cat/Diagram/Separator.lagda.md

@@ -27,7 +27,7 @@ open import Cat.Prelude
 
 open import Data.Dec.Base
 
-import Cat.Morphism.StrongEpi
+import Cat.Morphism.Strong.Epi
 import Cat.Reasoning
 ```
 -->
@@ -38,7 +38,7 @@ module Cat.Diagram.Separator {o ℓ} (C : Precategory o ℓ) where
 
 <!--
 ```agda
-open Cat.Morphism.StrongEpi C
+open Cat.Morphism.Strong.Epi C
 open Cat.Reasoning C
 open _=>_
 ```

src/Cat/Diagram/Separator/Regular.lagda.md

@@ -11,7 +11,7 @@ open import Cat.Diagram.Coequaliser
 open import Cat.Prelude
 
 import Cat.Diagram.Separator.Strong
-import Cat.Morphism.StrongEpi
+import Cat.Morphism.Strong.Epi
 import Cat.Diagram.Separator
 import Cat.Reasoning
 ```
@@ -26,7 +26,7 @@ module Cat.Diagram.Separator.Regular
 
 <!--
 ```agda
-open Cat.Morphism.StrongEpi C
+open Cat.Morphism.Strong.Epi C
 open Cat.Diagram.Separator.Strong C coprods
 open Cat.Diagram.Separator C
 open Cat.Reasoning C

src/Cat/Diagram/Separator/Strong.lagda.md

@@ -14,7 +14,7 @@ open import Cat.Functor.Joint
 open import Cat.Functor.Hom
 open import Cat.Prelude
 
-import Cat.Morphism.StrongEpi
+import Cat.Morphism.Strong.Epi
 import Cat.Diagram.Separator
 import Cat.Reasoning
 ```
@@ -29,7 +29,7 @@ module Cat.Diagram.Separator.Strong
 
 <!--
 ```agda
-open Cat.Morphism.StrongEpi C
+open Cat.Morphism.Strong.Epi C
 open Cat.Diagram.Separator C
 open Cat.Reasoning C
 open Copowers coprods
@@ -192,9 +192,9 @@ by showing that it is both a strong epi and a monomorphism.
 
 ```agda
 strong-separator→conservative {s = s} strong {A = a} {B = b} {f = f} f∘-inv =
-  strong-epi+mono→is-invertible
-    f-mono
+  strong-epi+mono→invertible
     f-strong-epi
+    f-mono
   where
     module f∘- = Equiv (f ∘_ , is-invertible→is-equiv f∘-inv)
 ```
@@ -238,7 +238,7 @@ immediately see that $f$ is a strong epi.
 ```agda
     f-strong-epi : is-strong-epi f
     f-strong-epi =
-      strong-epi-cancell f f* $
+      strong-epi-cancelr f f* $
       subst is-strong-epi (sym f*-factors) strong
 ```
 
@@ -302,9 +302,9 @@ so we omit the details.
 </summary>
 ```agda
 strong-separating-family→jointly-conservative Idx sᵢ strong {x = a} {y = b} {f = f} f∘ᵢ-inv =
-  strong-epi+mono→is-invertible
-    f-mono
+  strong-epi+mono→invertible
     f-strong-epi
+    f-mono
   where
     module f∘- {i : ∣ Idx ∣} = Equiv (_ , is-invertible→is-equiv (f∘ᵢ-inv i))
 
@@ -325,7 +325,7 @@ strong-separating-family→jointly-conservative Idx sᵢ strong {x = a} {y = b}
 
     f-strong-epi : is-strong-epi f
     f-strong-epi =
-      strong-epi-cancell f f* $
+      strong-epi-cancelr f f* $
       subst is-strong-epi (sym f*-factors) strong
 
 jointly-conservative→extremal-separating-family Idx sᵢ lex f∘-conservative m f p =

src/Cat/Functor/Adjoint.lagda.md

@@ -15,6 +15,7 @@ open import Cat.Functor.Base
 open import Cat.Prelude
 
 import Cat.Functor.Reasoning as Func
+import Cat.Natural.Reasoning
 import Cat.Reasoning
 ```
 -->
@@ -78,8 +79,8 @@ record _⊣_ (L : Functor C D) (R : Functor D C) : Type (adj-level C D) where
     unit   : Id => (R F∘ L)
     counit : (L F∘ R) => Id
 
-  module unit = _=>_ unit
-  module counit = _=>_ counit renaming (η to ε)
+  module unit = Cat.Natural.Reasoning unit
+  module counit = Cat.Natural.Reasoning counit renaming (η to ε)
 
   open unit using (η) public
   open counit using (ε) public
@@ -165,7 +166,7 @@ module _
 ```
 -->
 
-## Adjuncts {defines=adjuncts}
+## Adjuncts {defines="adjunct left-adjunct right-adjunct"}
 
 Another view on adjunctions, one which is productive when thinking about
 adjoint *endo*functors $L \dashv R$, is the concept of _adjuncts_. Any