Equality of psigma implies equality

Stream: general

[Tomas Skrivan]

I vaguely remember that an inductive type with a parameter, for example A : Type -> Type, is not injective i.e. in general A X = A Y does not imply X = Y.

What about this particular type of sigma type?

variables {α : Type} (a b : α)

example : (Σ' x, x = a) = (Σ' x, x = b) → (a = b) := sorry

Can this be proven? If not, can I assume it as an axiom or it can cause inconsistency?

[Chris Hughes]

I think that it is not provable, in Lean if two types have the same cardinality you cannot prove they are not equal. I think it is consistent though.

[Tomas Skrivan]

I would be nice to know if it is really consistent. On the other hand, what I really want is to prove is the following and it might be weaker/provable:

example {α : Type} (a b : α) (A : (Σ' x, x = a)) (h : (Σ' x, x = a) = (Σ' x, x = b))
  : (h ▸ A).1 = A.1 := sorry

[Tomas Skrivan]

Ohh, I think these two are equivalent.

[Tomas Skrivan]

It feels really wrong that this is not be provable, especially the second formulation :confused:

[Yaël Dillies]

How did you reach that point? Where does this equality of types come from?

[Floris van Doorn]

Equality between types is underdetermined in type theory. There are variants of type theory that extensively uses axioms/rules that imply A ≃ B → A = B, which contradicts your examples.
In Lean, you should avoid writing the equality of two types, unless you know what you're doing.

[Tomas Skrivan]

I'm using tactic mode to construct programs. It usually goes like this:

def foo : (Σ' x, x = b) :=
by
   <rewrite b into a>
   apply ⟨a, Eq.refl⟩

In my use case b is specification, usually noncomputable function, and you transform into something propositionaly equal to b but a is computable.

Later on when I work with foo.1 I want to either convert it back to a or b, depending on the scenario.

[Yaël Dillies]

Aren't you happy to have an equivalence of type rather than an equality?

[Tomas Skrivan]

Yaël Dillies said:

Aren't you happy to have an equivalence of type rather than an equality?

How would type equivalence be applied in my use case?

[Yaël Dillies]

Instead of rewriting with h : a = b, you will apply e, where e : Σ' x, x = a ≃ Σ' x, x = b.

[Yaël Dillies]

"using tactic mode to construct programs" is explicitly discouraged precisely because you might be tempted to rewrite the goal rather than applying functions.

[Tomas Skrivan]

It might be discouraged, but I'm exploring the space of doing exactly so and I think I can do some cool stuff with it.

[Yaël Dillies]

Well, if you can cope with the foundational problems that this approach entails :shrug:

[Tomas Skrivan]

I'm definitely interested what foundational problems this brings. If assuming (Σ' x, x = a) = (Σ' x, x = b) → (a = b) as an axiom is inconsistent then I will seriously rethink what I'm doing, if not I will probably keep on doing what I'm doing if no reasonable and similarly convenient way of doing things show up.

[Tomas Skrivan]

Yaël Dillies said:

Instead of rewriting with h : a = b, you will apply e, where e : Σ' x, x = a ≃ Σ' x, x = b.

This is definitely option, but I'm afraid I would have to re-implement my own tactic mode similar to conv based on this.

[Violeta Hernández]

To add to Floris' comment, the reason type equality is so badly behaved is that there's no axiom that can help you determine it

[Violeta Hernández]

You don't have anything like funext or propext for types

[Violeta Hernández]

So the only ways to prove α = β for two types is via rfl and other equalities between the arguments that make up each type