Source-linked AI summary
Weak omega-categories from intensional type theory
Peter LeFanu Lumsdaine
TL;DR
The paper asks how terms of a type and its higher identity types can form a weak ω-category. It constructs a contractible globular operad of Id-rule-definable composition laws and gives it an action on types. Consequently, the terms of any type and its iterated identity types carry a weak ω-category structure.
Problem
The paper addresses whether terms of a type together with its higher identity types form a weak ω-category.
Source: §1.1 · p. 2Method
It constructs a contractible globular operad of definable composition laws using the Id-rules and gives the operad an action on types.
Source: §1.2 · pp. 3–4Results
The terms of any type and its iterated identity types carry a PMLId-algebra structure and hence form a weak ω-category.
Source: §4.4 · p. 18Takeaways & Limitations
The Id-only fragment supplies the structure needed to give types in theories extending MLId a weak ω-category action.
Source: §1.2 · p. 4The method does not establish contractibility for the endomorphism operad of composition laws in the full type theory.
Source: §4.3 · p. 18
Abstract
from arXiv · showhide
We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the terms of any type and its identity types.
1. Introduction
The paper argues that terms of a type and its iterated identity types form a weak ω-category, and constructs a contractible globular operad of definable composition laws to provide that structure. It builds the operad in the Id-only fragment and uses its action on any type to obtain the result.
1.1. Overview.
- The proposed syntax-to-higher-category perspective treats types as objects, terms as arrows, and identity proofs as higher cells, with cell dimensions shifted down for a fixed type.The paper adopts Leinster’s definition of weak ω-category.Source: §1.1 · p. 2
1.2. Outline of the construction.
- Identity transitivity has two natural composites, cl and cr, which are not definitionally equal but are propositionally equal via a 2-cell.The alternatives arise by applying Id-elim to p or to q.Source: §1.2 · p. 3
- Leinster’s globular operad with contraction packages composition laws and supplies an action that defines a weak ω-category.The construction restricts to laws definable using Id-rules, allowing it to apply to a wider class of theories.Source: §1.2 · p. 3
- The operad PMLId is constructed from definable composition laws in MLId[X] and shown to be contractible.The construction uses the Id-rules and a generic base type X.Source: §1.2 · pp. 3–4
- For any type in a theory extending MLId, its terms and iterated identity types carry a PMLId-action and hence an internal weak ω-category structure.The theorem also covers dependent types over a closed context.Source: §1.2 · p. 4
2. Type-theoretic setting
The paper works in an Id-only fragment of intensional Martin-Löf type theory and develops its syntactic-category tools. These support translations, limits, and the transfer of the construction to other types and contexts.
2.1. The type theories MLId, MLId[X].
- The paper works in MLId, a fragment with only Id-types, and constructs the operad from this fragment to cover theories that may also have other type formers.The presentation requires care because rules equivalent with dependent products or sums may differ without them.Source: §2.1 · p. 4
- The presentation lists the assumed rules in Table 1 and gives the Id-rules in full in Table 2, including exchange and dependent contexts.The text notes that exchange and the extra dependent context are often omitted when Π-types are present.Source: §2.1 · pp. 4–5
- The notation A^n denotes the nth iterated identity type of A, with A^0 := A.The paper sometimes omits the superscript when it is unambiguous.Source: §2.1 · p. 5
2.2. Translations and syntactic categories.
- A translation preserves Id-types and their term constructors up to definitional equality; adjoining a fresh base type X lets a translation specify its image as a closed type.For any closed type A in a theory extending MLId, Proposition 2.1 gives a unique such translation from MLId[X] taking X to A.Source: §2.2 · pp. 5–6
- The syntactic category C(T) has closed contexts as objects and context maps as arrows, considered up to definitional equality.Context maps support substitution of types along the map.Source: §2.2 · p. 6
- The paper’s context diagrams yield limits in syntactic categories, which translations preserve, and a slice theory represents types and terms in a fixed context.The slice T/Γ adjoins a generic term of type Γ.Source: §2.2 · p. 6
3. Globular operads and weak ω-categories
Globular operads encode composition laws for pasting diagrams and how those laws compose. With a contraction, an operad can act on a globular object to give it weak ω-category structure; endomorphism operads make such actions available in suitable categories.
3.1. Globular sets and operads.
- A globular set consists of cells in each dimension with source and target maps, while its pasting diagrams represent free strictly associative composites of those cells.For a type A, contexts and dependent projections form a globular object in the type theory’s syntactic category.Source: §3.1 · p. 7
- A globular operad packages operations for composing pasting diagrams, with maps specifying identity operations and composition of operations.An action applies an operation to a diagram labelled by cells, producing a single cell.Source: §3.1 · p. 8
- A contraction supplies fillers for parallel pairs and ensures operations exist with associativity and coherence witnessed by higher cells.An operad with contraction maps to the initial such operad, whose algebras define weak ω-categories.Source: §3.1 · p. 9
3.2. Endomorphism operads and more general actions.
- For a globular object whose diagram limits exist, its endomorphism operad consists of maps composing diagrams of each shape into cells and yields an operad action on that object.Such an action also induces an action on maps into the object, since the hom functor preserves limits.Source: §3.2 · pp. 10, 12
4. The contractible globular operad PMLId
This section constructs PMLId, the operad of definable composition laws on the generic type, proves it contractible, and describes its action on dependent-type globular contexts in theories extending MLId. The resulting structures make the terms of a type and its iterated identity types into a weak ω-category.
4.1. Construction of PMLId.
- PMLId is the endomorphism operad of the generic globular context X•, whose operations are definable composition laws.For globular objects in C(T), endomorphism operads are preserved by translations of type theories.Source: §4.1 · pp. 12–13
4.2. X is initial in MLId[X].
- In MLId[X], the context x : X is initial: every closed context has a unique context map from it.The paper notes this initiality need not hold in extensions of MLId[X].Source: §4.2 · p. 14
4.3. Contractibility of PMLId.
- PMLId is contractible: every parallel pair of composition laws for a pasting diagram has a filler.The proof inducts on the number of cells, reducing higher-dimensional cells using Id-elim; for a one-cell diagram, initiality makes the boundary terms reflexivity terms, and reflexivity supplies the filler. The method applies to MLId, while the paper says it cannot establish contractibility for all composition laws in the full theory.Source: §4.3 · pp. 17–18
4.4. Types as weak ω-categories.
- For any theory T extending MLId, closed context Γ, and dependent type A over Γ, the globular context A• is a PMLId-algebra and, via the operad’s contraction, an L-algebra.The action of PMLId on A• is induced by the translation from the generic type to A.Source: §4.4 · p. 18
- The globular set of terms of A and its iterated identity types in context Γ, Δ carries a PMLId-algebra structure and hence is a weak ω-category.Source: §4.4 · p. 18
- The construction is expected to be strictly functorial in T, Γ, and Δ, but functoriality in A is expected only through weak maps and is a harder question.The authors identify treatment of maps of internal operad algebras as a missing ingredient for the strict functoriality claim.Source: §4.4 · p. 18
- Garner and van den Berg independently prove essentially the same result using contractible operads built from endomorphism operads of identity-type globular contexts.Source: §4.4 · p. 18