_Homotopy limits in type theory_. [[Jeremy Avigad]], [[Chris Kapulkin]], [[Peter LeFanu Lumsdaine]], Math. Structures Comput. Sci. 25 (2015), no. 5, 1040?1070. ## Links ## [arXiv:1304.0680](http://arxiv.org/abs/1304.0680) category: reference