How to prove this obvious theorem in type theory (LEAN prover)
If you used Type instead of Prop in the definition of P, then you could easily extract from axiom a1 a function f such that ∀b:B, P b (f b). However, there would be no guarantee that this function would satisfy f b = a for any given a and b that satisfy P b a. Given a decidable equality on B, you could turn the function that a1 gives you into your desired function via λ bb:B, if bb == b then a else fst (a1 bb). Without decidable equality, it's not clear how you would construct a function that you could prove would give a when given b.

As far as your informal argument, the problem is "picking" from the equivalence class. Constructive logic/type theory is compatible with everything being computable. (Formally, this is usually expressed via realizability.) To say that you can "pick" from an equivalence class subject to some constraints means you are providing an algorithm that can somehow "search" through (some representation of) the equivalence class and find an element that satisfies your constraints. However, you don't even know these types are computably enumerable. At any rate, "picking" is rarely "simple".

I'd have to look at the rules of LEAN to be sure, but with P going to Prop, you need the (real) Axiom of Choice to even get the function f at all before you ever got around to constraints. In fact, while I haven't thought about it too much, I believe the statement you give is equivalent to the (real) Axiom of Choice.