scholarly journals Cubical methods in homotopy type theory and univalent foundations

2021 ◽  
pp. 1-38
Author(s):  
Anders Mörtberg
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Summer School ◽  
Homotopy Type Theory ◽  
Consistency Results ◽  
New Type ◽  
Cubical Set ◽  
Independence Results ◽  
Original Motivation ◽  
Univalent Foundations

Abstract Cubical methods have played an important role in the development of Homotopy Type Theory and Univalent Foundations (HoTT/UF) in recent years. The original motivation behind these developments was to give constructive meaning to Voevodsky’s univalence axiom, but they have since then led to a range of new results. Among the achievements of these methods is the design of new type theories and proof assistants with native support for notions from HoTT/UF, syntactic and semantic consistency results for HoTT/UF, as well as a variety of independence results and establishing that the univalence axiom does not increase the proof theoretic strength of type theory. This paper is based on lecture notes that were written for the 2019 Homotopy Type Theory Summer School at Carnegie Mellon University. The goal of these lectures was to give an introduction to cubical methods and provide sufficient background in order to make the current research in this very active area of HoTT/UF more accessible to newcomers. The focus of these notes is hence on both the syntactic and semantic aspects of these methods, in particular on cubical type theory and the various cubical set categories that give meaning to these theories.

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.

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.

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.

Sign in / Sign up

Export Citation Format

Share Document