On Mon, Apr 15, 2013 at 5:59 PM, Altenkirch Thorsten <psztxa at exmail.nottingham.ac.uk> wrote: > What I mean is the following: there is an equivalence between > A -> Set > and > Sigma[ X : Set ] X -> A > > this is a trivial instance of the Grothendieck construction between > families and fibrations. I used UA to prove this, did you see a simpler construction?