TY - RPRT TI - Separating Path and Identity Types in Presheaf Models of Univalent Type Theory AU - Andrew Swan PY - 2018 UR - https://arxiv.org/abs/1808.00920 ID - 1808.00920 ER -