We consider fibrations in the 2-category Fib of fibrations as a setup to model a predicate logic on a polymorphic type theory. Using the lifting/factorisation of adjoints in Fib from [1], we give a structural decomposition of fibrations therein, which we apply to describe the categorical structure necessary to model the above logic. Similarly, we obtain a lifting of simple products for composite fibrations, from which we deduce that the above logic yields a fibration $(p;q) : t \to b$ between $\lambda$2-fibrations; the structure in $t$ expresses the so-called logical relations for polymorphic lambda calculus. We complete the set-up adding structural equality in order to express relational parametricity. We show how such fibrations in Fib arise by externalisation of internal ones, and present some relevant constructions.

References

1. C. Hermida, Some properties of Fib as a fibred 2-category. Journal of Pure and Applied Algebra, 134(1):83-109, 1999.
2. C. Hermida, Fibrations for Abstract Multicategories. In Proceedings of Workshop on Categorical Structures for Descent and Galois Theory, Hopf Algebras and Semiabelian Categories, Fields Institute, Toronto, September 23-28, 2002.