## Stream: general

### Topic: equality of pi types?

#### 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

#### 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'

#### 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

#### 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.)

#### 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

#### 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.

#### 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

#### Mario Carneiro (Apr 26 2018 at 02:31):

May I ask why you need this?

#### 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.

#### 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.

#### 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)

#### Scott Buckley (Apr 26 2018 at 03:12):

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

#### 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

@Kevin Buzzard

#### Kenny Lau (May 28 2018 at 14:38):

@Mario Carneiro is the converse true / provable?

#### Kenny Lau (May 28 2018 at 14:38):

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

#### Chris Hughes (May 28 2018 at 14:51):

Isn't that just rw

yes

#### Kenny Lau (May 28 2018 at 14:51):

what if the right hand side is a pi

#### Kenny Lau (May 28 2018 at 14:51):

does pi have an ext theorem?

#### Kenny Lau (May 28 2018 at 15:55):

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


#### Kenny Lau (May 28 2018 at 15:55):

Is this true/false/independent?

#### 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.

#### 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


hmm

#### Mario Carneiro (May 28 2018 at 20:05):

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

Last updated: Aug 03 2023 at 10:10 UTC