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.