2021/04/30 by Antoine Allioux, Allioux, Antoine, Eric Finster +3
Mathematics · Decision Sciences · Computer Science · #Homotopy and Cohomology in Algebraic Topology #Fuzzy and Soft Set Theory #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2105.00024
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 ∞-groupoid internal to type theory and we prove that the type of such ∞-groupoids is equivalent to the universe of types. That is, every type admits the structure of an ∞-groupoid internally, and this structure is unique.