We introduce a notion of Grothendieck logical relation and use it to characterise the definability of morphisms in stable bicartesian closed categories by terms of the simply-typed lambda calculus with finite products and finite sums. Our techniques are based on concepts from topos theory, however our exposition is elementary.
|Title of host publication||Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications|
|Place of Publication||London, UK, UK|
|Number of pages||15|
|Publication status||Published - 1999|