module Cat.Displayed.Cartesian.Right {o β o' β'} {β¬ : Precategory o β} (β° : Displayed β¬ o' β') where open Cat.Reasoning β¬ open Displayed β° open Cat.Displayed.Cartesian β° open Cat.Displayed.Morphism β° open Cat.Displayed.Reasoning β°

# Right fibrationsπ

A cartesian
fibration
$E$
is said to be a **right fibration** if every morphism in
$E$
is cartesian.

record Right-fibration : Type (o β β β o' β β') where no-eta-equality field is-fibration : Cartesian-fibration cartesian : β {x y} {f : Hom x y} β β {x' y'} (f' : Hom[ f ] x' y') β is-cartesian f f' open Cartesian-fibration is-fibration public

One notable fact is every vertical morphism of a right fibrations is invertible. In other words, if $E$ is a right fibration, then all of its fibre categories are groupoids. This follows directly from the fact that vertical cartesian maps are invertible.

right-fibrationβvertical-invertible : Right-fibration β β {x} {x' x'' : Ob[ x ]} β (f' : Hom[ id ] x' x'') β is-invertibleβ f' right-fibrationβvertical-invertible rfib f' = vertical+cartesianβinvertible (Right-fibration.cartesian rfib f')

More notably, this is an exact characterization of categories fibred in groupoids! If $E$ is a cartesian fibration where all vertical morphisms are invertible, then it must be a right fibration.

vertical-invertible+fibrationβright-fibration : Cartesian-fibration β (β {x} {x' x'' : Ob[ x ]} β (f' : Hom[ id ] x' x'') β is-invertibleβ f') β Right-fibration vertical-invertible+fibrationβright-fibration fib vert-inv .Right-fibration.is-fibration = fib vertical-invertible+fibrationβright-fibration fib vert-inv .Right-fibration.cartesian {x = x} {f = f} {x' = x'} {y' = y'} f' = f-cart where open Cartesian-fibration fib open Cartesian-lift renaming (x' to x-lift)

To see this, recall that cartesian morphisms are stable under vertical retractions. The cartesian lift $f_{β}$ of $f$ is obviously cartesian, so it suffices to show that there is a vertical retraction $x_{β}βx_{β²}.$ To construct this retraction, we shall factorize $f_{β²}$ over $fβid;$ which yields a vertical morphism $i_{β}:x_{β²}βx_{β}.$ By our hypotheses, $i_{β}$ is invertible, and thus is a retraction. What remains to be shown is that the inverse to $i_{β}$ factors $f_{β²}$ and $f_{β};$ this follows from the factorisation of $f_{β²}$ and the fact that $i_{β}$ is invertible.

x* : Ob[ x ] x* = has-lift f y' .x-lift f* : Hom[ f ] x* y' f* = has-lift f y' .lifting module f* = is-cartesian (has-lift f y' .cartesian) i* : Hom[ id ] x' x* i* = f*.universal' (idr f) f' module i*-inv = is-invertible[_] (vert-inv i*) i*β»ΒΉ : Hom[ id ] x* x' i*β»ΒΉ = i*-inv.inv' factors : f' β' i*β»ΒΉ β‘[ idr f ] f* factors = to-pathpβ» $ f' β' i*β»ΒΉ β‘β¨ shiftr _ (pushl' _ (symP $ f*.commutesp (idr f) f') {q = ap (f β_) (sym (idl _))}) β©β‘ hom[] (f* β' i* β' i*β»ΒΉ) β‘β¨ weave _ (elimr (idl id)) _ (elimr' _ i*-inv.invl') β©β‘ hom[] f* β f-cart : is-cartesian f f' f-cart = cartesian-vertical-retraction-stable (has-lift f y' .cartesian) (inverses[]βfrom-has-section[] i*-inv.inverses') factors

As a corollary, we get that all discrete fibrations are right fibrations. Intuitively, this is true, as sets are 0-groupoids.

discreteβright-fibration : Discrete-fibration β° β Right-fibration discreteβright-fibration dfib = vertical-invertible+fibrationβright-fibration (discreteβcartesian β° dfib) (discreteβvertical-invertible β° dfib)

## Fibred functors and right fibrationsπ

As every map in a right fibration is cartesian, every displayed functor into a right fibration is automatically fibred.

functor+right-fibrationβfibred : β {oβ ββ oβ' ββ'} β {π : Precategory oβ ββ} β {β± : Displayed π oβ' ββ'} β {F : Functor π β¬} β Right-fibration β (F' : Displayed-functor β± β° F) β Fibred-functor β± β° F functor+right-fibrationβfibred rfib F' .Fibred-functor.disp = F' functor+right-fibrationβfibred rfib F' .Fibred-functor.F-cartesian f' _ = Right-fibration.cartesian rfib (Fβ' f') where open Displayed-functor F'

Specifically, this implies that all displayed functors into a discrete fibrations are fibred. This means that we can drop the fibred condition when working with functors between discrete fibrations.

functor+discreteβfibred : β {oβ ββ oβ' ββ'} β {π : Precategory oβ ββ} β {β± : Displayed π oβ' ββ'} β {F : Functor π β¬} β Discrete-fibration β° β (F' : Displayed-functor β± β° F) β Fibred-functor β± β° F functor+discreteβfibred disc F' = functor+right-fibrationβfibred (discreteβright-fibration disc) F'