In homotopy type theory, why is function extensionality usually considered an axiom? My understanding is that function extensionality follows from univalence. But I often see both function extensionality and univalence assumed as axioms, e.g., here. Wouldn't it be better to have fewer axioms and postulate univalence only, treating funext as a theorem?
 A: Since the link you provided is specifically to the HoTT Coq library, I will answer why things are done the way they are in that library.  In that library, neither funext nor univalence are assumed as global axioms (i.e. with Coq's Axiom command).  The file you linked to is provided for the convenience of users of the library who want to assume such an axiom globally, but within the library we do not assume either of them globally.  Instead we track which theorems depend on which of them by using a dummy typeclass; thus a theorem that depends on funext would be written
Theorem foo `{Funext} (x : A) : B.

while a theorem that depends on univalence would be written
Theorem bar `{Univalence} (x : A) : B.

Of course, since univalence implies funext, any theorem that depends on univalence can also use funext, but not conversely.  The reason for doing this is that we want to be able to see in the type of a theorem which axioms it depends on (rather than having to Print Assumptions).
You say "it's hard to imagine doing HoTT without univalence", but it's surprising how much abstract synthetic homotopy theory does not depend on univalence.  This is useful to know because there are many more models of funext than there are of univalence: essentially any locally cartesian closed ($\infty$-)category models type theory with funext, while only $\infty$-toposes model univalence.
In other contexts, a reason one might treat these axioms separately is pedagogical.  For instance, in the HoTT Book we introduced function extensionality before univalence, considering it as simpler and easier to understand, and then proved later that the former follows from the latter.  Introductory textbooks on set theory often do similarly with the separation and replacement axioms that Zhen mentioned in a comment.
