This is only somewhat related to the talk on category theory in Agda but sometimes I get the impression that there's a lot of proofs where people will be like "oh this relies on axiom K and proof irrelevance and blah blah blah" as an argument for why the proof is ungood but to me this feels more like an argument for why more type theories should have such axioms etc. (or at least the possibility to enable them)
There was probably a design decision somewhere to use those axioms because it simplified proofs etc. which means they were helpful in making proofs easier to write and understand
There's a lot of the "what's the smallest set of axioms we can work off of" that I feel like comes from set theory and it's a valid desire but adding justifiable, intuitive, and consistent (ofc) axioms should be just as valid for practical purposes