Zulip Chat Archive

Stream: general

Topic: equality of pi types?


view this post on Zulip Scott Buckley (Apr 26 2018 at 02:05):

Hi guys, I'm stuck trying to prove the following, which seems intuitively true to me:

((T1 -> T2) = (T1 -> T2')) ->
T2 = T2'

If it helps, I have instances of T1, (T1 -> T2), and (T1 -> T2'). cases on the equality hypotheses doesn't get me anywhere. I've tried building proofs various ways, but I always come back to the fundamental problem.

Is this even true?

Cheers,
Scott.
EDIT: fixed parameterisation

view this post on Zulip Mario Carneiro (Apr 26 2018 at 02:16):

Could you post a complete statement of the claim? In particular I want to know what are the types of T1, T2, and T2'

view this post on Zulip Mario Carneiro (Apr 26 2018 at 02:18):

If T2 and T2' are propositions, then this follows purely from the ancillary instances you have; from T1 and T1 -> T2 we find that T2 is true, and similarly T2' is true, so they are equal by propext

view this post on Zulip Mario Carneiro (Apr 26 2018 at 02:24):

Oh, I just realized that you are misinterpreting the binding power of equality over arrow - I think you wanted to say

(T1 -> T2) = (T1 -> T2') -> T2 = T2'

This claim is known as injectivity of pi, and it is independent in lean's axiomatization. I am pretty sure it's consistent with DTT but for some reason it's never assumed in any interactive proof assistant I know. (Warning: Also seemingly reasonable is injectivity on the left, i.e. (T1 -> T2) = (T1' -> T2) -> T1 = T1', but this one is false when T2 is a proposition.)

view this post on Zulip Mario Carneiro (Apr 26 2018 at 02:26):

Oh wait, even injectivity on the right is false when T1 is empty and T2 and T2' are propositions, i.e. (false -> false) = (false -> true) but false != true

view this post on Zulip Scott Buckley (Apr 26 2018 at 02:30):

Thanks Mario. Yeah you're right, I mis-parameterised.
T1, T2, and T2' are Type. All are inhabited.

view this post on Zulip Mario Carneiro (Apr 26 2018 at 02:30):

I think I will stick with my original answer then - unprovable in Lean but consistent with it

view this post on Zulip Mario Carneiro (Apr 26 2018 at 02:31):

May I ask why you need this?

view this post on Zulip Mario Carneiro (Apr 26 2018 at 02:32):

I know it comes up in attempting to prove

f == g -> a == b -> f a == g b

which would be nice if it were provable but you have to assume f = g for it to work.

view this post on Zulip Scott Buckley (Apr 26 2018 at 02:37):

I'm proving type determinism for my operational semantics. Some expressions contain lean functions. If I have an application, its subexpressions must have function types, so the output of an application must have the same type. That's where this comes in.

view this post on Zulip Mario Carneiro (Apr 26 2018 at 02:57):

So the types of your functions are calculated dynamically? I think you want to bundle the types as auxiliary data for this kind of thing to work. It's not sufficient to know that they can be well typed, you need to keep track of the type itself so that one pi doesn't get swapped with another that is equal but has different parts (assuming pi is noninjective)

view this post on Zulip Scott Buckley (Apr 26 2018 at 03:12):

yeah that's a good point. thanks for the advice :)

view this post on Zulip Kenny Lau (Apr 26 2018 at 17:03):

I think I will stick with my original answer then - unprovable in Lean but consistent with it

this is very interesting

view this post on Zulip Kenny Lau (Apr 26 2018 at 17:03):

@Kevin Buzzard

view this post on Zulip Kenny Lau (May 28 2018 at 14:38):

@Mario Carneiro is the converse true / provable?

view this post on Zulip Kenny Lau (May 28 2018 at 14:38):

T2 = T2' -> ((T1 -> T2) = (T1 -> T2'))

view this post on Zulip Chris Hughes (May 28 2018 at 14:51):

Isn't that just rw

view this post on Zulip Kenny Lau (May 28 2018 at 14:51):

yes

view this post on Zulip Kenny Lau (May 28 2018 at 14:51):

what if the right hand side is a pi

view this post on Zulip Kenny Lau (May 28 2018 at 14:51):

does pi have an ext theorem?

view this post on Zulip Kenny Lau (May 28 2018 at 15:55):

 {α : Sort u} {β γ : α  Sort v}, ( (x : α), β x == γ x)  ((Π (x : α), β x) == Π (x : α), γ x)

view this post on Zulip Kenny Lau (May 28 2018 at 15:55):

Is this true/false/independent?

view this post on Zulip Johannes Hölzl (May 28 2018 at 16:02):

You don't need == to state this. The type of β x and γ x are the same. dito on the rhs.

view this post on Zulip Johannes Hölzl (May 28 2018 at 16:04):

universes u v
example {α : Sort u} {β γ : α  Sort v} (h :  (x : α), β x = γ x) :
  ((Π (x : α), β x) = Π (x : α), γ x) :=
have β = γ, from funext h,
by subst this

view this post on Zulip Kenny Lau (May 28 2018 at 16:10):

hmm

view this post on Zulip Mario Carneiro (May 28 2018 at 20:05):

The converse is false for some choices of T1, and independent for others


Last updated: May 13 2021 at 21:12 UTC