## Stream: new members

### Topic: function extensionality and transports

#### Edward Ayers (Aug 08 2018 at 18:40):

lemma my_ext
: ∀ (α :Type)
(P Q : α -> Type)
(f : Π (a : α), P a )
(g : Π (a : α), Q a)
(p : ∀ (a : α), P a = Q a),
(∀ (a : α), ((p a) ▸ (f a)) = g a)
-> ((funext p) ▸ f) = g
:= by sorry


Some questions:
1. How do I get the transport triangles to work? I get the same error if I reverse the arguments so I don't even know if I'm using it the right way round
2. How do I prove it?
3. Is it crazy to want to do this?

#### Chris Hughes (Aug 08 2018 at 18:44):

The triangles are for eq.subst which can only make proofs, not data. You have to use eq.rec I think. You could also use heq ==

#### Mario Carneiro (Aug 08 2018 at 18:48):

lemma my_ext (α :Type)
(P Q : α -> Type)
(f : Π (a : α), P a )
(g : Π (a : α), Q a)
(p : ∀ (a : α), P a = Q a) :
(∀ (a : α), (eq.rec_on (p a) (f a) : Q a) = g a)
-> (eq.rec_on (funext p : P = Q) f : Π (a : α), Q a) = g :=
by cases (funext p : P = Q); exact funext


Last updated: May 09 2021 at 19:11 UTC