{-# OPTIONS -vtc.decl:5 --lossy-unification -WnoEmptyWhere #-}
open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Colimit.Base
open import Cat.Instances.Functor
open import Cat.Diagram.Initial
open import Cat.Instances.Comma
open import Cat.Functor.Hom
open import Cat.Functor.Kan
open import Cat.Prelude

import Cat.Functor.Reasoning as Functor-kit
import Cat.Reasoning

module Cat.Functor.Kan.Nerve where


# Nerve and realisation🔗

Let $F : \mathcal{C} \to \mathcal{D}$ be a functor from a $\kappa$-small category $\mathcal{C}$ to a locally $\kappa$-small, $\kappa$-cocomplete category $\mathcal{D}$. $F$ induces a pair of adjoint functors, as in the diagram below, where $|-| \dashv {\mathbf{N}}$. In general, the left adjoint is called “realization”, and the right adjoint is called “nerve”.  An example to keep in mind is the inclusion $F : \Delta {\hookrightarrow}{{{\mathfrak{Cat}}}_{\mathrm{strict}}}$ from the simplex category to strict categories, which sends the $n$-simplex to the finite poset $[n]$. In this case, the left adjoint is the ordinary realisation of a simplicial set $[\Delta{^{{\mathrm{op}}}},{{\mathbf{Sets}}}]$ as a strict category, and the right adjoint gives the simplicial nerve of a strict category.

Since these adjunctions come for very cheap ($\kappa$-cocompleteness of the codomain category is all we need), they are built out of very thin abstract nonsense: The “realisation” left adjoint is given by the left Kan extension of $F$ along the Yoneda embedding ${よ}$, which can be computed as a particular colimit, and the “nerve” right adjoint is given by the restricted Yoneda embedding functor $X \mapsto {\mathbf{Hom}}(F(-), X)$.

  Nerve : {D : Precategory κ κ} → Functor D C → Functor C (PSh κ D)
Nerve F .F₀ x .F₀ y    = el (C.Hom (F .F₀ y) x) (C.Hom-set _ _)
Nerve F .F₀ x .F₁ f g  = g C.∘ F .F₁ f
Nerve F .F₀ x .F-id    = funext λ x → C.elimr (F .F-id)
Nerve F .F₀ x .F-∘ f g = funext λ x → C.pushr (F .F-∘ _ _)

Nerve F .F₁ f .η _ g            = f C.∘ g
Nerve F .F₁ _ .is-natural _ _ _ = funext λ _ → C.assoc _ _ _

Nerve F .F-id    = Nat-path λ _ → funext λ _ → C.idl _
Nerve F .F-∘ f g = Nat-path λ _ → funext λ _ → sym (C.assoc _ _ _)


The realisation left adjoint is constructed by general abstract nonsense.

  Realisation : {D : Precategory κ κ} → Functor D C → Functor (PSh κ D) C
Realisation {D} F = cocomplete→lan cocompl (よ D) F .Lan.Ext

Realisation⊣Nerve
: {D : Precategory κ κ} (F : Functor D C)
→ Realisation F ⊣ Nerve F


The construction of the nerve-realisation adjunction is done below in components, but understanding it is not necessary: Either ponder the $\Delta {\hookrightarrow}{{{\mathfrak{Cat}}}_{\mathrm{strict}}}$ example from above, or take it as a foundational assumption. However, if you’re feeling particularly brave, feel free to look at the code. Godspeed.

  Realisation⊣Nerve {D = D} F = adj where
module D = Cat.Reasoning D
open _⊣_
open ↓Obj
open ↓Hom
module F = Functor-kit F

hom′ : (P : Functor (D ^op) (Sets κ)) (i : D.Ob)
→ (arg : ∣ P .F₀ i ∣)
→ ↓Obj (よ D) _
hom′ P i arg .x = i
hom′ P i arg .y = tt
hom′ P i arg .map .η j h = P .F₁ h arg
hom′ P i arg .map .is-natural _ _ f = funext λ _ → happly (P .F-∘ _ _) _

Shape : (c : C.Ob) → Functor (よ D ↘ Nerve F .F₀ c) C
Shape c = F F∘ Dom (よ D) (const! (Nerve F .F₀ c))

cocone′ : ∀ ob → Cocone (Shape ob)
cocone′ ob .coapex = ob
cocone′ ob .ψ obj = obj .map .η _ D.id
cocone′ ob .commutes {x} {y} f =
sym (y .map .is-natural _ _ _) $ₚ _ ∙ ap (y .map .η (x .↓Obj.x)) D.id-comm-sym ∙ f .sq ηₚ _$ₚ _


Before proceeding, take a moment to appreciate the beauty of the adjunction unit and counit, and you’ll see that it makes sense that nerve and realisation are adjoints: The unit is given by the coprojections defining the left Kan extension as a colimit, and the counit is given by the unique “colimiting” map from that colimit.

    adj : Realisation F ⊣ Nerve F
adj .unit .η P .η i arg = cocompl _ .bot .ψ (hom′ P i arg)
adj .counit .η ob       = cocompl _ .has⊥ (cocone′ ob) .centre .hom

adj .unit .η P .is-natural x y f = funext λ arg →
sym $cocompl (F F∘ Dom (よ D) (Const P)) .bot .commutes (record { sq = Nat-path (λ _ → funext λ _ → P .F-∘ _ _$ₚ _) })

adj .unit .is-natural x y f = Nat-path λ i → funext λ arg → sym $cocompl (F F∘ Dom (よ D) (Const x)) .has⊥ (lan-approximate cocompl (よ D) F f) .centre .commutes (hom′ x i arg) ∙ ap (cocompl (F F∘ Dom (よ D) (Const y)) .bot .ψ) (↓Obj-path _ _ refl refl (Nat-path λ _ → funext λ _ → f .is-natural _ _ _$ₚ _))

adj .counit .is-natural x y f = ap hom $is-contr→is-prop (cocompl _ .has⊥ cocone₂) (cocone-hom _ λ o → C.pullr (cocompl (Shape x) .has⊥ _ .centre .commutes o) ∙ cocompl (Shape y) .has⊥ (cocone′ _) .centre .commutes _) (cocone-hom _ λ o → C.pullr (cocompl _ .has⊥ (cocone′ x) .centre .commutes _)) where cocone₂ : Cocone (Shape x) cocone₂ .coapex = y cocone₂ .ψ ob = f C.∘ ob .map .η _ D.id cocone₂ .commutes {x₂} {y₂} f = C.pullr ( sym (happly (y₂ .map .is-natural _ _ _) _) ∙ ap (y₂ .map .η _) (sym D.id-comm)) ∙ ap (_ C.∘_) (f .sq ηₚ _$ₚ D.id)

adj .zig {A} = ap hom $is-contr→is-prop (cocompl (F F∘ Dom (よ D) (const! A)) .has⊥ (cocompl _ .bot)) (cocone-hom _ λ o → C.pullr ( cocompl (F F∘ Dom (よ D) (Const A)) .has⊥ _ .centre .commutes o) ·· cocompl (Shape (Realisation F .F₀ A)) .has⊥ _ .centre .commutes _ ·· ap (cocompl (F F∘ Dom (よ D) (const! A)) .bot .ψ) {x = hom′ A (o .x) (o .map .η (o .x) D.id)} (↓Obj-path _ _ _ refl (Nat-path λ x → funext λ _ → sym (o .map .is-natural _ _ _$ₚ _) ∙ ap (o .map .η x) (D.idl _))))
(cocone-hom _ λ o → C.idl _)

adj .zag {B} = Nat-path λ x → funext λ a →
cocompl (F F∘ Dom (よ D) (const! (Nerve F .F₀ B))) .has⊥ (cocone′ B)
.centre .commutes (hom′ _ x a)
∙ F.elimr refl