On 6 September 2013 09:04, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:
To begin, consider a category C with finite limits. Suppose C has an internal category U such that the externalisation of U as a C-indexed category (or category fibred over C) is equivalent to the self-indexing of C. Since U is locally small as a C-indexed category, the self-indexing of C has the same property, so we deduce that C is locally cartesian closed.
Excellent observation! Thus C is a model for Martin-Loef type theory with Type : Type (as interpreted by U). It is known since Girard's paradox from 1970 that this type theory is inconsistent, i.e. that every type is inhabited. Thus, in particular, all identity types are inhabited which renders C trivial.
I am aware of Girard's paradox but I was under the (mistaken?) impression that slightly more than the structure of a locally cartesian closed category was needed, e.g. a Prop type.
For a more categorical account of the inconcistency of type theory with Type:Type see
A note on Russell's paradox in locally cartesian closed categories Andrew M. Pitts & Paul Taylor Studia Logica 48 (3):377 - 387 (1989)
which is much simpler than Girard's original proof.
Alex Simpson pointed out this paper to me yesterday. Thank you (to both of you!) for bringing it to my attention.
But I don't understand some of your subsequent arguments.
We have a universal fibration el U -> ob U (by restricting the fibration mor U -> ob U x ob U), so it follows that every object X admits a monomorphism X -> el U.
why? and if so what is the point? in a topos for every object X there is a mono 0 -> X
Let X be an object. Then it has a name, say u : 1 -> ob U, and by pulling back u along the universal fibration el U -> ob U, we get a monomorphism X -> el U. This allows us to run Russell's argument in the internal logic, cf [McLarty, _Failure of cartesian closedness in NF_]. -- Zhen Lin [For admin and other information see: http://www.mta.ca/~cat-dist/ ]