Re: A category internal to itself

[Andrej Bauer <andrej.bauer@andrej.com>]

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