open import Cat.Displayed.Base
open import Cat.Prelude

module Cat.Displayed.Cartesian
  {o β„“ oβ€² β„“β€²} {B : Precategory o β„“} (E : Displayed B oβ€² β„“β€²) where

open Precategory B
open Displayed E

Cartesian morphisms and FibrationsπŸ”—

While displayed categories give the essential framework we need to express the idea of families of categories indexed by a category, they do not quite capture the concept precisely. The problem is that while a category E\ca{E} displayed over B\ca{B} does indeed give a collection of fibre categories Eβˆ—(x)\ca{E}^*(x), this assignment isn’t necessarily functorial!

More precisely, we should have that a collection of categories, indexed by a category, should be a pseudofunctor B→Cat\ca{B} \to \Cat, where Cat\Cat is a bicategory of categories. It turns out that we can characterise this assignment entirely in terms of the displayed objects and morphisms in E\ca{E}!

Fix an arrow f:aβ†’bf : a \to b in the base category B\ca{B}, an object aβ€²a' over aa (resp. bβ€²b' over bb), and an arrow fβ€²:aβ€²β†’fbβ€²f' : a' \to_f b' over ff. We say that fβ€²f' is cartesian if, up to very strong handwaving, it fits into a β€œpullback diagram”. The barred arrows with triangle tips here indicate the β€œprojection” from a displayed object to its base, and so are implicit in the type dependency.

record
  Cartesian {a b aβ€² bβ€²} (f : Hom a b) (fβ€² : Hom[ f ] aβ€² bβ€²) : Type (o βŠ” β„“ βŠ” oβ€² βŠ” β„“β€²)
  where
  no-eta-equality

More specifically, let u:Bu : \ca{B} and uβ€²u' be over uu, and suppose that we have a map m:uβ†’am : u \to a (below, in violet), and a map hβ€²:uβ€²β†’mbβ€²h' : u' \to_m b' lying over the composite fmfm (in red). The universal property of a Cartesian map says that we have a universal factorisation of hβ€²h' through a map uβ€²β†’aβ€²u' \to a' (in green, marked βˆƒ!\exists!).

  field
    universal : βˆ€ {u uβ€²} (m : Hom u a) (hβ€² : Hom[ f ∘ m ] uβ€² bβ€²) β†’ Hom[ m ] uβ€² aβ€²
    commutes  : βˆ€ {u uβ€²} (m : Hom u a) (hβ€² : Hom[ f ∘ m ] uβ€² bβ€²)
              β†’ fβ€² βˆ˜β€² universal m hβ€² ≑ hβ€²
    unique    : βˆ€ {u uβ€²} {m : Hom u a} {hβ€² : Hom[ f ∘ m ] uβ€² bβ€²}
              β†’ (mβ€² : Hom[ m ] uβ€² aβ€²) β†’ fβ€² βˆ˜β€² mβ€² ≑ hβ€² β†’ mβ€² ≑ universal m hβ€²

Given a β€œright corner” like that of the diagram below, and note that the input data consists of aa, bb, f:aβ†’bf : a \to b and bβ€²b' over aa,

we call an object aβ€²a' over aa together with a Cartesian arrow fβ€²:aβ€²β†’bβ€²f' : a' \to b' a Cartesian lift of ff. Cartesian lifts, defined by universal property as they are, are unique when they exist, so that β€œhaving Cartesian lifts” is a property, not a structure.

record
  Cartesian-lift {x y} (f : Hom x y) (yβ€² : Ob[ y ]) : Type (o βŠ” β„“ βŠ” oβ€² βŠ” β„“β€²)
  where
  no-eta-equality
  field
    {xβ€²}      : Ob[ x ]
    lifting   : Hom[ f ] xβ€² yβ€²
    cartesian : Cartesian f lifting
  open Cartesian cartesian public

We note that the classical literature often differentiates between fibrations β€” those displayed categories for which there exist Cartesian lifts for every right corner β€” and cloven fibrations, those for which the Cartesian lifts are β€œalgebraic” in a sense. This is because, classically, essentially unique means that there are still some choices to be made, and invoking the axiom of choice makes an β€œarbitrary” set of such choices. But, in the presence of univalence, there is exactly one choice to be made, that is, no choice at all. Thus, we do not dwell on the distinction.

record Cartesian-fibration : Type (o βŠ” β„“ βŠ” oβ€² βŠ” β„“β€²) where
  no-eta-equality
  field
    has-lift : βˆ€ {x y} (f : Hom x y) (yβ€² : Ob[ y ]) β†’ Cartesian-lift f yβ€²

A Cartesian fibration is a displayed category having Cartesian lifts for every right corner.

Why?πŸ”—

Admittedly, the notion of Cartesian morphism is slightly artificial. It arises from studying the specific properties of the pullback functors fβˆ—:C/yβ†’C/xf^* : \ca{C}/y \to \ca{C}/x which exist in a category of pullbacks, hence the similarity in universal property!

In fact, the quintessential example of a Cartesian fibration is the codomain fibration, which is a category displayed over C\ca{C}, where the fibre over xx is the slice category C/x\ca{C}/x. We may investigate further (to uncover the name β€œcodomain”): the total space of this fibration is the arrow category Arr(C)\id{Arr}(\ca{C}), and the projection functor is the codomain functor Arr(C)β†’C\id{Arr}(\ca{C}) \to \ca{C}.

This displayed category extends to a pseudofunctor exactly when C\ca{C} has all pullbacks, because in a world where the vertical arrows are β€œjust” arrows, a Cartesian morphism is exactly a pullback square.

Other examples exist:

  • The family fibration exhibits any category C\ca{C} as displayed over Sets\sets. The fibres are functor categories (with discrete domains), reindexing is given by composition.
  • The category of modules is fibred over the category of rings. The fibre over a ring RR is the category of RR-modules, Cartesian lifts are given by restriction of scalars.