A category internal to itself

A category internal to itself

[Andrej Bauer]

Chatting at a conference, the question came up why there is no
(non-trivial) category which is "internal to itself" (interpret this
in some sensible sense). And over coffee we thought this must be well
known, but not to us. Can somene shed some light on the matter?

With kind regards,

Andrej


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: A category internal to itself

[Eduardo J. Dubuc]

On 04/09/13 06:23, Andrej Bauer wrote:
> Chatting at a conference, the question came up why there is no
> (non-trivial) category which is "internal to itself" (interpret this
> in some sensible sense). And over coffee we thought this must be well
> known, but not to us. Can somene shed some light on the matter?
>
> With kind regards,
>
> Andrej
>

Interesting and difficult question. Related to incompletness problems
and diagonal arguments.

Joyal considered arithmetic universes U (*), and an initial such U_0.
(for example, for U = Sets: U_0[1, N] = standard Natural Numbers).

Then show that within any arithmetic universe U you can construct
internally a U_0. In particular U_0 exist (called U'_0) inside U_0. You
have U[1, U'_0] = U_0. With this he proves Godel Incompletness.

(*) A pretopos U such that admits free monoids:
       X \in U, X ---> M(X), in particular, N = M(0).
(with this you have primitive recursive arithmetics and construct U_0).

I sort of remember also that Penon considered a topos object E' internal
to a topos E and such that E[1, E'] = E.

It is a challenge to to fill all the technical details and make rigorous
sense of all this.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: A category internal to itself

[Colin McLarty]

In the set theory New Foundations (NF)  using Quine's type-level pairing (so
a pair has the same type in a stratification as its components) you can
define small categories and small functors the usual way.  Then, just as
there is a set of all sets, there is a small category of all small
categories.  This is not a tautology.  You have to verify a few things.

Notably, in this context there is a set of all small functors because there
is a set of all functions (yet the category of sets is not cartesian
closed, because it lacks evaluation functions).   Since a function is
stratified at the same level as its domain and codomain sets there is no
problem defining domain, codomain, composition, and identity-assigning
functors for this category.

This category is internal to itself.  This example is even left exact.  But
it is not cartesian closed.

Of course the consistency of NF is not settled.  But I think everyone
supposes it is equiconsistent with some more usual set theory (likely with
ETCS).

best, Colin




On Wed, Sep 4, 2013 at 5:23 AM, Andrej Bauer <andrej.bauer@andrej.com>wrote:

> Chatting at a conference, the question came up why there is no
> (non-trivial) category which is "internal to itself" (interpret this
> in some sensible sense). And over coffee we thought this must be well
> known, but not to us. Can somene shed some light on the matter?
>
> With kind regards,
>
> Andrej
>

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: A category internal to itself

[Edmund Robinson]

There are some forms of set theory in which there are restrictions on the forms of comprehension allowed, and as a result there is a set of all sets. Quine's New Foundations is one of these. It has a simple restriction on the forms of predicates allowed in comprehensions. Put simply this is that you can assign (integer) levels to the variables in the formula so that x e y only occurs when y is at the level immediately above x. This means that in models of this set theory there is also an internal category of all sets. 

best
Edmund



On 4 Sep 2013, at 10:23, Andrej Bauer wrote:

> Chatting at a conference, the question came up why there is no
> (non-trivial) category which is "internal to itself" (interpret this
> in some sensible sense). And over coffee we thought this must be well
> known, but not to us. Can somene shed some light on the matter?
> 
> With kind regards,
> 
> Andrej
> 


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: A category internal to itself

[Zhen Lin Low]

Dear Andrej,

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.

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. Now, if we add the assumption that C
(or U) is well-powered as a C-indexed category, then C must be an
elementary topos. But then the existence of el U implies that the
internal logic of C is inconsistent, so C must be the degenerate
topos.

It appears we need to relax the notion of "internal" to get something
more reasonable. Here is one idea: instead of taking just one internal
category, we take a (large) filtered diagram of them. More precisely,
let U be a diagram of shape J in the category of internal categories
in C, where J is filtered and the transition functors are (internally)
fully faithful, and define a C-indexed category whose fibre over X is
the (external) category colim Hom(X, U). When C is an elementary
topos, there exists a diagram U such that this construction yields a
C-indexed category that is equivalent to the self-indexing of C: take
J to be the poset of all finite subsets of ob C, and take as the
internal category at a finite set {X_1, ..., X_n} of objects of C to
be the internal full subcategory whose objects are the subobjects of
the power object P(X_1 + ... + X_n). In the converse direction, if
such a diagram of internal categories exists, then one can still
deduce (from the condition on transition functors) that the
self-indexing of C is locally small.

But perhaps there is a strange locally cartesian closed category out
there that is self-internal in the naive sense.

Best regards,
--
Zhen Lin

On 4 September 2013 10:23, Andrej Bauer <andrej.bauer@andrej.com> wrote:
> Chatting at a conference, the question came up why there is no
> (non-trivial) category which is "internal to itself" (interpret this
> in some sensible sense). And over coffee we thought this must be well
> known, but not to us. Can somene shed some light on the matter?
>
> With kind regards,
>
> Andrej
>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: A category internal to itself

[Colin McLarty]

Perhaps this is not really what you want, though.  What I would like to
know, related to this, is can there be a non-trivial category internally
fibred over itself?

This question, like your question, leaves some room to ask just what it
means.

If we just try to Grothendieck-fiber this category of all categories in NF
over itself we meet type problems.  A type-level notion of pair will not
let us form the set of all pairs of a category and an object in it.  Maybe
a routine NF trick gets around this, maybe not.  I wanted to share this
thought, and clarify it for myself, before plunging into the world of NF
tricks.

best, Colin


On Wed, Sep 4, 2013 at 6:11 PM, Colin McLarty <colin.mclarty@case.edu>wrote:

>
> In the set theory New Foundations (NF)  using Quine's type-level pairing (so
> a pair has the same type in a stratification as its components) you can
> define small categories and small functors the usual way.  Then, just as
> there is a set of all sets, there is a small category of all small
> categories.  This is not a tautology.  You have to verify a few things.
>
> Notably, in this context there is a set of all small functors because
> there is a set of all functions (yet the category of sets is not
> cartesian closed, because it lacks evaluation functions).   Since
> a function is stratified at the same level as its domain and codomain
> sets there is no problem defining domain, codomain, composition, and
> identity-assigning functors for this category.
>
> This category is internal to itself.  This example is even left exact.
>  But it is not cartesian closed.
>
> Of course the consistency of NF is not settled.  But I think everyone
> supposes it is equiconsistent with some more usual set theory (likely with
> ETCS).
>
> best, Colin
>
>
>
>
> On Wed, Sep 4, 2013 at 5:23 AM, Andrej Bauer <andrej.bauer@andrej.com>wrote:
>
>> Chatting at a conference, the question came up why there is no
>> (non-trivial) category which is "internal to itself" (interpret this
>> in some sensible sense). And over coffee we thought this must be well
>> known, but not to us. Can somene shed some light on the matter?
>>
>> With kind regards,
>>
>> Andrej

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: A category internal to itself

[Alex Simpson]

A comment on Zhen Lin's reply to Andrej:

> 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.
>
> 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. Now, if we add the assumption that C
> (or U) is well-powered as a C-indexed category ...

Just to remark that there is no need to add any assumption here. If a
locally cartesian closed category has a "universal fibration" as you
call it (called "generic family" in the reference below), then it is
degenerate. This appears in:

    Pitts, Andrew M.; Taylor, Paul.
    A note on Russell's paradox in locally Cartesian closed categories.
    Studia Logica 48 (1989), no. 3, 377?387. (MR1059248)

With best wishes,
Alex

-- 
Alex Simpson, LFCS, School of Informatics, Univ. of Edinburgh, UK
Email: Alex.Simpson@ed.ac.uk             Tel: +44 (0)131 650 5113
Web: http://homepages.inf.ed.ac.uk/als   Fax: +44 (0)131 651 1426

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.




[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: A category internal to itself

[Zhen Lin Low]

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

Re: A category internal to itself

[Andrej Bauer]

I would like to thank everyone for so many wonderful answers.

It seems that there is an "easy" case and a "difficult" case.

In the easy case we look at the global points of the internal category
and expect to see the external category. This can be arranged so that
the category is even a topos (the free one), as explained by Peter
Johnstone. And there are other possibilities, such as the arithmetical
universe.

The difficult case involves looking at general points, which leads to
questions about fibrations. As we know from Andy Pitts and Paul
Taylor, an lccc which is internal in the stronger sense is trivial.
But I wonder if there is a category C which contains a universal
object U such that Hom(-, U) gives a model of dependent type theory
(without identity types!) which is the same as some fibration
involving C. What I have in mind is the following (I will speak
indexly instead of fibrantly).

Consider a cartesial-closed category Dom of domains containing a
universal object U in the sense that every other object is a retract
of U. For instance, to keep everything very pretty we could take
countably-based algebraic lattices, in which P(⍵) is universal. For
each domain D in Dom we have the continuous functors Cont(D, Dom), a
la Ulrich Bergers Habilitationschrift, that gives an indexed category.
But such functors ought to correspond closely to the continuous maps D
-> U because the elements of U rerpesent retracts of U which are the
object of Dom. All of this needs to be massaged a bit, and before I do
it, I would prefer to hear whether I am reinventing the wheel.

The results would be a model of type theory (with Σ and Π but no Id)
which models Type : Type. It is not trivial, but all types are
inhabited (and have the fixed-point property). We can still interpret
Girard's paradox in it, but it is not really a paradox without
identity types as the type structure does not collapse. Has something
like that known? (I fully expect Thomas to pull something out of his
beard.)

With kind regards,

Andrej


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: A category internal to itself

[Thomas Streicher]

> The results would be a model of type theory (with ?? and ?? but no Id)
> which models Type : Type. It is not trivial, but all types are
> inhabited (and have the fixed-point property). We can still interpret
> Girard's paradox in it, but it is not really a paradox without
> identity types as the type structure does not collapse. Has something
> like that known? (I fully expect Thomas to pull something out of his
> beard.)

Indeed this was done in the Thesis of Nancy J. McCracken in 1979
supervised by John Reynolds. Its title is

   An investigation of programming languages with a polymorphic type
   structure.

Cardelli and Wegner got interested in this in the mid 1980s. There are
2 paper on this one can find on the web

Cardelli & Wegner  On Understanding Types Data Abstraction and Polymorphism
                    Computing Surveys, Vol.17 (1985)

Cardelli  A Polymorphic Lambda Calculus with Type:Type
           a DEC report from 1986

That's what I have wrung out of my beard
Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]