Essential and lax fibres

Stream: Displayed Categories

[Sina Hazratpour 𓃵]

This issue was raised, so just putting it here for anyone else who might have the same question.

In Displayed.Basic.Lean we have essential iso and lax displayed structures associated to a functor. If I remember correctly the idea here was to get Street fibrations and all functors via the corresponding essential and lax displayed structures which have enough Cartesian lifts. But this was not fully proved, and would be great for instance to show that we actually obtain all functors as "lax fibrations"

[Fernando Chu]

Could you please sketch the main ideas of lax fibrations? Like what is the definition, and sketch how to obtain a functor from it