TY - RPRT TI - Isomorphism within Naive Type Theory AU - David McAllester PY - 2018 UR - https://arxiv.org/abs/1407.7274 ID - 1407.7274 ER -