Skip to content

Instantly share code, notes, and snippets.

@andrejbauer

andrejbauer/gist:4272538

Created December 12, 2012 23:10
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save andrejbauer/4272538 to your computer and use it in GitHub Desktop.
Save andrejbauer/4272538 to your computer and use it in GitHub Desktop.
Download ZIP
A lemma which explains how transport and function extensionalty interact.
Raw
gistfile1.txt
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
Copy link
Author

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