17 citations · 30 across the 21 of their papers we have counts for
Showing math.LOShow all
2 papers · 1 filter
math.LO2020★ 1 cited
2-adjoint equivalences in homotopy type theory
Daniel Carranza, Jonathan Chang, Chris Kapulkin +1
We introduce the notion of (half) 2-adjoint equivalences in Homotopy Type Theory and prove their expected properties. We formalized these results in the Lean Theorem Prover.
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.