Zulip Chat Archive

Stream: maths

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

view this post on Zulip 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:Πf,g:Πx:AC(x)(Πx,y:Af(x)=C(x)g(x))f=Πx:AC(x)gequal: \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) f(x) =_{C(x)} g(x) and I want to show that f=Πx:AC(x)g f =_{\Pi_{x:A} C(x)} g ?

view this post on Zulip Johan Commelin (Oct 14 2020 at 09:28):

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

view this post on Zulip 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.

view this post on Zulip 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