Combinatorial realizability models of type theory - Pieter Hofstra; Michael A. Warren (2012)