# Zulip Chat Archive

## Stream: general

### Topic: Type theory of Lean

#### Mario Carneiro (Apr 22 2019 at 17:05):

I just delivered my master's thesis on lean's type theory, and the talk was recorded: https://www.youtube.com/watch?v=3sKrSNhSxik . It builds up the motivation for all the complexity in DTT, so if you have a basic understanding of how proof judgments are presented you should be able to follow it. The repo with the full thesis is https://github.com/digama0/lean-type-theory/releases .

#### Rob Lewis (Apr 22 2019 at 17:13):

Congrats!

#### Patrick Massot (Apr 22 2019 at 17:41):

http://phdcomics.com/comics/archive.php?comicid=590

#### Patrick Massot (Apr 22 2019 at 17:44):

Who would have believed to see this before Lean 4?

#### Wojciech Nawrocki (Apr 23 2019 at 13:41):

Congrats!

#### Wojciech Nawrocki (Apr 23 2019 at 15:13):

f == g -> x == y -> f x == g y is unprovable

Oops, so that's why I couldn't do it when I tried recently. Do you know if this is consistent as an added axiom?

#### Kevin Buzzard (Apr 23 2019 at 17:48):

Don't add axioms! It's not really how Lean works, and support for them is poor. If you need it, add a variable. But people in general try to avoid `heq`

completely. Why do you think you need it at all?

#### Wojciech Nawrocki (Apr 24 2019 at 12:15):

I agree that adding axioms is probably undesirable, but it would be interesting to see whether this one is consistent with Lean from a purely type-theoretical point of view

#### Mario Carneiro (Apr 25 2019 at 01:29):

It's consistent, because it follows from injectivity of pi

#### Simon Hudon (Apr 25 2019 at 01:34):

Are you saying that adding injectivity of pi is sufficient to prove it? Is there a down side to having that axiom?

#### Mario Carneiro (Apr 25 2019 at 04:02):

One downside, as Carlo mentioned to me, is that it breaks the types-as-sets model, and the types-as-cardinalities model

#### Mario Carneiro (Apr 25 2019 at 04:03):

plus axioms always have computation / canonicity troubles

#### Mario Carneiro (Apr 25 2019 at 04:11):

axiom pi_injective₁ {α : Sort*} {β : α → Type*} {α' : Sort*} {β' : α' → Type*} (H : (Π a, β a) = (Π a, β' a)) : α = α' axiom pi_injective₂ {α : Sort*} {β β' : α → Type*} (H : (Π a, β a) = (Π a, β' a)) (a) : β a = β' a theorem heq_congr {α : Sort*} {β : α → Type*} {α' : Sort*} {β' : α' → Type*} {f : Π a, β a} {g : Π a, β' a} {x : α} {y : α'} (h₁ : f == g) (h₂ : x == y) : f x == g y := begin cases pi_injective₁ (type_eq_of_heq h₁), cases (funext $ pi_injective₂ (type_eq_of_heq h₁) : β = β'), cases h₁, cases h₂, refl end

#### Patrick Massot (Apr 25 2019 at 15:23):

Who would have believed to see this before Lean 4?

That was a very narrow win...

#### Simon Hudon (Apr 25 2019 at 15:49):

Do you have a release date for Lean 4?

#### Patrick Massot (Apr 25 2019 at 15:50):

We didn't need a release to see it

#### Wojciech Nawrocki (Jun 13 2019 at 15:16):

What about functional extensionality over `heq`

? I think it doesn't hold in pure CiC, but maybe it's provable in Lean's theory (or in Lean+`pi_injective`

)? Something like

axiom heq_funext {α β: Type u} {A: α → Type v} {B: β → Type v} (f: Π a: α, A a) (g: Π b: β, B b) : α = β → (∀ (a: α) (b: β), a == b → f a == g b) → f == g

#### Reid Barton (Jun 13 2019 at 15:22):

This looks provable in Lean

#### Reid Barton (Jun 13 2019 at 15:27):

Here is my unoptimized proof

lemma heq_funext {α β: Type u} {A: α → Type v} {B: β → Type v} (f: Π a: α, A a) (g: Π b: β, B b) : α = β → (∀ (a: α) (b: β), a == b → f a == g b) → f == g := begin rintro rfl h, have : A = B, { apply funext, intro a, apply type_eq_of_heq (h a a heq.rfl) }, subst this, apply heq_of_eq, apply funext, intro a, apply eq_of_heq (h a a heq.rfl) end

#### Wojciech Nawrocki (Jun 13 2019 at 15:38):

Thanks!

#### Chris Hughes (Jun 13 2019 at 15:39):

Golfed

lemma heq_funext {α β: Type u} {A: α → Type v} {B: β → Type v} (f: Π a: α, A a) (g: Π b: β, B b) : α = β → (∀ (a: α) (b: β), a == b → f a == g b) → f == g := function.hfunext

#### Wojciech Nawrocki (Jun 13 2019 at 15:41):

:smiley: I was looking for this in `heq`

parts of the library

#### Chris Hughes (Jun 13 2019 at 15:43):

Alternatively

lemma heq_funext {α β: Type u} {A: α → Type v} {B: β → Type v} (f: Π a: α, A a) (g: Π b: β, B b) : α = β → (∀ (a: α) (b: β), a == b → f a == g b) → f == g := by library_search

#### Kevin Buzzard (Jun 13 2019 at 15:58):

`library_search`

is still not my first instinct with these sorts of things, and it probably should be. Sometimes I think "probably I need `import mathlib`

for the search to work".

#### Kevin Buzzard (Jun 13 2019 at 15:59):

Of course, Chris' triumph should be seen within the context of the hours of pain he had when trying to deal with `heq`

last year.

Last updated: May 16 2021 at 05:21 UTC