TY - RPRT TI - The local universes model: an overlooked coherence construction for dependent type theories AU - Peter LeFanu Lumsdaine AU - Michael A. Warren PY - 2015 DO - 10.1145/2754931 UR - https://arxiv.org/abs/1411.1736 ID - 1411.1736 ER -