HEq congr and inconsistency

Stream: Type theory

[Andrés Goens]

Maybe a bit of a naive question because I don't grasp the foundations so well (as a follow-up to https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/HEq.20congr/near/476274468 too): does the existence of non-standard models where heterogeneous congruence is a non-theorem mean that adding it as an axiom is inconsistent?

In other words, if I add congruence of HEq as an axiom (something like)

axiom heq_congr {α₁} {α₂} {β₁} {β₂} {a : α₁} {b : α₂} {f : α₁ → β₁} {g : α₂ → β₂} (h₁ : HEq a b) (h₂ : HEq f g) : HEq (f a) (g b)

Can I use that to prove False? Or do I just get a type theory that doesn't have as many models?

[Mario Carneiro]

As long as there is some model in which it is true, it is safe to add as an axiom, and you just get a type theory that has fewer models.

[Kevin Buzzard]

Is there a model where HEq a b <-> a = b?

[Kyod]

Kevin Buzzard said:

Is there a model where HEq a b <-> a = b?

There is at least a model of dependent type theory, namely Extensional Type Theory featuring equality reflection that collapses propositional equality with conversion (a.k.a. definitional equality).

[Kevin Buzzard]

I guess my question was specifically about Lean's type theory, motivated by the fact that if Andres could add that as an axiom instead whilst maintaining consistency, his life might be even easier!

[Kyle Miller]

There seems to be an issue that this axiom isn't well-typed, unless somehow the underlying rule is "if h : a = b then a is defeq to b (and h is defeq to rfl)"

[Mario Carneiro]

Kevin Buzzard said:

Is there a model where HEq a b <-> a = b?

This is provable in lean :)

[Mario Carneiro]

example : HEq a b ↔ a = b := by simp

[Andrés Goens]

Kyle Miller said:

There seems to be an issue that this axiom isn't well-typed, unless somehow the underlying rule is "if h : a = b then a is defeq to b (and h is defeq to rfl)"

not sure I quite understand, what is not well-typed precisely? (at least Lean doesn't complain it's not well-typed)

[Kyle Miller]

Make sure to look at the type's of a and b here — it's better not to rely on autoimplicits if you want to be sure everything is what you think it is.

[Andrés Goens]

I still don't get what you mean. I am not relying on autoimplicit (in fact, turning it off doesn't break things), the types of a and b are explicit there. I'm only relying on {α₁} being elaborated to something like {α₁ : Sort u}

[Andrés Goens]

set_option autoImplicit false
universe u
axiom heq_congr {α₁ : Sort u} {α₂: Sort u} {β₁: Sort u} {β₂ : Sort u} {a : α₁} {b : α₂} {f : α₁ → β₁} {g : α₂ → β₂} (h₁ : HEq a b) (h₂ : HEq f g) : HEq (f a) (g b)

Lean doesn't complain here either (also not if I remove the Sort u annotations)

[Andrés Goens]

all that being said, I just wrote down the first sensible version that Lean didn't complain about, it's not about this precise term (and that's why I wrote "something like this"). I'm asking the more general question, can something like congruence of HEq be added as an axiom, and would that make things inconsistent or just rule out some non-standard models (that I don't know if I care about)

[Andrés Goens]

(but I'd be curious to undersand why it's not well-typed!)

[Kyle Miller]

That's not HEq a b ↔ a = b though, I'm confused? I'm responding to Kevin's question.

[Andrés Goens]

oh, gotcha, that's the confusion! I thought you meant my question before that!

[Martin Dvořák]

Mario Carneiro said:

example : HEq a b ↔ a = b := by simp

What happens in the example? What are the types?

[Marcus Rossel]

Martin Dvořák said:

Mario Carneiro said:

example : HEq a b ↔ a = b := by simp

What happens in the example? What are the types?

I think the point here is that for the term a = b to even be well-typed, a and b must have the same (definitionally equal) type. If a and b didn't have the same type, you couldn't even state this theorem. And then simp presumably uses docs#eq_of_heq.