I have the following code:
constant B:Type constant A:Type constant P:B → A → Prop definition F:Type := B → A axiom a1: ∀b:B, ∃a:A, P b a theorem thrm1: ∀b:B, ∀a:A, (P b a) → ∃f:F, (f b = a) ∧ ∀bb:B, P bb (f bb) := λ b:B, λ a:A, assume h: P b a, sorry
It should be almost trivial to prove this, yet I'm not sure how to do it in type theory. Perhaps my intuition is implicitly based on some axiom from classical logic?
The informal argument is as follows: If for a particular $b$ and $a$ the property $P \; b\; a$ holds, then we can consider the equivalence class of functions $f:B \to A$ for which $f \; b= a$. Moreover, since for any $b\in B$, there is an $a\in A$ such that $P \; b \; a$ holds, we can simply pick from this the function $f$ which also assigns for every other $b$ some $a$ such that $P\; b\; a$ holds. Such a function must always exist, since we can freely adjust the output for each input independently.
But how do we formalize this argument in type theory?