Source-linked AI summary
Cubical Type Theory: a constructive interpretation of the univalence axiom
Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
TL;DR
The paper develops a constructive type theory and semantics supporting direct manipulation of cubes while preserving computational interpretations for postulated constants. It refines cubical semantics, designs operations for composition and glueing, and proves univalence, while identifying a limitation concerning standard judgmental equalities for identity types.
Problem
The work seeks a constructive justification of Voevodsky’s univalence axiom while preserving type theory’s computational properties.
Method
The paper refines cubical semantics with de Morgan-algebra operations and diagonal structure, then designs contexts, restriction, composition, glueing, and face-lattice operations for an extended type system.
Results
The system expresses and proves the univalence axiom, and its Path-type formulation transfers to the Martin-Löf identity type through a Path-equivalence.
Takeaways & Limitations
The construction supports cubical reasoning about identity types and provides semantic justifications for examples including spheres and propositional truncation.
Takeaways & Limitations
The model does not generally interpret the standard judgmental equalities of Martin-Löf identity types because constant paths need not induce constant substitution functions.
Abstract
from arXiv · showhide
This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.
1 Introduction
The paper develops a constructive justification of univalence through refined cubical semantics and a type system inspired by that semantics. It presents the system, its cubical-set semantics, and extensions including identity and higher inductive types.
- The work continues a program to provide a constructive justification of Voevodsky’s univalence axiom while preserving computational interpretations for postulated constants.
- The semantics refine prior work with de Morgan-algebra operations, a diagonal operation, and a new identity type equivalent but not judgmentally equal to path types.These changes support semantic justifications for spheres and propositional truncation and address the identity-type computation-rule problem.
- The type system extends Martin-Löf type theory with dimension names, context restriction, extensibility, Kan composition, and operations expressing preservation under equivalences.Univalence and composition for the universe are expressible using the new operation on types.
- The paper is organized into a type-system presentation, cubical-set semantics, and extensions with identity types and higher inductive types.
2 Basic type theory
The paper begins with a standard dependent type theory containing natural numbers, dependent functions, and dependent pairs, specified through syntax, inference rules, substitutions, and admissible structural properties.
- The basic theory includes natural numbers but no universes, together with β- and η-conversion for dependent functions and surjective pairing for dependent pairs.Universes are considered later in the paper.
- The syntax comprises variables, dependent functions, dependent pairs, natural-number constructors and recursion, and associated type formers.
- Contexts, terms, and types are governed by inference rules, with substitutions acting by simultaneous replacement and α-equivalence identifying bound-variable renamings.
- Substitutions are defined inductively over contexts, extending a substitution with a term of the appropriately substituted type.
- Substitution is admissible, and weakening follows: judgments valid in a context remain valid in any extension of that context.
3 Path types
Path types represent dimensions of cubes using names from a de Morgan interval, with abstraction, application, faces, and connections supporting geometric reasoning. They enable direct constructions such as function extensionality, singleton contractibility, and equality operations.
- 3.1 Syntax and inference rules: The interval is modeled as a free de Morgan algebra on dimension names, with lattice operations and involution representing formal interval expressions.Its elements have a grammar built from 0, 1, names, involution, conjunction, and disjunction.
- 3.1 Syntax and inference rules: Path types extend the syntax with Path A t u, path abstraction, and path application, while substitutions at 0 and 1 represent cube faces.
- 3.1 Syntax and inference rules: Names in contexts represent cube directions, and substitutions using conjunction or disjunction produce connection operations corresponding to special square degeneracies.
- 3.2 Examples: Path types support equality-like constructions, including a path witnessing the relationship between pairs of points and paths.
- 3.2 Examples: The resulting operation satisfies judgmental equalities that do not hold judgmentally for inductively defined identity types.
- 3.2 Examples: Function extensionality is directly provable for path types by abstracting over a dimension in pointwise paths between functions.
- 3.2 Examples: Singletons are shown contractible, and composition operations are added to justify elimination principles for paths.
4 Systems, composition, and transport
This section extends dependent type theory with face formulas, restricted contexts, systems, and composition operations for manipulating compatible subfaces of cubes. Composition supports transport, path constructions, and Kan filling.
- The face lattice: Face formulas form a distributive lattice whose elements describe sub-polyhedra and whose equality is decidable.They are generated by endpoint equations, conjunction, and disjunction; every element has a disjunctive normal form.
- Context restriction: Restricted contexts represent compatible unions of cube faces, allowing types and terms to be specified on sub-polyhedra.For example, a restriction by (i = 0) ∨(j = 1) describes two faces of a square.
- Systems: Systems combine locally defined types or terms when their face extents cover the context and agree on overlaps.The inference rules require Γ ⊢ ϕ1 ∨ · · · ∨ ϕn = 1F : F, including an empty-system case.
- Systems: An extensible partial element on a face is represented by a total element agreeing with it on that face.This notation also expresses paths by specifying compatible endpoint values on opposite faces.
- Composition and transport: Composition preserves extensibility along paths and satisfies a substitution equality expressing uniformity.It takes a partial element and a starting endpoint and produces an element at the opposite endpoint.
- Composition and transport: Compositions yield transport and Kan filling, so open boxes can be computed together with their fillings.When the extent is the boundary formula, the construction recovers the Kan operation for cubical sets.
5 Derived notions and operations
This section develops contractibility, equivalences, and preservation operations needed for later constructions. It characterizes contractible types and shows that suitable extension data can establish equivalence.
- Contractibility: Contractibility is represented by a center together with paths from every element to that center.The type is defined as isContr A = (x : A) × ((y : A) → Path A x y).
- Contractibility: The contr operation composes paths from a contractibility witness to extend partial elements across a face.It uses the composition operation to produce an element agreeing with the prescribed partial data.
- Contractibility: A contractibility characterization constructs a witness by connecting an arbitrary element to a canonical element with a fresh interval name.The proof assigns the two endpoints of the interval to the canonical and arbitrary elements, then forms a path.
- Preservation operations: The pres operation states that functions preserve composition up to path equality.Its output connects composition after applying a function with applying the function after composition.
- Equivalences: An equiv operation packages local equivalence data, and conversely such an operation can prove that a function is an equivalence.The construction uses contractibility of fibers of the function.
6 Glueing
This section introduces glueing to make extensibility invariant under equivalence and uses it to construct universe composition and prove univalence. Glueing combines a partial type with a total type along an equivalence.
- Purpose of glueing: Glueing expresses that extensibility is invariant under equivalence and supplies the basis for universe composition and univalence.These later constructions are explicitly obtained from the glueing operation.
- Glueing syntax: Glue types and terms combine a partial type T and an equivalence to a total type A along a face formula.The corresponding unglue operation maps glued elements back through the equivalence.
- Glueing syntax: A glued element has type T on the restricted extent where the partial equivalence is specified.This follows directly from the glue inference rules.
- Glueing examples: An equivalence between A and B yields a path between them by glueing A to B with the identity equivalence at the endpoint.The construction defines E with E(i0) = A and E(i1) = B.
- Glueing examples: In the universe, glueing defines a function from equivalent types to paths between those types.The function has type (A B : U) → Equiv A B → Path U A B.
- Composition for glueing: Composition for a glue type computes through the partial type, function preservation, equivalence data, and composition in the total type.When the face formula is total, the definition agrees with composition for the partial type.
- Composition for glueing: The glue composition agrees with partial-type composition when the side condition makes the face formula equal to 1F.This agreement is required because the glued type then coincides with the partial type.
7 Universe and the univalence axiom
The universe construction turns paths in the universe into equivalences and uses this construction to prove univalence in cubical type theory.
- Constructing equivalences: A line E between types A and B is used to construct an equivalence equivi E : Equiv A B.The construction defines maps in both directions using transport and filling, then proves the resulting map is an equivalence.
- Glue and composition: Universe composition is defined by replacing the composed family with a Glue type built from the endpoint equivalence.The composition operation has the form comp_i^U [ϕ ↦ E] A0 = Glue [ϕ ↦ (E(i1), equivi E(i/1 − i))] A0.
- Glue and composition: The proof establishes that unglue : B → A is an equivalence for glued types.This result supports the universe composition operation and the later contractibility argument.
- Univalence: For any type A : U, the type of pairs consisting of a universe object and an equivalence to A is contractible.This contractibility result is used to derive the univalence axiom.
- Univalence: The map t A B : Path U A B → Equiv A B is an equivalence, establishing the univalence axiom.The paper also notes that alternative proofs of univalence appear in Appendix B.
8 Semantics
The semantics interprets cubical type theory in cubical sets, a presheaf model that supports dependent type formers, paths, and fibrant types constructively.
- Cubical sets: Cubical sets are defined as presheaves on a category whose objects are finite sets of names and whose morphisms use the free de Morgan algebra.The category of cubes is constructed through the Kleisli category of the free de Morgan algebra monad.
- Cubical sets: Cubical sets assign sets to cubes together with restriction maps satisfying identity and composition laws.These restriction maps model the behavior of terms under substitutions between cubes.
- Type-theoretic structure: Dependent types and terms are interpreted as presheaf-like families over semantic contexts, with reindexing along substitutions.Context extension, substitution, dependent sums, and dependent functions are defined from these families.
- Fibrancy and soundness: The cubical-set model supports dependent products, dependent sums, natural numbers, and an extension to fibrant types.The paper then uses this structure to interpret the full cubical type theory.
- Path types: Path types are represented by name abstraction over an additional cube dimension, with endpoints obtained by substituting 0 and 1.This gives paths as equivalence classes of families over a fresh name.
- Fibrancy and soundness: The interpretation of the syntax is sound, with all interpretation occurrences in the conclusions defined.The semantics uses a partial interpretation function from raw syntax into the CwF with fibrant types.
9 Extensions: identity types and higher inductive types
The paper extends cubical type theory with an identity type recovered from paths and with higher inductive types including spheres and propositional truncation.
- Identity types: The standard Martin-Löf identity type is not directly interpreted because transport along constant paths need not be judgmentally constant.The paper identifies this as a limitation of the path-based interpretation.
- Identity types: A new identity type marks paths known to be constant, allowing the desired judgmental computation rule for elimination.The reflexivity term is defined using a path together with a constancy witness, and J d a (r a) = d holds judgmentally.
- Identity types: The identity and path types are Path-equivalent, so contractibility transfers between them and univalence holds for the identity type.The univalence result proved for Path therefore extends to Id.
- Higher inductive types: The circle is introduced as a higher inductive type with a base point, a loop, and composition as a constructor.Its dependent eliminator maps the base point and loop into a dependent type while respecting composition.
- Higher inductive types: The same construction defines spheres S^n using constructors base and loop(r1, . . . , rn).The paper presents this as a generalization of the circle construction.
- Higher inductive types: Propositional truncation is defined with an inclusion, a squash constructor, and restricted composition operations.The general composition operation is obtained using squeeze and transport, while elimination maps into types with path-connected points.
10 Related and future work
The paper relates cubical techniques to equality reasoning and reports formal verification of substantial semantic components. It closes by identifying normalization, inductive-family semantics, higher inductive types, and resizing as open directions.
- Cubical techniques simplify reasoning about equality in homotopy type theory through judgmental equalities and notation for higher-dimensional cubes.
- The paper’s semantics has been formally verified in NuPrl, including Kan filling via composition and composition for glueing.
- The authors expect their presheaf semantics could support proofs of normalization and decidability of type checking.
- Open problems include extending identity-type semantics to inductive families and developing general syntax and semantics for higher inductive types.
- Another open direction is adding resizing rules and proving normalization.
4. Is there a model where Path and Id coincide?
The glueing-composition construction builds a final glued element through successive approximations, partial data, paths, and compatibility checks. The construction is illustrated for a specified extent and cubical boundary conditions.
- Intermediate steps progressively construct the final elements t1 and a1 while satisfying increasingly many required equations.
- Figure 5 illustrates the construction with ψ = (j = 1) and ϕ = (i = 0) ∨(j = 1) ∨(i = 1).
- The construction sets δ = ∀i.ϕ, making δ independent of i and representing the picture’s right-hand side in the example.
- The first approximation a′1 need not lie in the image of f(i1), while t′1 is a partial result and ω is a partial path.
- The fourth step constructs t1 and a path α between a′1 and f(i1) t1 over ϕ(i1).
- The final step builds a1 from a′1 and α, yielding the glued element b1.
B Univalence from glueing
The appendix gives alternative proofs of univalence using the glue construction. The proofs establish that paths between universe elements correspond to equivalences, with one route passing through a retract and contractibility argument.
- The appendix presents two alternative proofs of the univalence axiom using only the glue construction.
- For an equivalence f : Equiv A B, the construction defines eqToPathf using a Glue type over the interval.
- The canonical map pathToEq : (A B : U) → Path U A B → Equiv A B satisfies the univalence axiom.
- The first proof identifies the canonical map pathToEq with a path-indexed equivalence construction using function extensionality and path induction.
- The second proof makes Equiv A B a retract of Path U A B, so the corresponding dependent type is a retract of a contractible type.
- The second proof uses only the first two points of Lemma 25, whereas the first uses all three.
C Singular cubical sets
The singular cubical set construction uses idempotent retractions on interval-valued cubes and proves their uniformity under strict maps. This yields a composition structure for singular cubical sets associated with topological spaces.
- The construction assumes idempotent functions rI that fix points exactly when ∂Iu = 1 or z = 0 and satisfy a strict-map compatibility law.
- A geometric retraction from above center provides an example satisfying the required properties for strict maps.
- For each formula ψ, the induced idempotent rψ fixes points where ψu = 1 or z = 0.
- The functions rψ are uniform under maps f, satisfying rψ(f × id) = (f × id)rψf.
- A special case distinguishes ∂Jf from ∂I in general.
- The singular cubical set associated with a topological space has a composition structure.