introduce total categories (#535)

I wanted to introduce total categories (see #489) and some of their
properties, in particular their adjoint functor theorem (that any
cocontinuous functor from a total category has a right adjoint).

This turned out to be really hard, and I didn't finish it (but I'm still
working). In particular, adjoint functor theorems seem to be *all about*
size conditions, and these are a bit tricky when converting from
classical texts to the 1lab.

Instead, I explored a lot of concepts, dualized many more, and I thought
it'd be best to PR what I have before it gets any more bloated.

Notable (non-dual) additions are:
- ~wide pullbacks~
- free objects are colimits
- diagonal adjoints are (co)limits
- absolute kans are adjoints
- all presheaf epis are regular

---------

Co-authored-by: Amélia Liao <[email protected]>

Author: 4e554c4c

src/Cat/Base.lagda.md

@@ -401,6 +401,16 @@ Id .Functor.F-id    = refl
 Id .Functor.F-∘ f g = refl
 ```
 
+<!--
+```agda
+Id^op≡Id : ∀ {o ℓ} {C : Precategory o ℓ} → Functor.op (Id {C = C}) ≡ Id
+Id^op≡Id  i .Functor.F₀ z = z
+Id^op≡Id  i .Functor.F₁ f = f
+Id^op≡Id  i .Functor.F-id = refl
+Id^op≡Id  i .Functor.F-∘ f g = refl
+```
+-->
+
 # Natural transformations {defines="natural-transformation"}
 
 Another common theme in category theory is that roughly _every_ concept

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

@@ -537,7 +537,7 @@ module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory
   Colimit-is-prop cat = Lan-is-prop cat
 ```
 
-# Cocompleteness {defines="cocomplete-category"}
+# Cocompleteness {defines="cocomplete cocomplete-category"}
 
 A category is **cocomplete** if it admits colimits for diagrams of arbitrary shape.
 However, in the presence of excluded middle, if a category admits

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

@@ -0,0 +1,44 @@
+<!--
+```agda
+open import Cat.Diagram.Limit.Initial
+open import Cat.Diagram.Colimit.Base
+open import Cat.Diagram.Limit.Base
+open import Cat.Diagram.Terminal
+open import Cat.Diagram.Duals
+open import Cat.Morphism
+open import Cat.Prelude
+
+import Cat.Reasoning as Cat
+
+open make-is-colimit
+open Terminal
+```
+-->
+
+```agda
+module Cat.Diagram.Colimit.Terminal {o ℓ} {C : Precategory o ℓ} where
+```
+
+# Terminal objects as colimits
+
+This module provides a characterisation of [[terminal objects]] as
+[[*colimits*]] rather than as [[limits]]. Namely, while an terminal
+object is the limit of the empty diagram, it is the *co*limit of the
+identity functor, considered as a diagram.
+
+Proving this consists of reversing the arrows in the proof that
+[[initial objects are limits]].
+
+```agda
+Id-colimit→Terminal : Colimit (Id {C = C}) → Terminal C
+Id-colimit→Terminal L = Coinitial→terminal
+  $ Id-limit→Initial
+  $ natural-iso→limit (path→iso Id^op≡Id)
+  $ Colimit→Co-limit L
+
+Terminal→Id-colimit : Terminal C → Colimit (Id {C = C})
+Terminal→Id-colimit terminal = Co-limit→Colimit
+  $ natural-iso→limit (path→iso (sym Id^op≡Id))
+  $ Initial→Id-limit
+  $ Terminal→Coinitial terminal
+```

src/Cat/Diagram/Coproduct/Copower.lagda.md

@@ -94,9 +94,8 @@ uniqueness properties of colimiting maps.
     coprods X (λ _ → A) .match λ i → coprods Y (λ _ → B) .ι (idx i) ∘ obj
   Copowering .F-id {X , A} = sym $
     coprods X (λ _ → A) .unique _ λ i → sym id-comm
-  Copowering .F-∘ {X , A} f g = sym $
-    coprods X (λ _ → A) .unique _ λ i →
-      pullr (coprods _ _ .commute) ∙ extendl (coprods _ _ .commute)
+  Copowering .F-∘ {X , A} f g = sym $ coprods X (λ _ → A) .unique _ λ i →
+    pullr (coprods _ _ .commute) ∙ extendl (coprods _ _ .commute)
 ```
 
 ```agda

src/Cat/Diagram/Coproduct/Indexed.lagda.md

@@ -24,7 +24,7 @@ there for motivation and exposition.
 
 <!--
 ```agda
-import Cat.Reasoning C as C
+open import Cat.Reasoning C as C
 private variable
   o' ℓ' : Level
   Idx : Type ℓ'

src/Cat/Diagram/Coseparator.lagda.md

@@ -0,0 +1,108 @@
+<!--
+```agda
+open import Cat.Diagram.Product.Indexed
+open import Cat.Diagram.Product.Power
+open import Cat.Functor.Properties
+open import Cat.Functor.Hom
+open import Cat.Prelude
+
+import Cat.Reasoning
+import Cat.Morphism
+```
+-->
+
+```agda
+module Cat.Diagram.Coseparator {o ℓ} (C : Precategory o ℓ) where
+```
+
+<!--
+```agda
+open Cat.Reasoning C
+open _=>_
+```
+-->
+# Coseparating objects {defines="coseparating-object cogenerating-object coseparator"}
+
+
+A coseparating (or cogenerating) object is formally the dual of a
+[[separator]].
+
+
+```agda
+is-coseparator : Ob → Type _
+is-coseparator c =
+  ∀ {x y} {f g : Hom x y}
+  → (∀ (m : Hom y c) → m ∘ f ≡ m ∘ g)
+  → f ≡ g
+```
+
+Equivalently, an object $S$ is a coseparator if the hom functor $\cC(-,S)$
+is [[faithful]].
+
+```agda
+coseparator→faithful : ∀ {s} → is-coseparator s → is-faithful (よ₀ C s)
+coseparator→faithful cos p = cos (happly p)
+
+faithful→coseparator : ∀ {s} → is-faithful (よ₀ C s) → is-coseparator s
+faithful→coseparator faithful p = faithful (ext p)
+```
+
+# Coseparating families {defines="coseparating-family"}
+
+Likewise, a coseparating family is dual to a [[separating family]].
+
+```agda
+is-coseparating-family : ∀ {ℓi} {Idx : Type ℓi} → (Idx → Ob) → Type _
+is-coseparating-family s =
+  ∀ {x y} {f g : Hom x y}
+  → (∀ {i} (mᵢ : Hom y (s i)) → mᵢ ∘ f  ≡ mᵢ ∘ g )
+  → f ≡ g
+```
+
+## Coseparators and powers
+
+Equivalently to approximating objects with [[separators and copowers]], we
+may approximate them with coseparators and powers.
+
+```agda
+module _ (powers : (I : Set ℓ) → has-products-indexed-by C ∣ I ∣) where
+  open Powers powers
+
+  coseparator→mono
+    : ∀ {s x} → is-coseparator s → is-monic (⋔!.tuple (Hom x s) s λ f → f)
+  coseparator→mono {s} {x} cosep f g p = cosep λ m →
+    m ∘ f                                   ≡⟨ pushl (sym $ ⋔!.commute _ _) ⟩
+    ⋔!.π _ _ m ∘ (⋔!.tuple _ _ λ f → f) ∘ f ≡⟨ refl⟩∘⟨ p ⟩
+    ⋔!.π _ _ m ∘ (⋔!.tuple _ _ λ f → f) ∘ g ≡⟨ pulll $ ⋔!.commute _ _ ⟩
+    m ∘ g                                   ∎
+
+  mono→coseparator
+    : ∀ {s} → (∀ {x} → is-monic (⋔!.tuple (Hom x s) s λ f → f)) → is-coseparator s
+  mono→coseparator monic {f = f} {g = g} p = monic f g $ ⋔!.unique₂ _ _ λ m →
+    assoc _ _ _ ∙ p _ ∙ sym (assoc _ _ _)
+
+  coseparating-family→mono
+    : ∀ (Idx : Set ℓ) (sᵢ : ∣ Idx ∣ → Ob)
+    → is-coseparating-family sᵢ
+    → ∀ {x} → is-monic (∏!.tuple (Σ[ i ∈ ∣ Idx ∣ ] Hom x (sᵢ i)) (sᵢ ⊙ fst) snd )
+  coseparating-family→mono Idx sᵢ cosep f g p = cosep λ {i} mᵢ →
+    mᵢ ∘ f                                     ≡⟨ pushl (sym $ ∏!.commute _ _) ⟩
+    ∏!.π _ _ (i , mᵢ) ∘ (∏!.tuple _ _ snd) ∘ f ≡⟨ refl⟩∘⟨ p ⟩
+    ∏!.π _ _ (i , mᵢ) ∘ (∏!.tuple _ _ snd) ∘ g ≡⟨ pulll $ ∏!.commute _ _ ⟩
+    mᵢ ∘ g                                     ∎
+
+  coseparating-family→make-mono
+    : ∀ (Idx : Set ℓ) (sᵢ : ∣ Idx ∣ → Ob)
+    → is-coseparating-family sᵢ
+    → ∀ {x} → x ↪ ∏!.ΠF (Σ[ i ∈ ∣ Idx ∣ ] Hom x (sᵢ i)) (sᵢ ⊙ fst)
+  coseparating-family→make-mono Idx sᵢ cosep = make-mono _ $
+    coseparating-family→mono Idx sᵢ cosep
+
+  mono→coseparating-family
+    : ∀ (Idx : Set ℓ)
+    → (sᵢ : ∣ Idx ∣ → Ob)
+    → (∀ {x} → is-monic (∏!.tuple (Σ[ i ∈ ∣ Idx ∣ ] Hom x (sᵢ i)) (sᵢ ⊙ fst) snd))
+    → is-coseparating-family sᵢ
+  mono→coseparating-family Idx sᵢ monic {f = f} {g = g} p = monic f g $
+    ∏!.unique₂ _ _ λ (i , mᵢ) → assoc _ _ _ ∙ p _ ∙ sym (assoc _ _ _)
+```

src/Cat/Diagram/Duals.lagda.md

@@ -1,18 +1,32 @@
 <!--
 ```agda
+open import Cat.Functor.Naturality.Reflection
+open import Cat.Diagram.Coproduct.Indexed
+open import Cat.Instances.Shape.Terminal
+open import Cat.Diagram.Product.Indexed
 open import Cat.Diagram.Colimit.Cocone
 open import Cat.Diagram.Colimit.Base
 open import Cat.Diagram.Coequaliser
+open import Cat.Functor.Kan.Duality
 open import Cat.Diagram.Limit.Base
 open import Cat.Diagram.Limit.Cone
+open import Cat.Functor.Kan.Unique
+open import Cat.Functor.Naturality
 open import Cat.Diagram.Coproduct
 open import Cat.Diagram.Equaliser
+open import Cat.Functor.Coherence
 open import Cat.Diagram.Pullback
 open import Cat.Diagram.Terminal
+open import Cat.Functor.Constant
+open import Cat.Functor.Kan.Base
 open import Cat.Diagram.Initial
 open import Cat.Diagram.Product
 open import Cat.Diagram.Pushout
 open import Cat.Prelude
+open import Cat.Base
+
+import Cat.Functor.Reasoning
+import Cat.Reasoning
 ```
 -->
 
@@ -22,8 +36,15 @@ module Cat.Diagram.Duals where
 
 <!--
 ```agda
+private
+  variable
+    o' ℓ' : Level
+    Idx : Type ℓ'
 module _ {o ℓ} {C : Precategory o ℓ} where
-  private module C = Precategory C
+  private
+    module C = Cat.Reasoning C
+    variable
+      S : C.Ob
 ```
 -->
 
@@ -35,7 +56,9 @@ particular, we have the following pairs of "redundant" definitions:
 
 [agda-categories]: https://arxiv.org/abs/2005.07059
 
-- [[Products]] and coproducts
+- [[Products]] and coproducts (and their [[indexed|indexed product]]
+versions)
+- [[Pullbacks]] and pushouts
 - [[Pullbacks]] and pushouts
 - [[Equalisers]] and coequalisers
 - [[Terminal objects]] and initial objects
@@ -71,6 +94,22 @@ $C\op$. We prove these correspondences here:
     where module iscop = is-coproduct iscop
 ```
 
+## Indexed Co/products
+
+```agda
+  is-indexed-co-product→is-indexed-coproduct
+    : ∀ {F : Idx → C.Ob} {ι : ∀ i → C.Hom (F i) S} → is-indexed-product (C ^op) F ι
+    → is-indexed-coproduct C F ι
+  is-indexed-co-product→is-indexed-coproduct prod =
+    record { is-indexed-product prod renaming (tuple to match) }
+
+  is-indexed-coproduct→is-indexed-co-product
+    : ∀ {F : Idx → C.Ob} {ι : ∀ i → C.Hom (F i) S} → is-indexed-coproduct C F ι
+    → is-indexed-product (C ^op) F ι
+  is-indexed-coproduct→is-indexed-co-product coprod =
+    record { is-indexed-coproduct coprod renaming (match to tuple) }
+```
+
 ## Co/equalisers
 
 ```agda
@@ -109,17 +148,33 @@ $C\op$. We prove these correspondences here:
     : ∀ {A} → is-terminal (C ^op) A → is-initial C A
   is-coterminal→is-initial x = x
 
+  is-terminal→is-coinitial
+    : ∀ {A} → is-terminal C A → is-initial (C ^op) A
+  is-terminal→is-coinitial x = x
+
   is-initial→is-coterminal
     : ∀ {A} → is-initial C A → is-terminal (C ^op) A
   is-initial→is-coterminal x = x
 
+  is-coinitial→is-terminal
+    : ∀ {A} → is-initial (C ^op) A → is-terminal C A
+  is-coinitial→is-terminal x = x
+
   Coterminal→Initial : Terminal (C ^op) → Initial C
   Coterminal→Initial term .bot = term .top
   Coterminal→Initial term .has⊥ = is-coterminal→is-initial (term .has⊤)
 
+  Terminal→Coinitial : Terminal C → Initial (C ^op)
+  Terminal→Coinitial term .bot = term .top
+  Terminal→Coinitial term .has⊥ = is-terminal→is-coinitial (term .has⊤)
+
   Initial→Coterminal : Initial C → Terminal (C ^op)
   Initial→Coterminal init .top = init .bot
   Initial→Coterminal init .has⊤ = is-initial→is-coterminal (init .has⊥)
+
+  Coinitial→terminal : Initial (C ^op) → Terminal C
+  Coinitial→terminal init .top = init .bot
+  Coinitial→terminal init .has⊤ = is-coinitial→is-terminal (init .has⊥)
 ```
 
 ## Pullback/pushout
@@ -157,6 +212,7 @@ $C\op$. We prove these correspondences here:
 ```agda
   module _ {o ℓ} {J : Precategory o ℓ} {F : Functor J C} where
     open Functor F renaming (op to F^op)
+    private module F = Cat.Functor.Reasoning F
 
     open Cocone-hom
     open Cone-hom
@@ -233,4 +289,15 @@ We could work around this, but it's easier to just do the proofs by hand.
       mc .universal eta p = lim.universal eta p
       mc .factors eta p = lim.factors eta p
       mc .unique eta p other q = lim.unique eta p other q
+
+module _ {o ℓ} {C : Precategory o ℓ} where
+  co-is-complete→is-cocomplete : is-complete o' ℓ' (C ^op) → is-cocomplete o' ℓ' C
+  co-is-complete→is-cocomplete co-complete F = Co-limit→Colimit $
+    co-complete $ Functor.op F
+
+  is-cocomplete→co-is-complete : is-cocomplete o' ℓ' (C ^op) → is-complete o' ℓ' C
+  is-cocomplete→co-is-complete cocomplete F = to-limit (to-is-limit ml) where
+    dual = Colimit→Co-limit $ cocomplete $ Functor.op F
+    ml : make-is-limit F $ Limit.apex dual
+    ml = record { Limit dual }
 ```

src/Cat/Diagram/Limit/Initial.lagda.md

@@ -15,7 +15,7 @@ open Initial
 module Cat.Diagram.Limit.Initial where
 ```
 
-# Initial objects as limits
+# Initial objects as limits {defines="initial-objects-are-limits"}
 
 This module provides a characterisation of [[initial objects]] as
 [[*limits*]], rather than as [[colimits]]. Namely, while an initial