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

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?

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


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