Skip to content

Cubical Set

Represent a combinatorial or homotopical object as a contravariant set-valued functor on a declared cube category, with functorial face, degeneracy, and optional richer cube operations.

Version
v2 · 2026-09-06 · History
Domain-specific #
1600
Origin domain
mathematics
Subdomain
algebraic topology
Aliases
Cubical presheaf

Core Idea

Fix a cube category Box whose objects are formal n-dimensional cubes and whose morphisms describe the allowed ways of inserting endpoints, deleting or identifying dimensions, permuting coordinates, or adding connection operations. A cubical set is a presheaf

\[ X:\Box^{op}\to\mathbf{Set}. \]

The set X_n=X(Box^n) is the collection of abstract n-cubes of X. A cube map alpha:Boxm→Boxn induces a structure map X(alpha):X_n→X_m. The reversal of arrows is load-bearing: probing an n-cube along a lower-dimensional cube map produces its lower-dimensional face or specialization.

Scope of Application

Algebraic homotopy theory. Cube categories that are test categories let their presheaves present classical homotopy types after an appropriate localization. Cubical boundaries, horns or boxes, fillers, and geometric realization supply combinatorial analogues of paths and homotopies.

Homotopy type theory. Cartesian and De Morgan cubical sets provide interval objects and path semantics. Awodey develops a cartesian cubical model of homotopy type theory, while Cohen, Coquand, Huber, and Mörtberg use a richer cubical model to give constructive computational meaning to univalence and to handle function extensionality and selected higher inductive types.

Clarity

The shortest recognition test asks three questions: What is Box? What is X(Box^n) in each dimension? What maps does X assign to each morphism of Box? If the answer gives only cubes but no contravariant structure maps, it is not yet a cubical set.

Manages Complexity

Higher-dimensional attachment data can require many separate compatibility equations. The functor packages them into one law: identity maps act as identities and composite cube maps act by composite restrictions in reverse order. The cubical identities are no longer ad hoc bookkeeping; they are instances of functoriality.

Abstract Reasoning

Use this protocol:

  1. Declare Box and list its generating morphisms and equations.
  2. Specify X_n for each needed dimension.
  3. Give the induced face, degeneracy, and optional richer operations.
  4. Verify their cubical identities, or derive them from functoriality.
  5. Define morphisms as natural transformations commuting with every operation.
  6. Add fillers, labels, basepoints, realizations, or model structures only as separately declared layers.

Knowledge Transfer

Literal transfer occurs when topology, concurrency, type theory, or higher category theory retains the same presheaf grammar. The meanings of a 2-cell may differ, but Box, contravariance, dimension fibers, and functorial boundary maps remain recognizable.

Transfer from cubical to simplicial methods needs an explicit adjunction, triangulation, nerve, or comparison functor. Calling squares triangles does not preserve their face combinatorics. Transfer from a cubical set to a topological space likewise passes through geometric realization and may be considered only up to the declared equivalence.

Relationships to Other Abstractions

Local relationship map for Cubical SetParents appear above the current abstraction, mutual partners to the right, and children below. Node labels state whether each abstraction is prime or domain-specific; colors identify relation types.Cubical SetDOMAINDomain-specific abstraction: Functor — is a kind ofFunctorDOMAIN

Current abstraction Cubical Set Domain-specific

Parents (1) — more general patterns this builds on

  • Cubical Set is a kind of Functor Domain-specific

    Functor. A cubical set is literally a contravariant functor from a cube category to Set.

Hierarchy paths (4) — routes to 4 parentless roots

Neighborhood in Abstraction Space

Cubical Set sits in a sparse region of the domain-specific corpus (69th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Unclustered & Miscellaneous (1565 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-09-08