Add equifibered dependent span diagrams and improve universe polymorphism for descent data of pushouts

[fredrik-bakke]

• [X] Improve universe polymorphism of descent data for pushouts
• [X] Define equifibered dependent span diagrams
• [ ] ~State flattening lemma for equifibered dependent span diagrams~
• [ ] ~Prove flattening lemma for equifibered dependent span diagrams~

Copy of #1365