This is just bits and pieces for now; something more coherent will come later.
Of course, we should be able to treat an -type as an -type for any . When and this corresponds to replacing a proposition by the set , while when and it corresponds to treating a set as a discrete category. It should also be true that the resulting -type is appropriately truncated.
The following operations allow us to interpret an -type as an -type whenever .
It follows that if , then , since as both are terms of a -type . Thus, is in fact a subsingleton as desired. What remains to assert is that if then is a discrete category.
In theory, the ways to type the formation of dependent sums are parametrized by three sorts: the sort of , the sort of , and the sort of the result. In our case, we allow two general classes of dependent sums.
- In the first, must be a proposition, while can be anything, and in this case the result is a proposition. This construction gives existential quantifiers, so we will notate it as .
- In the second, must be a set, while can be anything, and the result has the same sort as . This construction gives “indexed disjoint unions,” and we will use the ordinary dependent sum notation for it.
Note that in the overlap case when is a set and is a proposition, we get two different ways to form a dependent sum depending on what the result type is. If the result is a proposition, then it is the proposition , while if the result is a set, then it is the set . The difference from a computational point of view is that in the second case, it is possible to extract the witness , while in the first it is not.
There should also be dependent sums of the second sort where is a category, with the result being a category. However, in this case, unless the dependence of on is given functorially, then it is not possible to determine the morphisms in the dependent sum. We will study the general case of functorially dependent types elsewhere, but here we do need one particular case.
Strong dependent sums
Note that when and is independent of , then is canonically isomomorphic to . In ordinary type theory, one doesn’t need to define both binary products and dependent sums, since the former can be constructed from the latter in this way. However, since we aren’t allowing dependent sums over categories, we need binary products for categories given separately.
When we also have rules for morphisms.
As with dependent sums, in general the operation is parametrized by the sorts of , of , and of the result. Since exponentials in a 2-category require fibrations and variance, for now we restrict to the case when and are both propositions. When is a set or a category, this gives universal quantification, which we write as , while when is also a proposition it gives implication, which we write as .