3 citations · 3 across the 1 of their papers we have counts for
3 papers
math.CT2021★ 3 cited
Synthetic Spectra via a Monadic and Comonadic Modality
Mitchell Riley, Eric Finster, Daniel R. Licata
We extend Homotopy Type Theory with a novel modality that is simultaneously a monad and a comonad. Because this modality induces a non-trivial endomap on every type, it requires a…
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…