scholarly journals Introduction – from type theory and homotopy theory to univalent foundations

2015 ◽  
Vol 25 (5) ◽  
pp. 1005-1009
Author(s):  
STEVE AWODEY ◽  
NICOLA GAMBINO ◽  
ERIK PALMGREN
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Homotopy Theory ◽  
Foundations Of Mathematics ◽  
Special Issue ◽  
Research Papers ◽  
Homotopy Type Theory ◽  
Main Ideas ◽  
Univalent Foundations

We give an overview of the main ideas involved in the development of homotopy type theory and the univalent foundations of Mathematics programme. This serves as a background for the research papers published in the special issue.

Preface to the MSCS Issue 31.1 (2021) Homotopy Type Theory and Univalent Foundations

2021 ◽  
Vol 31 (1) ◽  
pp. 1-2
Author(s):  
Benedikt Ahrens ◽  
Simon Huber ◽  
Anders Mörtberg
Keyword(s):  
Computer Science ◽  
Homotopy Type ◽  
Type Theory ◽  
Special Issue ◽  
Mathematical Structures ◽  
Homotopy Type Theory ◽  
Univalent Foundations

This issue of Mathematical Structures in Computer Science is Part I of a Special Issue dedicated to the emerging field of Homotopy Type Theory and Univalent Foundations.

scholarly journals Homotopy Type Theory: A Synthetic Approach to Higher Equalities

2018 ◽  
Author(s):  
Michael Shulman
Keyword(s):  
Set Theory ◽  
Homotopy Type ◽  
Type Theory ◽  
Synthetic Approach ◽  
Homotopy Type Theory ◽  
Inductive Types ◽  
Basic Ideas ◽  
Univalent Foundations ◽  
Modern Mathematics

Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which two objects can be equal, ways in which those ways-to-be-equal can be equal, ad infinitum. Though apparently complicated, such structures are increasingly important in mathematics. Philosophically, they are an inevitable result of the notion that whenever we form a collection of things, we must simultaneously consider when two of those things are the same. The “synthetic” nature of HoTT/UF enables a much simpler description of infinity groupoids than is available in set theory, thereby aligning with modern mathematics while placing “equality” back in the foundations of logic. This chapter will introduce the basic ideas of HoTT/UF for a philosophical audience, including Voevodsky’s univalence axiom and higher inductive types.

scholarly journals The Cantor–Schröder–Bernstein Theorem for $$\infty $$-groupoids

2021 ◽  
Author(s):  
Martín Hötzel Escardó
Keyword(s):  
Homotopy Type ◽  
Classical Logic ◽  
Type Theory ◽  
The Other ◽  
Bernstein Theorem ◽  
Homotopy Types ◽  
Homotopy Type Theory ◽  
Univalent Foundations

AbstractWe show that the Cantor–Schröder–Bernstein Theorem for homotopy types, or $$\infty $$ ∞ -groupoids, holds in the following form: For any two types, if each one is embedded into the other, then they are equivalent. The argument is developed in the language of homotopy type theory, or Voevodsky’s univalent foundations (HoTT/UF), and requires classical logic. It follows that the theorem holds in any boolean $$\infty $$ ∞ -topos.

scholarly journals Sets in homotopy type theory

2015 ◽  
Vol 25 (5) ◽  
pp. 1172-1202 ◽  
Author(s):  
EGBERT RIJKE ◽  
BAS SPITTERS
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Connected Components ◽  
Homotopy Type Theory ◽  
Universe Of Sets ◽  
Univalent Foundations ◽  
Subobject Classifier ◽  
Theoretical Foundations ◽  
Special Case

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.

scholarly journals FROM MULTISETS TO SETS IN HOMOTOPY TYPE THEORY

2018 ◽  
Vol 83 (3) ◽  
pp. 1132-1146 ◽  
Author(s):  
HÅKON ROBBESTAD GYLTERUD
Keyword(s):  
Set Theory ◽  
Homotopy Type ◽  
Type Theory ◽  
Homotopy Type Theory ◽  
Constructive Set Theory ◽  
Inductive Types ◽  
Univalent Foundations

AbstractWe give a model of set theory based on multisets in homotopy type theory. The equality of the model is the identity type. The underlying type of iterative sets can be formulated in Martin-Löf type theory, without Higher Inductive Types (HITs), and is a sub-type of the underlying type of Aczel’s 1978 model of set theory in type theory. The Voevodsky Univalence Axiom and mere set quotients (a mild kind of HITs) are used to prove the axioms of constructive set theory for the model. We give an equivalence to the model provided in Chapter 10 of “Homotopy Type Theory” by the Univalent Foundations Program.

scholarly journals Natural models of homotopy type theory

2016 ◽  
Vol 28 (2) ◽  
pp. 241-286 ◽  
Author(s):  
STEVE AWODEY
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Homotopy Theory ◽  
Inference Rules ◽  
Basic System ◽  
Homotopy Type Theory ◽  
Algebraic Formulation

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.

Sign in / Sign up

Export Citation Format

Share Document