equality of lambda-abstractions in HoTT

Stream: maths

[Matt Yan]

(deleted)

[Matt Yan]

11BD39D9-8178-4A77-A17E-C56FBD72DD74.jpg

[Adam Topaz]

I don't know what the question was, but we have docs#funext which IIRC is proved via the existence of quotients in lean.

[Matt Yan]

typing on my phone and can't really embed an image nicely in text sorry :)

[Matt Yan]

It's more of a HoTT question, I'm at the early chapters of HoTT, I find it a huge jump from this definition to "it shows that f is uniquely determined by its values".
In order to reach the conclusion, it seems that this is implied (correct me if I'm wrong) $$ \lamda x: A. \Phi \equiv \lamda x: B. \Theta $$ as long as $A = B$ and that for every $x \in A$ subsititution in $\Phi , \Theta$ result in equal values...additionally changing the temporary variable doesn't produce a new lamda-abstraction.

[Reid Barton]

Is this the HoTT book?

[Matt Yan]

the equality of lamda expressions seems to be meta-HoTT but I think definitely worth mentioning

[Reid Barton]

I just want to know the context of what you're reading so I can know what kind of answer is sensible.

[Matt Yan]

@Reid Barton yes, section 1.2 on functions

[Reid Barton]

So this is a kind of "definitional" (maybe the HoTT book says "judgmental") version of "a function is determined by its values".

[Reid Barton]

More specifically, suppose that $x : A \vdash f[x] \equiv g[x] : B$. (Here $f[x]$ and $g[x]$ are terms with free variable $x$, i.e., $x : A \vdash f[x] : B$ and $x : A \vdash g[x] : B$. Also, we could allow $B$ to depend on $x$ but let's not for simplicity.)

[Reid Barton]

Then we have $\vdash f \equiv (\lambda x. f[x]) \equiv (\lambda x. g[x]) \equiv g : A \to B$.

[Reid Barton]

Actually now I realize this is a confusing way to present it.

[Reid Barton]

Instead of saying $f[x]$ and $g[x]$ are terms with free variable $x$, let me instead say that $f$ and $g$ were terms of type $A \to B$.

[Reid Barton]

Then if $x : A \vdash f(x) \equiv g(x) : B$, then we have $\vdash f \equiv g : A \to B$ by that argument.

[Reid Barton]

I think this is what they mean by saying "a function is determined [up to judgmental equality] by its values [up to judgmental equality]". At this point they probably haven't introduced any other notion of equality yet.

[Reid Barton]

What does not follow is that for the typal equality/path type/what we normally think of as equality $=$, a function is determined (up to $=$) by its values (up to $=$)

[Matt Yan]

Thanks! I understand your idea now, and it seems to me you are suggesting that lamda-abstraction like $\lambda x : A. f(x)$ is just syntactic sugar of something like $x: A \vdash f(x): B$

[Matt Yan]

Then if $x : A \vdash f(x) \equiv g(x) : B$, then we have $\vdash f \equiv g : A \to B$ by that argument.

This is exactly what I think is missing in the book.

[Matt Yan]

I think it can be expressed using only the lambda-abstraction language, could be something along the lines of:
"for functions $f$ and $g$, $\lambda x. f(x) = \lambda x. g(x)$ if and only if $a: A$ implies $\lambda x. f(x) (a) = \lambda x. g(x) (a)$

[Matt Yan]

noting that a function has two kinds of constructors, with certain lambda-abstractions being one of them and the other being construction by definiton (named functions). the above is really just a propositional uniqueness of functions contructed by lambda-abstructions. And the definitional equality in the screenshot serves as the bridge between the uniqueness of named functions and the uniqueness of lambda functions