Benno van den Berg & Richard Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370--394, 2011. https://doi.org/10.1112/plms/pdq026 https://arxiv.org/abs/0812.0298v2
Benno van den Berg & Richard Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370--394, 2011. https://doi.org/10.1112/plms/pdq026 https://arxiv.org/abs/0812.0298v2