TY - RPRT TI - Directed proof-relevant logical relations in simplicial HoTT AU - Runming Li AU - Harrison Grodin AU - Robert Harper PY - 2026 UR - https://arxiv.org/abs/2607.08154 ID - 2607.08154 ER -