[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Vladimir, do you include equality? Best Sergei Soloviev On Thursday, July 19, 2012 17:16 CEST, Vladimir Voevodsky <[email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > Don't you have False (as 0=1 for instance) hence not A (as > > A ->False) hence exA (as forall notA -> False), hence everything? > > Thanks to everybody who pointed this out to me. I'll have to think whether my > question has a more sensible reformulation. > > Vladimir. > >
