poset-nerve.agda

open import Cat.Instances.Simplex
open import Cat.Instances.Functor
open import Cat.Instances.Comma
open import Cat.Diagram.Colimit.Base
open import Cat.Displayed.Total
open import Cat.Displayed.Univalence.Thin
open import Cat.Functor.Hom
open import Cat.Functor.Base
open import Cat.Functor.Dense
open import Cat.Prelude
open import Data.Fin
open import Cat.Functor.Kan.Nerve
open import Order.Base
import Data.Nat as N

module wip.poset-nerve where

to-nat-inj : ∀ {n} (x y : Fin n) → x ≤ y → y ≤ x → x ≡ y
to-nat-inj fzero fzero α β = refl
to-nat-inj (fsuc x) (fsuc y) α β = ap fsuc (to-nat-inj x y (N.≤-peel α) (N.≤-peel β))

Pos : ∀ {ℓ} → Functor Δ (Posets ℓ ℓ)
Pos .Functor.F₀ x = to-poset _ mkp where
  mkp : make-poset _ (Lift _ (Fin (suc x)))
  mkp .make-poset.rel (lift x) (lift y) = Lift _ (x ≤ y)
  mkp .make-poset.id = lift N.≤-refl
  mkp .make-poset.thin = Lift-is-hlevel 1 N.≤-is-prop
  mkp .make-poset.trans (lift x) (lift y) = lift (N.≤-trans x y)
  mkp .make-poset.antisym (lift x) (lift y) = ap lift (to-nat-inj _ _ x y)

Pos .Functor.F₁ f .hom (lift x) = lift (Δ-map.map f x)
Pos .Functor.F₁ f .preserves x y p = lift (Δ-map.ascending f _ _ (p .Lift.lower))
Pos .Functor.F-id = Homomorphism-path λ x → refl
Pos .Functor.F-∘ f g = Homomorphism-path λ x → refl

private module Pos {ℓ} = Functor (Pos {ℓ})
Δn : Functor (Posets lzero lzero) (PSh lzero Δ)
Δn = Nerve Pos

open _=>_

weaken-ascending : ∀ {n} (x y : Fin n) → x ≤ y → weaken x ≤ weaken y
weaken-ascending fzero fzero p = 0≤x
weaken-ascending fzero (fsuc y) p = 0≤x
weaken-ascending (fsuc x) (fsuc y) (N.s≤s p) = N.s≤s (weaken-ascending x y p)

Δn-ff : is-fully-faithful Δn
Δn-ff {X} {Y} = is-iso→is-equiv (iso to rinv linv) where
  private
    module X = Poset-on (X .snd)
    module Y = Poset-on (Y .snd)

  eval : (Δn .Functor.F₀ X => Δn .Functor.F₀ Y) → Posets.Hom (Pos .Functor.F₀ 0) X → ⌞ Y ⌟
  eval f x = f .η 0 x .hom (lift fzero)

  img : (Δn .Functor.F₀ X => Δn .Functor.F₀ Y) → ∀ x → ∣ Y .fst ∣
  img f x = eval f (total-hom (λ _ → x) (λ _ _ _ → X.≤-refl))

  evalp : ∀ (f : Δn .Functor.F₀ X => Δn .Functor.F₀ Y) {x}
        → eval f x ≡ img f (x .hom (lift fzero))
  evalp f = ap (eval f) $ Homomorphism-path λ where (lift fzero) → refl

  to : (Δn .Functor.F₀ X => Δn .Functor.F₀ Y)
     → Posets lzero lzero .Precategory.Hom X Y
  to f .hom x = img f x
  to f .preserves x y x≤y = subst {A = _ × _}
    (λ e → e .fst Y.≤ e .snd)
    (ap₂ _,_ (sym rem₁ ∙ evalp f) (sym rem₂ ∙ evalp f))
    (f .η 1 xtoy .preserves (lift fzero) (lift (fsuc fzero)) (lift 0≤x))
    where
      -- Turn an ascending sequence into a 1-simplex:
      xtoy : ∣ Functor.F₀ (Δn .Functor.F₀ X) 1 ∣
      xtoy .hom (lift fzero)    = x
      xtoy .hom (lift (fsuc _)) = y

      xtoy .preserves (lift fzero) (lift fzero) _       = X.≤-refl
      xtoy .preserves (lift fzero) (lift (fsuc _)) _    = x≤y
      xtoy .preserves (lift (fsuc _)) (lift (fsuc _)) _ = X.≤-refl

      -- These proofs have a nasty type but xtoy ∘ an ascending map 1→2
      -- projects out one of the endpoints of the line. Weaken projects
      -- the 0th endpoint and fsuc projects the 1st endpoint. That
      -- knowledge + naturality lets us conclude that the natural
      -- transformation f takes the simplex xtoy to a proof that x ≤ y
      rem₁ = ap hom (f .is-natural 1 0 (record { map = weaken ; ascending = weaken-ascending }) $ₚ xtoy) $ₚ lift fzero
      rem₂ = ap hom (f .is-natural 1 0 (record { map = fsuc   ; ascending = λ _ _ → N.s≤s    }) $ₚ xtoy) $ₚ lift fzero

  rinv : is-right-inverse to (Functor.F₁ Δn)
  rinv nt = Nat-path (λ card → funext λ g → Homomorphism-path (lemma card g)) where
    pt : ∀ {c} (g : Posets.Hom (Pos .Functor.F₀ c) X) x → ⌞ Y ⌟
    pt g x = img nt (g .hom x)

    -- Simplices in the nerve of a poset are determined by their points.
    -- Sharper version of a lemma saying that simplices in the nerve of
    -- a strict category are determined by their 1-d faces.
    -- Even sharper: Kerodon 1.4.7.3
    lemma : ∀ c (g : Posets.Hom (Pos .Functor.F₀ c) X)
          → ∀ x → pt g x ≡ nt .η c g .hom x
    lemma zero g (lift fzero) = sym (evalp nt)
    lemma (suc c) g (lift x) =
        sym (evalp nt)
      ∙ ap hom (nt .is-natural (suc c) 0
        (record { map       = λ _ → x
                ; ascending = λ _ _ _ → N.≤-refl
                }) $ₚ g) $ₚ lift fzero

  linv : is-left-inverse to (Functor.F₁ Δn)
  linv f = Homomorphism-path λ x → refl