Injectivity of function type constructor

Stream: lean4

[Trebor Huang]

Injectivity of type constructor is obviously anticlassical, as we can define an inductive type Bad : (Type -> Type) -> Type, whose sole existence implies an injective function from Type -> Type to Type, with which we can invoke Cantor's argument.

However, does injectivity of -> (let's not consider the dependent case first) break anything? This come up when I am contemplating the unprovability of HEq f g -> HEq x y -> HEq (f x) (g y). Is there any literature investigating this problem?

[Reid Barton]

I think the set-theoretic model like in Mario's thesis needs at most minor tweaks in order to validate injectivity of ->.

[Reid Barton]

Oh wait, it's slightly awkward to deal with A -> B with B empty but not A.

[Reid Barton]

Do you care about the interaction with propext? (false -> true) = (true -> true)

[Trebor Huang]

Ok, that breaks. So we definitely don't have HEq f g -> HEq x y -> HEq (f x) (g y) right? I will try to construct a disproof, but I should sleep now.

[James Gallicchio]

i suspect it's unprovable but not unsound when in Type u? :thinking: not sure though

[Eric Wieser]

Trebor Huang said:

Ok, that breaks. So we definitely don't have HEq f g -> HEq x y -> HEq (f x) (g y) right? I will try to construct a disproof, but I should sleep now.

docs#congr_heq ah, not quite

[Mario Carneiro]

For HEq f g -> HEq x y -> HEq (f x) (g y) you actually want injectivity only in the right argument - (A -> B) = (A -> C) implies B = C. As long as A is nonempty this is basically always true, but for A empty you need some additional tagging scheme to make it true (but it can still be done as long as B, C : Type u). For B, C : Prop it is false because of (false -> false) = (false -> true).

[Mario Carneiro]

For HEq f g -> HEq x y -> HEq (f x) (g y) this isn't an issue though, because x and y witness the nonemptiness of A

[Mario Carneiro]

For the values it is easy enough to ensure that this theorem holds, you just take HEq to mean ZFC = and then it is true