Re: A category internal to itself

[Zhen Lin Low <zll22@cam.ac.uk>]

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/ ]