6
$\begingroup$

I'm currently reading "Revisiting the categorical interpretation of dependent type theory" and they give a very terse description of the Giraud-Benabou construction:

For a fibration $p : \mathbb E \to \mathbb B $, the fibration $Rp : R\mathbb E \to \mathbb B$ is defined by

  • Obj $R\mathbb E$ is the set of pairs $(X,\phi)$ where $X \in \mathbb B$ and $\phi : \mathrm{dom}_X \to p$ is a morphism of fibrations from the restriction of the domain fibration to the slice categories $\mathrm{dom}_X: \mathbb B / X \to \mathbb B$. $Rp$ is the first projection.
  • $\mathrm{Hom}((X, \phi),(Y, \psi))$ consists of pairs $(t,\mu)$ where $t : X \to Y$ and $\mu : \phi \to \psi \circ \mathrm{dom}_t$ over $\mathbb B$.

They then prove that this is a split fibration in a single line ("for $t:X \to Y$, set $\phi [t] = \phi \circ \mathrm{dom}_X$, ie. $\phi[t](s) = \phi(t \circ s)$ for all $s:Z \to X$, and $t_\phi = (t,id)$. Moreover, $Rp$ is split by the associativity of composition in $\mathbb B$"), and it isn't clear to me exactly what the relation between $Rp$ and $p$ is.

Questions:

  1. Is there a slightly less terse reference for this that isn't buried somewhere in an almost 500 page book on non-abelian cohomology written in French?
  2. What exactly is the relation between $Rp$ and $p$?
  3. What's the intuition behind this construction? If I were trying to create a split fibration from a fibration, why might I think to do this?
  4. What does this do to the codomain fibration over Set? Does this have a simple description?
$\endgroup$

1 Answer 1

4
$\begingroup$

Section 2.2 of The local universes model gives a possible answer to (2) and (3): $R$ (or $(-)_*$ in their notation) is a right adjoint to the forgetful functor from split fibrations to non-split fibrations. Their description is no less terse, but perhaps beta-reduced a bit more:

An object of $T_*$ over $\Gamma\in C$ consists of an object $A$ of $T(Γ)$, together with for each $f : \Gamma'\to \Gamma$ some cartesian lifting $\bar{f} : A_f \to A$, such that $A_{1_\Gamma} = A$, $\bar{1_\Gamma} = 1_A$.

In the case of the codomain fibration, this means that an object of $T_*$ is a morphism equipped with a chosen pullback square along every morphism into its codomain, such that the chosen pullback along the identity is the identity square.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.