Discussion between Lawrence and Kristian Berry

Imported from a comment discussion on https://philosophy.stackexchange.com/questions/123367/why-did-voevodsky-choose-type-over-category/123373#123373