$\Pi$, $\Sigma$, and identity types without $\eta$ in comprehension categories

Question

In comprehension categories, dependent sums are defined as a choice of left adjoints for all reindexing functors along display maps, satisfying a Beck-Chevalley condition. Dependent products are right adjoints of the same functors, and identity types are left adjoints of reindexing functors along diagonal maps.

These definitions are too strong, however, when one wants to model type formers without the $\eta$ rule.

In categories with attributes (i.e. full split comprehension categories), one can replicate the usual syntactic definitions to get suitably weak notions of $\Pi$, $\Sigma$ and identity types (as Hofmann does), but I don't know how to generalise this approach.

Has someone given a definition of type formers without $\eta$ for general comprehension categories? I am mostly interested in identity types, but it would be nice to find a pattern that works for all type formers.

I suspect that somehow "weakening" the adjunctions should do the trick, but I'm not sure how to make this precise.

Answer 1

I'm not sure exactly what you're asking, but the general pattern for "positive" types is to assert that every "structured" display map over the type has a specified structured section. This matches the induction principle of a positive type former in type theory. One then needs to require a sort of "pullback-stability" condition as well in order to model substitution in type theory. A forthcoming paper of Lumsdaine and Warren will describe a general process of "strictification" of "weakly stable" structure in a comprehension category into "strictly coherent" structure in a fully strict structure. (Edit: this paper is now available, as Lumsdaine–Warren 2015 The local universes construction…)

For identity types, the categorical structure is essentially a well-behaved weak factorization system in which the display maps are (or generate) the right class: see for instance this paper.

Edit: One can be more precise about the notion of "structured section", for instance to say that a "strongly homotopy initial object" in a display-map category is an object $X$ such that every display map with codomain $X$ has a section. Since all ordinary categorical left universal properties can be reformulated as initial objects in some category, this gives a way to translate them into an $\eta$-free version as long as the category in question inherits a natural notion of display map (which is generally induced directly from the underlying category of types/contexts). Similarly, a strongly homotopy initial object is "weakly preserved" by a functor if its image under that functor is another strongly homotopy initial object (not necessarily the "chosen" such object in the codomain of the functor, if there is one). Weak stability then means that pullback functors weakly preserve the relevant SHIOs. I think this is as close to a "general pattern" as you can get.