Injectivity of Pi type "constructors"

Stream: Type theory

[Robert Maxton]

a) Is it even true in, or at least consistent with, Lean's type theory that ((a : α) → β a) = ((a' : α') → β' a') implies α = α'and β = β'?
b) If it is true, is it provable in Lean?

Normally, I'd try prove this by injectivity of constructors, but near as I can tell the dependent arrow is a low level construct that doesn't really have construtors... which is suspicious to me since even Eq has a constructor and a recOn, but if Pi or forall do I can't find it.

[Aaron Liu]

It is consistent but not provable.
In the cardinality model of Lean, Unit → Nat and Bool → Nat are the same cardinality, and so the same type.
On the other have, there is nothing stopping these from being distinct.

docs#Eq is an inductive type, but the dependent arrow is built into Lean, which is why Eq has a rec principle but the forall types do not.

[Robert Maxton]

I see. Unfortunate, but good to know for sure. Thanks.

[Robert Maxton]

And I suppose the same argument applied to, say, Bool → Nat and Bool → (Nat × Nat) demonstrates that even if we unify the index types, ((a : α) → β a) = ((a : α) → β' a) → β = β' isn't provable either?

[Kyle Miller]

That example is fine, because it could be the case that Nat = Nat × Nat (they have the same cardinality).

Nat -> Bool and Nat -> Nat gives a cardinality counterexample though.

[Robert Maxton]

Ah, okay. Thanks!

[Kyle Miller]

Aaron Liu said:

It is consistent

This seems plausible, but I'm not sure since type constructor injectivity isn't consistent. Do you have a source for it? (Maybe it's in #leantt)

[Walter Moreira]

Aaron Liu said:

In the cardinality model of Lean, Unit → Nat and Bool → Nat are the same cardinality, and so the same type.

Do you have a reference for the cardinality model of Lean? I checked #leantt, but I cannot find it there.

[Aaron Liu]

Kyle Miller said:

Aaron Liu said:

It is consistent

This seems plausible, but I'm not sure since type constructor injectivity isn't consistent. Do you have a source for it? (Maybe it's in #leantt)

To me this is just "obviously" true. If it is inconsistent you should be able to find a concrete counterexample, which seems impossible if the target is not a Prop. I looked for a source, but didn't find one. Maybe I'll try writing a proof later.

What is type constructor injectivity?

[Kevin Buzzard]

I'm not sure we can appeal to "obviously" here. This looks very delicate to me.

[Aaron Liu]

Maybe I haven't built up enough intuition, and I am wrong on this. I'll try writing a proof later.

[Kevin Buzzard]

Aaron Liu said:

What is type constructor injectivity?

This is certainly not my area of expertise but there's a discussion here #Type theory > `Quot` and subject reduction property @ 💬

[Kyle Miller]

#new members > ✔ Are parametric type constructors injective? @ 💬 has an example of an inductive type whose type constructor isn't injective. The way this one works doesn't apply to pi types however, since pi types have a universe bump.

[Mario Carneiro]

pi types are not injective. (Nat -> True) = (Unit -> True)

[Mario Carneiro]

@Kyle Miller I'm not sure what you mean about pi types having a universe bump - pi types don't bump the universe on their own

[Mario Carneiro]

For a codomain which is not a Prop, you can construct a model satisfying pi injectivity; there are some details on this construction in #leantt . Unfortunately the cardinality model is not described there, even though I recall writing some notes on it which must have died in a git stash somewhere

[Kyle Miller]

Mario Carneiro said:

pi types are not injective. (Nat -> True) = (Unit -> True)

I was going to mention this example, but Aaron said "which seems impossible if the target is not a Prop" so it didn't seem necessary.

Mario Carneiro said:

Kyle Miller I'm not sure what you mean about pi types having a universe bump - pi types don't bump the universe on their own

In the type constructor parameter example, you don't need the universe level of the resulting type to accommodate the parameter. Maybe 'universe bump' isn't descriptive enough, but in any case, the pi types lie in a large enough universe where the cantor trick doesn't seem to work.

[Kyle Miller]

Mario Carneiro said:

you can construct a model satisfying pi injectivity

Is a way it works that each pi type can be represented by a corresponding ZFC function set? (I'm assuming we model dependent functions by using the union of the codomains as the codomain.)

[Mario Carneiro]

See section 6.4 of #leantt. It works by interpreting types not as sets directly, but rather tagged sets that contain a semi-syntactic description of the way the type was constructed. So the representation of a pi type is [[(a : A) -> B a]] = ("Pi", [[A]], [[B]]) and we can use this to prove injectivity of pi wrt propositional equality in this model