## Stream: maths

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

#### Golol (Oct 14 2020 at 09:26):

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 (Oct 14 2020 at 09:28):

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

#### Golol (Oct 14 2020 at 09:36):

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 (Oct 14 2020 at 10:11):

@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

Last updated: May 14 2021 at 19:21 UTC