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