Re: topos logic arising nicely

Hi Paul,

"The neglect of sum types is the root of all evil."

To some extent this may be true for programming languages (but see recent work of Jim Laird). For logics it is less clear. Actually you mean the empty type, isn't it? Moreover, sunset types are slightly heavier than ordinary sum types. Subset types are rather dependent sum types. Thomas