Hard but obvious lemma

Stream: general

[Chris Hughes]

How to prove this? I don't need it, I'm just curious.

example {α β : Sort u} {γ : α → Sort v} {δ : β → Sort v} {f : Π a, γ a} {g : Π b, δ b}
  {a : α} {b : β} (hfg : f == g) (hab : a == b) : f a == g b :=

[Simon Hudon]

I think there’s a meta theorem that says it can’t be proved in DTT

[Simon Hudon]

@Mario Carneiro

[Chris Hughes]

In that case, same question for

example {α β : Sort u} {γ δ : Sort v} {f : α → γ} {g : β → δ}
  {a : α} {b : β} (hfg : f == g) (hab : a == b) : f a == g b

[Simon Hudon]

I think you would need an equality α = β and γ = δ for this to be provable. Then, you can deduce f = g. I saw the theorem in a talk by Cody Roux. If I remember correctly, when you want to prove f x₀ .. xᵢ = g y₀ .. yᵢ, from x₀ == y₀ .. xᵢ == yᵢ, you need f = g for the statement to be provable.

[Mario Carneiro]

Leo has a whole paper on how he works around the unprovability of this theorem

[Mario Carneiro]

(co-authored with Cody IIRC)

[Mario Carneiro]

Although I think the actual unprovability is only folklore, I don't know an explicit proof although there is probably a way to modify the set model to get it

[Simon Hudon]

He basically generates all the relevant theorems right? I think that's what congr does for heq goals

[Mario Carneiro]

yes, he's implemented a tactic meta-theorem for the version you stated