Showing 1–2 of 2 results for author: Sozeau, M

Types are Internal $\infty$-Groupoids

Authors: Antoine Allioux, Eric Finster, Matthieu Sozeau

Abstract: By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic structures. In particular, our approach leads to a definition of $\infty$-groupoid internal to type theory and we prove that the type of such $\infty$-groupoids is equivalent to the u… ▽ More By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic structures. In particular, our approach leads to a definition of $\infty$-groupoid internal to type theory and we prove that the type of such $\infty$-groupoids is equivalent to the universe of types. That is, every type admits the structure of an $\infty$-groupoid internally, and this structure is unique. △ Less

Submitted 30 April, 2021; originally announced May 2021.

Comments: Extended version of the LICS 2021 article

The HoTT Library: A formalization of homotopy type theory in Coq

Authors: Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters

Abstract: 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… ▽ More 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. △ Less

Submitted 9 December, 2016; v1 submitted 14 October, 2016; originally announced October 2016.

MSC Class: 03B70; 03B15; 55U35 ACM Class: F.4.1