open import Cat.Displayed.Instances.Elements
open import Cat.Displayed.Cartesian
open import Cat.Displayed.Functor
open import Cat.Instances.Functor
open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Displayed.Path
open import Cat.Prelude

import Cat.Displayed.Morphism

module Cat.Displayed.Cartesian.Discrete where

open Cartesian-fibration
open Cartesian-lift
open is-cartesian


# 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 is an alternate way of encoding a presheaf over i.e., a functor 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 over equipped with maps

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 is the unique lift of along We need to find a map Observe that we have a right corner (with vertices and over so that we an object over and map Initially, this looks like it might not help, but observe that and are lifts of the right corner with base given by so that by uniqueness, thus, we can use as our map

    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 be an object of Let us ponder the fibre we know that it is strict, since by assumption there is a set of objects over Let us show also that it is thin: imagine that we have two parallel, vertical arrows These assemble into a diagram like whence we see that and are both lifts for the lower corner given by lifting the identity map along β so, since lifts are unique, we have  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 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 encodes the same data as a presheaf on First, let us show that we can construct a presheaf from a discrete fibration.

module _ {o β} (B : Precategory o β)  where
private
module B = Precategory B

  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 we take the set of objects that lie over 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 we take the (displayed) category of elements of This is a natural choice, as it encodes the same data as 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 how do we show that Well, by the aforementioned characterisation of paths in displayed categories, itβll suffice to construct a functor (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 to that same object This is readily seen to be invertible. But the action on morphisms is slightly more complicated. Recall that, since is a discrete fibration, every span has a contractible space of Cartesian lifts Our functor must, given objects a map and a proof that produce a map β so we can take the canonical and transport it over the given

    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 But since is a discrete fibration, the space of objects over is a set, so this equation canβt ruin our day. Directly from the uniqueness of 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 (and the rest of the data we can recover a proof that is the chosen lift 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 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 = Isoβis-hlevel! 1 eqv