3 citations · 3 across the 2 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2021
Types are Internal -Groupoids
Antoine Allioux, Eric Finster, Matthieu Sozeau
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…
cs.LO2017
A Type-Theoretical Definition of Weak ω-Categories
Eric Finster, Samuel Mimram
We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categori…
cs.LO2016
A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
Kuen-Bang Hou, Eric Finster, Dan Licata +1
This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present…