Fact-checked by Grok 2 weeks ago

Homotopy type theory

Homotopy type theory (HoTT) is a foundational framework for mathematics that extends Martin-Löf's intensional dependent type theory by integrating concepts from homotopy theory, interpreting types as topological spaces, terms as points within those spaces, and identity types as paths connecting points.^[1] This synthesis enables a homotopical treatment of equality, where higher-dimensional paths capture equivalences between structures, providing a constructive alternative to traditional set-theoretic foundations.[](https://ncatlab.org/nlab/show/homotopy+type+ theory) Central to HoTT are the univalence axiom, which identifies equality of types with their equivalence up to homotopy, and higher inductive types, which allow the specification of types along with their higher homotopical structure, such as loops and spheres.^[2] The development of HoTT traces back to the late 2000s, when researchers uncovered profound connections between the semantics of type theory and homotopy theory, particularly through interpretations of identity types as path spaces in simplicial sets and other model categories.[](https://ncatlab.org/nlab/show/homotopy+type+ theory) Key early contributions came from Vladimir Voevodsky, who proposed the univalence axiom as part of his work on univalent foundations, and from collaborations involving Steve Awodey, Michael Warren, and others who formalized these ideas in proof assistants.^[2] The field crystallized in 2013 with the publication of Homotopy Type Theory: Univalent Foundations of Mathematics, a collaborative effort by participants in the Univalent Foundations Program at the Institute for Advanced Study, which established HoTT as a viable system for formal mathematics.^[1] HoTT's core strength lies in its ability to natively handle ∞-groupoids and higher category theory, serving as the internal language of (∞,1)-toposes and enabling precise reasoning about homotopy invariants like fundamental groups and cohomology.[](https://ncatlab.org/nlab/show/homotopy+type+ theory) Unlike classical foundations, it supports synthetic homotopy theory, where homotopical concepts are defined internally without reference to external set-based models, facilitating both theoretical insights and computational verification.^[2] Implementations in proof assistants such as Coq, Agda, and Lean have demonstrated HoTT's practicality for formalizing complex proofs, including synthetic versions of classical results in algebraic topology.[](https://ncatlab.org/nlab/show/homotopy+type+ theory) In applications, HoTT bridges mathematics and computer science by offering a uniform language for specifying and verifying software, protocols, and mathematical theorems, with ongoing research exploring extensions like cubical type theory for canonicity and observational equality. As of 2025, HoTT continues to evolve with active research in areas like non-standard models, synthetic homotopy, and applications to AI architectures, supported by annual workshops such as HoTT/UF 2024.[](https://ncatlab.org/nlab/show/homotopy+type+ theory)^[3]^[4] It has influenced fields beyond homotopy, including synthetic differential geometry and formal semantics of programming languages, positioning it as a promising paradigm for dependable computation and rigorous mathematics.^[2]

Overview

Definition and core ideas

Homotopy type theory (HoTT) is an extension of Martin-Löf's intensional dependent type theory, in which types are interpreted as topological spaces, terms as points within those spaces, and identity types (representing equalities between terms) as paths connecting points.^[1] This interpretation draws from homotopy theory, where paths can be continuously deformed, providing a geometric intuition for logical structures.^[5] At its core, HoTT emphasizes constructive proofs that yield computational evidence for assertions, alongside dependent types that allow the formation of types based on terms of other types.^[1] Equality in this system is understood up to homotopy: two terms are equal not just strictly, but if there exists a chain of paths (higher-dimensional equalities) connecting them, enabling a richer notion of equivalence.^[1] Identity types thus form a hierarchy, with paths between paths representing homotopies, and so on. The univalence axiom, which equates type isomorphisms with type equalities, further integrates these ideas but is treated as a foundational principle.^[1] This synthesis originated in the 2013 monograph Homotopy Type Theory: Univalent Foundations of Mathematics, produced by the Univalent Foundations Program at the Institute for Advanced Study.^[1] A representative example is the circle type S^1, formalized as a higher inductive type generated by two constructors: a 0-dimensional point base : S¹ and a 1-dimensional path loop : base = base, which encodes the non-trivial fundamental group of the circle.^[1]

Motivations from mathematics and logic

Homotopy type theory (HoTT) addresses longstanding issues in Zermelo-Fraenkel set theory with the axiom of choice (ZFC), the dominant foundation for classical mathematics. ZFC's rigid notion of equality treats isomorphic structures as distinct, complicating the handling of equivalences in modern mathematics, while its reliance on the axiom of choice (AC) enables non-constructive proofs that lack explicit algorithms or computational content.^[1] Similarly, ZFC incorporates the law of excluded middle (LEM), allowing existential claims without witnesses, which undermines constructivity and leads to impredicative definitions that can obscure proof structure.^[1] These features make ZFC ill-suited for formal verification in proof assistants and for capturing the higher-dimensional aspects of mathematics, such as those in algebraic topology.^[1] In response, constructive type theories, such as Martin-Löf intuitionistic type theory, offer an alternative by treating proofs as canonical terms with explicit computational content, ensuring that every proof of an existential statement provides a witness.^[1] This approach avoids AC and LEM by default, promoting verifiable and algorithmically meaningful mathematics suitable for computer implementation.^[1] However, traditional constructive type theories struggle with higher-dimensional mathematics, as their identity types lack the rich structure needed to model paths, homotopies, and higher coherences natively, often requiring external set-theoretic models that reintroduce classical assumptions.^[1] A key motivation from homotopy theory is the need for a foundational system that inherently captures ∞-groupoids and higher categories, where types serve as spaces and identities as paths between points.^[1] In classical foundations, ∞-groupoids—essential for modeling homotopy types—are awkward to formalize due to the absence of built-in higher-dimensional equalities, leading to cumbersome diagrammatic reasoning.^[6] HoTT resolves this by interpreting types as ∞-groupoids, allowing higher paths and homotopies to emerge naturally from the type structure, thus providing a direct language for higher category theory without ad hoc extensions.^[1] From a logical perspective, HoTT bridges proof theory, category theory, and topology by unifying their interpretations: proofs become paths in spaces, categories arise as type universes, and topological invariants are computed synthetically within the theory itself.^[1] This synthesis enables a common framework where advancements in one field inform the others, such as using univalence to equate isomorphic categories automatically.^[1] Ultimately, HoTT aims to enable synthetic reasoning about homotopy theory, where classical results like the computation of homotopy groups can be derived constructively without relying on ZFC's axioms or external models.^[1] This allows for direct, internal proofs of topological properties, such as the fundamental group of the circle being the integers, fostering a more intuitive and verifiable foundation for mathematics.^[1]

Historical development

Precursors in type theory and category theory

The foundations of homotopy type theory trace back to key developments in type theory and category theory during the 20th century, particularly the introduction of dependent types and homotopical structures that enabled interpreting logical equalities in geometric terms. In the 1970s, Per Martin-Löf formulated intuitionistic type theory, which incorporated dependent types—types that can depend on values of other types—allowing for more expressive logical systems where types serve as both classifications and propositions via the Curry-Howard correspondence.^[7] This framework posited propositions as types, meaning proofs of a proposition correspond to terms inhabiting the corresponding type, and introduced intensional equality, where equality types (Id_A(a,b)) capture propositional identities without collapsing distinct proofs into judgmental ones.^[8] Martin-Löf's system, detailed in his 1975 predicative formulation and later notes, provided a constructive foundation that distinguished intensional from extensional equality, setting the stage for later homotopical interpretations by preserving multiple paths between terms.^[9] Parallel advancements in category theory offered categorical semantics for these type-theoretic constructs, influencing how types could be modeled homotopically. Grothendieck toposes, introduced in the 1960s as categories equivalent to sheaves over sites, provided models for intuitionistic logic and higher-order predicates, where subobject classifiers enabled interpreting dependent types as families of objects varying over a base.^[10] Fibrations, formalized by Grothendieck and developed by Bénabou and Street in the 1970s-1980s, captured dependent types as fibered categories over a base, with Cartesian liftings modeling substitution and dependent products. These structures extended to higher toposes in the 1990s-2000s, as explored by Lurie, where ∞-toposes generalize classical toposes to incorporate homotopy, allowing types to be interpreted as spaces with higher-dimensional paths.^[10] In the 1990s, groupoid models bridged type theory and homotopy by interpreting types as groupoids, where terms are objects and identities are isomorphisms. Thomas Streicher and Martin Hofmann's 1994 work constructed a groupoid model of intensional Martin-Löf type theory using fibrations of groupoids, showing that identity types correspond to hom-sets and refuting the uniqueness of identity proofs (UIP) by exhibiting non-trivial automorphisms.^[11] Their full interpretation, expanded in 1998, mapped closed types to groupoids (categories with only isomorphisms), terms to objects, and identity proofs to morphisms, providing the first intensional model where equalities behave like paths in a space.^[12] This groupoid interpretation demonstrated the consistency of intensional equality without extensional collapse, paving the way for higher-categorical extensions. Homotopical algebra, formalized by Daniel Quillen in his 1967 monograph, introduced model categories as frameworks for homotopy theory within arbitrary categories, featuring weak equivalences, fibrations, and cofibrations to localize at homotopies.^[13] Quillen's structure abstracted homological algebra to homotopical settings, enabling derived functors and homotopy limits that later informed type-theoretic models of higher paths.^[14] Concurrently, John Baez and James Dolan's 1995 paper on higher-dimensional algebra proposed viewing n-categories as ∞-groupoids, where higher morphisms are invertible and compositions model topological quantum field theories, inspiring the treatment of identity types as higher groupoids in type theory.^[15] These precursors collectively shifted focus from set-based equalities to path-like structures, influencing the homotopical semantics of types.

Emergence of univalent foundations

The emergence of univalent foundations in the mid-2000s represented a pivotal shift in the foundations of mathematics, driven by the desire to integrate constructive type theory with homotopy-theoretic structures to enable reliable computer-assisted proofs. Vladimir Voevodsky, motivated by errors in his own work on motivic cohomology and the limitations of classical set-theoretic foundations like ZFC for handling higher-dimensional mathematics, began exploring univalent models around 2005.^[16] In February 2006, he released notes on homotopy λ-calculus, which laid early groundwork for interpreting type theory in a homotopical setting using simplicial sets, emphasizing constructive mathematics amenable to formal verification.^[17] Building on these ideas, Voevodsky proposed the univalence axiom around 2009–2010, which posits that type equality corresponds precisely to equivalence of types, thereby bridging intensional type equality with the extensional notion of isomorphism in a higher-categorical sense.^[18] Concurrently, in 2009, Steve Awodey and Michael Warren advanced the synthetic homotopy interpretation of type theory by demonstrating how Martin-Löf identity types could be modeled as paths in simplicial sets within a model category framework, providing a concrete homotopical semantics without relying on classical axioms.^[19] This work highlighted the potential for type theory to capture homotopy-theoretic notions like higher paths and equivalences natively, fostering a unified approach to logic and geometry. The culmination of these developments occurred during the 2012–2013 Special Year on Univalent Foundations at the Institute for Advanced Study, organized by Voevodsky, Awodey, and Thierry Coquand, which brought together logicians, category theorists, and homotopy specialists to collaborate on formalizing univalent ideas in proof assistants like Coq.^[20] This program not only refined the simplicial set model but also built a collaborative community, accelerating the transition from classical, set-level foundations—focused on extensional equality and point-set topology—to univalent, higher-dimensional ones where types behave as spaces and equalities as paths.^[16]

Key milestones and publications

The publication of Homotopy Type Theory: Univalent Foundations of Mathematics in 2013 marked a foundational milestone for the field, authored collectively by the Univalent Foundations Program at the Institute for Advanced Study. The official print edition was published in 2022 by the Institute for Advanced Study.^[1] This work synthesized emerging ideas into a cohesive framework, detailing the integration of homotopy theory with Martin-Löf type theory and introducing key constructs like the univalence axiom to enable equational reasoning about mathematical structures. Following this, cubical type theory emerged as a major advancement, providing a computational interpretation of univalence. In 2016, Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg published their seminal paper, which extends type theory with cubical dimensions to model paths and higher homotopies directly, allowing univalence to be provably computable in proof assistants like Agda and Coq. This development resolved longstanding issues in constructive foundations and spurred implementations in various systems.^[21] In the 2020s, HoTT integrated with synthetic algebraic geometry, enabling internal development of schemes and étale cohomology without classical set-theoretic assumptions. Foundational work in this area includes contributions by Egbert Rijke, Michael Shulman, and Bas Spitters in 2020, extended in subsequent works by researchers such as Felix Cherubini and Hugo Moeneclaey.^[22]^[23] A dedicated workshop at the University of Gothenburg in March 2024 highlighted applications to moduli stacks and differential geometry.^[24] Concurrently, formalizations of cohomology theories progressed, exemplified by the 2024 computational synthetic cohomology in HoTT, which leverages higher inductive types for sheaf cohomology computations in proof assistants.^[25] Key events have sustained momentum, including Oberwolfach workshops on homotopical type theory in 2014 and 2018, which facilitated interdisciplinary exchanges between logicians and topologists. The annual HoTT/UF workshops, inaugurated in 2014, continue to convene researchers for presentations on formalizations and theoretical advances.^[26] Advances in formalizing ∞-categories within proof assistants progressed with the announcement of the ∞-Cosmos project in Lean 4 in September 2024, which axiomatizes ∞-cosmos structures to support synthetic higher category theory, with talks presented at events like Lean Together 2025 in January 2025.^[27]^[28] The HoTT community has expanded significantly, with active contributions across GitHub repositories.

Foundational principles

Intensional Martin-Löf type theory

Intensional Martin-Löf type theory (MLTT) forms the syntactic and computational foundation of homotopy type theory, extending constructive type theory with an intensional equality type while preserving strong normalization and decidability properties. Developed primarily in the 1970s and 1980s, it emphasizes judgments as the core of its logical framework, including context judgments like \emptyset \vdash \Gamma \mathsf{ ctx} for the empty context and \Gamma, x : A \vdash \Gamma' \mathsf{ ctx} for context extension provided \Gamma \vdash A \mathsf{ type}, type formation \Gamma \vdash A \mathsf{ type}, and term typing \Gamma \vdash a : A. Each type constructor in MLTT is defined by four kinds of inference rules: formation rules to assert the type's well-formedness, introduction rules to construct terms of the type, elimination rules to use such terms, and computation (or reduction) rules specifying β-equivalence and normalization behavior. These rules ensure that MLTT supports dependent types, where types can depend on prior terms, enabling precise specification of computational content. A central feature of intensional MLTT is the dependent function type, denoted \Pi_{x : A} B(x), which generalizes both product types and function types to allow B to depend on x. The formation rule states that if \Gamma \vdash A \mathsf{ type} and \Gamma, x : A \vdash B(x) \mathsf{ type}, then \Gamma \vdash \Pi_{x : A} B(x) \mathsf{ type}. The introduction rule permits lambda abstraction: if \Gamma, x : A \vdash b(x) : B(x), then \Gamma \vdash \lambda x . b(x) : \Pi_{x : A} B(x). Elimination occurs via dependent application: given \Gamma \vdash f : \Pi_{x : A} B(x) and \Gamma \vdash a : A, infer \Gamma \vdash f \, a : B[a/x]. The computation rule enforces β-reduction, ensuring that (\lambda x . b(x)) \, a \equiv b[a/x] : B[a/x], which supports pattern matching in more general dependent elimination for inductive types. This structure allows for powerful programming constructs like higher-order functions while maintaining type safety.^[29] To avoid paradoxes like Girard's and stratify the type hierarchy, intensional MLTT incorporates cumulative universes U_i, a sequence of type universes where U_i : U_{i+1} for each level i \geq 0. The formation rule is \Gamma \vdash U_i \mathsf{ type}, and any type A inhabits a universe if \Gamma \vdash A : U_i; cumulativity ensures that if A : U_i, then A : U_{i+1}, allowing flexible typing without self-referential inconsistencies. Universes themselves are types but restricted from appearing in certain positions to preserve predicativity. Inductive types, such as the natural numbers \mathbb{N}, exemplify this system: formation gives \Gamma \vdash \mathbb{N} \mathsf{ type}; introductions include \mathsf{zero} : \mathbb{N} and \mathsf{succ}(n) : \mathbb{N} if n : \mathbb{N}; elimination uses a recursor \mathsf{rec}_{\mathbb{N}} of type \Pi_{C : \mathbb{N} \to U_0} \, \Pi_{z : C \, \mathsf{zero}} \, \Pi_{s : \Pi_{n : \mathbb{N}} (C \, n) \to C \, (\mathsf{succ} \, n)} \, (C \, m) for any m : \mathbb{N}, with computation rules \mathsf{rec}_{\mathbb{N}} \, C \, z \, s \, \mathsf{zero} \equiv z : C \, \mathsf{zero} and \mathsf{rec}_{\mathbb{N}} \, C \, z \, s \, (\mathsf{succ} \, n) \equiv s \, n \, (\mathsf{rec}_{\mathbb{N}} \, C \, z \, s \, n) : C \, (\mathsf{succ} \, n). These rules enable defining operations like addition via recursion.^[30] Intensional MLTT exhibits key metatheoretical properties, including canonicity—every closed term of a ground type, such as \mathbb{N}, reduces to a canonical form like a numeral—and decidable type checking, arising from the strong normalization theorem, which guarantees that all reduction sequences terminate. These ensure that type inference and equality checking are algorithmically feasible in principle, making the theory suitable for proof assistants and formal verification. Dependent elimination generalizes recursion and induction through pattern matching on constructors, aligning computational behavior with logical inference.

Homotopy-theoretic interpretations

In homotopy type theory (HoTT), the semantic interpretation views types as ∞-groupoids, where terms of a type serve as points, identity proofs between terms act as paths, and higher-dimensional identities correspond to homotopies between those paths.^[31] This perspective arises from interpreting intensional Martin-Löf type theory in the ∞-category of ∞-groupoids, aligning type-theoretic constructions with homotopical structures up to higher equivalences.^[32] Under this interpretation, every type forms a groupoid, with paths (identities) equipped with composition and inverses, enabling the treatment of equalities as reversible morphisms.^[33] Path composition follows the standard rules of identity types, such as reflexivity providing the unit and concatenation defining the operation, which satisfies groupoid axioms internally within the theory.^[34] Fibrational semantics further refines this by modeling dependent types as fibrations in categories of simplicial sets or display categories, where the base type corresponds to the total space and fibers capture dependent structure.^[35] In the simplicial set model, for instance, dependent product types are interpreted as right fibrations, preserving the homotopical content of dependent paths.^[35] HoTT supports synthetic homotopy theory, allowing proofs to be conducted internally using type-theoretic primitives without relying on external analytic models from classical homotopy theory.^[36] This contrasts with analytic approaches that embed types into specific topological or categorical models, as synthetic reasoning leverages the univalent structure directly for homotopy-invariant results.^[37] A representative example is the loop space of a pointed type (A, a), defined as \Omega A \equiv (a =_A a), which inherits a group structure from path concatenation and inversion.^[34] This construction captures the fundamental group \pi_1(A, a) as the connected components of \Omega A, with higher loop spaces \Omega^n A encoding higher homotopy groups synthetically.^[36] Homotopy levels classify types by truncation, where a type is n-truncated if its identity types are (n-1)-truncated, forming a hierarchy starting from (-2)-truncated types, which are contractible (equivalent to the unit type), (-1)-truncated types, known as propositions (where all elements are propositionally equal), and $0$-truncated types, or sets (where propositions are contractible).^[32] These levels enable precise control over higher-dimensional content, with truncation modalities projecting types to lower levels while preserving relevant homotopical information.^[36]

Univalence as a foundational axiom

In homotopy type theory, the univalence axiom serves as a cornerstone that bridges the gap between structural equivalences and equalities of types, fundamentally altering the foundations of mathematics by treating isomorphic structures as identical. Formally, the equivalence type A \simeq B between two types A and B is defined as a structure consisting of functions f : A \to B and g : B \to A, together with a homotopy witnessing that g is a left inverse of f up to homotopy, and symmetrically that f is a right inverse of g. This definition captures the notion of equivalence in a way that aligns with homotopy theory, where maps are considered up to homotopy rather than strict equality. The univalence axiom then posits a map \mathsf{ua} : (A \simeq B) \to (A = B) that converts equivalences into equalities, ensuring that equivalent types are treated as equal within the theory. The full statement of univalence in judgment form is \vdash \mathsf{ua} : \prod_{A B : \mathcal{U}} (A \simeq B) \to (A = B), where \mathcal{U} is the universe of types, and this axiom is added to intensional Martin-Löf type theory to form the basis of univalent foundations. This rule implies that the type of equivalences between types A and B is equivalent to the type of equalities between them, i.e., (A \simeq B) \simeq (A = B), providing a precise mechanism for "transporting" structure along equalities while preserving homotopy-theoretic content. The justification for univalence lies in its provability within certain models of type theory, such as the simplicial set model, where the homotopy category of spaces interprets types and equalities in a way that validates the axiom without contradiction. In these models, univalence ensures that transport along equalities induced by equivalences respects the higher-dimensional structure of paths and homotopies, avoiding the rigidities of classical set theory. Among its key implications, univalence renders function extensionality—a principle stating that pointwise equal functions are equal—as a theorem rather than an axiom, derivable directly from the conversion of equivalences to equalities. Furthermore, it obviates the need for foundational axioms like replacement or choice in set theory, as the univalent treatment of types allows for the direct manipulation of isomorphic structures without additional machinery to assert their equality. A central theorem arising from univalence is that isomorphic structures within the theory are indeed equal, resolving longstanding issues in transporting definitions and proofs across equivalent but syntactically distinct objects, thereby enabling a more coherent and flexible mathematical foundation.

Core concepts

Types and propositions

In homotopy type theory (HoTT), the Curry-Howard correspondence interprets propositions as types and proofs as terms inhabiting those types, extending the propositions-as-types paradigm from intuitionistic logic to a homotopical setting. Unlike traditional type theories where propositions may allow multiple distinct proofs, HoTT refines this by designating propositions as (-2)-truncated types, meaning they are mere propositions (h-propositions) with at most one inhabitant up to propositional equality, ensuring proof irrelevance where all proofs of a proposition are considered equivalent. Logical connectives and quantifiers arise naturally from type formers: implication corresponds to dependent function types (Π-types), where a proof of P \to Q is a dependent function from proofs of P to proofs of Q, while conjunction uses dependent pair types (Σ-types) for pairs of proofs. The universal quantifier \forall x : A . P(x) is encoded as the Π-type \Pi_{x : A} P(x), where A and P(x) are types, and existential quantification \exists x : A . P(x) uses Σ-types, \Sigma_{x : A} P(x). These constructions support a constructive logic, where existence proofs must be explicitly constructed rather than assumed. HoTT's logic remains intuitionistic at its core, rejecting the law of excluded middle (A \lor \lnot A) as a theorem for arbitrary types A, though it can be assumed axiomatically for specific (-2)-truncated types without contradicting consistency. The univalence axiom introduces choice principles, such as unique choice for propositions, by equating type equivalences with equalities, enabling the transport of proofs along equivalences in a way that mimics classical selection for h-propositions. A canonical example is the universe of propositions, denoted Prop, which collects all (-2)-truncated types; for any type A, the propositional truncation map \|A\|_{-2} : A \to \|A\|_{-2} collapses higher homotopical structure into a mere proposition indicating mere existence, with \|A\|_{-2} inhabited if and only if A is. This truncation ensures that proofs of existence are irrelevant beyond their propositional content, distinguishing HoTT from classical logic where proof irrelevance holds universally. In particular, for propositions P and Q, the implication P \to Q is equivalent to transporting along the unique path from the unit type to P into Q, leveraging the singleton nature of propositional identities.

Identity types and paths

In homotopy type theory, which extends intensional Martin-Löf type theory with a homotopy-theoretic interpretation, identity types formalize equality between terms of a given type. For a type A and a term a : A, the identity type a = a, often denoted \mathsf{Id}_A(a, a), is a type whose terms represent proofs that a equals itself. More generally, identity types form a dependent type family \mathsf{Id}_A : A \to A \to \mathsf{Type}, so that for any a, b : A, the type a =_A b (or \mathsf{Id}_A(a, b)) collects the equalities between a and b. The introduction rule for identity types is reflexivity: for each a : A, there is a canonical term \mathsf{refl}_a : a = a, witnessing the equality of a to itself. This constructor is the only basic way to inhabit an identity type, with all other paths derived via elimination. The elimination principle, called J-induction, governs how to reason about or define functions depending on identity types. Given a type family P : \prod_{x : A} (x = a) \to \mathsf{Type} over the identities ending at a and a term d : P(a, \mathsf{refl}_a), J provides a dependent function

J(P, d, x, p) : P(x, p)

for all x : A and p : x = a. This rule is accompanied by a judgmental equality (computation rule)

J(P, d, a, \mathsf{refl}_a) \equiv d,

ensuring that reflexivity behaves as expected in definitions. J-induction is the core rule inherited from Martin-Löf type theory, enabling path-based proofs without assuming extensionality. Path composition, or concatenation, extends identities to chains: if p : x = y and q : y = z, then there exists a composed path p \cdot q : x = z. This operation is defined using J-induction, by taking P(u, r) \equiv (u = z) and applying J to q along p, yielding the concatenation as J(P, q, x, p). In the homotopy interpretation, composition corresponds to concatenating paths in the space represented by the type. Higher paths, or homotopies, arise as identities between identities: for paths p, q : x = y, a homotopy is a term of the identity type p = q in the type of paths from x to y. These form the "\infty"-dimensional structure of HoTT, where homotopies themselves can be composed and inverted, recursively applying the rules for identity types. Examples of path operations include inversion and whiskering. For any path p : x = y, J-induction proves the existence of an inverse p^{-1} : y = x such that p \cdot p^{-1} \equiv \mathsf{refl}_y and p^{-1} \cdot p \equiv \mathsf{refl}_x, with the inverse constructed via a suitable P depending on p. Whiskering transports paths along functions: for f : A \to B and p : x = y in A, the whiskered path \mathsf{ap}_f(p) : f(x) = f(y) is defined by J-induction with P(u, r) \equiv f(u) = f(y), yielding \mathsf{ap}_f(p) \equiv J(P, \mathsf{refl}_{f(y)}, x, p). These manipulations underpin path algebra in HoTT, analogous to homotopy groups in topology. In addition to these homotopical interpretations, an alternative syntactic approach to modeling identity types and paths in homotopy type theory is based on computational paths, which represent equalities as explicit sequences of rewrites that simulate path spaces via term rewrite systems. This method enables direct computation of path compositions and inverses through syntactic manipulations, providing a computational counterpart to the homotopical interpretation. It facilitates the development of foundational aspects like the fundamental groupoid and allows for the calculation of fundamental groups in homotopy type theory. This approach has also been validated through formalization in the Lean proof assistant.^[38]^[39]^[40]^[41]

Equivalences between types

In homotopy type theory, an equivalence between two types A and B, denoted A \simeq B, is defined as the dependent sum type \sum_{f : A \to B} \mathrm{isequiv}(f), where \mathrm{isequiv}(f) asserts that f has a quasi-inverse.^[1]^[42] This structure captures the notion of A and B being "the same up to homotopy," generalizing isomorphisms from set theory to higher-dimensional settings without relying on truncation levels. The components of such an equivalence consist of a forward map f : A \to B, a backward map g : B \to A serving as the quasi-inverse, and two homotopies witnessing invertibility: \eta : \prod_{x : A} (g \circ f \, x) = x and \varepsilon : \prod_{y : B} (f \circ g \, y) = y.^[1] Here, \eta provides a unit homotopy ensuring that composing g after f is homotopic to the identity on A, while \varepsilon is the corresponding counit for B. These homotopies are paths in the identity types, emphasizing the homotopy-theoretic interpretation.^[42] Equivalences admit an induction principle analogous to the path induction rule J but adapted for structure-preserving maps. Specifically, to define a term over an equivalence e : A \simeq B, it suffices to provide a map that respects the forward function and the equivalence witness, allowing recursive constructions that transport properties along equivalences while preserving higher homotopy structure.^[1] A representative example arises in linear algebra: two vector spaces over a field k are equivalent if and only if they have the same dimension, with the equivalence witnessed by a linear isomorphism f that admits a linear inverse g, along with the evident homotopies \eta and \varepsilon derived from the uniqueness of additive inverses.^[1] Another illustration is the equivalence between propositional truncations of equivalent types; if A \simeq B, then \|A\|_\mathbf{0} \simeq \|B\|_\mathbf{0}, where the forward map induces a well-defined homotopy on the truncations via the universal property.^[42] A key property of equivalences is that they preserve all type-theoretic structure, including homotopy levels such as connectivity and truncation ranks, ensuring that equivalent types behave identically in higher inductive definitions and synthetic constructions.^[1]

Advanced structures

Higher inductive types

Higher inductive types (HITs) extend the notion of ordinary inductive types in Martin-Löf type theory by allowing constructors not only for points in the type but also for paths between those points, thereby directly incorporating higher-dimensional structure into the inductive definition.^[1] This generalization enables the synthetic definition of types with nontrivial homotopy, where path constructors specify equalities that must hold in the resulting type.^[43] A canonical example is the circle S^1, defined as the HIT with two constructors: a point constructor \mathsf{base} : S^1 and a path constructor \mathsf{loop} : \mathsf{base} = \mathsf{base}.^[1] This directly encodes the fundamental group of the circle as \mathbb{Z}, with \mathsf{loop} generating the infinite cyclic group under concatenation.^[43] Recursion and induction principles for HITs are formulated using higher eliminators that respect both point and path constructors. For the circle, the recursion principle \mathsf{rec}_{S^1}(f, z) : f(\mathsf{base}) = z applies a function f : S^1 \to A to \mathsf{base} and a proof z : f(\mathsf{base}) = f(\mathsf{base}) for \mathsf{loop}, ensuring that the induced map on the circle respects the loop path.^[1] The induction principle extends this to dependent types, allowing proofs about paths generated by the constructors.^[43] In computational models of homotopy type theory, such as cubical type theory, paths defined by HIT constructors compute via strict equality, enabling canonical terms for path equalities and supporting effective proof checking.^[1] HITs play a crucial role in synthetic topology by facilitating the definition of quotients, such as set quotients where path constructors enforce equivalence relations, truncations that collapse higher paths to propositions, and higher-dimensional topological spaces without relying on external set-theoretic constructions.^[43] Notably, HITs permit the constructive formalization of uncountable structures, such as the real numbers defined via Cauchy completion as a higher inductive-inductive type generated by rational Cauchy sequences with constructors for equivalence and completeness.^[1]

Synthetic homotopy theory

Synthetic homotopy theory in homotopy type theory (HoTT) refers to the internal development of homotopy-theoretic results directly within the type theory, treating types as spaces and identities as paths without relying on external set-theoretic or topological models. This approach leverages the univalence axiom and higher inductive types (HITs) to prove classical theorems synthetically, meaning proofs are conducted using type-theoretic constructions that mirror geometric intuitions. For instance, recursion principles on HITs, such as the circle type S^1, allow for the computation of homotopy groups by defining maps and homotopies internally. A foundational example is the proof that the fundamental group of the circle is the integers, \pi_1(S^1) \simeq \mathbb{Z}. This is established synthetically by constructing the circle as a HIT with a basepoint and a loop, then using recursion to define a universal covering map from the integers to S^1, and showing it induces an equivalence on loop spaces via path induction and transport. The result demonstrates how HoTT captures the winding number interpretation of loops on the circle through type-theoretic recursion.^[44] The Seifert-van Kampen theorem has also been formalized synthetically in HoTT, characterizing the fundamental group of a pushout of types in terms of the fundamental groups of the components and their intersections. In this setting, the theorem applies to homotopy pushouts, computing \pi_1 of glued spaces as the colimit of the \pi_1 of the pieces under the maps induced by inclusions, all verified using path algebra and higher paths. This synthetic version extends naturally to higher dimensions via truncation levels.^[45] Higher homotopy groups are computed using higher paths and truncation levels, where the n-th homotopy group \pi_n(X, x_0) is defined as the n-truncation of the n-fold loop space \Omega^n X at the basepoint x_0. Truncations forget higher-dimensional information, allowing synthetic definitions of homotopy groups as sets or abelian groups for n \geq 2. For example, the fundamental groupoid of a space X is the type of paths in X up to homotopy, with objects as points and morphisms as paths, capturing the \infty-groupoid structure internally. A specific nontrivial result is the computation of \pi_3(S^2) \simeq \mathbb{Z}, shown via the Hopf fibration S^1 \to S^3 \to S^2, formalized in HoTT using HITs for spheres and the long exact sequence of homotopy groups. The fibration is constructed synthetically as a dependent type, with the connecting homomorphism revealing the generator corresponding to the Hopf invariant 1, confirming the group's infinitude. This was part of early formalizations around 2013, with extensions in later synthetic developments. The advantages of synthetic homotopy theory in HoTT include providing constructive, machine-checkable proofs of classical results, enabling verification in proof assistants like Coq or Agda without classical axioms. These proofs are uniform across models, applying simultaneously to topological, simplicial, and cubical interpretations, and facilitate new computations by internalizing geometric arguments.^[46]

Models including cubical type theory

One prominent semantic model of homotopy type theory is the simplicial set model, where types are interpreted as Kan complexes in the category of simplicial sets, and identity types correspond to path spaces equipped with simplicial homotopy relations. In this model, univalence holds because equivalences between Kan complexes induce unique homotopy classes of maps between their path spaces, validating the axiom through the structure of simplicial homotopies. This interpretation, originally observed by Voevodsky, provides a set-theoretic foundation for homotopy type theory within ZFC, establishing its consistency relative to classical set theory via the well-known model structure on simplicial sets.^[47] Cubical type theory, introduced in 2017, offers a computational model of homotopy type theory by incorporating an interval type I with endpoints 0 and 1, where paths are represented as maps from cubes [I]^n into types, supported by face and line operators that project dimensions.^[21] The interval I forms a De Morgan algebra, enabling dualities such as the equivalence between path reversal and transport along the negation of the interval, which ensures that path constructions are judgmental and supports canonicity for identity types.^[21] These features allow univalence to be realized computationally as a propositional equality with definitional content, avoiding the need for axioms by deriving it from the cubical structure.^[21] Path composition in cubical type theory, denoted p @ q, is defined using diagonal arguments on cubes: for paths p : Path_A(a, b) and q : Path_A(b, c), the composition fills the prism formed by p and the transport of q along the first dimension via a diagonal map that contracts the extra dimension. This operation ensures associative and unital path concatenation, preserving the homotopy-invariant properties of the model.^[21] Other models include observational type theory, which defines identity types observationally based on structural equality at base types and extends to higher structure via parametricity, providing an alternative constructive semantics without explicit path spaces.^[48] Set-level models, such as those in simplicial sets or cubical sets constructed within ZFC, confirm the consistency of homotopy type theory by embedding it into classical foundations while preserving univalence and higher inductive types. In recent developments during the 2020s, glue types in cubical type theory—dependent sums over partial maps that "glue" a partial type to a total one along an equivalence—have facilitated synthetic domain theory by enabling the internal construction of Scott domains and continuous functions without classical assumptions.^[49] More recent work includes the Higher Observational Type Theory, which integrates higher homotopical structure into observational models (ERC project, active as of 2025),^[50] and non-standard models constructed via filter quotients for alternative semantics (2025).^[4]

Applications

Formal verification and theorem proving

Homotopy type theory (HoTT) has found significant application in formal verification and mechanized theorem proving through implementations in proof assistants like Coq. The HoTT library for Coq provides a foundational framework incorporating univalence and higher inductive types, enabling the development of univalent libraries for verifying complex mathematical statements.^[51] This setup supports synthetic algebraic topology, where classical results are proved directly in type-theoretic terms without reference to set-theoretic models.^[51] Key verified theorems in HoTT include the computation of homotopy groups, such as the fundamental group of the circle, formalized as π₁(S¹) ≃ ℤ in the HoTT library around 2015.^[51] These formalizations leverage synthetic homotopy theory to establish results like the isomorphism between path spaces and integer windings, demonstrating HoTT's capacity for rigorous, computer-checked proofs in algebraic topology.^[51] The univalence axiom enhances such proofs by allowing equivalences between types to be treated as identities, which aids in transporting properties and structures—effectively permitting changes in "coordinate systems" during verification without manual isomorphism constructions. The UniMath library, initiated in 2014 by merging foundational repositories including Voevodsky's Foundations, has grown into a comprehensive Coq-based project for univalent mathematics, encompassing formalized lemmas across categories, homotopy theory, and beyond.^[52]^[53] A notable example within this framework is the synthetic verification of the Brouwer fixed-point theorem, proved using real-cohesive extensions of HoTT to handle continuous maps on Euclidean balls.^[54] Recent extensions in UniMath, such as formalizations in universal algebra and displayed categories, continue to expand its scope as of 2025.^[55]^[56] Despite these advances, challenges persist in formal verification with HoTT, particularly in handling higher inductive types within code extractors, as standard Coq extraction mechanisms do not fully support their non-constructive aspects, limiting executable code generation from verified proofs.^[51]

Programming languages and type systems

Homotopy type theory (HoTT) has significantly influenced the design of dependent type systems in programming languages, enabling more expressive and verifiable code through concepts like univalence and higher inductive types (HITs). Languages such as Agda and Idris incorporate HoTT ideas to support the development of verified programs, where types encode both data and proofs of properties. In Agda's cubical mode, dependent types are extended with computational paths, allowing equality proofs to be executed during program evaluation, which facilitates the construction of programs that are provably correct with respect to higher-dimensional equalities.^[57] Similarly, Idris leverages dependent types inspired by HoTT to define totality checks and refinement types, ensuring that programs terminate and satisfy specified invariants, though its support for full univalence remains partial compared to Agda. Univalence, a cornerstone of HoTT, enables equivalence-based refactoring by treating type equivalences as equalities, allowing programmers to prove that transformations preserve program behavior up to homotopy. This means that if two types are equivalent, there is a canonical way to transport structures and computations between them computationally, without losing information or requiring manual proof obligations. For instance, refactoring a data structure from lists to trees can be justified by establishing an equivalence, with univalence ensuring the refactored code computes identically to the original. Equivalences in this context provide a brief foundation for such proofs, emphasizing structure-preserving maps between types.^[58] Higher inductive types (HITs) in HoTT extend type systems to model complex effects, such as state and concurrency, by directly specifying higher paths alongside constructors. HITs allow definitions of types like the circle or torus, which can abstractly represent state transitions or concurrent processes where paths encode equivalences between execution traces. In programming, this supports effectful computations by defining free algebras for monads with built-in homotopy relations, enabling verified handling of nondeterminism or parallelism without ad-hoc annotations. For example, HITs have been used to model directed paths in concurrent systems, where homotopies relate different interleavings of operations.^[59] A concrete example is the formal verification of sorting algorithms using homotopy-respecting equalities in cubical Agda. Here, sorting is defined intrinsically by indexing permutations over multisets, with identity types capturing not just correctness but also higher equalities between sorting paths, ensuring that equivalent inputs yield homotopic outputs. This approach verifies that algorithms like insertion sort preserve order up to homotopy, allowing computational extraction of the sorted list while proving stability properties. Language extensions like Cubical Agda, introduced in 2018, integrate these features directly into practical coding by providing computational interpretations of paths and univalence. Cubical Agda extends standard dependent types with interval types and face/interval restrictions, enabling programmers to write code where equalities are paths that can be filled and computed with, supporting applications from verified data structures to synthetic geometry. This makes HoTT operable in everyday programming, with pattern matching over higher-dimensional cubes.^[60]^[61] Overall, HoTT bridges programming and mathematics by enabling differential programming through synthetic differential geometry, where infinitesimal neighborhoods and gradients are defined synthetically via types, allowing verified optimization in numerical code. This impact manifests in tools for automatic differentiation that respect homotopy equivalences, facilitating robust machine learning implementations.^[62]

Connections to algebraic topology

Homotopy type theory (HoTT) establishes deep connections to algebraic topology by interpreting types as ∞-groupoids, enabling synthetic treatments of topological structures where higher-dimensional paths capture homotopical data directly. In this framework, higher inductive types (HITs) facilitate the definition of key topological objects without relying on classical point-set constructions. For instance, manifolds can be defined synthetically as types equipped with additional structure via HITs that enforce local Euclidean properties and smoothness up to homotopy, allowing proofs of topological invariants to proceed uniformly across models.^[6] Principal bundles are similarly formalized using HITs to classify them via their homotopy types, such as the infinite projective space serving as a synthetic classifier for line bundles over spheres.^[63] Spectra, central to stable homotopy theory, are constructed synthetically as reduced types under a monadic and comonadic modality, where a spectrum E satisfies \backslash E being contractible, and structure maps arise from suspension and loop adjunctions without explicit sequential colimits. A hallmark of these connections is the development of formalized cohomology theories within HoTT, providing computational access to topological invariants. Synthetic cohomology is built using Eilenberg-MacLane spectra defined via HITs, satisfying the Eilenberg-Steenrod axioms and enabling computations like the Mayer-Vietoris sequence for pushouts and cohomology of sphere products.^[64] For example, the cohomology of S^k \times X is computed as H_n(S^k \times X) \simeq H_{n-k}(S^0) \times H_n(X) \times H_{n-k}(X), formalized in proof assistants to verify exact sequences.^[64] While specific synthetic K-theory formalizations emerged around 2020, these efforts extend general cohomology frameworks to capture vector bundle classifications topologically. In HoTT, types function as ∞-groupoids, with elements as objects, paths as 1-morphisms, and higher paths as higher-dimensional morphisms, allowing the universe of types to be enriched over itself as an (∞,1)-category.^[65] This enrichment manifests through operations like path concatenation and inversion, endowing types with the full structure of weak ∞-groupoids, as proven by the Eckmann-Hilton theorem for loop spaces.^[65] Bridging further to topology, the univalence axiom equates type equivalences with identities, corresponding to descent conditions in ∞-topoi where colimits in the base yield limits in the fibers, ensuring that equivalent types are interchangeable in topological constructions.^[66] Truncation levels in HoTT mirror Postnikov towers by decomposing types into layers of successively lower homotopy dimensions. A type A is n-truncated if \Omega^{n+1}(A, a) is contractible for all a : A, with the n-truncation \|A\|_n constructed as a HIT that is an n-type and universal for maps from n-types.^[67] This yields a tower \cdots \to \|A\|_n \to \|A\|_{n-1} \to \cdots \to \|A\|_0, analogous to the Postnikov tower where each stage kills homotopy groups above n, enabling synthetic proofs of convergence properties like those for universes U_n.^[65] Such truncations extend synthetic homotopy theory to broader topological settings, including explorations of low-dimensional phenomena via higher paths. The HoTT/UF 2024 workshop highlighted ongoing research in synthetic stable homotopy theory, including advancements in spectra and cohomology relevant to algebraic topology.^[3]

Implementations

Proof assistants and libraries

Homotopy type theory (HoTT) has been implemented in several proof assistants, enabling formal verification of mathematical statements within its univalent foundations. These systems extend traditional dependent type theories with features like univalence and higher inductive types (HITs), often through plugins, modes, or dedicated libraries. Key implementations include Coq, Agda, and Lean, each offering distinct advantages in computational behavior and usability for synthetic homotopy reasoning.^[51]^[68]^[69] In Coq, the HoTT library provides a foundational formalization of HoTT, including axioms for univalence and HITs implemented as private inductive types to support synthetic homotopy theory. This library draws from Vladimir Voevodsky's Foundations and has facilitated developments like the UniMath library, which formalizes substantial mathematics under univalent foundations, including results in algebraic topology.^[70]^[51] Agda supports HoTT through its built-in cubical mode, introduced to implement cubical type theory with computational univalence and native HITs, allowing direct computation with homotopies without axiomatization. The Cubical.Agda library serves as a standard library for this mode, providing primitives for path spaces, intervals, and higher-dimensional structures essential for HoTT proofs.^[68]^[71] Lean integrates HoTT via libraries such as the one developed in the 2010s for synthetic homotopy theory, featuring HITs and cubical fibrancy, though subsequent versions like Lean 4 have seen community efforts like Ground Zero to maintain HoTT support without kernel modifications. Recent work includes HoTTLean, which formalizes the meta-theory of HoTT in Lean 4. These implementations leverage Lean's dependent type theory kernel for efficient theorem proving in HoTT.^[69]^[72]^[73] Other systems include Isabelle/HoTT, which embeds HoTT in Isabelle using a shallow axiomatic approach in a simply typed logical framework, enabling formalization of HoTT concepts like identity types and univalence within Isabelle's higher-order logic.^[74] Core libraries for HoTT include the HoTT/Coq repository, which forms the basis for Coq-based formalizations, and homotopy.io, a web-based assistant specialized in synthetic geometry via globular higher categories, allowing interactive construction of homotopy types and diagrams. As of 2024, homotopy.io supports finitely-presented semistrict higher categories with translation to HoTT via tools like CaTT.^[70]^[75]^[76]

Software tools and formalizations

Several integrated development environment (IDE) tools and extensions facilitate working with Homotopy Type Theory (HoTT) in proof assistants. For Coq, the CoqIDE supports the HoTT library through standard Coq plugins and configuration options, such as enabling universe polymorphism and private inductive types, allowing users to develop and verify HoTT proofs interactively.^[70] Agda-mode provides robust support for Cubical Agda, an implementation of HoTT; it integrates with Emacs via the official Agda Emacs mode for features like syntax highlighting, type checking, and Unicode input, and with Visual Studio Code through the agda-mode-vscode extension, which enables interactive editing and compilation.^[77]^[78] The Lean theorem prover offers interfaces via its official VS Code extension and Emacs mode, supporting metaprogramming and automation that can be adapted for HoTT formalizations, though dedicated HoTT support remains experimental.^[79] Notable formalization projects demonstrate the practical application of HoTT in proof assistants. The synthetic homotopy library, part of the HoTT library for Coq released in 2016, formalizes key concepts including univalence, higher inductive types, and synthetic homotopy theory, enabling proofs of homotopy-theoretic results directly in type theory without external models.^[51] In Cubical Agda, a 2022 project implemented Errett Bishop's constructive real numbers, complete with arithmetic operations, ordering relations, and fundamental theorems like uncountability and Cauchy completeness, providing a foundation for analysis in a cubical setting.^[80] HoTT proofs can be extracted and executed in functional programming languages using cubical models. In Coq, the extraction mechanism compiles verified HoTT terms to OCaml or Haskell code, preserving computational content while discarding proof irrelevancies, as facilitated by the HoTT library's compatibility with Coq's extraction pipeline. Similarly, Cubical Agda supports extraction to Haskell, allowing HoTT-based definitions and computations to run efficiently in a dependently typed subset of Haskell. Community tools enhance collaboration on HoTT formalizations. The HoTT Zulip chat server serves as a primary forum for discussions, with streams dedicated to topics like proof assistants, libraries, and ongoing projects.^[81] Numerous GitHub repositories under the HoTT organization host collaborative efforts, including the Coq-HoTT library for synthetic homotopy and Agda formalizations of introductory HoTT texts, enabling version control, issue tracking, and pull requests for shared developments.^[82] A prominent example is the formalization of the Blakers-Massey excision theorem in the UniMath library for Coq, completed in 2016, which mechanizes the connectivity theorem relating homotopy groups in pushout diagrams, advancing synthetic homotopy theory.^[83]

References

[1]
The HoTT Book | Homotopy Type Theory
Homotopy Type Theory: Univalent Foundations of Mathematics The Univalent Foundations Program Institute for Advanced Study. Buy a hardcover copy for $21.00.
[2]
homotopy type theory in nLab
### Summary of Homotopy Type Theory
[3]
Homotopy Type Theory Permits 'Logic of Homotopy Types' - Ideas
Homotopy type theory combines homotopy theory and type theory, bringing new ideas to mathematics, including the univalence axiom and higher inductive types.Missing: sources | Show results with:sources
[4]
homotopy type theory in nLab
Aug 20, 2025 · Homotopy type theory is a type theory that formalizes path space objects in homotopy theory, treating homotopy theory and ∞-groupoids natively.Missing: sources | Show results with:sources<|control11|><|separator|>
[5]
[PDF] Homotopy Type Theory: A synthetic approach to higher equalities
Arising from a surprising synthesis of constructive intensional type theory and abstract homotopy theory, Homotopy Type Theory and Univalent Foundations (hott/ ...
[6]
[PDF] Per Martin-Löf - INTUITIONISTIC TYPE THEORY
What then remained was the simple theory of types. Its official justification (Wittgenstein,. Ramsey) rests on the interpretation of propositions as truth ...
[7]
[PDF] Intuitionistic Type Theory
This is the formulae-as-types (propositions-as-sets) interpretation on which intuitionistic type theory is based. 7. Page 14. Rules of equality. We now begin ...
[8]
[PDF] Propositions as types - PhilArchive
Martin-Löf, P. (1975). An intuitionistic theory of types: Predicative part. In Rose, H. E. and Shepherdson, J. C., editors, Logic Colloquium '73, pages 73–118.
[9]
[PDF] Higher topos theory / Jacob Lurie
Let X be a nice topological space (for example, a CW complex). One goal of algebraic topology is to study the topology of X by means of algebraic.
[10]
The groupoid model refutes uniqueness of identity proofs
We give a model of intensional Martin-Lof type theory based on groupoids and fibrations of groupoids in which identity types may contain two distinct elements.Missing: Thomas | Show results with:Thomas
[11]
[PDF] The groupoid interpretation of type theory
Aug 27, 1996 · Types (at least non-dependent ones) will be interpreted as groupoids, their closed terms as objects of groupoids. The r^ole of the morphisms in ...
[12]
[PDF] Homotopical Algebra - Aareyan Manzoor's website
In section 1.4 we present an abstract form of this result which asserts that two model categories have the same homotopy theory provided there are a pair of ...
[13]
[PDF] Quillen model categories
When Quillen wrote “Homotopical Algebra”, then, some outlines of what a ho- motopy theory should be were clear. One should definitely start with a category C.Missing: precursors | Show results with:precursors
[14]
Higher-dimensional Algebra and Topological Quantum Field Theory
Title:Higher-dimensional Algebra and Topological Quantum Field Theory. Authors:John C. Baez, James Dolan. View a PDF of the paper titled Higher-dimensional ...
[15]
The Origins and Motivations of Univalent Foundations - Ideas
The origins and motivations of univalent foundations: A personal mission to develop computer proof verification to avoid mathematical mistakes.
[16]
https://www.ias.edu/ideas/2014/voevodsky-origins
[17]
[PDF] Univalent Foundations Project - Institute for Advanced Study
Oct 1, 2010 · Univalent foundations can be used both for constructive and for non-constructive mathemat- ics. To see what homotopy theory has to do with ...
[18]
[0709.0248] Homotopy theoretic models of identity types - arXiv
Sep 3, 2007 · This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any ...
[19]
Univalent Foundations of Mathematics - Institute for Advanced Study
Univalent Foundations of Mathematics, Coorganized by Steve Awodey (IAS/CMU), Thierry Coquand (IAS/University of Gothenburg) and Vladimir Voevodsky (IAS).
[20]
Cubical Type Theory: a constructive interpretation of the univalence ...
Nov 7, 2016 · This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.)
[21]
Workshop on Synthetic Algebraic Geometry - Homotopy Type Theory
Oct 25, 2023 · We are organizing a workshop on synthetic algebraic geometry at the University of Gothenburg/Chalmers from the 11th to 15th of March 2024.Missing: 2020-2025 | Show results with:2020-2025
[22]
Computational Synthetic Cohomology Theory in Homotopy Type ...
Jan 29, 2024 · This paper discusses the development of synthetic cohomology in Homotopy Type Theory (HoTT), as well as its computer formalisation.
[23]
HoTT/UF 2026
Workshop on Homotopy Type Theory / Univalent Foundations 2026. Aarhus, Denmark, 1–2 June 2026. Overview. Homotopy Type Theory is a young area of logic, ...HoTT/UF 2024, Leuven · HoTT/UF 2023, Vienna · HoTT/UF 2022, HaifaMissing: Oberwolfach | Show results with:Oberwolfach
[24]
Announcing the ∞-Cosmos Project | Lean community blog
Sep 17, 2024 · We propose an alternate approach to the formalization of ∞-category theory starting from the axiomatic notion of an ∞-cosmos.Missing: HoTT | Show results with:HoTT
[25]
Workshop on Homotopy Type Theory / Univalent Foundations 2025
Apr 16, 2025 · I'll discuss our proposed axiomatization of synthetic categories that allows us to develop most of (∞-)category theory from first principles, ...
[26]
Martin-Löf dependent type theory in nLab
### Summary of Intensional Martin-Löf Dependent Type Theory
[27]
type universe in nLab
### Summary of Hierarchical Type Universes $U_i$ in Martin-Löf Type Theory
[28]
[PDF] Sets in homotopy type theory - arXiv
Apr 24, 2014 · Homotopy Type Theory may be seen as an internal language for the ∞- category of weak ∞-groupoids which in particular models the univalence axiom ...
[29]
[PDF] Higher Structures in Homotopy Type Theory - arXiv
Jul 5, 2018 · Non-homotopical constructive systems can often be modeled in toposes, more precisely, 1-toposes, which can be seen either as generalizations of ...
[30]
[PDF] A Model of Type Theory in Groupoid Assemblies - arXiv
Jul 21, 2025 · As a result types in Homotopy Type Theory can be interpreted as “infinity groupoids”. This further induces a shift from the notion of equality ...
[31]
[PDF] Homotopies for Free! - arXiv
... type A and its inhabitant a : A called a base point. For a pointed type (A, a) and a natural number n ≥ 0, the n-th loop space Ωn(A, a) of A at a is a.
[32]
The Simplicial Model of Univalent Foundations (after Voevodsky)
Nov 12, 2012 · We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets.
[33]
[PDF] Synthetic Homology in Homotopy Type Theory - arXiv
Dec 21, 2018 · Since an ∞-groupoid can be viewed as a space, it follows that types can be viewed as spaces. In this context the univalence axiom says that any ...
[34]
[PDF] On the homotopy groups of spheres in homotopy type theory - arXiv
Jun 19, 2016 · However, unlike the axiom of choice or excluded middle it is widely believed that the univalence axiom and higher inductive types are ...
[35]
equivalence of types in nLab
### Summary of Type Equivalence in Homotopy Type Theory (Pre-Univalence)
[36]
[PDF] Homotopy Type Theory: Univalent Foundations of Mathematics
Homotopy Type Theory is a new style of informal type theory, tied to a foundation of mathematics that can be implemented in a computer proof assistant.
[37]
Calculating the Fundamental Group of the Circle in Homotopy Type ...
Jan 15, 2013 · In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers.Missing: π₁( S¹) ≃ ℤ
[38]
The Seifert-van Kampen Theorem in Homotopy Type Theory - DROPS
Aug 29, 2016 · Here we consider the Seifert-van Kampen theorem, which characterizes the loop structure of spaces obtained by gluing. This is useful in homotopy theory.
[39]
Homotopy Theory in Homotopy Type Theory: Introduction
Mar 8, 2013 · For example, the circle is inductively generated by base:S1 and loop:Path base base —an inductive type with one point and one non-trivial loop.
[40]
Homotopy type theory and Voevodsky's univalent foundations - arXiv
Oct 20, 2012 · In this paper we give an introduction to homotopy type theory in Voevodsky's setting, paying attention to both theoretical and practical issues.Missing: 2006 | Show results with:2006
[41]
[PDF] Towards Higher Observational Type Theory
In the present work we attempt to find a different way to formulate a Type Theory with univalence, which we call Higher Observational Type Theory. The basic ...<|separator|>
[42]
[PDF] First Steps in Synthetic Tait Computability
Oct 16, 2021 · Synthetic Tait computability is a mathematical machine to reduce difficult problems of type theory and programming languages to trivial theorems ...
[43]
The HoTT Library: A formalization of homotopy type theory in Coq
Oct 14, 2016 · The HoTT library is a formalization of homotopy type theory in Coq, including univalence, higher inductive types, and synthetic homotopy theory.Missing: UniMath 2025
[44]
[PDF] Univalent Foundations and the UniMath Library - PhilSci-Archive
We give a concise presentation of the Univalent Foundations of mathematics outlining the main ideas, followed by a discussion of the UniMath library of ...
[45]
GitHub - UniMath/UniMath: This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
### Summary of UniMath Library
[46]
Brouwer's fixed-point theorem in real-cohesive homotopy type theory
Sep 25, 2015 · We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of adjoint logic.Missing: synthetic formalization
[47]
Cubical — Agda 2.6.0 documentation
The Cubical mode extends Agda with a variety of features from Cubical Type Theory. In particular, computational univalence and higher inductive types.
[48]
Homotopy Type Theory: Univalent Foundations of Mathematics - arXiv
Aug 3, 2013 · Title:Homotopy Type Theory: Univalent Foundations of Mathematics. Authors:The Univalent Foundations Program. View a PDF of the paper titled ...
[49]
[PDF] directed homotopy type theory - Paige Randall North
A directed space is a space together with a subset of its paths which are marked as directed. Page 11. Directed spaces and concurrency.
[50]
Cubical Agda | Homotopy Type Theory
Dec 6, 2018 · Cubical Agda is a cubical proof assistant for cubical type theory, inheriting Agda's pattern matching, and using higher dimensional cubes.
[51]
Cubical agda: a dependently typed programming language with ...
Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence ...
[52]
Synthetic differential geometry within homotopy type theory I - arXiv
Jun 21, 2016 · This paper gives a first step towards developing synthetic differential geometry within homotopy type theory. Its model theory will be discussed ...Missing: programming gradients
[53]
The real projective spaces in homotopy type theory - IEEE Xplore
Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles. These constructions in ...
[54]
[PDF] Synthetic Cohomology in Homotopy Type Theory - Evan Cavallo
Dec 16, 2015 · This is a case study in higher type theory, the study of the infinite-dimensional structure which arises from the identity type of ...
[55]
[PDF] Univalent Foundations of Mathematics - Homotopy Type Theory
The present work has its origins in our collective attempts to develop a new style of “informal type theory” that can be read and understood by a human be- ing, ...
[56]
[PDF] Descent & Univalence
May 2, 2019 · The purpose of the talk is to explain the connection between the notion of descent, characteristic of ∞-topoi, and the notion of univalence, ...Missing: topology | Show results with:topology
[57]
[PDF] TRUNCATION LEVELS IN HOMOTOPY TYPE THEORY Nicolai Kraus
Jun 7, 2015 · We present several original results in homotopy type theory which are related to the truncation level of types, a concept due to Voevodsky.Missing: Postnikov | Show results with:Postnikov
[58]
Cubical — Agda 2.9.0 documentation
The Cubical mode extends Agda with a variety of features from Cubical Type Theory. In particular, it adds computational univalence and higher inductive types.
[59]
[1704.06781] Homotopy Type Theory in Lean - arXiv
Apr 22, 2017 · This paper discusses a homotopy type theory library in Lean, geared toward synthetic homotopy theory, using higher inductive types and cubical ...
[60]
HoTT/Coq-HoTT: A Coq library for Homotopy Type Theory - GitHub
The HoTT library is a development of homotopy-theoretic ideas in the Coq proof assistant. It draws many ideas from Vladimir Voevodsky's Foundations library.
[61]
An experimental library for Cubical Agda - GitHub
A standard library for Cubical Agda. The source code has a glorious clickable rendered version. There is also a discord server, shared with agda-unimath and ...
[62]
rzrn/ground_zero: Ground Zero: Lean 4 HoTT Library - GitHub
This is an attempt to develop Homotopy Type Theory in Lean 4. As in gebner/hott3, no modifications to the Lean kernel are made.
[63]
homotopy.io in nLab
Sep 14, 2025 · This page describes homotopy.io, a web-based proof assistant for finitely-presented globular n-categories, for arbitrary n n .
[64]
Emacs Mode — Agda 2.6.4.1 documentation
### Summary of Agda-mode for Emacs and VSCode Support for Cubical Agda
[65]
agda-mode on VS Code - GitHub
You can install multiple versions of Agda or ALS by adding more paths to agdaMode.connection.paths in the settings, and switch between them with C-c C-r .Missing: Cubical HoTT
[66]
Lean Programming Language
### Summary of Lean Theorem Prover Interface for HoTT, Extensions, and Modes
[67]
Constructive Analysis in the Agda Proof Assistant
### Summary of Constructive Analysis in the Agda Proof Assistant (arXiv:2205.08354)
[68]
https://agda.readthedocs.io/en/latest/language/cubical.html
[69]
HoTT - Homotopy Type Theory - GitHub
A formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems.Missing: verified | Show results with:verified
[70]
A Mechanization of the Blakers-Massey Connectivity Theorem in ...
We present a mechanized proof of a result called the Blakers-Massey connectivity theorem, which relates the higher-dimensional loop structures of two spaces ...Missing: UniMath | Show results with:UniMath
[71]
Explicit Computational Paths
Paper introducing computational paths as a syntactic approach to identity types in homotopy type theory, published on arXiv.
[72]
On the Use of Computational Paths in Path Spaces of Homotopy Type Theory
Explores the application of computational paths to path spaces in HoTT, building on syntactic rewrite sequences.
[73]
On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths
Discusses using computational paths for calculating fundamental groups in HoTT contexts.
[74]
Formalizing Computational Paths and Fundamental Groups in Lean
arXiv preprint arXiv:2511.19142, published 2025-11-24, which formalizes computational paths in homotopy type theory and related computations, such as the fundamental group of the circle, using the Lean proof assistant.