TY - RPRT TI - Homotopy type theory as a language for diagrams of $\infty$-logoses AU - Taichi Uemura PY - 2026 DO - 10.46298/lmcs-22(1:25)2026 UR - https://arxiv.org/abs/2212.02444 ID - 2212.02444 ER -