Categories of domains with totality
Dag Normann · 1997
We investigate domains with totality where density in general does not hold. We define three categories of domains X with totality X satisfying certain structural properties. We then define the category of evaluation structures. These will induce domains with totality. We show that the category of evaluation structures is closed under dependent sums and products, under a universe constructor and under direct limits. This is applied to domains with totality defined by in- duction.