
> 
> Is there a standard method for showing that a functor $F:\mathcal{C}\to\mathcal{D}$ is a fibration, aside from constructing a cleavage?
> 
> 
> 


In the proof of the Grothendieck construction, the fibration we obtain from an indexed category $\Psi:\mathcal{B}^{op}\to\mathfrak{Cat}$ is automatically cloven since we're constructing a specific Cartesian arrow $(u,1\_{\Psi(u)(Y)})$ for each arrow $u:I\to J\in\mathcal{B}$ and object $(J,Y)\in\int\Psi$ above $J$.


Every time I want to show that a functor is a fibration, I end up constructing Cartesian arrows parametrized as above and thusly showing that it's a cloven fibration -- is this by necessity?


Any method of showing that a functor is a fibration without choosing a cleavage is welcome, but in particular something similar to the adjoint functor theorem for fibrations would be cool. That is, a statement along the lines of



> 
> If $F:\mathcal{C}\to\mathcal{D}$ is a functor and $\mathcal{C}$ is blah and $\mathcal{D}$ is bloop and $F$ preserves/reflects blorps then $F$ is a fibration.
> 
> 
> 



Can we show that a functor is a fibration without choosing a cleavage?
Just as an example, given a category $\mathcal{C}$ with finite limits, showing $\mathrm{cod}\colon \mathcal{C}^\mathbf{2}\to \mathcal{C}$ is a fibration does not involve choosing a cleaving. All that you need is that a pullback square *exists* for each piece of relevant data. A cleaving would be a specified choice of pullback square for each cospan.


More generally, any time that one uses a universal property to show the existence of a cartesian lift, then you aren't exactly constructing a cleaving, since you don't have to specify precisely which item with the universal property you are using.


I'm thinking also of the result at [the nLab page on Grothendieck fibrations](https://ncatlab.org/nlab/show/Grothendieck+fibration#in_terms_of_adjoints):



> 
> A functor $p \colon E \to B$ is a cloven fibration if and only if the canonical functor $i \colon E \to B\downarrow p$ has a right adjoint $r$ in $\mathbf{Cat} / B$.
> 
> 
> 


where instead of asking that that the adjoint is given, one just has that an adjoint functor theorem is applicable. "Constructing" the adjoint is (probably) equivalent to choosing a cleaving.


