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
$\mathcal{B}$
is an alternate way of encoding a presheaf over
$\mathcal{B}$,
i.e., a functor
$\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'$ over $x$ equipped with maps $x' \to_f y'$.

module _ {o β o' β'} {B : Precategory o β} (E : Displayed B o' β') where private module B = Precategory B module E = Displayed E open Cat.Displayed.Morphism E open Displayed E

record Discrete-fibration : Type (o β β β o' β β') where field fibre-set : β x β is-set E.Ob[ x ] lifts : β {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' \to b'$ is the unique lift of $f$ along $b'$. We need to find a map $u' \to_m a'$. Observe that we have a right corner (with vertices $u$ and $a'$ over $a$), so that we an object $u_2$ over $u$ and map $l : u_2 \to_m a'$. Initially, this looks like it might not help, but observe that $u' \xrightarrow{h'}_{f \circ m} b'$ and $u_2 \xrightarrow{l}_{u} a' \xrightarrow{f'}_f b'$ are lifts of the right corner with base given by $u \to a \to b$, so that by uniqueness, $u2 = u'$: thus, we can use $l$ as our map $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
$x$
be an object of
$\mathcal{B}$.
Let us ponder the fibre
$\mathcal{E}^*(x)$:
we know that it is strict, since by assumption there is a *set*
of objects over
$x$.
Let us show also that it is thin: imagine that we have two parallel,
vertical arrows
$f, g : a \to_{\operatorname{id}_{}} b$.
These assemble into a diagram like

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

discreteβthin-fibres : β 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.id b) (a , f) (a , g) where open Discrete-fibration disc

## Morphisms in discrete fibrationsπ

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

discreteβvertical-id : Discrete-fibration β β {x} {x'' : E.Ob[ x ]} (f' : Ξ£[ x' β E.Ob[ x ] ] (E.Hom[ B.id ] x' x'')) β (x'' , E.id') β‘ f' discreteβvertical-id disc {x'' = x''} f' = sym (lifts B.id _ .paths (x'' , E.id')) β lifts B.id 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βvertical-invertible : Discrete-fibration β β {x} {x' x'' : E.Ob[ x ]} β (f' : E.Hom[ B.id ] x' x'') β is-invertibleβ f' discreteβvertical-invertible disc {x' = x'} {x'' = x''} f' = make-invertibleβ (subst (Ξ» x' β E.Hom[ B.id ] x'' x') x''β‘x' E.id') (to-pathp (discreteβthin-fibres _ disc _ _)) (to-pathp (discreteβthin-fibres _ disc _ _)) where 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 $\mathcal{B}$ encodes the same data as a presheaf on $\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 : \mathcal{B}$,
we take the set of objects
$E$
that lie over
$X$.
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 B.id X' .paths (X' , E.id')) 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 $P$, we take the (displayed) category of elements of $P$. This is a natural choice, as it encodes the same data as $P$, 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 $P \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} X$, how do we show that $\int P \equiv P$? Well, by the aforementioned characterisation of paths in displayed categories, itβll suffice to construct a functor $(\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 $c \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} x$ to that same object $c$; This is readily seen to be invertible. But the action on morphisms is slightly more complicated. Recall that, since $P$ is a discrete fibration, every span $b' \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} b \xleftarrow{f} a$ has a contractible space of Cartesian lifts $(a', f')$. Our functor must, given objects $a'', b'$, a map $f : a \to b$, and a proof that $a'' = a'$, produce a map $a'' \to_f b$ β so we can take the canonical $f' : a' \to_f b$ and transport it over the given $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
$a$).
But since
$P$
is a discrete fibration, the space of objects over
$a$
is a set, so this equation *canβt* ruin our day. Directly from
the uniqueness of
$(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'' \to b$ (and the rest of the data $a$, $b$, $f : a \to b$, $b' \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} b$), we can recover a proof that $a''$ is the chosen lift $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 $P$ 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!