137 citations · 500 across the 20 of their papers we have counts for
1 paper · 1 filter
Peter LeFanu Lumsdaine
We show that for any type in Martin-Löf Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely…