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.Functor.Adjoint
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 : \ca{C} \to \ca{D}$ be a functor from a $\kappa$-small category $\ca{C}$ to a locally $\kappa$-small, $\kappa$-cocomplete category $\ca{D}$. $F$ induces a pair of adjoint functors, as in the diagram below, where $|-| \dashv \bf{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 \mono \strcat$ 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^op,\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 $\yo$, which can be computed as a particular colimit, and the “nerve” right adjoint is given by the restricted Yoneda embedding functor $X \mapsto \hom(F(-), X)$.

  Nerve : {D : Precategory κ κ} → Functor D C → Functor C (PSh κ D)
  Nerve F .F₀ x .F₀ y    = 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 F (よ D) .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 \mono \strcat$ 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-∘ _ _) _

    cocone′ : ∀ ob → Cocone (F F∘ Dom (よ D) (const! (Nerve F .F₀ ob)))
    cocone′ ob .coapex = ob
    cocone′ ob .ψ obj = obj .map .η _ D.id
    cocone′ ob .commutes {x} {y} f =
      happly (sym (y .map .is-natural _ _ _)) _
      ∙ ap (y .map .η (x .↓Obj.x)) (sym D.id-comm)
      ∙ happly (ap (λ e → e .η (x .↓Obj.x)) (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 _ .bot .commutes {x = obj′ arg}
          ( record { sq = Nat-path (λ _ → refl) })
          ∙ ap (cocompl _ .bot .ψ)
            (↓Obj-path _ _ refl refl
              (Nat-path λ _ → funext λ _ → happly (P .F-∘ _ _) _)))
      where
        obj′ : ∀ arg → ↓Obj (よ _) _
        obj′ arg .↓Obj.x = y
        obj′ arg .↓Obj.y = tt
        obj′ arg .map .η j h = P .F₁ (f D.∘ h) arg
        obj′ arg .map .is-natural X Y F = funext λ A →
            happly (P .F-∘ _ _) _
          ∙ happly (P .F-∘ _ _) _
          ∙ λ i → P .F₁ F (P .F-∘ A f (~ i) arg)

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

    adj .counit .is-natural x y f = ap hom $
      is-contr→is-prop
        (cocompl (F F∘ Dom (よ D) (const! (Nerve F .F₀ x))) .has⊥ cocone₂)
        (cocone-hom _ λ o →
            C.pullr (cocompl _ .has⊥ (lan-approximate cocompl _ _ _)
                      .centre .commutes _)
          ∙ cocompl _ .has⊥ (cocone′ y) .centre .commutes _)
        (cocone-hom _ λ o →
          C.pullr (cocompl _ .has⊥ (cocone′ x) .centre .commutes _))
      where
        cocone₂ : Cocone _
        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.∘_) (happly (ap (λ e → e .η (x₂ .↓Obj.x)) (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 _ .has⊥ (lan-approximate cocompl _ _ _)
                               .centre .commutes _)
          ∙ cocompl _ .has⊥ (cocone′ _) .centre .commutes _
          ∙ ap (cocompl (F F∘ Dom (よ D) (const! A)) .bot .ψ)
                  (↓Obj-path _ _ _ refl (Nat-path λ x → funext λ _ →
                      sym (happly (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