82 citations · 120 across the 21 of their papers we have counts for
Showing 2023Show all
2 papers · 1 filter
cs.LO2023★ 1 cited
A topological counterpart of well-founded trees in dependent type theory
Maria Emilia Maietti, Pietro Sabelli
Within dependent type theory, we provide a topological counterpart of well-founded trees (for short, W-types) by using a proof-relevant version of the notion of inductively generat…
math.CT2023
Quotients, pure existential completions and arithmetic universes
Maria Emilia Maietti, Davide Trotta
We provide a new description of Joyal's arithmetic universes through a characterization of the exact and regular completions of pure existential completions. We show that the regul…