True. But for the purpose of reasoning, it's totally normal to ignore the “obviously wrong but admitted anyway” inhabitants like bottom. And I would go as far

True. But for the purpose of reasoning, it's totally normal to ignore the “obviously wrong but admitted anyway” inhabitants like bottom. And I would go as far as to claim that for our purposes, `Either Void ()` can indeed be made isomorphic with `()`, since the functions the converts between them will be total: they will provide a unique canonical term of the one for every canonical term of the other. It makes no sense to say that it's not total on the grounds that “it is not accounting for the extra inhabitant, the bottom”, because bottom is not a canonical term of any type. So the isomorphism is very real, and can be trusted as such. It's better to maintain an attainable definition of totality in a language, and a distinction between canonical and non-canonical terms, than to just say “There is no total function, because Bottom!”, whence we lose important distinctions for reasoning and gain nothing. For these reasons, I tend to use the term “inhabited by” to refer to canonical terms.