Adjoints in terms of representability (#280)

- finish the proof that representable iff terminal element, dualise
- R is a right adjoint iff Hom(d, R-) is representable ∀ d
- universal property of copowers
- R : C → Sets is a right adjoint iff representable (assuming C
copowered)

## 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`.
- [X] All new code blocks have "agda" as their language.

If a commit 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 with `chore:`
or include the word `NOAUTHOR` anywhere.

src/1Lab/HIT/Truncation.lagda.md

@@ -250,7 +250,9 @@ and $(b, y)$ in the image. We know, morally, that $x$ (respectively $y$) give us
 some $f^*(a) : A$ and $p : f(f^*a) = a$ (resp $q : f(f^*(b)) = b$) ---
 which would establish that $a \equiv b$, as we need, since we have $a =
 f(f^*(a)) = f(f^*(b)) = b$, where the middle equation is by constancy of
-$f$ --- but crucially, the
+$f$ --- but $p$ and $q$ are hidden under propositional truncations, so
+we crucially need to use the fact that $B$ is a set so that $a = b$ is a
+proposition.
 
 ```agda
 is-constant→image-is-prop bset f f-const (a , x) (b , y) =

src/1Lab/Type/Pi.lagda.md

@@ -196,5 +196,24 @@ funext-square
   → (∀ a → Square (p $ₚ a) (q $ₚ a) (s $ₚ a) (r $ₚ a))
   → Square p q s r
 funext-square p i j a = p a i j
+
+Π-⊤-eqv
+  : ∀ {ℓ ℓ'} {B : Lift ℓ ⊤ → Type ℓ'}
+  → (∀ a → B a) ≃ B _
+Π-⊤-eqv .fst b = b _
+Π-⊤-eqv .snd = is-iso→is-equiv λ where
+  .is-iso.inv b _ → b
+  .is-iso.rinv b → refl
+  .is-iso.linv b → refl
+
+Π-contr-eqv
+  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
+  → (c : is-contr A)
+  → (∀ a → B a) ≃ B (c .centre)
+Π-contr-eqv c .fst b = b (c .centre)
+Π-contr-eqv {B = B} c .snd = is-iso→is-equiv λ where
+  .is-iso.inv b a → subst B (c .paths a) b
+  .is-iso.rinv b → ap (λ e → subst B e b) (is-contr→is-set c _ _ _ _) ∙ transport-refl b
+  .is-iso.linv b → funext λ a → from-pathp (ap b (c .paths a))
 ```
 -->

src/Cat/Base.lagda.md

@@ -147,7 +147,7 @@ We can define the type of *all* morphisms in a precategory as the total space of
 ```
 -->
 
-## Opposites
+## Opposites {defines="opposite-category"}
 
 A common theme throughout precategory theory is that of _duality_: The dual
 of a categorical concept is same concept, with "all the arrows

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

@@ -652,9 +652,9 @@ is-cocontinuous oshape hshape {C = C} F =
   → preserves-colimit F Diagram
 ```
 
-## Cocompleteness
+# Cocompleteness
 
-A category is **cocomplete** if admits for limits of arbitrary shape.
+A category is **cocomplete** if it admits colimits for diagrams of arbitrary shape.
 However, in the presence of excluded middle, if a category admits
 coproducts indexed by its class of morphisms, then it is automatically
 [thin]. Since excluded middle is independent of type theory, we can not

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

@@ -3,8 +3,11 @@
 open import Cat.Diagram.Colimit.Coproduct
 open import Cat.Diagram.Coproduct.Indexed
 open import Cat.Diagram.Colimit.Base
+open import Cat.Functor.Naturality
 open import Cat.Instances.Discrete
 open import Cat.Instances.Product
+open import Cat.Instances.Sets
+open import Cat.Functor.Hom
 open import Cat.Prelude
 
 import Cat.Reasoning
@@ -15,7 +18,7 @@ import Cat.Reasoning
 module Cat.Diagram.Coproduct.Copower where
 ```
 
-# Copowers
+# Copowers {defines="copower copowered"}
 
 Let $\cC$ be a category admitting [$\kappa$-small] [indexed
 coproducts], for example a $\kappa$-[cocomplete] category. In the same
@@ -46,13 +49,12 @@ over $\Sets_\kappa$.
 
 <!--
 ```agda
-module
-  _ {o ℓ} {C : Precategory o ℓ}
-  (coprods : (S : Set ℓ) (F : ∣ S ∣ → Precategory.Ob C) → Indexed-coproduct C F)
+module Copowers
+  {o ℓ} {C : Precategory o ℓ}
+  (coprods : (S : Set ℓ) → has-coproducts-indexed-by C ∣ S ∣)
   where
 
   open Functor
-  open is-indexed-coproduct
   open Indexed-coproduct
   open Cat.Reasoning C
 ```
@@ -63,6 +65,20 @@ module
   X ⊗ A = coprods X (λ _ → A) .ΣF
 ```
 
+Copowers satisfy a universal property: $X \otimes A$ is a [[representing object]]
+for the functor that takes an object $B$ to the $X$th power of the set of morphisms
+from $A$ to $B$; in other words, we have a natural isomorphism
+$\hom_\cC(X \otimes A, -) \cong \hom_{\Sets}(X, \hom_\cC(A, -))$.
+
+```agda
+  copower-hom-iso
+    : ∀ {X A}
+    → Hom-from C (X ⊗ A) ≅ⁿ Hom-from (Sets ℓ) X F∘ Hom-from C A
+  copower-hom-iso {X} {A} = iso→isoⁿ
+    (λ _ → equiv→iso (hom-iso (coprods X (λ _ → A))))
+    (λ _ → ext λ _ _ → assoc _ _ _)
+```
+
 The action of the copowering functor is given by simultaneously changing
 the indexing along a function of sets $f : X \to Y$ and changing the
 underlying object by a morphism $g : A \to B$. This is functorial by the
@@ -82,6 +98,6 @@ uniqueness properties of colimiting maps.
 cocomplete→copowering
   : ∀ {o ℓ} {C : Precategory o ℓ}
   → is-cocomplete ℓ ℓ C → Functor (Sets ℓ ×ᶜ C) C
-cocomplete→copowering colim = Copowering λ S F →
+cocomplete→copowering colim = Copowers.Copowering λ S F →
   Colimit→IC _ (is-hlevel-suc 2 (S .is-tr)) F (colim _)
 ```

src/Cat/Diagram/Duals.lagda.md

@@ -97,14 +97,24 @@ is-coequaliser→is-co-equaliser coeq =
 ```agda
 import Cat.Diagram.Terminal (C ^op) as Coterm
 import Cat.Diagram.Initial C as Init
+open Coterm.Terminal
+open Init.Initial
 
-is-initial→is-coterminal
+is-coterminal→is-initial
   : ∀ {A} → Coterm.is-terminal A → Init.is-initial A
-is-initial→is-coterminal x = x
+is-coterminal→is-initial x = x
 
-is-coterminal→is-initial
+is-initial→is-coterminal
   : ∀ {A} → Init.is-initial A → Coterm.is-terminal A
-is-coterminal→is-initial x = x
+is-initial→is-coterminal x = x
+
+Coterminal→Initial : Coterm.Terminal → Init.Initial
+Coterminal→Initial term .bot = term .top
+Coterminal→Initial term .has⊥ = is-coterminal→is-initial (term .has⊤)
+
+Initial→Coterminal : Init.Initial → Coterm.Terminal
+Initial→Coterminal init .top = init .bot
+Initial→Coterminal init .has⊤ = is-initial→is-coterminal (init .has⊥)
 ```
 
 ## Pullback/pushout
@@ -147,16 +157,12 @@ open import Cat.Diagram.Colimit.Base
 open import Cat.Diagram.Colimit.Cocone
 open import Cat.Diagram.Limit.Base
 open import Cat.Diagram.Limit.Cone
-open import Cat.Diagram.Terminal
-open import Cat.Diagram.Initial
 
 module _ {o ℓ} {J : Precategory o ℓ} {F : Functor J C} where
   open Functor F renaming (op to F^op)
 
   open Cocone-hom
   open Cone-hom
-  open Terminal
-  open Initial
   open Cocone
   open Cone
 

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

@@ -237,7 +237,7 @@ triangles
 
 The rest of the data says that $\psi$ is the universal family of maps
 with this property: If $\eta_j : x \to Fj$ is another family of maps
-with the same commutativty property, then each $\eta_j$ factors through
+with the same commutativity property, then each $\eta_j$ factors through
 the apex by a single, _unique_ universal morphism:
 
 ```agda

src/Cat/Displayed/Bifibration.lagda.md

@@ -96,7 +96,7 @@ module _ (bifib : is-bifibration) where
     → cobase-change f ⊣ base-change f
   cobase-change⊣base-change {x} {y} f =
     hom-natural-iso→adjoints $
-      (opfibration→hom-iso opfibration f ni⁻¹) ni∘ fibration→hom-iso fibration f
+      (opfibration→hom-iso opfibration f ni⁻¹) ∘ni fibration→hom-iso fibration f
 ```
 
 In fact, if $\cE \liesover \cB$ is a cartesian fibration where every
@@ -127,7 +127,7 @@ module _ (fib : Cartesian-fibration) where
   left-adjoint-base-change→opfibration L adj =
     cartesian+weak-opfibration→opfibration fib $
     hom-iso→weak-opfibration L λ u →
-      fibration→hom-iso-from fib u ni∘ (adjunct-hom-iso-from (adj u) _ ni⁻¹)
+      fibration→hom-iso-from fib u ∘ni (adjunct-hom-iso-from (adj u) _ ni⁻¹)
 ```
 
 <!--

src/Cat/Functor/Adjoint.lagda.md

@@ -124,7 +124,7 @@ commutative diagrams:
 
 </div>
 
-# Universal morphisms
+# Universal morphisms {defines="universal-morphism"}
 
 <!--
 ```agda
@@ -516,10 +516,13 @@ universal arrows into $R$:
   L⊣R→universal-maps x .Initial.has⊥ = L⊣R→map-to-R-is-initial x
 ```
 
-<!-- TODO [Amy 2022-03-02]
-prove that we recover L by going L⊣R → universal maps → L⊣R. this is
-straightforward but I'm tired
--->
+By going from the adjunction to universal maps and then back to an adjunction, we
+recover $L$:
+
+```agda
+  L→universal-maps→L : universal-maps→L R L⊣R→universal-maps ≡ L
+  L→universal-maps→L = Functor-path (λ _ → refl) λ f → L.pushr refl ∙ D.eliml adj.zig
+```
 
 # Adjuncts {defines=adjuncts}
 

src/Cat/Functor/Adjoint/Hom.lagda.md

@@ -9,6 +9,7 @@ description: |
 open import Cat.Instances.Functor
 open import Cat.Instances.Product
 open import Cat.Functor.Adjoint
+open import Cat.Instances.Sets
 open import Cat.Functor.Hom
 open import Cat.Prelude
 
@@ -37,9 +38,9 @@ module _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
 ```
 -->
 
-# Adjoints as hom-isomorphisms
+# Adjoints as hom-isomorphisms {defines="adjoints-as-hom-isomorphisms"}
 
-Recall from the page on [[adjoint functors]] that an adjoint pair $L
+Recall from the page on [[adjoint functors|adjuncts]] that an adjoint pair $L
 \dashv R$ induces an isomorphism
 
 $$
@@ -48,7 +49,8 @@ $$
 
 of $\hom$-sets, sending each morphism to its left and right _adjuncts_,
 respectively. What that page does not mention is that any functors $L,
-R$ with such a correspondence --- as long as the isomorphism is natural
+R$ with such a correspondence --- as long as the isomorphism is
+[[natural|natural transformation]]
 --- actually generates an adjunction $L \dashv R$, with the unit and
 counit given by the adjuncts of each identity morphism.
 
@@ -60,7 +62,7 @@ f(g \circ x \circ Lh) = Rg \circ fx \circ h
 $$
 
 holds. While this may seem un-motivated, it's really a naturality square
-for a transformation between the functors $\hom_\cC(L-,-)$ and
+for a transformation between the bifunctors $\hom_\cC(L-,-)$ and
 $\hom_\cD(-,R-)$ whose data has been "unfolded" into elementary
 terms.
 
@@ -159,7 +161,6 @@ module _ {o ℓ o'} {C : Precategory o ℓ} {D : Precategory o' ℓ}
     module L = Func L
     module R = Func R
 
-
   hom-natural-iso→adjoints
     : (Hom[-,-] C F∘ (Functor.op L F× Id)) ≅ⁿ (Hom[-,-] D F∘ (Id F× R))
     → L ⊣ R
@@ -180,40 +181,22 @@ module _ {o ℓ o'} {C : Precategory o ℓ} {D : Precategory o' ℓ}
     module L = Func L
     module R = Func R
 
-  adjunct-hom-iso-from
-    : ∀ a → (Hom-from C (L.₀ a)) ≅ⁿ (Hom-from D a F∘ R)
-  adjunct-hom-iso-from a = to-natural-iso mi where
-    open make-natural-iso
+    hom-equiv : ∀ {a b} → C.Hom (L.₀ a) b ≃ D.Hom a (R.₀ b)
+    hom-equiv = _ , L-adjunct-is-equiv adj
 
-    mi : make-natural-iso (Hom-from C (L.₀ a)) (Hom-from D a F∘ R)
-    mi .eta x = L-adjunct adj
-    mi .inv x = R-adjunct adj
-    mi .eta∘inv _ = funext λ _ → L-R-adjunct adj _
-    mi .inv∘eta _ = funext λ _ → R-L-adjunct adj _
-    mi .natural _ _ f = funext λ g → sym (L-adjunct-naturalr adj f g)
+  adjunct-hom-iso-from
+    : ∀ a → Hom-from C (L.₀ a) ≅ⁿ Hom-from D a F∘ R
+  adjunct-hom-iso-from a = iso→isoⁿ (λ _ → equiv→iso hom-equiv)
+    λ f → funext λ g → sym (L-adjunct-naturalr adj _ _)
 
   adjunct-hom-iso-into
-    : ∀ b → (Hom-into C b F∘ Functor.op L) ≅ⁿ (Hom-into D (R.₀ b))
-  adjunct-hom-iso-into b = to-natural-iso mi where
-    open make-natural-iso
-
-    mi : make-natural-iso (Hom-into C b F∘ Functor.op L) (Hom-into D (R.₀ b))
-    mi .eta x = L-adjunct adj
-    mi .inv x = R-adjunct adj
-    mi .eta∘inv _ = funext λ _ → L-R-adjunct adj _
-    mi .inv∘eta _ = funext λ _ → R-L-adjunct adj _
-    mi .natural _ _ f = funext λ g → sym $ L-adjunct-naturall adj g f
+    : ∀ b → Hom-into C b F∘ Functor.op L ≅ⁿ Hom-into D (R.₀ b)
+  adjunct-hom-iso-into b = iso→isoⁿ (λ _ → equiv→iso hom-equiv)
+    λ f → funext λ g → sym (L-adjunct-naturall adj _ _)
 
   adjunct-hom-iso
-    : (Hom[-,-] C F∘ (Functor.op L F× Id)) ≅ⁿ (Hom[-,-] D F∘ (Id F× R))
-  adjunct-hom-iso = to-natural-iso mi where
-    open make-natural-iso
-
-    mi : make-natural-iso (Hom[-,-] C F∘ (Functor.op L F× Id)) (Hom[-,-] D F∘ (Id F× R))
-    mi .eta x = L-adjunct adj
-    mi .inv x = R-adjunct adj
-    mi .eta∘inv _ = funext λ _ → L-R-adjunct adj _
-    mi .inv∘eta _ = funext λ _ → R-L-adjunct adj _
-    mi .natural _ _ (f , h) = funext λ g → sym $ L-adjunct-natural₂ adj h f g
+    : Hom[-,-] C F∘ (Functor.op L F× Id) ≅ⁿ Hom[-,-] D F∘ (Id F× R)
+  adjunct-hom-iso = iso→isoⁿ (λ _ → equiv→iso hom-equiv)
+    λ (f , h) → funext λ g → sym (L-adjunct-natural₂ adj _ _ _)
 ```
 -->