(Ho)TT question on showing functions equal in identity type

Stream: maths

[Golol]

Hi, I want to learn HoTT at the moment but I think this question is strictly type theory.
Tl;dr: Is this type is inhabited? (Given C is a type family over A)

$$equal: \Pi_{f,g : \Pi_{x:A} C(x)} \left( \Pi_{x,y:A} f(x) =_{C(x)} g(x) \right) \longrightarrow f =_{\Pi_{x:A} C(x)} g$$

There is an equality principle for functions saying that they are uniquely defined by their values in the sense of judgmental equality. But what if their values are only equal in the sense that
$f(x) =_{C(x)} g(x)$ and I want to show that $f =_{\Pi_{x:A} C(x)} g$?

[Johan Commelin]

Isn't this just function extensionality? I guess I'm missing something.

[Golol]

Thanks, it seems like that's it. It only gets introduced later in the text I'm reading (HoTT) book. So the function I am asking for exists basically as an axiom.

[Mario Carneiro]

@Golol In HoTT, function extensionality is a consequence of univalence, although it is often considered as a separate axiom. In lean, function extensionality is derived from the existence of quotient types