The Experts below are selected from a list of 8001 Experts worldwide ranked by ideXlab platform
Michael Shulman - One of the best experts on this subject based on the ideXlab platform.
-
Homotopy Type theory a synthetic approach to higher equalities
arXiv: Logic, 2018Co-Authors: Michael ShulmanAbstract:This is an introduction to Homotopy Type Theory and Univalent Foundations for philosophers, written as a chapter for the book "Categories for the Working Philosopher" (ed. Elaine Landry)
-
modalities in Homotopy Type theory
Logical Methods in Computer Science, 2017Co-Authors: Egbert Rijke, Michael Shulman, Bas SpittersAbstract:Univalent Homotopy Type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in Homotopy Type theory, including their construction using a "localization" higher inductive Type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
-
Homotopy Type theory the logic of space
arXiv: Category Theory, 2017Co-Authors: Michael ShulmanAbstract:This is an introduction to Type theory, synthetic topology, and Homotopy Type theory from a category-theoretic and topological point of view, written as a chapter for the book "New Spaces for Mathematics and Physics" (ed. Gabriel Catren and Mathieu Anel).
-
CPP - The HoTT library: a formalization of Homotopy Type theory in Coq
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2017, 2017Co-Authors: Andrej Bauer, Michael Shulman, Jason Gross, Peter Lefanu Lumsdaine, Matthieu Sozeau, Bas SpittersAbstract:We report on the development of the HoTT library, a formalization of Homotopy Type theory in the Coq proof assistant. It formalizes most of basic Homotopy Type theory, including univalence, higher inductive Types, and significant amounts of synthetic Homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of Homotopy Type theory with recently introduced features of Coq, such as universe polymorphism and private inductive Types.
-
the hott library a formalization of Homotopy Type theory in coq
arXiv: Logic in Computer Science, 2016Co-Authors: Andrej Bauer, Michael Shulman, Jason Gross, Peter Lefanu Lumsdaine, Matthieu Sozeau, Bas SpittersAbstract:We report on the development of the HoTT library, a formalization of Homotopy Type theory in the Coq proof assistant. It formalizes most of basic Homotopy Type theory, including univalence, higher inductive Types, and significant amounts of synthetic Homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of Homotopy Type theory with recently introduced features of Coq, such as universe polymorphism and private inductive Types.
Steve Awodey - One of the best experts on this subject based on the ideXlab platform.
-
natural models of Homotopy Type theory
Mathematical Structures in Computer Science, 2018Co-Authors: Steve AwodeyAbstract:The notion of a natural model of Type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer, which can be regarded as an algebraic formulation of Type theory. We determine conditions for such models to satisfy the inference rules for dependent sums Σ, dependent products Π, and intensional identity Types Id, as used in Homotopy Type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic Homotopy theory: they should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for Homotopy theory also admit natural models of the basic system of Homotopy Type theory.
-
Homotopy Type theory unified foundations of mathematics and computation
ACM SIGLOG News, 2015Co-Authors: Steve Awodey, Robert HarperAbstract:Homotopy Type theory is a recently-developed unification of previously disparate frameworks, which can serve to advance the project of formalizing and mechanizing mathematics. One framework is based on a computational conception of the Type of a construction, the other is based on a homotopical conception of the Homotopy Type of a space. The computational notion of Type has its origins in Brouwer's program of intuitionism, and Church's λ-calculus, both of which sought to ground mathematics in computation (one would say "algorithm" these days). The homotopical notion comes from Grothendieck's late conception of Homotopy Types of spaces as represented by ∞-groupoids [Grothendieck 1983]. The computational perspective was developed most fully by Per Martin-Lof, leading in particular to his Intuitionistic Theory of Types [Martin-Lof and Sambin 1984], on which the formal system of Homotopy Type theory is based. The connection to Homotopy theory was first hinted at in the groupoid interpretation of Hofmann and Streicher [Hofmann and Streicher 1994; 1995]. It was then made explicit by several researchers, roughly simultaneously. The connection was clinched by Voevodsky's introduction of the univalence axiom, which is motivated by the homotopical interpretation, and which relates Type equality to Homotopy equivalence [Kapulkin et al. 2012; Awodey et al. 2013].
-
Homotopy Type theory
Indian Conference on Logic and Its Applications, 2015Co-Authors: Steve AwodeyAbstract:Homotopy Type Theory is a new, homotopical interpretation of constructive Type theory. It forms the basis of the recently proposed Univalent Foundations of Mathematics program. Combined with a computational proof assistant, and including a new foundational axiom – the Univalence Axiom – this program has the potential to shift the theoretical foundations of mathematics and computer science, and to affect the practice of working scientists. This talk will survey the field and report on some of the recent developments.
-
voevodsky s univalence axiom in Homotopy Type theory
Notices of the American Mathematical Society, 2013Co-Authors: Steve Awodey, Alvaro Pelayo, Michael A WarrenAbstract:In this short note we give a glimpse of Homotopy Type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir Voevodsky’s univalent interpretation of it. This interpretation has given rise to the univalent foundations program, which is the topic of the current special year at the Institute for Advanced Study. The Institute for Advanced Study in Princeton is hosting a special program during the academic year 2012-2013 on a new research theme that is based on recently discovered connections between Homotopy theory, a branch of algebraic topology, and Type theory, a branch of mathematical logic and theoretical computer science. In this brief paper our goal is to take a glance at these developments. For those readers who would like to learn more about them, we recommend a number of references throughout. Type theory was invented by Bertrand Russell [20], but it was first developed as a rigorous formal system by Alonzo Church [3, 4, 5]. It now has numerous applications in computer science, especially in the theory of programming languages [19]. Per Martin-Lof [15, 11, 13, 14], among others, developed a generalization of Church’s system which is now usually called dependent, constructive, or simply Martin-Lof Type theory; this is the system that we consider here. It was originally intended as a rigorous framework for constructive mathematics. In Type theory objects are classified using a primitive notion of Type, similar to the data-Types used in programming languages. And as in programming languages, these elaborately structured Types can be used to express detailed specifications of the objects classified, giving rise to principles of reasoning about them. To take a simple example, the objects of a product Type A × B are known to be of the form 〈a, b〉, and so one automatically knows how to form them and how to decompose them. This aspect of Type
-
voevodsky s univalence axiom in Homotopy Type theory
arXiv: History and Overview, 2013Co-Authors: Steve Awodey, Alvaro Pelayo, Michael A WarrenAbstract:In this short note we give a glimpse of Homotopy Type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir Voevodsky's univalent interpretation of it. This interpretation has given rise to the univalent foundations program, which is the topic of the current special year at the Institute for Advanced Study.
Egbert Rijke - One of the best experts on this subject based on the ideXlab platform.
-
localization in Homotopy Type theory
Higher Structures, 2020Co-Authors: Daniel J Christensen, Egbert Rijke, Morgan Opie, Luis ScoccolaAbstract:We study localization at a prime in Homotopy Type theory, using self maps of the circle. Our main result is that for a pointed, simply connected Type X, the natural map X → X (p) induces algebraic localizations on all Homotopy groups. In order to prove this, we further develop the theory of reflective subuniverses. In particular, we show that for any reflective subuniverse L, the subuniverse of L-separated Types is again a reflective subuniverse, which we call L'. Furthermore, we prove results establishing that L' is almost left exact. We next focus on localization with respect to a map, giving results on preservation of coproducts and connectivity. We also study how such localizations interact with other reflective subuniverses and orthogonal factorization systems. As key steps towards proving the main theorem, we show that localization at a prime commutes with taking loop spaces for a pointed, simply connected Type, and explicitly describe the localization of an Eilenberg-Mac Lane space K(G,n) with G abelian. We also include a partial converse to the main theorem.
-
higher groups in Homotopy Type theory
Logic in Computer Science, 2018Co-Authors: Ulrik Buchholtz, Floris Van Doorn, Egbert RijkeAbstract:We present a development of the theory of higher groups, including infinity groups and connective spectra, in Homotopy Type theory. An infinity group is simply the loops in a pointed, connected Type, where the group structure comes from the structure inherent in the identity Types of Martin-Lof Type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an n-Type can be delooped n + 2 times, then it is an infinite loop Type. Most of the results have been formalized in the Lean proof assistant.
-
The real projective spaces in Homotopy Type theory
2017 32nd Annual ACM IEEE Symposium on Logic in Computer Science (LICS), 2017Co-Authors: Ulrik Buchholtz, Egbert RijkeAbstract:Homotopy Type theory is a version of Martin-Löf Type theory taking advantage of its homotopical models. In particular, we can use and construct objects of Homotopy theory and reason about them using higher inductive Types. In this article, we construct the real projective spaces, key players in Homotopy theory, as certain higher inductive Types in Homotopy Type theory. The classical definition of ℝPn, as the quotient space identifying antipodal points of the n-sphere, does not translate directly to Homotopy Type theory. Instead, we define ℝPn by induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take ℝP-1 to be the empty Type. In the inductive step, we take ℝPn+1 to be the mapping cone of the projection map of the tautological bundle of ℝPn, and we use its universal property and the univalence axiom to define the tautological bundle on ℝPn+1. By showing that the total space of the tautological bundle of ℝPn is the n-sphere Sn, we retrieve the classical description of ℝPn+1 as ℝPn with an (n + 1)-disk attached to it. The infinite dimensional real projective space ℝP∞, defined as the sequential colimit of ℝPn with the canonical inclusion maps, is equivalent to the Eilenberg-MacLane space K(ℤ/2ℤ, 1), which here arises as the subType of the universe consisting of 2-element Types. Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles. These constructions in Homotopy Type theory further illustrate the utility of Homotopy Type theory, including the interplay of Type theoretic and Homotopy theoretic ideas.
-
modalities in Homotopy Type theory
Logical Methods in Computer Science, 2017Co-Authors: Egbert Rijke, Michael Shulman, Bas SpittersAbstract:Univalent Homotopy Type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in Homotopy Type theory, including their construction using a "localization" higher inductive Type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
-
LICS - The real projective spaces in Homotopy Type theory
2017 32nd Annual ACM IEEE Symposium on Logic in Computer Science (LICS), 2017Co-Authors: Ulrik Buchholtz, Egbert RijkeAbstract:Homotopy Type theory is a version of Martin-Lof Type theory taking advantage of its homotopical models. In particular, we can use and construct objects of Homotopy theory and reason about them using higher inductive Types. In this article, we construct the real projective spaces, key players in Homotopy theory, as certain higher inductive Types in Homotopy Type theory. The classical definition of RPn, as the quotient space identifying antipodal points of the n-sphere, does not translate directly to Homotopy Type theory. Instead, we define RPn by induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take RP-1 to be the empty Type. In the inductive step, we take RPn+1 to be the mapping cone of the projection map of the tautological bundle of RPn, and we use its universal property and the univalence axiom to define the tautological bundle on RPn+1. By showing that the total space of the tautological bundle of RPn is the n-sphere Sn, we retrieve the classical description of RPn+1 as RPn with an (n + 1)-disk attached to it. The infinite dimensional real projective space RP∞, defined as the sequential colimit of RPn with the canonical inclusion maps, is equivalent to the Eilenberg-MacLane space K(Z/2Z, 1), which here arises as the subType of the universe consisting of 2-element Types. Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles. These constructions in Homotopy Type theory further illustrate the utility of Homotopy Type theory, including the interplay of Type theoretic and Homotopy theoretic ideas.
Bas Spitters - One of the best experts on this subject based on the ideXlab platform.
-
internal universes in models of Homotopy Type theory
arXiv: Logic in Computer Science, 2018Co-Authors: Daniel R Licata, Ian Orton, Andrew M Pitts, Bas SpittersAbstract:We begin by recalling the essentially global character of universes in various models of Homotopy Type theory, which prevents a straightforward axiomatization of their properties using the internal language of the presheaf toposes from which these model are constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-Mortberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to an elementary axiomatization of that and related models of Homotopy Type theory within what we call crisp Type theory.
-
modalities in Homotopy Type theory
Logical Methods in Computer Science, 2017Co-Authors: Egbert Rijke, Michael Shulman, Bas SpittersAbstract:Univalent Homotopy Type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in Homotopy Type theory, including their construction using a "localization" higher inductive Type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
-
CPP - The HoTT library: a formalization of Homotopy Type theory in Coq
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2017, 2017Co-Authors: Andrej Bauer, Michael Shulman, Jason Gross, Peter Lefanu Lumsdaine, Matthieu Sozeau, Bas SpittersAbstract:We report on the development of the HoTT library, a formalization of Homotopy Type theory in the Coq proof assistant. It formalizes most of basic Homotopy Type theory, including univalence, higher inductive Types, and significant amounts of synthetic Homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of Homotopy Type theory with recently introduced features of Coq, such as universe polymorphism and private inductive Types.
-
the hott library a formalization of Homotopy Type theory in coq
arXiv: Logic in Computer Science, 2016Co-Authors: Andrej Bauer, Michael Shulman, Jason Gross, Peter Lefanu Lumsdaine, Matthieu Sozeau, Bas SpittersAbstract:We report on the development of the HoTT library, a formalization of Homotopy Type theory in the Coq proof assistant. It formalizes most of basic Homotopy Type theory, including univalence, higher inductive Types, and significant amounts of synthetic Homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of Homotopy Type theory with recently introduced features of Coq, such as universe polymorphism and private inductive Types.
-
sets in Homotopy Type theory
Mathematical Structures in Computer Science, 2015Co-Authors: Egbert Rijke, Bas SpittersAbstract:Homotopy Type theory may be seen as an internal language for the ∞-category of weak ∞-groupoids. Moreover, weak ∞-groupoids model the univalence axiom. Voevodsky proposes this (language for) weak ∞-groupoids as a new foundation for Mathematics called the univalent foundations. It includes the sets as weak ∞-groupoids with contractible connected components, and thereby it includes (much of) the traditional set theoretical foundations as a special case. We thus wonder whether those ‘discrete’ groupoids do in fact form a (predicative) topos. More generally, Homotopy Type theory is conjectured to be the internal language of ‘elementary’ of ∞-toposes. We prove that sets in Homotopy Type theory form a ΠW-pretopos. This is similar to the fact that the 0-truncation of an ∞-topos is a topos. We show that both a subobject classifier and a 0-object classifier are available for the Type theoretical universe of sets. However, both of these are large and moreover the 0-object classifier for sets is a function between 1-Types (i.e. groupoids) rather than between sets. Assuming an impredicative propositional resizing rule we may render the subobject classifier small and then we actually obtain a topos of sets.
David Carchedi - One of the best experts on this subject based on the ideXlab platform.
-
On the profinite Homotopy Type of log schemes.
arXiv: Algebraic Geometry, 2019Co-Authors: David Carchedi, Sarah Scherotzke, Nicolò Sibilla, Mattia TalpoAbstract:We complete the program, initiated in [6], to compare the many different possible definitions of the underlying Homotopy Type of a log scheme. We show that, up to profinite completion, they all yield the same result, and thus arrive at an unambiguous definition of the profinite Homotopy Type of a log scheme. Specifically, in [6], we define this to be the profinite etale Homotopy Type of the infinite root stack, and show that, over $\mathbb{C},$ this agrees up to profinite completion with the Kato-Nakayama space. Other possible candidates are the profinite shape of the Kummer etale site $X_{\mbox{ket}},$ or of the representable etale site of $\sqrt[\infty]{X}.$ Our main result is that all of these notions agree, and moreover the profinite etale Homotopy Type of the infinite root stack is not sensitive to whether or not it is viewed as a pro-system in stacks, or as an actual stack (by taking the limit of the pro-system). We furthermore show that in the log regular setting, all these notions also agree with the etale Homotopy Type of the classical locus $X^{\mbox{triv}}$ (up to an appropriate completion). We deduce that, over an arbitrary locally Noetherian base, the etale Homotopy Type of $\mathbb{G}_m^N$ agrees with that of $B\mu_\infty^N$ up to completion.
-
kato nakayama spaces infinite root stacks and the profinite Homotopy Type of log schemes
Geometry & Topology, 2017Co-Authors: David Carchedi, Sarah Scherotzke, Nicolò Sibilla, Mattia TalpoAbstract:For a log scheme locally of finite Type over C, a natural candidate for its profinite Homotopy Type is the profinite completion of its Kato-Nakayama space. Alternatively, one may consider the profinite Homotopy Type of the underlying topological stack of its infinite root stack. Finally, for a log scheme not necessarily over C, another natural candidate is the profinite \'etale Homotopy Type of its infinite root stack. We prove that, for a fine saturated log scheme locally of finite Type over C, these three notions agree. In particular, we construct a comparison map from the Kato-Nakayama space to the underlying topological stack of the infinite root stack, and prove that it induces an equivalence on profinite completions. In light of these results, we define the profinite Homotopy Type of a general fine saturated log scheme as the profinite \'etale Homotopy Type of its infinite root stack.
-
on the Homotopy Type of higher orbifolds and haefliger classifying spaces
Advances in Mathematics, 2016Co-Authors: David CarchediAbstract:Abstract We describe various equivalent ways of associating to an orbifold, or more generally a higher etale differentiable stack, a weak Homotopy Type. Some of these ways extend to arbitrary higher stacks on the site of smooth manifolds, and we show that for a differentiable stack X arising from a Lie groupoid G , the weak Homotopy Type of X agrees with that of B G . Using this machinery, we are able to find new presentations for the weak Homotopy Type of certain classifying spaces. In particular, we give a new presentation for the Borel construction M × G E G of an almost free action of a Lie group G on a smooth manifold M as the classifying space of a category whose objects consist of smooth maps R n → M which are transverse to all the G-orbits, where n = dim M − dim G . We also prove a generalization of Segal's theorem, which presents the weak Homotopy Type of Haefliger's groupoid Γ q as the classifying space of the monoid of self-embeddings of R q , B ( Emb ( R q ) ) , and our generalization gives analogous presentations for the weak Homotopy Type of the Lie groupoids Γ 2 q S p and R Γ q which are related to the classification of foliations with transverse symplectic forms and transverse metrics respectively. We also give a short and simple proof of Segal's original theorem using our machinery.
-
on the etale Homotopy Type of higher stacks
arXiv: Algebraic Geometry, 2015Co-Authors: David CarchediAbstract:A new approach to \'etale Homotopy theory is presented which applies to a much broader class of objects than previously existing approaches, namely it applies not only to all schemes (without any local Noetherian hypothesis), but also to arbitrary higher stacks on the \'etale site of such schemes, and in particular to all algebraic stacks. This approach also produces a more refined invariant, namely a pro-object in the infinity category of spaces, rather than in the Homotopy category. We prove a profinite comparison theorem at this level of generality, which states that if $\mathcal{X}$ is an arbitrary higher stack on the \'etale site of affine schemes of finite Type over $\mathbb{C},$ then the \'etale Homotopy Type of $\mathcal{X}$ agrees with the Homotopy Type of the underlying stack $\mathcal{X}_{top}$ on the topological site, after profinite completion. In particular, if $\mathcal{X}$ is an Artin stack locally of finite Type over $\mathbb{C}$, our definition of the \'etale Homotopy Type of $\mathcal{X}$ agrees up to profinite completion with the Homotopy Type of the underlying topological stack $\mathcal{X}_{top}$ of $\mathcal{X}$ in the sense of Noohi. In order to prove our comparison theorem, we provide a modern reformulation of the theory of local systems and their cohomology using the language of $\infty$-categories which we believe to be of independent interest.