TY - GEN
T1 - Types are internal ∞-groupoids
AU - Finster, Eric
AU - Sozeau, Matthieu
AU - Allioux, Antoine
PY - 2021/7/7
Y1 - 2021/7/7
N2 - 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.
AB - 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.
U2 - 10.1109/LICS52264.2021.9470541
DO - 10.1109/LICS52264.2021.9470541
M3 - Conference contribution
SN - 9781665448956
SN - 9781665448963 (PoD)
T3 - Proceedings - Symposium on Logic in Computer Science
BT - 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
PB - Institute of Electrical and Electronics Engineers (IEEE)
ER -