{"ID":6267055,"CreatedAt":"2026-07-10T01:11:38.759438437Z","UpdatedAt":"2026-07-13T01:02:08.706470581Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2607.08154","arxiv_id":"2607.08154","title":"Directed proof-relevant logical relations in simplicial HoTT","abstract":"Intrinsically-typed presentations of type theory often use equality in the meta-language to represent object-language judgmental equality. In such equational syntax, proof-relevant logical relations define computability predicates on judgmental equivalence classes of types and terms. This approach, however, does not directly account for reduction, which is directed and plays a central role in many logical-relations arguments. This paper develops a directed version of proof-relevant logical relations in simplicial homotopy type theory, where reductions are internalized as \\emph{inequality types}. We construct object syntax as a directed quotient inductive type. The central observation is that contravariant families in simplicial type theory provide exactly the proof-relevant form of closure under expansion for logical relations: computability evidence can be transported backward along reductions, with the required functoriality and universal property built in. Using this observation, we construct a unary logical relations model with contravariant computability predicates and prove directed Boolean canonicity: every closed Boolean term reduces to either true or false. We then extend the construction to dependent types and universes, where a comonadic flat modality provides the discreteness needed for type conversion and universe predicates. Finally, we adapt the method to binary logical relations, separating vertical reduction from horizontal parametricity and obtaining a proof-relevant account of representation independence.","short_abstract":"Intrinsically-typed presentations of type theory often use equality in the meta-language to represent object-language judgmental equality. In such equational syntax, proof-relevant logical relations define computability predicates on judgmental equivalence classes of types and terms. This approach, however, does not di...","url_abs":"https://arxiv.org/abs/2607.08154","url_pdf":"https://arxiv.org/pdf/2607.08154v1","authors":"[\"Runming Li\",\"Harrison Grodin\",\"Robert Harper\"]","published":"2026-07-09T06:49:13Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.PL\"]","methods":"[]","has_code":false}