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 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 Homotopy type-theoretic interpretations of constructive set theories

2019 ◽  
pp. 1-32
Author(s):  
Cesare Gallozzi
Keyword(s):  
Comparative Analysis ◽  
Set Theory ◽  
Homotopy Type ◽  
Type Theory ◽  
Axiom Of Choice ◽  
Homotopy Type Theory ◽  
Constructive Set Theory

Abstract We introduce a family of (k, h)-interpretations for 2 ≤ k ≤ ∞ and 1 ≤ h ≤ ∞ of constructive set theory into type theory, in which sets and formulas are interpreted as types of homotopy level k and h, respectively. Depending on the values of the parameters k and h, we are able to interpret different theories, like Aczel’s CZF and Myhill’s CST. We also define a proposition-as-hproposition interpretation in the context of logic-enriched type theories. The rest of the paper is devoted to characterising and analysing the interpretations considered. The formulas valid in the prop-as-hprop interpretation are characterised in terms of the axiom of unique choice. We also analyse the interpretations of CST into homotopy type theory, providing a comparative analysis with Aczel’s interpretation. This is done by formulating in a logic-enriched type theory the key principles used in the proofs of the two interpretations. Finally, we characterise a class of sentences valid in the (k, ∞)-interpretations in terms of the ΠΣ axiom of choice.

scholarly journals W-types in homotopy type theory

2014 ◽  
Vol 25 (5) ◽  
pp. 1100-1115 ◽  
Author(s):  
BENNO VAN DEN BERG ◽  
IEKE MOERDIJK
Keyword(s):  
Set Theory ◽  
Homotopy Type ◽  
Type Theory ◽  
Detailed Account ◽  
Simplicial Sets ◽  
Homotopy Type Theory ◽  
Simplicial Presheaves ◽  
Models Of Set Theory

We will give a detailed account of why the simplicial sets model of the univalence axiom due to Voevodsky also models W-types. In addition, we will discuss W-types in categories of simplicial presheaves and an application to models of set theory.

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.

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 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 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.

Sign in / Sign up

Export Citation Format

Share Document