Search papers, labs, and topics across Lattice.
This paper introduces a directed version of proof-relevant logical relations within simplicial homotopy type theory, addressing the limitations of traditional equational syntax that fails to incorporate reduction. By internalizing reductions as inequality types and utilizing contravariant families, the authors construct a unary logical relations model that ensures computability evidence can be effectively transported along reductions. A key result is the proof of directed Boolean canonicity, demonstrating that every closed Boolean term reduces to either true or false, which is then extended to dependent types and universes, enhancing the framework's applicability.
Every closed Boolean term reduces to either true or false, revealing a novel approach to logical relations that integrates reduction directly into type theory.
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.
CMU ML