Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
A lemma which explains how transport and function extensionalty interact.
Variable A : Type.
Variable P : A -> Type.
Variable Q : forall x, P x -> Type.
Lemma transport_funext (f g : forall x, P x) (n : forall x, Q x (f x)) (E : forall x, f x = g x) (x : A) :
(transport (fun h => forall x, Q x (h x)) (funext E) n) x = transport (Q x) (E x) (n x).
@andrejbauer

This comment has been minimized.

Copy link
Owner Author

andrejbauer commented Dec 12, 2012

Note: funext takes a pointwise equality of functions and turns it into equality of functions. It is the opposite of happly.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.