34 citations · 50 across the 9 of their papers we have counts for
1 paper · 1 filter
Nicolai Kraus, Martín Escardó, Thierry Coquand +1
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedber…