diff --git a/src/1Lab/HIT/Truncation.lagda.md b/src/1Lab/HIT/Truncation.lagda.md
index 86d09b6e7..ad40b6dc9 100644
--- a/src/1Lab/HIT/Truncation.lagda.md
+++ b/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) =
diff --git a/src/1Lab/Type/Pi.lagda.md b/src/1Lab/Type/Pi.lagda.md
index 8538e7d61..6dcd9bdb6 100644
--- a/src/1Lab/Type/Pi.lagda.md
+++ b/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))
```
-->
diff --git a/src/Cat/Base.lagda.md b/src/Cat/Base.lagda.md
index d1f89c6fd..5ee6ed38c 100644
--- a/src/Cat/Base.lagda.md
+++ b/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
diff --git a/src/Cat/Diagram/Coproduct/Copower.lagda.md b/src/Cat/Diagram/Coproduct/Copower.lagda.md
index 088c94218..16d74ceee 100644
--- a/src/Cat/Diagram/Coproduct/Copower.lagda.md
+++ b/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$.
+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}
diff --git a/src/Cat/Functor/Adjoint/Hom.lagda.md b/src/Cat/Functor/Adjoint/Hom.lagda.md
index b2db5c47b..13430ab6d 100644
--- a/src/Cat/Functor/Adjoint/Hom.lagda.md
+++ b/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 _ _ _)
```
-->
diff --git a/src/Cat/Functor/Adjoint/Representable.lagda.md b/src/Cat/Functor/Adjoint/Representable.lagda.md
new file mode 100644
index 000000000..2248e1c25
--- /dev/null
+++ b/src/Cat/Functor/Adjoint/Representable.lagda.md
@@ -0,0 +1,201 @@
+
+
+```agda
+module Cat.Functor.Adjoint.Representable {o ℓ} {C : Precategory o ℓ} where
+```
+
+# Adjoints in terms of representability
+
+Building upon our characterisation of [[adjoints as Hom isomorphisms]], we now
+investigate the relationship between [[adjoint functors]] and [[representable
+functors]].
+
+In this section, we show that for a functor $R : \cC \to \cD$ to be a right adjoint
+is equivalent to the functor $\hom_\cD(d, R-) : \cC \to \Sets$ having a representing
+object for all $d : \cD$.
+
+The forward direction follows directly from the natural isomorphism $\hom_\cC(Ld, -)
+\cong \hom_\cD(d, R-)$, which exhibits $Ld$ as a representing object.
+
+
+
+```agda
+ right-adjoint→objectwise-rep
+ : ∀ d → Corepresentation (Hom-from D d F∘ R)
+ right-adjoint→objectwise-rep d .corep = L .F₀ d
+ right-adjoint→objectwise-rep d .corepresents =
+ adjunct-hom-iso-from L⊣R d ni⁻¹
+
+ left-adjoint→objectwise-rep
+ : ∀ c → Corepresentation (Hom-into C c F∘ Functor.op L)
+ left-adjoint→objectwise-rep c .corep = R .F₀ c
+ left-adjoint→objectwise-rep c .corepresents =
+ adjunct-hom-iso-into L⊣R c
+ ∘ni path→iso (sym (Hom-from-op _))
+```
+
+The other direction should be more surprising: if we only have a family of objects
+$Ld$ representing the functors $\hom_\cD(d, R-)$, why should we expect them to
+assemble into a *functor* $L : \cD \to \cC$?
+
+We answer the question indirectly^[for a more direct construction based on the Yoneda
+embedding, see the [nLab](https://ncatlab.org/nlab/show/adjoint+functor#AdjointFunctorFromObjectwiseRepresentingObject)]:
+what is a sufficient condition for $R$ to have a left adjoint?
+Well, by our characterisation in terms of [[universal morphisms]], it should be
+enough to have [[initial objects]] for each [[comma category]] $d \swarrow R$.
+But we have also `established`{.Agda ident=corepresentation→initial-element}
+that a (covariant) functor into $\Sets$ is representable
+if and only if its [[category of elements|covariant category of elements]]
+has an initial object.
+
+Now we simply observe that the comma category $d \swarrow R$ and the category of
+elements of $\hom_\cD(d, R-)$ are exactly the same: both are made out of pairs of
+an object $c : \cC$ and a map $d \to Rc$, with the morphisms between them obtained
+in the obvious way from morphisms in $\cC$.
+
+
+
+```agda
+ private
+ ↙≡∫ : ∀ d → d ↙ R ≡ ∫ C (Hom-from D d F∘ R)
+```
+
+
+The proof is by obnoxious data repackaging, so we hide it away.
+
+```agda
+ ↙≡∫ d = Precategory-path F F-is-precat-iso where
+ open is-precat-iso
+
+ F : Functor (d ↙ R) (∫ C (Hom-from D d F∘ R))
+ F .F₀ m = elem (m .↓Obj.y) (m .↓Obj.map)
+ F .F₁ f = elem-hom (f .↓Hom.β) (sym (f .↓Hom.sq) ∙ D.idr _)
+ F .F-id = Element-hom-path _ _ refl
+ F .F-∘ f g = Element-hom-path _ _ refl
+
+ F-is-precat-iso : is-precat-iso F
+ F-is-precat-iso .has-is-iso = is-iso→is-equiv is where
+ is : is-iso (F .F₀)
+ is .is-iso.inv e = ↓obj (e .Element.section)
+ is .is-iso.rinv e = refl
+ is .is-iso.linv o = ↓Obj-path _ _ refl refl refl
+ F-is-precat-iso .has-is-ff = is-iso→is-equiv is where
+ is : is-iso (F .F₁)
+ is .is-iso.inv h = ↓hom (D.idr _ ∙ sym (h .Element-hom.commute))
+ is .is-iso.rinv h = Element-hom-path _ _ refl
+ is .is-iso.linv h = ↓Hom-path _ _ refl refl
+```
+
+
+```agda
+ objectwise-rep→universal-maps : ∀ d → Universal-morphism d R
+ objectwise-rep→universal-maps d = subst Initial (sym (↙≡∫ d))
+ (corepresentation→initial-element (corep d))
+
+ objectwise-rep→L : Functor D C
+ objectwise-rep→L = universal-maps→L R objectwise-rep→universal-maps
+
+ objectwise-rep→L⊣R : objectwise-rep→L ⊣ R
+ objectwise-rep→L⊣R = universal-maps→L⊣R R objectwise-rep→universal-maps
+```
+
+## Right adjoints into Sets are representable
+
+For functors into $\Sets_\ell$, we can go one step further: under certain conditions,
+being a right adjoint is equivalent to being representable.
+
+Indeed, if $R$ has a left adjoint $L : \Sets_\ell \to \cC$, then $R$ is automatically
+represented by $L\{*\}$, the image of the singleton set by $L$, because we have
+$\hom_\cC(L\{*\}, c) \cong (\{*\} \to Rc) \cong Rc$.
+
+
+
+```agda
+ open Terminal (Sets-terminal {ℓ})
+
+ right-adjoint→corepresentable : Corepresentation R
+ right-adjoint→corepresentable .corep = L .F₀ top
+ right-adjoint→corepresentable .corepresents =
+ iso→isoⁿ (λ _ → equiv→iso (Π-⊤-eqv e⁻¹)) (λ _ → refl)
+ ∘ni adjunct-hom-iso-from L⊣R top ni⁻¹
+```
+
+Going the other way, if we assume that $\cC$ is [[copowered]] over $\Sets_\ell$
+(in other words, that it admits $\ell$-small [[indexed coproducts]]), then any
+functor $R$ with representing object $c$ has a left adjoint given by taking copowers
+of $c$: for any set $X$, we have $\hom_\cC(X \otimes c, -) \cong
+(X \to \hom_\cC(c, -)) \cong (X \to R-)$.
+
+
+
+```agda
+ private
+ open Copowers (λ _ → copowered)
+
+ Hom[X,R-]-rep : ∀ X → Corepresentation (Hom-from (Sets ℓ) X F∘ R)
+ Hom[X,R-]-rep X .corep = X ⊗ R-corep .corep
+ Hom[X,R-]-rep X .corepresents =
+ F∘-iso-r (R-corep .corepresents)
+ ∘ni copower-hom-iso ni⁻¹
+
+ corepresentable→L : Functor (Sets ℓ) C
+ corepresentable→L = objectwise-rep→L Hom[X,R-]-rep
+
+ corepresentable→L⊣R : corepresentable→L ⊣ R
+ corepresentable→L⊣R = objectwise-rep→L⊣R Hom[X,R-]-rep
+```
diff --git a/src/Cat/Functor/Dense.lagda.md b/src/Cat/Functor/Dense.lagda.md
index 69cf791be..cfc5cf3b7 100644
--- a/src/Cat/Functor/Dense.lagda.md
+++ b/src/Cat/Functor/Dense.lagda.md
@@ -24,10 +24,10 @@ by those of $\cC$, in a certain canonical way. In particular, any
functor $F$ and object $d : \cD$ can be put into a diagram
$$
-J : (F \searrow d) \xto{\mathrm{pr}} C \xto{\iota} D\text{,}
+J : (F \searrow d) \xto{\mathrm{pr}} C \xto{F} D\text{,}
$$
-where $(\iota \searrow d) \to C$ is the projection functor from the
+where $(F \searrow d) \to C$ is the projection functor from the
corresponding [comma category], in such a way that the object $d$ is the
nadir of a cocone over $J$.
@@ -60,7 +60,7 @@ module
```
The functor $F$ is called _dense_ if this cocone is colimiting for every
-$d : \cD$. The important of density is that, for a dense functor $F$,
+$d : \cD$. The importance of density is that, for a dense functor $F$,
the induced [nerve] functor is fully faithful.
[nerve]: Cat.Functor.Kan.Nerve.html
diff --git a/src/Cat/Functor/Hom/Duality.lagda.md b/src/Cat/Functor/Hom/Duality.lagda.md
new file mode 100644
index 000000000..70e13bccc
--- /dev/null
+++ b/src/Cat/Functor/Hom/Duality.lagda.md
@@ -0,0 +1,51 @@
+
+
+```agda
+module Cat.Functor.Hom.Duality where
+```
+
+# Duality of Hom functors
+
+We prove the obvious dualities between $\hom$ functors of opposite categories, and
+between representable and corepresentable functors.
+
+
+
+```agda
+Hom-from-op : ∀ c → Hom-from (C ^op) c ≡ Hom-into C c
+Hom-from-op c = Functor-path (λ _ → refl) (λ _ → refl)
+
+Hom-into-op : ∀ c → Hom-into (C ^op) c ≡ Hom-from C c
+Hom-into-op c = Functor-path (λ _ → refl) (λ _ → refl)
+
+corepresentable→co-representable
+ : ∀ {F : Functor C (Sets ℓ)}
+ → Corepresentation F → Representation {C = C ^op} F
+corepresentable→co-representable F-corep .rep = F-corep .corep
+corepresentable→co-representable F-corep .represents = F-corep .corepresents
+ ∘ni path→iso (sym (Hom-into-op _))
+
+co-representable→corepresentable
+ : ∀ {F : Functor (C ^op) (Sets ℓ)}
+ → Representation {C = C} F → Corepresentation F
+co-representable→corepresentable F-rep .corep = F-rep .rep
+co-representable→corepresentable F-rep .corepresents = F-rep .represents
+ ∘ni path→iso (sym (Hom-from-op _))
+```
diff --git a/src/Cat/Functor/Hom/Representable.lagda.md b/src/Cat/Functor/Hom/Representable.lagda.md
index 56f3bafe1..6d86d1ad2 100644
--- a/src/Cat/Functor/Hom/Representable.lagda.md
+++ b/src/Cat/Functor/Hom/Representable.lagda.md
@@ -9,9 +9,11 @@ open import Cat.Instances.Elements
open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Morphism.Duality
+open import Cat.Diagram.Initial
open import Cat.Functor.Hom
open import Cat.Prelude
+import Cat.Instances.Elements.Covariant as Co
import Cat.Reasoning
```
-->
@@ -34,7 +36,7 @@ open _=>_
```
-->
-# Representable functors {defines="representable-functor"}
+# Representable functors {defines="representable-functor corepresentable-functor representing-object"}
A functor $F : \cC\op \to \Sets_\kappa$ (from a [locally
$\kappa$-small category][univ]) is said to be **representable** when it
@@ -102,7 +104,6 @@ immediately from the lemma above: we also need to show that the
isomorphism computed by the full-faithfulness of the Yoneda embedding
commutes with the specified representation isomorphism.
This follows by construction, but the proof needs to commute
-
applications of functors and paths-from-isos, which is never pretty:
```agda
@@ -134,12 +135,13 @@ Representation-is-prop {F = F} c-cat x y = path where
We begin to connect the idea of representing objects to other universal
constructions by proving this alternative characterisation of
representations: A functor $F$ is representable if, and only if, its
-[category of elements](Cat.Instances.Elements.html) $\int F$ has a
+[[category of elements]] $\int F$ has a
[[terminal object]].
```agda
terminal-element→representation
- : {F : Functor (C ^op) (Sets κ)} → Terminal (∫ C F) → Representation F
+ : {F : Functor (C ^op) (Sets κ)}
+ → Terminal (∫ C F) → Representation F
terminal-element→representation {F} term = f-rep where
module F = Functor F
open Terminal term
@@ -174,9 +176,42 @@ constitutes a natural isomorphism.
invertible→invertibleⁿ nat inv
```
+In the other direction, we take the terminal element to be the image of the
+identity on the representing object.
+
+```agda
+representation→terminal-element
+ : {F : Functor (C ^op) (Sets κ)}
+ → Representation F → Terminal (∫ C F)
+representation→terminal-element {F} F-rep = term where
+ open Terminal
+ module F = Functor F
+ module Iso = Isoⁿ (F-rep .represents)
+
+ term : Terminal (∫ C F)
+ term .top .ob = F-rep .rep
+ term .top .section = Iso.from .η _ C.id
+ term .has⊤ (elem o s) .centre .hom = Iso.to .η _ s
+ term .has⊤ (elem o s) .centre .commute =
+ F.₁ (Iso.to .η o s) (Iso.from .η _ C.id) ≡˘⟨ Iso.from .is-natural _ _ _ $ₚ _ ⟩
+ Iso.from .η _ ⌜ C.id C.∘ Iso.to .η o s ⌝ ≡⟨ ap! (C.idl _) ⟩
+ Iso.from .η _ (Iso.to .η o s) ≡⟨ Iso.invr ηₚ o $ₚ s ⟩
+ s ∎
+ term .has⊤ (elem o s) .paths h = Element-hom-path _ _ $
+ Iso.to .η o ⌜ s ⌝ ≡˘⟨ ap¡ comm ⟩
+ Iso.to .η o (Iso.from .η _ (h .hom)) ≡⟨ Iso.invl ηₚ o $ₚ _ ⟩
+ h .hom ∎
+ where
+ comm =
+ Iso.from .η _ ⌜ h .hom ⌝ ≡˘⟨ ap¡ (C.idl _) ⟩
+ Iso.from .η _ (C.id C.∘ h .hom) ≡⟨ Iso.from .is-natural _ _ _ $ₚ _ ⟩
+ F.₁ (h .hom) (Iso.from .η _ C.id) ≡⟨ h .commute ⟩
+ s ∎
+```
+
## Universal constructions
-We now show a partial converse to the calculation above: That terminal
+In particular, we can show that terminal
objects are representing objects for a particular functor. Consider, to
be more specific, the constant functor $F : \cC\op \to \Sets$ which
sends everything to the terminal set. When is $F$ representable?
@@ -187,7 +222,7 @@ an object $X$ for which, given any other object $Y$, we have an
isomorphism of sets $\hom(Y,X) \cong \{*\}$^[which varies naturally in
$Y$, but this naturality is not used in this simple case]. Hence, a
representing object for the "constantly $\{*\}$" functor is precisely a
-terminal object. It turns out the
+terminal object.
```agda
representable-unit→terminal
@@ -197,6 +232,10 @@ representable-unit→terminal repr .Terminal.has⊤ ob = retract→is-contr
(Rep.from repr) (λ _ → lift tt) (Rep.η repr) (hlevel 0)
```
+This can be seen as a special case of the construction [above](#as-terminal-objects):
+$F$ is representable just when its category of elements has a terminal object,
+but in this case the category of elements of $F$ is just $\cC$!
+
## Corepresentable functors
As noted earlier, we can dualise the definition of a representable
@@ -244,7 +283,7 @@ corepresentation-unique X Y =
(iso→co-iso (Cat[ C , Sets κ ]) ni)
where
ni : Hom-from C (Y .corep) ≅ⁿ Hom-from C (X .corep)
- ni = (Y .corepresents ni⁻¹) ni∘ X .corepresents
+ ni = (Y .corepresents ni⁻¹) ∘ni X .corepresents
```
@@ -284,6 +323,76 @@ Corepresentation-is-prop {F = F} c-cat X Y = path where
```
+Dualising [the representable case](#as-terminal-objects), we have that a functor is
+corepresentable if and only if its [[covariant category of elements]] has an
+[[initial object]].
+
+```agda
+initial-element→corepresentation
+ : {F : Functor C (Sets κ)}
+ → Initial (Co.∫ C F) → Corepresentation F
+
+corepresentation→initial-element
+ : {F : Functor C (Sets κ)}
+ → Corepresentation F → Initial (Co.∫ C F)
+```
+
+
+The proofs are again entirely analogous to the representable case.
+
+```agda
+initial-element→corepresentation {F} init = f-corep where
+ module F = Functor F
+ open Co.Element
+ open Co.Element-hom
+ open Initial init
+ nat : F => Hom-from C (bot .ob)
+ nat .η ob section = has⊥ (Co.elem ob section) .centre .hom
+ nat .is-natural x y f = funext λ sect → ap hom $ has⊥ _ .paths $ Co.elem-hom _ $
+ F.₁ (f C.∘ has⊥ _ .centre .hom) (bot .section) ≡⟨ happly (F.F-∘ _ _) _ ⟩
+ F.₁ f (F.₁ (has⊥ _ .centre .hom) (bot .section)) ≡⟨ ap (F.₁ f) (has⊥ _ .centre .commute) ⟩
+ F.₁ f sect ∎
+
+ inv : ∀ x → Sets.is-invertible (nat .η x)
+ inv x = Sets.make-invertible
+ (λ f → F.₁ f (bot .section))
+ (funext λ x → ap hom $ has⊥ _ .paths (Co.elem-hom x refl))
+ (funext λ x → has⊥ _ .centre .commute)
+
+ f-corep : Corepresentation F
+ f-corep .corep = bot .ob
+ f-corep .corepresents = [C,Sets].invertible→iso nat $
+ invertible→invertibleⁿ nat inv
+
+corepresentation→initial-element {F} F-corep = init where
+ open Initial
+ open Co.Element
+ open Co.Element-hom
+ module F = Functor F
+ module Iso = Isoⁿ (F-corep .corepresents)
+
+ init : Initial (Co.∫ C F)
+ init .bot .ob = F-corep .corep
+ init .bot .section = Iso.from .η _ C.id
+ init .has⊥ (Co.elem o s) .centre .hom = Iso.to .η _ s
+ init .has⊥ (Co.elem o s) .centre .commute =
+ F.₁ (Iso.to .η o s) (Iso.from .η _ C.id) ≡˘⟨ Iso.from .is-natural _ _ _ $ₚ _ ⟩
+ Iso.from .η _ ⌜ Iso.to .η o s C.∘ C.id ⌝ ≡⟨ ap! (C.idr _) ⟩
+ Iso.from .η _ (Iso.to .η o s) ≡⟨ Iso.invr ηₚ o $ₚ s ⟩
+ s ∎
+ init .has⊥ (Co.elem o s) .paths h = Co.Element-hom-path _ _ $
+ Iso.to .η o ⌜ s ⌝ ≡˘⟨ ap¡ comm ⟩
+ Iso.to .η o (Iso.from .η _ (h .hom)) ≡⟨ Iso.invl ηₚ o $ₚ _ ⟩
+ h .hom ∎
+ where
+ comm =
+ Iso.from .η _ ⌜ h .hom ⌝ ≡˘⟨ ap¡ (C.idr _) ⟩
+ Iso.from .η _ (h .hom C.∘ C.id) ≡⟨ Iso.from .is-natural _ _ _ $ₚ _ ⟩
+ F.₁ (h .hom) (Iso.from .η _ C.id) ≡⟨ h .commute ⟩
+ s ∎
+```
+
+
## Corepresentable functors preserve limits
A useful fact about corepresentable functors is that they preserve
diff --git a/src/Cat/Functor/Naturality.lagda.md b/src/Cat/Functor/Naturality.lagda.md
index b64159cf9..e90a0c055 100644
--- a/src/Cat/Functor/Naturality.lagda.md
+++ b/src/Cat/Functor/Naturality.lagda.md
@@ -57,12 +57,15 @@ morphisms by a superscript `ⁿ`:
idni : ∀ {F} → F ≅ⁿ F
idni = CD.id-iso
- _ni∘_ : ∀ {F G H} → F ≅ⁿ G → G ≅ⁿ H → F ≅ⁿ H
- _ni∘_ = CD._∘Iso_
+ _∘ni_ : ∀ {F G H} → F ≅ⁿ G → G ≅ⁿ H → F ≅ⁿ H
+ _∘ni_ = CD._∘Iso_
_ni⁻¹ : ∀ {F G} → F ≅ⁿ G → G ≅ⁿ F
_ni⁻¹ = CD._Iso⁻¹
+ infixr 30 _∘ni_
+ infix 31 _ni⁻¹
+
≅ⁿ-pathp : ∀ {a c b d : Functor C D} (p : a ≡ c) (q : b ≡ d) {f : a ≅ⁿ b} {g : c ≅ⁿ d}
→ (∀ x → PathP (λ i → D.Hom (p i .F₀ x) (q i .F₀ x)) (Isoⁿ.to f .η x) (Isoⁿ.to g .η x))
→ PathP (λ i → p i CD.≅ q i) f g
@@ -138,6 +141,19 @@ to an invertible natural transformation, resp. natural isomorphism.
D.make-iso (α.to .η x) (α.from .η x) (α.invl ηₚ x) (α.invr ηₚ x)
where module α = Isoⁿ α
+ iso→isoⁿ
+ : ∀ {F G}
+ → (is : ∀ x → F .F₀ x D.≅ G .F₀ x)
+ → (∀ {x y} f → G .F₁ f D.∘ is x .D.to ≡ is y .D.to D.∘ F .F₁ f)
+ → F ≅ⁿ G
+ iso→isoⁿ {F} {G} is nat = to-natural-iso mk where
+ mk : make-natural-iso F G
+ mk .eta x = is x .D.to
+ mk .inv x = is x .D.from
+ mk .eta∘inv x = is x .D.invl
+ mk .inv∘eta x = is x .D.invr
+ mk .natural _ _ = nat
+
is-invertibleⁿ→isoⁿ : ∀ {F G} {α : F => G} → is-invertibleⁿ α → F ≅ⁿ G
is-invertibleⁿ→isoⁿ nat-inv = CD.invertible→iso _ nat-inv
diff --git a/src/Cat/Instances/Comma.lagda.md b/src/Cat/Instances/Comma.lagda.md
index 28870b14f..71060287e 100644
--- a/src/Cat/Instances/Comma.lagda.md
+++ b/src/Cat/Instances/Comma.lagda.md
@@ -221,7 +221,7 @@ square.
module _ {A : Precategory ao ah} {B : Precategory bo bh} where
private module A = Precategory A
- infix 4 _↙_ _↘_
+ infix 5 _↙_ _↘_
_↙_ : A.Ob → Functor B A → Precategory _ _
X ↙ T = const! X ↓ T
diff --git a/src/Cat/Instances/Elements.lagda.md b/src/Cat/Instances/Elements.lagda.md
index 4a9370568..247bae31a 100644
--- a/src/Cat/Instances/Elements.lagda.md
+++ b/src/Cat/Instances/Elements.lagda.md
@@ -19,10 +19,11 @@ private
```
-->
-# The Category of Elements
+# The category of elements {defines="category-of-elements contravariant-category-of-elements"}
-The category of elements of a presheaf $P : \cC\op \to \Sets$ is a means
-of unpacking the data of the presheaf. Its objects are pairs of an
+The (contravariant^[there is a separate [[covariant category of elements]] for
+covariant functors]) category of elements of a presheaf $P : \cC\op \to \Sets$
+is a means of unpacking the data of the presheaf. Its objects are pairs of an
object $x$, and a section $s : P x$.
```agda
diff --git a/src/Cat/Instances/Elements/Covariant.lagda.md b/src/Cat/Instances/Elements/Covariant.lagda.md
new file mode 100644
index 000000000..80c6f3e56
--- /dev/null
+++ b/src/Cat/Instances/Elements/Covariant.lagda.md
@@ -0,0 +1,117 @@
+
+
+```agda
+module Cat.Instances.Elements.Covariant {o ℓ s} (C : Precategory o ℓ)
+ (P : Functor C (Sets s)) where
+```
+
+
+
+# The covariant category of elements {defines="covariant-category-of-elements"}
+
+While the [[category of elements]] comes up most often in the context of presheaves
+(i.e., contravariant functors into $\Sets$), the construction makes sense for
+covariant functors as well.
+
+Sadly, we cannot simply reuse the contravariant construction,
+instantiating $\cC$ as $\cC\op$: the resulting category would be the
+[[opposite|opposite category]] of what we want. Indeed, in both the covariant and
+contravariant cases, we want the projection $\pi : \int F \to \cC$ to be covariant.
+
+Thus we proceed to dualise the whole construction.
+
+```agda
+record Element : Type (o ⊔ s) where
+ constructor elem
+ field
+ ob : Ob
+ section : ∣ P.₀ ob ∣
+
+open Element
+
+record Element-hom (x y : Element) : Type (ℓ ⊔ s) where
+ constructor elem-hom
+ no-eta-equality
+ field
+ hom : Hom (x .ob) (y .ob)
+ commute : P.₁ hom (x .section) ≡ y .section
+
+open Element-hom
+
+Element-hom-path : {x y : Element} {f g : Element-hom x y} → f .hom ≡ g .hom → f ≡ g
+Element-hom-path p i .hom = p i
+Element-hom-path {x = x} {y = y} {f = f} {g = g} p i .commute =
+ is-prop→pathp (λ j → P.₀ (y .ob) .is-tr (P.₁ (p j) (x .section)) (y .section))
+ (f .commute)
+ (g .commute) i
+
+private unquoteDecl eqv = declare-record-iso eqv (quote Element-hom)
+Element-hom-is-set : ∀ (x y : Element) → is-set (Element-hom x y)
+Element-hom-is-set x y = Iso→is-hlevel 2 eqv T-is-set where
+ T-is-set : is-set _
+ T-is-set = hlevel!
+
+∫ : Precategory (o ⊔ s) (ℓ ⊔ s)
+∫ .Precategory.Ob = Element
+∫ .Precategory.Hom = Element-hom
+∫ .Precategory.Hom-set = Element-hom-is-set
+∫ .Precategory.id {x = x} = elem-hom id λ i → P.F-id i (x .section)
+∫ .Precategory._∘_ {x = x} {y = y} {z = z} f g = elem-hom (f .hom ∘ g .hom) comm
+ where
+ abstract
+ comm : P.₁ (f .hom ∘ g .hom) (x .section) ≡ z .section
+ comm =
+ P.₁ (f .hom ∘ g .hom) (x .section) ≡⟨ happly (P.F-∘ (f .hom) (g .hom)) (x .section) ⟩
+ P.₁ (f .hom) (P.₁ (g .hom) (x .section)) ≡⟨ ap (P.F₁ (f .hom)) (g .commute) ⟩
+ P.₁ (f .hom) (y .section) ≡⟨ f .commute ⟩
+ z .section ∎
+∫ .Precategory.idr f = Element-hom-path (idr (f .hom))
+∫ .Precategory.idl f = Element-hom-path (idl (f .hom))
+∫ .Precategory.assoc f g h = Element-hom-path (assoc (f .hom) (g .hom) (h .hom))
+
+πₚ : Functor ∫ C
+πₚ .F₀ x = x .ob
+πₚ .F₁ f = f .hom
+πₚ .F-id = refl
+πₚ .F-∘ f g = refl
+```
+
+We can now relate the two constructions: the covariant category of elements of $P$
+is the opposite of the contravariant category of elements of $P$ seen as a
+contravariant functor on $\cC\op$ (thus a functor $(\cC\op)\op = \cC \to \Sets$).
+
+```agda
+co-∫ : ∫ ≡ Contra.∫ (C ^op) P ^op
+co-∫ = Precategory-path F F-is-precat-iso where
+ F : Functor ∫ (Contra.∫ (C ^op) P ^op)
+ F .F₀ e = Contra.elem (e .ob) (e .section)
+ F .F₁ h = Contra.elem-hom (h .hom) (h .commute)
+ F .F-id = refl
+ F .F-∘ _ _ = Contra.Element-hom-path _ _ refl
+
+ F-is-precat-iso : is-precat-iso F
+ F-is-precat-iso .is-precat-iso.has-is-iso = is-iso→is-equiv λ where
+ .is-iso.inv e → elem (e .Contra.Element.ob) (e .Contra.Element.section)
+ .is-iso.rinv e → refl
+ .is-iso.linv e → refl
+ F-is-precat-iso .is-precat-iso.has-is-ff = is-iso→is-equiv λ where
+ .is-iso.inv h → elem-hom (h .Contra.Element-hom.hom) (h .Contra.Element-hom.commute)
+ .is-iso.rinv h → Contra.Element-hom-path _ _ refl
+ .is-iso.linv h → Element-hom-path refl
+```
diff --git a/src/Cat/Instances/Functor.lagda.md b/src/Cat/Instances/Functor.lagda.md
index e90d30ef4..ee6b03d96 100644
--- a/src/Cat/Instances/Functor.lagda.md
+++ b/src/Cat/Instances/Functor.lagda.md
@@ -1,8 +1,10 @@
* Lemma 3.9.1: `is-prop→equiv∥-∥`{.Agda}
-* Lemma 3.9.2: Implicit in e.g. `∥-∥-univ`, `∥-∥-proj`{.Agda}
+* Lemma 3.9.2: Implicit in e.g. `∥-∥-univ`{.Agda}, `∥-∥-proj`{.Agda}
### 3.11 Contractibility
@@ -307,6 +307,8 @@ _ = is-contr
_ = is-contr-is-prop
_ = retract→is-contr
_ = Singleton-is-contr
+_ = Σ-contract
+_ = Σ-contr-eqv
```
-->
@@ -314,6 +316,7 @@ _ = Singleton-is-contr
* Definition 3.11.4: `is-contr-is-prop`{.Agda}
* Definition 3.11.7: `retract→is-contr`{.Agda}
* Definition 3.11.8: `Singleton-is-contr`{.Agda}
+* Lemma 3.11.9: `Σ-contract`{.Agda}, `Σ-contr-eqv`{.Agda}
### Exercises
@@ -364,8 +367,8 @@ _ = is-iso→is-contr-rinv
* Definition 4.2.1: `is-half-adjoint-equiv`{.Agda}
* Definition 4.2.3: `is-iso→is-half-adjoint-equiv`{.Agda}
-* Definition 4.2.4: `fibre`
-* Lemma 4.2.5: `fibre-paths`
+* Definition 4.2.4: `fibre`{.Agda}
+* Lemma 4.2.5: `fibre-paths`{.Agda}
* Theorem 4.2.6: `is-half-adjoint-equiv→is-equiv`{.Agda}
* Definition 4.2.7: `linv`{.Agda}, `rinv`{.Agda}
* Lemma 4.2.8: `is-equiv→pre-is-equiv`{.Agda}, `is-equiv→post-is-equiv`{.Agda}
@@ -767,14 +770,14 @@ _ = hom-iso→adjoints
* Definition 9.5.1: `_^op`{.Agda}
* Definition 9.5.2: `_×ᶜ_`{.Agda}
-* Lemma 9.5.3: `Curry`{.Agda}, `Uncurry`
+* Lemma 9.5.3: `Curry`{.Agda}, `Uncurry`{.Agda}
* The $\hom$-functor: `Hom[-,-]`{.Agda}
* The Yoneda embedding: `よ`{.Agda}
* Corollary 9.5.6: `よ-is-fully-faithful`{.Agda}
* Corollary 9.5.7: _As a corollary of `Representation-is-prop`{.Agda}_
* Definition 9.5.8: `Representation`{.Agda}
* Theorem 9.5.9: `Representation-is-prop`{.Agda}
-* Lemma 9.5.10: `hom-iso→adjoints`
+* Lemma 9.5.10: [Adjoints in terms of representability](Cat.Functor.Adjoint.Representable.html)
### 9.6 Strict categories
diff --git a/src/index.lagda.md b/src/index.lagda.md
index 40f45c9a3..7ecdad566 100644
--- a/src/index.lagda.md
+++ b/src/index.lagda.md
@@ -408,6 +408,7 @@ About [[adjoint functors]], and their associated monads:
open import Cat.Diagram.Monad -- Definition of monads
open import Cat.Functor.Adjoint -- Unit-counit adjunctions and universal arrows
open import Cat.Functor.Adjoint.Hom -- Adjoints in terms of Hom-isomorphisms
+open import Cat.Functor.Adjoint.Representable -- Adjoints in terms of representables
open import Cat.Functor.Adjoint.Monad -- Monad from an adjunction
open import Cat.Functor.Adjoint.Unique -- Uniqueness of adjoints
open import Cat.Functor.Adjoint.Monadic -- Monadic adjunctions
@@ -445,6 +446,7 @@ open import Cat.Functor.Hom -- Hom functor, Yoneda embedding
open import Cat.Functor.Hom.Cocompletion -- Universal property of PSh(C)
open import Cat.Functor.Hom.Coyoneda -- The Coyoneda lemma
open import Cat.Functor.Hom.Representable -- Representable functors
+open import Cat.Functor.Hom.Duality -- Duality of Hom functors
open import Cat.Functor.Hom.Displayed
-- Hom functors of displayed categories
diff --git a/support/web/css/default.scss b/support/web/css/default.scss
index 55b999765..040eba712 100644
--- a/support/web/css/default.scss
+++ b/support/web/css/default.scss
@@ -344,6 +344,7 @@ table {
}
details {
+ margin-block: 1em;
border-left: 5px solid var(--note-bg);
padding-left: 1rem;