Peter LeFanu Lumsdaine. Weak ω-categories from intensional type theory. Logical Methods in Computer Science, 6(3), 2010-09-17. https://doi.org/10.2168/lmcs-6(3:24)2010 https://arxiv.org/abs/0812.0409v4
Peter LeFanu Lumsdaine. Weak ω-categories from intensional type theory. Logical Methods in Computer Science, 6(3), 2010-09-17. https://doi.org/10.2168/lmcs-6(3:24)2010 https://arxiv.org/abs/0812.0409v4