open import Cat.Displayed.Cartesian.Discrete
open import Cat.Displayed.Functor
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Cartesian
import Cat.Displayed.Reasoning
import Cat.Displayed.Morphism
import Cat.Reasoning

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 is said to be a right fibration if every morphism in 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 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 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 of is obviously cartesian, so it suffices to show that there is a vertical retraction To construct this retraction, we shall factorize over which yields a vertical morphism By our hypotheses, is invertible, and thus is a retraction. What remains to be shown is that the inverse to factors and this follows from the factorisation of and the fact that 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'