Fibrations, Logical Predicates and Indeterminates

Abstract

Within the framework of categorical logic/type theory, we provide a category-theoretic account of some logical concepts, i.e. first-order logical predicates for simply typed lambda-calculus, structural induction for inductive data types, and indeterminates for polymorphic calculi. The main concept which underlies the issues above is that of fibration, which gives an abstract presentation of the indexing present in all cases: predicates indexed by types/contexts in first-order logic and types indexed by kinds in polymorphic calculi. The characterisation of the logical concepts in terms of fibrations relies on a fundamental property of adjunctions between fibrations, which in particular relates some structure in the total category of a fibration with that of the fibres. Suitable instances of this property reflect the above-mentioned logical concepts in an abstract way, independently of their syntactic presentation, thereby illuminating their main features.