Strict Equality in Higher Identity Types: Axioms, Completeness, Decidability

Keri D'Angelo; Liron Cohen; Luke Serafin; Dexter Kozen

Home/Archive/arXiv

arXiv · 2610.28906

Strict Equality in Higher Identity Types: Axioms, Completeness, Decidability

Keri D'Angelo·Liron Cohen·Luke Serafin·Dexter Kozen

View original source ↗Read source document ↗Export metadata ↓

Abstract

Reasoning about higher identity types uses two equalities, strict equality and equivalence of cells witnessed by a path. Strict equality is a congruence for every operation on cells, but associativity and the identity laws fail for it. Equivalence of cells satisfies those two laws, but it is not a congruence. Representations of higher identity types often conflate equational properties that hold strictly with those that hold only up to a path. We separate the two and axiomatize the former, introducing SEq, an equational theory generated by eleven axioms for strict equality between cells. We prove soundness and completeness for homotopy models, and completeness already over finite CW-complexes. Nine of these axioms form a strongly normalizing rewrite system whose normal forms are unique up to picture equivalence, and the resulting word problem is decidable in exponential time. We also give presheaf models over a cubical base category in which composition arises from a pushout in the base category itself, without requiring Kan filling structure. The same pushout structure provides explicit higher-dimensional witnesses for associativity and the identity laws.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Keri D'Angelo, Liron Cohen, Luke Serafin, Dexter Kozen. 2026-10-20. Strict Equality in Higher Identity Types: Axioms, Completeness, Decidability. https://arxiv.org/abs/2610.28906

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Formula size game and model checking for modal substitution calculus

Recent research has applied modal substitution calculus (MSC) and its variants to characterize various computational frameworks such as graph neural networks (GNNs) and distributed computing systems. For example, it has been shown that floating-point recurrent graph neural networks have the same expressive power as graded modal substitution calculus GMSC, which is the extension of MSC with counting modalities. GMSC can be further extended with the counting global modality, resulting in the logic GGMSC, which corresponds to floating-point GNNs with global readout mechanisms. In this paper, we introduce a formula size game that characterizes the expressive power of MSC, GMSC, GGMSC, and related logics. Furthermore, we study the expressiveness and model checking of logics in this family. We prove that MSC and its extensions (GMSC, GGMSC) are as expressive as linear tape-bounded Turing machines, while asynchronous variants are linked to the modal mu-calculus and modal computation logic MCL. We establish that for MSC, GMSC and GGMSC, both the combined and data complexity of model checking are PSPACE-complete, and for their asynchronous variants, both complexities are PTIME-complete. We also establish that for the propositional fragment SC of MSC, the combined complexity of model checking is PSPACE-complete, while for asynchronous SC it is PTIME-complete, and in both cases, the data complexity is constant. As a corollary, we observe that SC satisfiability is PSPACE-complete and NP-complete for its asynchronous variant. Finally, we construct a universal reduction from all recursively enumerable problems to MSC model checking.

cs.LO↗

arXiv2026

Theorem prover Arend

This paper is an exposition of the theorem prover Arend developed at JetBrains Research. Arend language has been designed to facilitate the formalization of mathematics within the framework of univalent foundations and with the focus on constructive mathematics. It is based on a variant of homotopy type theory with cubical syntax that is more closely aligned with Martin-Löf Type Theory (MLTT) than fully computational cubical type theories, while still retaining some of their computational properties useful in practice. Among the most notable features of the Arend language is its powerful system of classes and records supporting subsumptive subtyping, partial implementations and anonymous extensions, which provides extensive flexibility for constructing hierarchies of definitions. Formalization in Arend is streamlined by the IntelliJ Arend plugin, which transforms IntelliJ IDEA into a full-fledged integrated development environment (IDE) for the Arend language. The main Arend library arend-lib includes formalizations in constructive algebra, topology and synthetic homotopy theory.

cs.LO↗

arXiv2026

Post-Pruning vs. Early Stopping: Which Works Better for Link Prediction with AnyBurl?

Rule-based link prediction combines symbolic and statistical artificial intelligence methods by inductively learning a set of rules from a knowledge graph (KG), with the aim of completing the graph when a query cannot be answered from the KG alone. Several systems have been proposed, and while they perform well on classical benchmarks, even compared with embedding-based systems, many of them produce a large number of rules. This compromises scalability in the query-answering phase, especially under strong hardware constraints. In this work, we investigate the behavior of AnyBurl, a state-of-the-art rule learner for link prediction, to determine whether running it for a given time and then pruning the learned rules yields better query-answering performance at test time than a simpler approach that stops rule generation earlier.

cs.LO↗