3 citations · 3 across the 1 of their papers we have counts for
3 papers
math.LO2020
A general definition of dependent type theories
Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine
We define a general class of dependent type theories, encompassing Martin-Löf's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and…
math.LO2020★ 3 cited
The law of excluded middle in the simplicial model of type theory
Chris Kapulkin, Peter LeFanu Lumsdaine
We show that the law of excluded middle holds in Voevodsky's simplicial model of type theory. As a corollary, excluded middle is compatible with univalence.
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…