Subject: categories: further references on semi-categories

From: Thomas Streicher <[email-masked]>
Date: Tue, 29 Nov 2005 10:14:51 +0100 (CET)

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