TY - RPRT TI - Types are Internal $\infty$-Groupoids AU - Antoine Allioux AU - Eric Finster AU - Matthieu Sozeau PY - 2021 UR - https://arxiv.org/abs/2105.00024 ID - 2105.00024 ER -