PaperlayerView exact revision on arXiv

Source-linked AI summary

Univalence for inverse diagrams and homotopy canonicity

Michael Shulman

arXiv:1203.3253v3math.CT

TL;DR

The paper addresses whether univalence models extend beyond simplicial sets and whether univalence preserves computational canonicity up to homotopy. It develops homotopical gluing and inverse-diagram constructions, obtaining new univalence models and a partial homotopy-canonicity result for natural numbers.

  • Problem

    The paper addresses open meta-theoretical questions about univalence, including whether models exist beyond simplicial sets and whether univalence preserves canonicity.

  • Method

    The paper develops homotopical relational and gluing models using inverse diagrams, Reedy homotopy theory, and oplax limits, including type-theoretic fibration categories.

  • Results

    In 1-truncated type theory with one univalent universe of sets, every closed natural-number term is provably homotopic to a numeral, and inverse-diagram constructions yield further univalent models.

  • Takeaways & Limitations

    Univalence does not imply excluded middle and preserves computational content up to homotopy in the stated type-theoretic setting.

  • Takeaways & Limitations

    The homotopy-canonicity argument requires at least propositional η-conversion for dependent products.

Abstract

from arXiv · show

We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (infinity,1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.

1. Introduction

The paper develops constructions that preserve univalence across inverse diagrams and oplax limits, addressing semantic, logical, and computational questions about univalent type theory. Its applications produce new univalent models in higher toposes and establish a partial homotopy-canonicity result.

  • Logical consequences: The arrow-category model sSet^2 shows that univalence does not imply excluded middle.The original simplicial-set model lies in a classical metatheory, whereas the constructed arrow-category model does not satisfy excluded middle.
  • Constructions and semantics: Univalence is preserved when a model is extended to the functor category C^I for any inverse category I.Inverse categories have no infinite composable strings of nonidentity morphisms, enabling well-founded construction of diagrams and a univalent universe.
  • Logical consequences: The internal logics of sSet^I refute every propositional statement that is not an intuitionistic tautology.This follows from the propositional logic of sSet^I being the Heyting algebra of cosieves on I.
  • Constructions and semantics: The construction resolves a coherence problem for presenting univalent type theory as an internal language of the (∞,1)-topos ∞Gpd^I.The model category sSet^I presents this higher topos, while the paper connects univalence with object classifiers.
  • Homotopy canonicity: Gluing along a groupoid-valued global sections functor yields a partial answer to homotopy canonicity.In 1-truncated type theory with one univalent universe of sets, every closed natural-number term is provably homotopic to a numeral, preserving computational content up to homotopy.
  • Homotopy canonicity: The homotopy-canonicity result is weaker than the related judgmental-canonicity result of Licata and Harper.That work uses stricter equality rules under which univalence is true by definition and proves strict equality to a numeral.
  • Computational significance: Canonicity remains important for programming because added axioms can produce terms not provably equal to any specific numeral.The paper contrasts univalence's preservation of computational content up to homotopy with excluded middle, which can yield a term conditional on a Gödel sentence.

Organization.

The paper first develops categorical and type-theoretic foundations, then constructs and analyzes univalent structures for arrow and general inverse categories. It concludes by extending the method to oplax limits and applying it to gluing and canonicity.

  • Foundations: The paper begins by defining type-theoretic fibration categories and developing their basic homotopy theory and interpretation of intensional type theory.These categories support dependent sums, dependent products, identity types, and sometimes natural numbers, and include relevant syntactic and model categories.
  • Arrow categories: Sections 8–10 construct type-theoretic structure in the arrow category C^2 and prove that its universes inherit univalence.The arrow category is the first nontrivial inverse-category example treated in detail.
  • Inverse categories: Section 11 generalizes the construction to arbitrary inverse categories using Reedy homotopy theory.For general C, finite coslice categories and stability of acyclic cofibrations under homotopy pullbacks provide the needed conditions.
  • Oplax limits and applications: Section 12 extends the arguments to oplax limits, followed by applications to gluing constructions and canonicity in Section 13.The paper thereby moves from the inverse-category construction to its homotopy-canonicity application.

2. Type-theoretic fibration categories

Type-theoretic fibration categories package the categorical structure needed to interpret dependent type theory and homotopy-theoretic path objects. Their axioms support factorization, pullback stability, and path-object constructions.

  • A type-theoretic fibration category supports dependent sums, dependent products, identity types, and sometimes natural numbers through categorical fibration structure.The structure includes a terminal object, fibrations, pullbacks, dependent products, and specified factorization properties.
  • Its axioms require every morphism to factor as an acyclic cofibration followed by a fibration, with acyclic cofibrations stable under specified pullbacks.The factorization and stability conditions are expressed directly in axioms (5) and (6).
  • Path objects provide the factorization of diagonals needed to model identity types and support concatenation and homotopy constructions.The path-object factorization uses an acyclic cofibration into a path object followed by a fibration to the fibered product.
  • The resulting construction is motivated by mapping path spaces, but it works here because acyclic cofibrations are stable under pullback along fibrations.The corresponding mapping-path construction can fail in classical model structures without this stability property.

3. Homotopy theory in type-theoretic fibration categories

Type-theoretic fibration categories support an internal homotopy theory based on path objects and homotopy equivalences. The paper proves that they form categories of fibrant objects with homotopy equivalences as weak equivalences.

  • Type-theoretic fibration categories supply path-object homotopies whose relation is independent of the chosen path object.Homotopies are defined by lifts into path objects, and factorization through one path object implies compatibility with every other.
  • Homotopies compose, invert, and are preserved by precomposition and postcomposition, yielding weak higher-groupoidal operations.The induced operations respect concatenation up to homotopy and support fiberwise homotopy comparisons.
  • Acyclic cofibrations are characterized by homotopy inverses whose composite homotopy is constant on the source.This characterization underlies the cancellation result for acyclic cofibrations.
  • Every type-theoretic fibration category is a category of fibrant objects whose weak equivalences are the homotopy equivalences.This is the section's principal structural theorem.

4. Categorical semantics of type theory

The categorical semantics interprets type theory through type-theoretic fibration categories, while coherence results address the mismatch between strict substitution and pullback up to isomorphism. Split structures make the semantics strictly manageable.

  • A type-theoretic fibration category provides an internal language for intensional dependent type theory, subject to a coherence issue for pullback-based substitution.Substitution is strictly functorial syntactically, whereas categorical pullbacks preserve structure only up to isomorphism.
  • Coherence theorems can be applied after construction, while special constructions may preserve coherence directly when stricter information is needed.The paper uses the latter approach for the arrow-category case and the former for generalizations.
  • Cloven structures add specified fibration structures, pullbacks, dependent products, path objects, and liftings to make categorical semantics explicit.The additional structure includes specified natural-number fibrations when natural numbers are present.
  • Every type-theoretic fibration category can be cloven, and slice categories inherit cloven structure canonically.The paper gives this as Examples 4.2 and 4.3.
  • The syntactic category of any type theory is initial among split type-theoretic fibration categories with the corresponding structure.Split structures are essentially algebraic, with strict functors preserving the specified structure on the nose.

5. Homotopy type theory

The section develops type-theoretic operations for paths, transport, contractibility, propositions, and equivalences, together with their categorical interpretations. It also relates function extensionality to equivalence predicates and acyclicity preservation.

  • Paths and transport: Path concatenation and inversion provide the type-theoretic counterparts of categorical path-object operations.The concatenation operation p · q composes paths x ⇝y and y ⇝z.
  • Contractibility and propositions: Contractibility and h-propositions are characterized categorically through path objects and sections of associated fibrations.A global element of isContr(A) witnesses homotopy equivalence with the terminal object, while isProp(A) expresses that any two maps into A are homotopic.
  • Equivalences: The predicates hEquiv(f) and isEquiv(f) are equivalent in inhabitation, while isEquiv(f) is better behaved under the stated constructions.The paper constructs maps in both directions between the two types.
  • Function extensionality: Function extensionality makes the relevant equivalence predicates h-propositions and is equivalent to dependent products preserving acyclic fibrations.Theorem 5.6 states that the function happly is an equivalence under the displayed condition.
  • Paths and transport: Transport interprets categorically as the morphism used in the Acyclic Fibration Lemma.It sends b : B(x) to p∗b : B(y) along a path p : x ⇝y.

6. Universes

The section formalizes universes categorically as fibrations classifying small fibrations and equips them with structure for type formation. It then defines cloven, split, and embedded universes and explains their interpretation in type-theoretic fibration categories.

  • Universe structure: A universe is a fibration whose small fibrations are closed under composition, dependent products, and the specified factorization condition.Small fibrations are defined as pullbacks of the universe fibration.
  • Universe structure: Universe structure supplies categorical representatives for unit types, dependent sums and products, identity types, and optionally natural numbers.A cloven universe specifies morphisms implementing these operations.
  • Cloven and split universes: Split universes require the specified pullbacks to agree with the ambient structured fibrations, yielding the definitional equalities of the type-theoretic operations.Every universe can be made split in an equivalent category, while syntactic universes are split.
  • Cloven and split universes: A categorical universe interprets a type-theoretic universe in any type-theoretic fibration category containing the corresponding universe fibration.The interpretation uses the coherence theorem together with the split structure.
  • Universe embeddings: Universe embeddings preserve the universe fibration and its operations across nested universes, with a unique induced structure under the stated monicity and no-new-names assumptions.The construction extends to collections with a largest universe.

7. The univalence axiom

The section presents univalence as an equivalence between paths in a universe and equivalences of its types, then gives univalent universes in toposes, groupoids, and simplicial sets. These examples support nested and truncated universes but also expose scope limitations.

  • Definition and categorical form: Univalence asserts that the canonical map from paths in the universe to equivalences between types is an equivalence.Categorically, the map PU → E over U × U is required to be an equivalence.
  • Examples: In an elementary topos, the subobject classifier gives a univalent universe classifying monomorphisms, whose internal types are h-propositions.For Set, the only small objects for this universe are ∅ and 1.
  • Examples: The groupoid model has a univalent universe of small sets because its equivalence fibration is isomorphic to the universal isomorphism fibration.The fiber over sets (a,b) is the set of isomorphisms from a to b.
  • Examples: Simplicial sets support intensional type theory with as many univalent universes as there are inaccessible cardinals.The underlying univalent universe classifies Kan fibrations with fibers below the chosen size bound.
  • Scope and limitations: Subuniverses of n-truncated Kan fibrations yield univalent universes with increasing truncation levels, while not every larger groupoid universe is univalent.The groupoid universe of all small groupoids is explicitly identified as a non-univalent example.

8. The Sierpinski (∞, 1)-topos

The arrow category of a type-theoretic fibration category inherits its type-theoretic structure through Reedy fibrant diagrams. This construction preserves key homotopical and extensional structure, including function extensionality and natural numbers objects.

  • Reedy fibrant diagrams: Reedy fibrant objects in the arrow category model two-type contexts, with a base type followed by a dependent type.A Reedy fibrant arrow has fibrant domain and a fibration as its structure map.
  • Reedy structure: Theorem 8.8 establishes that Reedy fibrant arrows form a type-theoretic fibration category.The proof supplies terminal objects, fibrations, pullbacks, dependent products, and acyclic cofibrations using Reedy constructions.
  • Natural numbers: When the base category has a natural numbers object, the Reedy category inherits one that is also strictly preserved by the codomain functor.This extends the preserved type-theoretic structure beyond dependent operations and identity types.
  • Homotopical properties: Reedy homotopy equivalences are exactly levelwise homotopy equivalences, while acyclic fibrations admit equivalent componentwise characterizations.This identifies the homotopical content of the diagram model with that of its two levels.
  • Extensionality: The construction preserves function extensionality and can choose its witness strictly preserved by the codomain functor.The same strict preservation holds for a supplied witness of function extensionality.

9. Universes in the Sierpinski (∞, 1)-topos

A universe in the base category induces a universe for Reedy small fibrations in the arrow category. Universe embeddings and internal universe structure lift as well, with strict preservation by the codomain functor.

  • Constructing the universe: Theorem 9.4 shows that V is a universe for Reedy small fibrations, with cloven or split structure strictly preserved by codomain.Its levels are built from U and the universe of dependent types U^(1).
  • Constructing the universe: The constructed universe V classifies exactly the Reedy small fibrations in the arrow category.A map is V-small precisely when it is a pullback of the universal fibration q over V.
  • Internal interpretation: The induced universe represents a dependent type over a type family, allowing dependent sums, products, and path types to be constructed in the arrow category.These operations are obtained by interpreting the corresponding specified operations of the base universe.
  • Universe embeddings: Every universe embedding in the base category induces an embedding of the corresponding universes in the arrow category, even when it adds new names.This also permits lifting countably infinite sequences of universe embeddings.
  • Universe embeddings: The number of internal universes is preserved, and all lifted universes are strictly preserved by the codomain functor.Thus the construction scales to any collection of internal universes already present in the base type theory.

10. Univalence in the Sierpinski (∞, 1)-topos

Univalence transfers from a universe in the base category to the induced universe in the Reedy arrow category. The proof reduces the new level to equivalences supplied by function extensionality and base-category univalence, yielding new simplicial-set models.

  • Univalence transfer: If U is univalent in the base category, then the corresponding universe V in the Reedy arrow category is univalent.The proof establishes the universal identity-equivalence section as an equivalence at both levels.
  • Proof of univalence: The level-one argument factors through path-to-equivalence and function-extensionality maps, each shown to be an equivalence.Base univalence supplies pathToEquiv, while strong function extensionality supplies happly.
  • Application: The construction therefore supplies a new model of the univalence axiom and enlarges the class of models obtained from inverse-diagram homotopy theory.The arrow-category case is the first nontrivial example treated in detail.
  • Application: The Reedy model category sSet^2 supports intensional type theory with dependent sums, products, identity types, and as many univalent universes as there are inaccessible cardinals.Its homotopy theory presents the Sierpinski (∞,1)-topos.

11. Diagrams on inverse categories

The section develops Reedy homotopy theory for diagrams indexed by inverse categories, using well-founded induction and matching objects to extend type-theoretic structure. It shows that admissible inverse-diagram categories inherit type-theoretic fibration categories and univalent universes, yielding models in simplicial-set diagrams with strong logical properties.

  • Inverse diagrams: Inverse categories support inductive diagram construction because their nonidentity-morphism relation is well-founded, with matching objects controlling extensions at each object.An extension at x consists of an object A_x together with a map to its matching object M_xA.
  • Reedy structure: Reedy fibrations are defined by requiring matching objects and fibrations from each diagram component to the corresponding matching pullback.For a Reedy fibrant diagram A, each map A_x → M_xA is a fibration.
  • Inverse diagrams: Reedy fibrant diagrams over finite inverse categories correspond to contexts of a certain form in the underlying type theory.For general inverse categories, the analogous objects are treated as a type of infinite context.
  • Admissibility: Type-theoretic model categories have Reedy limits for every small inverse category, while type-theoretic fibration categories obtain them under suitable finiteness or product assumptions.In particular, finite inverse categories are admissible for any type-theoretic fibration category.
  • Inherited models: For an admissible inverse category I, the Reedy fibrant diagram category (C^I)_f is a type-theoretic fibration category, and univalent universes in C induce univalent universes there.The induced universe is built for Reedy small fibrations.
  • Applications: For any small inverse category I, the Reedy model category sSet^I supports intensional type theory with dependent sums and products, identity types, and many univalent universes.The number of available univalent universes is tied to inaccessible cardinals larger than |I|.
  • Applications: The internal propositional logic of sSet^I matches that of Set^I, and cosieves on inverse categories suffice to refute every non-intuitionistic propositional statement.Thus the univalence axiom does not imply any such non-intuitionistic statement.

12. Oplax limits

The section generalizes Reedy constructions from diagram categories to oplax limits of inverse diagrams of type-theoretic fibration categories. This framework preserves type-theoretic structure and univalence, encompassing gluing, scones, and logical-relations constructions.

  • Oplax limits: Oplax limits generalize diagram categories and include gluing constructions, scones, logical relations, and homotopical canonicity applications.The oplax limit of a constant diagram at C is the ordinary diagram category C^I.
  • Technical foundation: Strong fibration functors preserve equivalences because they preserve fibrations and acyclic cofibrations, hence path objects and homotopies.This preservation supports the homotopical structure needed by the oplax-limit construction.
  • Oplax limits: An oplax-limit object assigns an object A_x in each component category and coherent transition maps A_x → α*(A_y) for every arrow α.Morphisms are componentwise maps satisfying the corresponding compatibility equations.
  • Reedy structure: Reedy fibrancy in an oplax limit is characterized by matching objects and fibrations A_x → M_xA in each component category.The matching object at x is formed from the diagram of pulled-back objects indexed by the incoming nonidentity arrows.
  • Inherited structure: For an admissible diagram C:I^op→TTFC, the Reedy fibrant oplax limit is a type-theoretic fibration category with levelwise homotopy equivalences.Function extensionality is inherited when every component category has it.
  • Universes: Admissibility for component universes produces a universe for Reedy small fibrations, and universe embeddings assemble into an induced embedding in the oplax limit.The induced universe is univalent when the component universes are univalent.

13. Gluing, scones, and canonicity

The gluing construction uses homotopical global sections and oplax limits to build scones that preserve univalence and establish homotopy-canonicity results under truncation assumptions.

  • Gluing construction: The oplax-limit construction specializes to the comma category (D ↓Γ), whose Reedy fibrant objects are fibrations A1 ։ Γ(A0).For the gluing application, Γ is a strong fibration functor, and the index category is 2.
  • Gluing construction: The homotopical global-sections functor Γ0 is obtained by quotienting ordinary global sections by homotopy because ordinary global sections do not preserve equivalences.When the source is 0-truncated, Γ0 is a strong fibration functor.
  • Gluing construction: The 0-scone equips each object with a homotopy-invariant family of sets over its global sections and inherits a univalent universe from a 0-truncated source with one.Its small objects are source-small objects equipped with homotopy-invariant subsets of global sections.
  • Scope and limitations: A 0-truncated univalent universe is constrained because any small type with a nontrivial automorphism creates a nonidentity self-path in the universe.Consequently, the construction considers universes whose types are h-propositions, while the natural numbers object is kept outside the universe.
  • Canonicity: Every term of natural number type is homotopic to a numeral in 0-truncated univalent type theory with function extensionality and a shnno.The theory assumes one univalent universe; the shnno need not belong to that universe.
  • Groupoid-valued gluing: For the groupoid-valued construction, soundness of the natural numbers object is preserved, and the resulting model has two nested univalent universes with the natural numbers object in the second.The syntactic category’s shnno is sound because its strict functor to Set preserves it.
  • Scope and limitations: The proof of the groupoid-valued result uses the law of excluded middle in the metatheory, and whether this can be avoided is left open.
  • Canonicity: Every term of natural number type is likewise homotopic to a numeral with 1-truncation, function extensionality, two nested univalent universes, and a shnno in the second universe.The proof lifts closed natural-number terms into a groupoid-valued gluing model.
Loading 1203.3253v3…