The most famous example of incompatible axioms is (I think) axiom K and univalence. Axiom K makes it easier to pattern match (à la Agda) and univalence is getting more popular as it is supposed to make formal proofs closer to usual mathematics. Equations https://github.com/mattam82/Coq-Equations is an example of plugin that used to rely heavily on axiom K and has been changed to be configurable (and thus usable in a HoTT / UniMath context).
A famous of axiom-free library is the math-comp library https:// github.com/math-comp/math-comp, where booleans are used to represent decidable properties instead. And yet, this library is mostly designed to do maths.
On the other hand, there are examples of libraries choosing to adopt classical axioms and to assume them. The best example is Arthur Charguéraud’s TLC library https://gitlab.inria.fr/charguer/tlc which uses quite strong classical axioms (including the axiom of indefinite description, which is also something that can usually be found in HOL theorem provers). Another (heavily relied on) example is the Reals library in Coq’s standard library. It was recently suggested to split the axioms of the Reals library in two parts: constructive and classical layers. I personally regret that Coq doesn’t have a sort of interface files + virtual library mechanism, i.e. the file containing the Reals axioms could be “instantiated”, if the user wants to, by an actual implementation and proofs of these axioms.
The axiom of functional extensionality is I think one of the most easily admitted axiom. It is a consequence of many others, including the axiom of univalence.