PaperlayerView exact revision on arXiv

Source-linked AI summary

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

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

arXiv:2610.28906v1cs.LO

TL;DR

Higher identity type presentations can conflate strict equality with equivalence witnessed by a path, despite their different algebraic properties. The paper introduces SEq for strict equality and develops cubical presheaf models whose base-category pushouts provide composition. SEq is complete for homotopy models and finite CW-complexes, and its word problem is decidable in exponential time.

  • Problem

    Higher identity type presentations can conflate strict equalities with laws that hold only up to path equivalence, although strict equality is a congruence and path equivalence is not.

    Source: §1 · pp. 1–2

  • Method

    The paper axiomatizes strict equality in SEq and constructs presheaf models with composition arising from pushouts in the cubical base category.

    Source: §1 · p. 2

  • Results

    SEq is sound and complete for homotopy models, complete over finite CW-complexes, and its word problem is decidable in exponential time.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The pushout construction supplies composition and explicit witnesses for associativity and identity laws in the presheaf setting.

    Source: §1 · p. 2

    The decision procedure has no matching lower bound, and its array representation is likely wasteful, leaving the word problem's true complexity open.

    Source: §4.5 · p. 19

Abstract

from arXiv · show

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.

1 Introduction

Higher identity types admit strict equality and path-witnessed equivalence, but standard presentations can conflate laws that hold strictly with laws that hold only up to a path. The paper isolates strict equality in SEq and develops completeness, decidability, and cubical presheaf models with composition on the base category.

1 Introduction

  • Strict equality is a congruence for cell operations, whereas associativity and identity laws hold only up to path equivalence, which is not a congruence for identity.Composition also requires boundaries to agree strictly, and no path can witness a boundary equation before it holds.Source: §1 · pp. 1–2
  • Standard weak ω-category and computad presentations impose strict and path-level laws together, obscuring distinctions such as exchange holding strictly in standard topological composition.When identity laws are weakened to path equivalences, the equation id α = id α ◦n n−1 id α must be stated separately.Source: §1 · p. 2
  • SEq axiomatizes strict equality with eleven equations involving globular maps, identities, and compositions, separating it from path-level equivalence.Its axioms include globular laws and exchange; the theory differs from computads and strong ω-categories.Source: §1 · p. 2
  • SEq is sound and complete for homotopy models, complete over finite CW-complexes, and admits an exponential-time decision procedure.The introduction also presents presheaf models with native composition and a calculus for constructing witnesses to associativity and identity laws.Source: §1 · p. 2
  • Cubical presheaf models place primitive composition on the base category via a pushout, rather than requiring each type to carry Kan composition.This recovers composition natively and in a way that respects higher-identity-type structure.Source: §1 · pp. 2–3
  • The pushout structure also supplies explicit higher-dimensional witnesses for associativity and identity laws, with coherence such as the pentagon verified equationally.The paper gives a calculus for the mediating morphisms used to construct these witnesses.Source: §1 · pp. 2–3
  • The paper establishes completeness for homotopy models and finite CW-complexes, alongside an exponential-time decision procedure for strict equality.These are separate results: completeness is proved for the two model classes, while decidability concerns the equational theory.Source: §1 · p. 3
  • The paper relates higher identity types viewed as iterated path spaces to their representation as cubical sets by a homeomorphism.The two views of the motivating homotopy models are described as homeomorphic.Source: §1 · p. 3

2 Homotopy Models

Homotopy models represent higher identity types either as iterated spaces of paths or as boundary-preserving maps from cubes into a space. Their sections and faces support definitions of identities, composition, and cells.

2 Homotopy Models

  • Homotopy models have equivalent views as an inductive hierarchy of path spaces and as boundary-preserving continuous maps I^n → X.The correspondence is a homeomorphism obtained by currying and uncurrying.Source: §2 · p. 3
  • Sections of a homotopy evaluate selected coordinates, while its source and target are its first-coordinate faces at 0 and 1.A homotopy is viewed as a deformation from source to target through intermediate sections.Source: §2 · p. 3

2.1 Identities and Composition

  • Identities extend a cell constantly in the first coordinate, and cells compose along a shared face when the adjoining sections agree.For k = 1, this composition is path concatenation; the matching face condition ensures continuity.Source: §2.1 · p. 4

2.2 Cells

  • An n-cell for n ≥ 2 has cell-valued intermediate sections and identity-valued faces along its second coordinate at 0 and 1.The cubical representation of a 3-cell factors through a spherical diagram.Source: §2.2 · p. 4

3 Equational Presentation

Section 3 presents an equational theory for a broad class of algebraic models, including the homotopy models of §2, with axioms separating strict-equality properties such as congruence and the globular and exchange rules. It also shows that adding higher-stage elements creates no new equations among elements of dimension n or less, using picture equivalence of irreducible forms.

3.1 Syntax

  • Terms are built from dimensioned atomic symbols using src, tgt, id, and dimension-indexed composition, with well-formedness and dimension determined by inference rules.The section distinguishes well-formed terms from terms that are meaningful in a model.Source: §3.1 · p. 5

3.2 Axioms for Equality

  • The axioms for equality extend the usual equality and congruence rules with globular rules (viii) and (ix) and the exchange rule (xi), defining SEq.The section calls (viii) and (ix) the globular rules and (xi) the exchange rule.Source: §3.2 · p. 5

3.3 Algebraic Semantics

  • Meaningful compositions require matching boundaries under the equational theory, and meaningful terms modulo the equations form a free model of those equations and the axioms.For composition u ◦n m v, the required equality is src^(n−m) u = tgt^(n−m) v; when m=n−1, this is src u = tgt v.Source: §3.3 · p. 5

3.4 Free Globular Models

  • Free globular models are built from staged equational theories linked to globular maps, and higher stages conservatively extend earlier ones.The passage also states that the substructure generated at stage n is already determined at that stage.Source: §3.4 · pp. 6–7

3.5 Properties of Free Globular Models

  • In Tn, every term of dimension k≥n is Est-equivalent to an iterated identity on an n-dimensional term, and adding higher-stage elements creates no new terms of dimension at most n.Source: §3.5 · p. 7
  • The oriented rewrite system is strongly normalizing and confluent on Tn, with irreducible forms unique up to picture equivalence.The theorem also states that when u and v are Est-equivalent, their irreducible forms are picture-equivalent.Source: §3.5 · pp. 7–8
  • For the remaining critical-pair case, the irreducible forms of the two terms are equivalent via (xi).The other cases yield common irreducible forms; in the remaining case, the forms are related by applying (xi) to irreducible subterms.Source: §3.5 · p. 10
  • Adding higher-stage elements creates no new equations among elements of dimension n or less.If Est ⊢ u = v for elements of equal dimension at most n, their irreducible forms satisfy Est_n ⊢ u′ = v′.Source: §3.5 · p. 10
  • The proof places both irreducible forms in Tn and applies Theorem 3.5 to show they are picture equivalent.Because irreducible forms contain no src or tgt, dimension cannot increase along paths from roots to leaves.Source: §3.5 · p. 10

4 Completeness and Decidability

The section uses the picture interpretation to establish SEq completeness for homotopy models and finite CW-complexes, and to decide equality of terms in exponential time. Its decision procedure also determines whether a term denotes a cell.

4.1 Pictures

  • Pictures interpret terms over an indiscrete ambient space, preserve boundaries, and encode cells with finite arrays of dyadic samples.The passages note that all maps into this ambient space are continuous, so boundary preservation is the relevant structure.Source: §4.1 · p. 11

4.2 Finite Representation

  • Each picture Pic(t) is determined by finitely many values on a dyadic grid Ik1 × ··· × Ikn.The grid depths are chosen to satisfy the bounds in Theorem 4.5.Source: §4.2 · p. 13

4.3 Completeness over Homotopy Models

  • SEq proves exactly the term equalities that hold in all homotopy models with the given globular maps.The proof uses Pic as a complete invariant: terms with the same picture are provably equivalent.Source: §4.3 · p. 16

4.4 Completeness over Finite CW-Complexes

  • Completeness also holds over finite CW-complexes: equality in every such model implies provable equality in SEq.The picture model is a retract of a CW-complex, and a finite subcomplex suffices to distinguish terms with different pictures.Source: §4.4 · p. 17
  • SEq is sound and complete over CW-complexes, and any unequal terms are distinguished in a finite CW-complex.Although the constructed ambient complex may be infinite, each pair of terms maps into a finite subcomplex.Source: §4.4 · p. 18

4.5 Decision Procedure

  • The same algorithm decides whether a term denotes a cell, but no matching lower bound is known and the true word-problem complexity remains open.The authors note that the array representation is almost certainly wasteful.Source: §4.5 · p. 19
  • Equality of terms is decidable in exponential time in the irreducible composition-height measure h.The procedure constructs finite picture arrays and compares them; the grid resolution depends on composition nesting depth.Source: §4.5 · p. 19

5 Soundness over Presheaf Models

The section constructs presheaf models whose base-category pushouts provide composition while respecting globularity, then proves SEq sound for presheaves satisfying boundary preservation.

5 Soundness over Presheaf Models

  • Unlike standard presheaf presentations, this construction places composition in the base category rather than requiring each type to carry Kan composition structure.The base category has interval-like morphisms and is assumed generated by its subcategory on objects [0] and.Source: §5 · p. 19

5.1 Boundary preservation

  • Boundary preservation identifies specified face maps, and Theorem 5.2 derives the globular axioms from that condition.The theorem equates the presheaf images of maps differing in the listed face coordinates.Source: §5.1 · p. 20

5.2 Composition

  • Composition is internalized in the base category through a pushout, enabling presheaf composition without connections or Kan filling.The pushout structure also supplies the morphisms used to define composites.Source: §5.2 · p. 21

5.3 Soundness of the axioms

  • SEq is sound for presheaf models over the cubical base category, with boundary-preserving structures modeling higher identity types.The soundness result assumes presheaves preserve pullbacks as well as boundaries.Source: §5.3 · pp. 21–22

6 Witnesses for the Weak Laws

The same pushout structure that defines composition also supplies higher-dimensional witnesses for associativity and identity laws. A calculus of base-category morphisms verifies these witnesses and their coherence equationally.

6 Witnesses for the Weak Laws

  • The pushout structure yields witnesses for associativity and identity laws, while five equations on base-category morphisms verify their coherence, including the pentagon.Unlike the de Morgan approach described here, the witnesses arise from pushout mediating morphisms rather than Kan filling.Source: §6 · p. 25

6.1 A Calculus for the Morphisms of 

  • The faithful functor K represents base-category morphisms as functions on J^n, so morphism identities can be checked pointwise.J is the index set of interval maps δ_t, equipped with the metric induced by its inclusion into the real unit interval.Source: §6.1 · p. 25

6.2 Connections and Associativity

  • A connection built from an endpoint-preserving morphism c defines an interpolation used to construct associativity witnesses.The section states that associativity up to ≃ is witnessed by applying the presheaf to the resulting morphism.Source: §6.2 · p. 26

6.3 Higher Coherence

  • The pentagon identity follows by equational reasoning, and reassociation morphisms are constructed mechanically from the source and target bracketings.The construction and verification of coherence use five equations rather than diagram chasing.Source: §6.3 · pp. 27–28

7 Conclusion

The conclusion consolidates SEq’s semantic and rewriting results, then identifies limits of the presheaf models and decision procedure. It also frames future work on dependent-type structure and more succinct representations.

7 Conclusion

  • SEq’s eleven axioms are exactly the equations holding in every homotopy model and already in every finite CW-complex.Nine axioms form a strongly normalizing rewrite system with normal forms unique up to picture equivalence; adding higher-dimensional generators proves no new lower-dimensional equations.Source: §7 · p. 28
  • The resulting word problem is decidable, although the decision procedure materializes pictures as arrays and gives only a rough exponential upper bound.The authors suggest comparing succinct representations rather than whole arrays as a possible improvement.Source: §7 · p. 28
  • Pushout-based composition makes SEq hold strictly in boundary- and pullback-preserving presheaves, while the same structure supplies witnesses for laws holding only up to ≃.The conclusion identifies dependent-type fibration structure as absent and an open direction for these models.Source: §7 · p. 28

A Soundness over Homotopy Models

The appendix characterizes cells through conditions on their sections and boundaries, and records consequences for identities and sections of cells.

A Soundness over Homotopy Models

A.1 Soundness

The section establishes the remaining strict-equality soundness axioms, including identity composition and exchange. It also distinguishes path equivalence from strict equality by showing that path equivalence fails to be preserved by the identity operation.

A.1 Soundness

  • Axiom (x) holds: composing the identity cell with itself yields that identity cell.The lemma states id α ◦n n−1 id α = id α.Source: §A.1 · p. 32
  • The exchange law is the other remaining soundness case, stated for cells satisfying the requisite boundary conditions.The section says all other equations of §3.2 were established earlier.Source: §A.1 · p. 32
  • Path equivalence is a congruence for source, target, and composition, but not for the identity operation.If id α and id β are path equivalent, then α and β must be strictly equal.Source: §A.1 · p. 32

B.1 Set Representation

The section represents morphisms as functions on tuples through a faithful set-valued functor K. It establishes continuity properties of these functions and bounds the Lipschitz constant of composition.

B.1 Set Representation

  • K is faithful: a morphism is determined by its action on tuple representations of morphisms from [0].The tuples (t1, …, tn) correspond to δt1 ⊗ · · · ⊗ δtn.Source: §B.1 · p. 33
  • Every function Kf for a morphism → is uniformly continuous, while KL and KR contract distances by a factor of 1/2.KL(t) = t/2 and KR(t) = (t + 1)/2.Source: §B.1 · p. 33
  • The function K(f ♢g) is Lipschitz with constant 2 max cf, cg.The composition is evaluated piecewise using Kf or Kg on rescaled inputs on either side of 1/2.Source: §B.1 · p. 33

B.2 Equations for 1

The section gives sound equations and reduces morphism terms in the single-object category to a grammar with a unique reduced representation. Semantic equality of reduced terms entails syntactic identity.

B.2 Equations for 𝒜1

  • Lemma B.1’s equations are sound when both sides exist, and whenever a left-hand side exists, so does its right-hand side.The proof uses distributivity and uniqueness of the mediating morphism for the stated cases.Source: §B.2 · p. 34
  • Every generated morphism has a representation in the grammar S ::= S ♢ S | X | δt ◦ σ, with X built from L, R, and 1[1].The reduction applies distributivity, simplifies compositions, and then performs further reductions such as (U ◦ L) ♢ (U ◦ R) to U.Source: §B.2 · p. 34
  • Reduced terms that are semantically equal are syntactically identical, yielding unique reduced forms.The proof distinguishes compositions of L and R by their binary values and lengths.Source: §B.2 · pp. 34–35

C Properties of 

The section develops structural properties of the category, including faithful tensor and set representations. Morphisms admit reduced decompositions that are unique and are determined by their action on tuples.

C Properties of 𝒜

  • The identity δt ⊗ σ = δt ◦ σ = σ ⊗ δt relates tensor and composition forms.Source: C Properties of  · p. 35
  • The tensor product is faithful, and the functor N from sequences of objects and morphisms to their tensor products is faithful.The tensor product’s faithfulness means equality of tensor products determines equality of each factor.Source: C Properties of  · pp. 35–36
  • Every morphism has a reduced decomposition into specified types of factors, with adjacent δt ; σ pairs excluded.The reduction deletes null identities, reduces → factors, and uses δt ⊗ σ = σ ⊗ δt to reorder factors.Source: C Properties of  · p. 36
  • Morphisms agreeing on all tuple inputs have identical reduced decompositions.The proof establishes matching leftmost factor types and proceeds by induction.Source: C Properties of  · pp. 36–37
  • Closure under composition and tensor product adds no morphisms beyond those generated in 𝒜1 by δt, σ, L, and R.Source: C Properties of  · p. 37

D Higher Identity Types as Cells and Iterated Path Spaces

This appendix relates higher identity types built as iterated path spaces to cubical cells, using compact-open topologies to establish homeomorphisms and identify the corresponding identity types.

D Higher Identity Types as Cells and Iterated Path Spaces

  • Higher identity types are constructed inductively as path spaces, beginning with points of X and then paths, paths between paths, and higher paths.Path spaces use the compact-open topology, whose subbasic open sets specify that a compact subset of the domain maps into an open subset of the codomain.Source: D Higher Identity Types as Cells and… · pp. 37–38
  • When K is compact Hausdorff, currying gives a bijection between continuous maps A × K → B and continuous maps A → BK with the compact-open topology.For compact Hausdorff K1 and K2, this extends to a homeomorphism BK1×K2 → (BK2)K1.Source: D Higher Identity Types as Cells and… · pp. 37–38
  • Each inhabited identity type is a subspace of its ambient iterated path space, with the induced topology agreeing with its compact-open topology.The proof checks that subbasic open sets are restrictions of subbasic open sets in the ambient space.Source: D Higher Identity Types as Cells and… · p. 39
  • For every n, the space Hn of continuous maps In → A with the compact-open topology is homeomorphic to the iterated path-space view Vn.The inductive construction uses currying on the first argument.Source: D Higher Identity Types as Cells and… · p. 39
  • Boundary-equivalence classes of n-cells correspond bijectively to inhabited level-n identity types, with each class mapped homeomorphically to its corresponding type.The map also sends the set of n-cells onto the union of the level-n identity types.Source: D Higher Identity Types as Cells and… · p. 40
Loading 2610.28906v1…