# Zulip Chat Archive

## 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

#### Simon Hudon (Jun 22 2018 at 23:14):

@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: Dec 20 2023 at 11:08 UTC