In order to provide a categorical semantics of typed $\lambda$-calculus without $\eta$-rule Susumu Hayashi used semicategories in MR0841025 (87i:18005) Hayashi, Susumu Adjunction of semifunctors: categorical structures in nonextensional lambda calculus. Theoret. Comput. Sci. 41 (1985), no. 1, 95--104. This was later taken up by R.Hoofman in his Thesis on "Nonstable Models of Linear Logic" (see the first 7 items when you type in "Hoofman, R*" in Math.Reviews). However, in my opinion for the purpose of modelling $\lambda\beta$-calculus it is more natural to use the following kind of structures: (small) categories \C with finite products such that y(Y)^{y(X)} (taken in Psh(\C)) is a retract of some y(E). Thomas Streicher