Homotopy Type Theory
natural model

See http://www.andrew.cmu.edu/user/awodey/preprints/natural.pdf