Homotopy Type Theory semantics > history

< categorical model of dependent types