## Stream: general

### Topic: Hard but obvious lemma

#### Chris Hughes (Jun 22 2018 at 23:10):

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 (Jun 22 2018 at 23:14):

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

@Mario Carneiro

#### Chris Hughes (Jun 22 2018 at 23:18):

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 (Jun 22 2018 at 23:28):

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 (Jun 23 2018 at 02:48):

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

#### Mario Carneiro (Jun 23 2018 at 02:48):

(co-authored with Cody IIRC)

#### Mario Carneiro (Jun 23 2018 at 02:50):

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 (Jun 23 2018 at 02:50):

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

#### Mario Carneiro (Jun 23 2018 at 02:51):

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

Last updated: Aug 03 2023 at 10:10 UTC