function extensionality and transports

Stream: new members

[Edward Ayers]

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]

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]

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