module Cat.Displayed.Cartesian.Discrete where

Discrete fibrations🔗

A discrete fibration is a displayed category whose fibre categories are all discrete categories: thin, univalent groupoids. Since thin, univalent groupoids are sets, a discrete fibration over B\mathcal{B} is an alternate way of encoding a presheaf over B\mathcal{B}, i.e., a functor Bop→Sets\mathcal{B}^{\mathrm{op}}\to\mathbf{Sets}. Here, we identify a purely fibrational property that picks out the discrete fibrations among the displayed categories, without talking about the fibres directly.

A discrete fibration is a displayed category such that each type of displayed objects is a set, and such that, for each right corner

there is a contractible space of objects xâ€Čx' over xx equipped with maps xâ€Č→fyâ€Čx' \to_f y'.

  record Discrete-fibration : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where
      fibre-set : ∀ x → is-set E.Ob[ x ]
        : ∀ {x y} (f : B.Hom x y) (y' : E.Ob[ y ])
        → is-contr (Σ[ x' ∈ E.Ob[ x ] ] E.Hom[ f ] x' y')

Discrete fibrations are cartesian🔗

To prove that discrete fibrations deserve the name discrete fibrations, we prove that any discrete fibration is a Cartesian fibration. By assumption, every right corner has a unique lift, which is in particular a lift: we just have to show that the lift is Cartesian.

  discrete→cartesian : Discrete-fibration → Cartesian-fibration E
  discrete→cartesian disc = r where
    open Discrete-fibration disc
    r : Cartesian-fibration E
    r .has-lift f y' .x' = lifts f y' .centre .fst
    r .has-lift f y' .lifting = lifts f y' .centre .snd

So suppose we have an open diagram

where fâ€Č:aâ€Č→bâ€Čf' : a' \to b' is the unique lift of ff along bâ€Čb'. We need to find a map uâ€Č→maâ€Ču' \to_m a'. Observe that we have a right corner (with vertices uu and aâ€Ča' over aa), so that we an object u2u_2 over uu and map l:u2→maâ€Čl : u_2 \to_m a'. Initially, this looks like it might not help, but observe that uâ€Č→hâ€Čf∘mbâ€Ču' \xrightarrow{h'}_{f \circ m} b' and u2→luaâ€Č→fâ€Čfbâ€Ču_2 \xrightarrow{l}_{u} a' \xrightarrow{f'}_f b' are lifts of the right corner with base given by u→a→bu \to a \to b, so that by uniqueness, u2=uâ€Ču2 = u': thus, we can use ll as our map uâ€Č→aâ€Ču' \to a'.

    r .has-lift f y' .cartesian .universal {u} {u'} m h' =
      subst (λ x → E.Hom[ m ] x (lifts f y' .centre .fst))
        (ap fst $ is-contr→is-prop (lifts (f B.∘ m) y')
          (_ , lifts f y' .centre .snd E.∘' lifts m _ .centre .snd)
          (u' , h'))
        (lifts m (lifts f y' .centre .fst) .centre .snd)
    r .has-lift f y' .cartesian .commutes m h' =
      Σ-inj-set (fibre-set _) $ is-contr→is-prop (lifts (f B.∘ m) y') _ _
    r .has-lift f y' .cartesian .unique {u} {u'} {m} m' x =
      Σ-inj-set (fibre-set u) $ is-contr→is-prop (lifts m _) (u' , m') (u' , _)

Fibres of discrete fibrations🔗

Let xx be an object of B\mathcal{B}. Let us ponder the fibre E∗(x)\mathcal{E}^*(x): we know that it is strict, since by assumption there is a set of objects over xx. Let us show also that it is thin: imagine that we have two parallel, vertical arrows f,g:a→id⁡bf, g : a \to_{\operatorname{id}_{}} b. These assemble into a diagram like

whence we see that (aâ€Č,f)(a', f) and (aâ€Č,g)(a', g) are both lifts for the lower corner given by lifting the identity map along bâ€Čb' — so, since lifts are unique, we have f=gf = g.

    : ∀ x → Discrete-fibration → ∀ {a b} → is-prop (Fibre E x .Precategory.Hom a b)
  discrete→thin-fibres x disc {a} {b} f g =
    ÎŁ-inj-set (fibre-set x) $
      is-contr→is-prop (lifts b) (a , f) (a , g)
    where open Discrete-fibration disc

Morphisms in discrete fibrations🔗

If E\mathcal{E} is a discrete fibration, then the only vertical morphisms are identities. This follows directly from lifts being contractible.

    : Discrete-fibration
    → ∀ {x} {x'' : E.Ob[ x ]} (f' : Σ[ x' ∈ E.Ob[ x ] ] (E.Hom[ ] x' x''))
    → (x'' ,') ≡ f'
  discrete→vertical-id disc {x'' = x''} f' =
    sym (lifts _ .paths (x'' ,')) ∙ lifts x'' .paths f'
    where open Discrete-fibration disc

We can use this fact in conjunction with the fact that all fibres are thin to show that every vertical morphism in a discrete fibration is invertible.

    : Discrete-fibration
    → ∀ {x} {x' x'' : E.Ob[ x ]} → (f' : E.Hom[ ] x' x'') → is-invertible↓ f'
  discrete→vertical-invertible disc {x' = x'} {x'' = x''} f' =
      (subst (λ x' → E.Hom[ ] x'' x') x''≡x'')
      (to-pathp (discrete→thin-fibres _ disc _ _))
      (to-pathp (discrete→thin-fibres _ disc _ _))
      x''≡x' : x'' ≡ x'
      x''≡x' = ap fst (discrete→vertical-id disc (x' , f'))

Discrete fibrations are presheaves🔗

As noted earlier, a discrete fibration over B\mathcal{B} encodes the same data as a presheaf on B\mathcal{B}. First, let us show that we can construct a presheaf from a discrete fibration.

  discrete→presheaf : ∀ {o' ℓ'} (E : Displayed B o' ℓ') → Discrete-fibration E
                    → Functor (B ^op) (Sets o')
  discrete→presheaf {o' = o'} E disc = psh where
    module E = Displayed E
    open Discrete-fibration disc

For each object in X:BX : \mathcal{B}, we take the set of objects EE that lie over XX. The functorial action of f : Hom X Y is then constructed by taking the domain of the lift of f. Functoriality follows by uniqueness of the lifts.

    psh : Functor (B ^op) (Sets o')
    psh .Functor.F₀ X = el E.Ob[ X ] (fibre-set X)
    psh .Functor.F₁ f X' = lifts f X' .centre .fst
    psh .Functor.F-id = funext λ X' → ap fst (lifts X' .paths (X' ,'))
    psh .Functor.F-∘ {X} {Y} {Z} f g = funext λ X' →
      let Y' : E.Ob[ Y ]
          Y' = lifts g X' .centre .fst

          g' : E.Hom[ g ] Y' X'
          g' = lifts g X' .centre .snd

          Z' : E.Ob[ Z ]
          Z' = lifts f Y' .centre .fst

          f' : E.Hom[ f ] Z' Y'
          f' = lifts f Y' .centre .snd
      in ap fst (lifts (g B.∘ f) X' .paths (Z' , (g' E.∘' f' )))

To construct a discrete fibration from a presheaf PP, we take the (displayed) category of elements of PP. This is a natural choice, as it encodes the same data as PP, just rendered down into a soup of points and bits of functions. Discreteness follows immediately from the contractibilty of singletons.

  presheaf→discrete : ∀ {Îș} → Functor (B ^op) (Sets Îș)
                    → ÎŁ[ E ∈ Displayed B Îș Îș ] Discrete-fibration E
  presheaf→discrete {Îș = Îș} P = ∫ B P , discrete where
    module P = Functor P

    discrete : Discrete-fibration (∫ B P)
    discrete .Discrete-fibration.fibre-set X =
      P.₀ X .is-tr
    discrete .Discrete-fibration.lifts f P[Y] =
      contr (P.₁ f P[Y] , refl) Singleton-is-contr

We conclude by proving that the two maps defined above are, in fact, inverses. Most of the complexity is in characterising paths between displayed categories, but that doesn’t mean that the proof here is entirely trivial, either. Well, first, we note that one direction is trivial: modulo differences in the proofs of functoriality, which do not matter for identity, turning a functor into a discrete fibration and back is the identity.

  open is-iso

  presheaf≃discrete : ∀ {Îș} → is-iso (presheaf→discrete {Îș = Îș})
  presheaf≃discrete .inv  (d , f) = discrete→presheaf d f
  presheaf≃discrete .linv x       = Functor-path (λ _ → n-path refl) λ _ → refl

The other direction is where the complication lies. Given a discrete fibration PXP \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} X, how do we show that ∫P≡P\int P \equiv P? Well, by the aforementioned characterisation of paths in displayed categories, it’ll suffice to construct a functor (∫P)→P(\int P) \to P (lying over the identity), then show that this functor has an invertible action on objects, and an invertible action on morphisms.

  presheaf≃discrete .rinv (P , p-disc) = ÎŁ-prop-path hl âˆ«â‰Ądx where
    open Discrete-fibration p-disc
    open Displayed-functor
    open Displayed P

The functor will send an object cxc \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} x to that same object cc; This is readily seen to be invertible. But the action on morphisms is slightly more complicated. Recall that, since PP is a discrete fibration, every span bâ€Čb←fab' \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} b \xleftarrow{f} a has a contractible space of Cartesian lifts (aâ€Č,fâ€Č)(a', f'). Our functor must, given objects aâ€Čâ€Č,bâ€Ča'', b', a map f:a→bf : a \to b, and a proof that aâ€Čâ€Č=aâ€Ča'' = a', produce a map aâ€Čâ€Č→fba'' \to_f b — so we can take the canonical fâ€Č:aâ€Č→fbf' : a' \to_f b and transport it over the given aâ€Čâ€Č=aâ€Ča'' = a'.

    pieces : Displayed-functor (∫ B (discrete→presheaf P p-disc)) P Id
    pieces .F₀' x = x
    pieces .F₁' {f = f} {a'} {b'} x =
      subst (λ e → Hom[ f ] e b') x $ lifts f b' .centre .snd

This transport threatens to throw a spanner in the works, since it is an equation between objects (over aa). But since PP is a discrete fibration, the space of objects over aa is a set, so this equation can’t ruin our day. Directly from the uniqueness of (aâ€Č,fâ€Č)(a', f') we conclude that we’ve put together a functor.

    pieces .F-id' = from-pathp (ap snd (lifts _ _ .paths _))
    pieces .F-∘' {f = f} {g} {a'} {b'} {c'} {f'} {g'} =
      ap (λ e → subst (λ e → Hom[ f B.∘ g ] e c') e
            (lifts _ _ .centre .snd)) (fibre-set _ _ _ _ _)
      ∙ from-pathp (ap snd (lifts _ _ .paths _))

It remains to show that, given a map aâ€Čâ€Č→ba'' \to b (and the rest of the data aa, bb, f:a→bf : a \to b, bâ€Čbb' \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} b), we can recover a proof that aâ€Čâ€Ča'' is the chosen lift aâ€Ča'. But again, lifts are unique, so this is immediate.

    âˆ«â‰Ądx : ∫ B (discrete→presheaf P p-disc) ≡ P
    âˆ«â‰Ądx = Displayed-path pieces (λ _ → id-equiv) (is-iso→is-equiv p) where
      p : ∀ {a b} {f : B.Hom a b} {a'} {b'} → is-iso (pieces .F₁' {f = f} {a'} {b'})
      p .inv f  = ap fst $ lifts _ _ .paths (_ , f)
      p .rinv p = from-pathp (ap snd (lifts _ _ .paths _))
      p .linv p = fibre-set _ _ _ _ _

We must additionally show that the witness that PP is a discrete fibration will survive a round-trip through the type of presheaves, but this witness lives in a proposition (it is a pair of propositions), so it survives automatically.

    private unquoteDecl eqv = declare-record-iso eqv (quote Discrete-fibration)
    hl : ∀ x → is-prop _
    hl x = is-hlevel≃ 1 (Iso→Equiv eqv) $
      ×-is-hlevel 1 (Π-is-hlevel 1 λ _ → is-hlevel-is-prop 2) hlevel!