The intuition behind the type theoretical axiom of choice is that the choice is given by a (hypothetical) proof of the "∀x ∈ A ∃ y …"-statement. The constructive interpretation of the statement is precisely that there is such a choice function — so it becomes a tautology (provable without any extra axioms). And I believe that agrees with the naive intuition one has why the axiom of choice is true. The problem is when the logic allows proofs (or semantics) which does not preserve the equality. In type theory the equality is intensional and thus preserved by structure.
Unique choice is besides the point here. There may be a unique function, or there may be many. The intuition of choosing is the same.
I also have no issue with B-T, as I expect weird consequences of ZFC; the axioms and logic being so profoundly non-constructive and removed from my intuitions in the first place. That said, I would not deny the set-theorists enjoying their theory, I merely observe that there are subtle things their theories fail to describe.
Type theory does not shout anything, but is carefully constructed from the needs of its creators. Some people want to extract algorithms from their proofs, or want to prove that their algorithms are correct. And if you want this, the nuances of type theory are actually nuances of things you care about — algorithms and proofs. If these are not among your interests, then type theory is not for you. Thats fine, I am sure you have other interests.
Unique choice is besides the point here. There may be a unique function, or there may be many. The intuition of choosing is the same.
I also have no issue with B-T, as I expect weird consequences of ZFC; the axioms and logic being so profoundly non-constructive and removed from my intuitions in the first place. That said, I would not deny the set-theorists enjoying their theory, I merely observe that there are subtle things their theories fail to describe.
Type theory does not shout anything, but is carefully constructed from the needs of its creators. Some people want to extract algorithms from their proofs, or want to prove that their algorithms are correct. And if you want this, the nuances of type theory are actually nuances of things you care about — algorithms and proofs. If these are not among your interests, then type theory is not for you. Thats fine, I am sure you have other interests.