Dependent Unions (WIP)

- [x] Type Formation
- [x] Type Equality
- [x] Term Introduction
- [x] Term Equality
- [ ] Term Elimination