[decasteve]

HoTT even more than that. Type theory does what you describe without the "homotopy".

See: http://golem.ph.utexas.edu/category/2013/06/the_hott_book.ht...

[tome]

It will be easier to convince mathematicians that homotopy theory is maths than it will be to convince them that type theory is (in general).