Zulip Chat Archive

Stream: new members

Topic: function extensionality and transports


view this post on Zulip 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?

view this post on Zulip 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 ==

view this post on Zulip 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