Yes, this is provable—indeed, it is provable by reflexivity. This is because Coq has eta-equality of functions built in. Definitional equality also has a congruence rule for lambdas, which does look kind of like function extensionality, but which exists at the judgmental level, and is about definitional equality rather than propositional equality. This does not allow us to prove function extensionality, because the premise in function extensionality is a propositional equality and not a definitional one. In the presence of an equality reflection rule, this would furnish a proof of function extensionality, which is why type systems with equality reflection, eta for functions, and defeq congruence for functions validate function extensionality.

Yes, this is provable—indeed, it is provable by reflexivity. This is because Coq has eta-equality of functions built into its notion of definitional equality. Definitional equality also has a congruence rule for lambdas, which does look kind of like function extensionality, but which exists at the judgmental level, and is about definitional equality rather than propositional equality. This does not allow us to prove function extensionality, because the premise in function extensionality is a propositional equality and not a definitional one. In the presence of an equality reflection rule, this would furnish a proof of function extensionality, which is why type systems with equality reflection, eta for functions, and defeq congruence for lambdas validate function extensionality.

Yes, this is provable—indeed, it is provable by reflexivity. This is because Coq has eta-equality of functions built in—we have a rule that looks like function extensionality, but which exists at the judgmental level, and is about definitional equality rather than propositional equality. This does not allow us to prove function extensionality, however, because the premise in function extensionality is a propositional equality and not a definitional one. In the presence of an equality reflection rule, this would furnish a proof of function extensionality, which is why type systems with equality reflection and eta for functions validate function extensionality.

Yes, this is provable—indeed, it is provable by reflexivity. This is because Coq has eta-equality of functions built in. Definitional equality also has a congruence rule for lambdas, which does look kind of like function extensionality, but which exists at the judgmental level, and is about definitional equality rather than propositional equality. This does not allow us to prove function extensionality, because the premise in function extensionality is a propositional equality and not a definitional one. In the presence of an equality reflection rule, this would furnish a proof of function extensionality, which is why type systems with equality reflection, eta for functions, and defeq congruence for functions validate function extensionality.