As the person who introduced the name "display map", I would like to emphasise that the whole point of doing so was to be able to do dependent type theory in categories that are NOT locally cartesian closed but "relatively" so. In an LCCC all maps are display maps.

see Chapter VIII of "Practical Foundations of Mathematics" (CUP 1999)

Mike, if you consider that locally cartesian closed categories provide the canonical semantics for dependent type theories then you may as well just use sets, for which any function $p:A\to X$ provides a dependent type $A[x]=\{a|p((a)=x\}$.

Not only is this a very dull notion of dependent type, but it gives no account of the way in which $A{x]$ might depend "continuously" on $x$, something that we probably need to understand in order to give a meaning to the word "recursive".

(Local, relative or ordinary) cartesian closure is needed to interpret function- or Pi-types, which do not feature in your question. The appropriate arena is a category with some finite limits and something infinitary to capture the recursion.

A class of display maps is a class of morphisms that is closed under (composition with isomorphisms and) pullback against arbitrary maps in the category.

This categorical notion is equivalent to that of a dependent type theory in the basic algebraic sense, ie with types, terms, equations and structural rules. As I believe you are more comfortable with a categorical language, you can solve your problem in that setting and then use the equivalence to reformulate it symbolically.

In particular, the class of display maps includes

• all isomorphisms iff the type theory includes singleton dependent types;
• composites iff the type theory has Sigma types;
• inclusions of diagonals and hence all maps iff the type theory has equality types;
• relative cartesian closure corresponds to Pi types.

I had originally interpreted your "recursively dependent" types to mean an infinite chain of dependencies, and hence of display maps. For that you would want the class of displays to be closed under cofiltered limits.

Neel, on the other hand, read it as a fixed point equation, which we can interpret categorically as the fixed point of a functor.

Unsurprisingly, domain theory would be a useful setting in which to look for models of these situations. Indeed my PhD thesis introduced classes of display maps in order to study dependent types in domain theory, and you might like to look at the last chapter for investigations of appropriate notions of displays of domains.

For the theory of display maps and their equivalence with dependent types, my thesis was completely superseded by Chapter VIII of my book, "Practical Foundations of Mathematics" (CUP 1999).

For the interpretation of dependent types in domain theory, Martin Hyland and Andrew Pitts gave a comprehensive account in their paper The Theory of Constructions: Categorical Semantics and Topos-Theoretic Models in Categories in Computer Science and Logic edited by John Gray and Andre Scedrov, AMS Contemporary Mathematics 92 (1989).