Interesting examples of non-fibered prefibered cats?

Stream: maths

[Fernando Chu]

As the title asks, are there any interesting examples of non-fibered prefibered categories that arise in nature?
I'm using these definitions. I'm wondering because an alternative formulation of fibered cat would be just requiring that every morphism in the base category has an strongly cartesian lift, which (I'd guess) makes some things nicer?

[Joël Riou]

We have docs#CategoryTheory.Functor.IsFibered.of_exists_isStronglyCartesian

[Fernando Chu]

Yup, I know. Since (I'd guess) this is the actual thing you want to use (and prove), I was wondering if there is any benefit to having the pre-fibered concept

[Joël Riou]

In algebraic K-theory, there are technical homotopical results which are stated under the assumption that a certain functor is prefibered or precofibered.
Note also that in the 2-categorical context, we not only have pseudofunctors, but also lax functors, for which mapId or mapComp may not be isomorphisms.
Also, even in the process of verifying that a functor is fibered, it may occasionnaly be useful to prove first that it is prefibered (existence of adjoint functors), and then show they compose well.

[Fernando Chu]

I see, thanks a lot for the in depth examples and explanations!