Facts about Adjoints

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