A request for two references....

Good afternoon, I'd like references on these two subjects: 1. The relationship between categories and Martin-Löf types. 2. Any attempts to develop a computer language/system in which categories are first class citizens. Thanks in advance.... best steve