Extensional Equality

Adding the correct equalities for the built-in types. Resolves #18, #6, #7.

- [x] Extensional for binder types (pi, sigma)
- [x] Extensional equality for functions
- [x] Extensional equality for pairs (requires #6)
- [x] Extensional equality for equality proofs (UIP)
- [x] `refl` should probably just be replaced with `<>` à la nuprl