3 citations · 4 across the 2 of their papers we have counts for
Showing math.LOShow all
2 papers · 1 filter
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.