Coded up a form of the Grothendieck construction: https://github.com/jcreedcmu/HoTT-Agda/blob/experimental/Jcreed/Grothendieck.agda
