5 citations · 10 across the 4 of their papers we have counts for
Showing 2022Show all
2 papers · 1 filter
cs.LO2022
The directed plump ordering
Daniel Gratzer, Michael Shulman, Jonathan Sterling
Based on Taylor's hereditarily directed plump ordinals, we define the directed plump ordering on W-types in Martin-Löf type theory. This ordering is similar to the plump ordering b…
cs.LO2022★ 4 cited
An inductive-recursive universe generic for small families
Daniel Gratzer
We show that it is possible to construct a universe in all Grothendieck topoi with injective codes a la Pujet and Tabareau which is nonetheless generic for small families. As a tri…