Characterization of various families over pushouts

[VojtechStep]

This PR characterizes (as in "provides the expected descent data and shows equivalence") the following type families over pushouts:

• families of function types, x ↦ P x → Q x
• families of equivalence types, x ↦ P x ≃ Q x
• families of based identity types at x₀ : X, x ↦ x₀ = x

It also introduces sections of descent data, which correspond to sections of the associated type family