Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 10 of 10
Heya. I haven’t actually made the necessary changes, but the various pages on dependent type theory make the statement that every DTT or MLTT is the internal logic of an LCCC and every LCCC is the categorical semantics of some DTT/MLTT. However, this is extremely confusing (it took me 2 or 3 hours to find a page where it was made completely clear), since it makes explicit use of super-strong extensionality (I think this is called beta-translation), that is to say, it is a theorem about extensional DTTs/MLTTs.
It’s not even totally clear to me that every intensional type theory actually has an (∞,1)-categorical semantics without the consideration of the univalence axiom. I would make this clearer, but I am really out of my depth with type theories, so I’m just alerting you to the fact that this is stated confusingly almost everywhere (the only place where it’s clear is in the page on identity types).
By the way, to my very untrained eye, it seems like intensional type theories correspond to Segal spaces, while univalent type theories correspond to complete segal spaces (just saying).
I was once told that the problem boils down to the existence of equalisers – because, apparently, cartesian closed categories can interpret intensional type theory, but equalisers make something (I forget what) undecidable.
@Zhen Lin: That is incorrect (see what it says right over at identity type) and also irrelevant. The problem is defining identity types in HoTT without univalence.
I’m not talking about HoTT, just ordinary type theory and ordinary cartesian closed categories.
I think you mean “eta-conversion” as the strong form of extensionality. But yes, this should be made clearer. I think the statement that “every LCCC is the categorical semantics of some DTT/MLTT” is literally true, since in that case you get to choose the DTT and you can pick it to be an extensional one. But in the other direction, I think it is false.
The point is indeed that intensional identity types do not give equalizers in the syntactic category. Making them strongly extensional does give you equalizers, and then it’s type-checking that becomes undecidable because it now depends on type inhabitation (since two types can be judgmentally equal, hence equivalent for type-checking, depending on whether an identity type is inhabited). So undecidability is not the same problem as the nonexistence of equalizers; one is caused by extensionality and solved by intensionality, and the other is caused by intensionality and solved by extensionality.
I can’t tell what you’re thinking of with “the problem is defining identity types in HoTT without univalence”, though. Intensional identity types make perfect sense without univalence; in fact we need to have identity types first in order to write down univalence. Starting from a DTT with intensional identity types, its syntactic category is a category of fibrant objects and therefore presents an -category; no univalence required. The generality in which we can go the other direction is an open question due to coherence issues, but morally, there is no problem there either.
Univalence has to do with whether the internal Segal-space object derived from the universe type is complete, as Urs pointed out here. But externally, I think we are always working in an -category, which can of course be presented by a complete Segal space if we wish.
Mike, I’m talking about if you do a semantics without a universe object.
Well, in that case it doesn’t even make sense to ask whether univalence holds, but intensional identity types still correspond to path objects and hence to homotopy theory.
(By the way, Peter Lumsdaine and Michael Warren have recently essentially solved the problem of coherence for semantics of intensional DTT without universes. I don’t know when their paper will be available, though.)
1 to 10 of 10