Fibred Fibration Categories

We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-L of type theory. Fibred type- theoretic fibration categories give a categorical description of logical predicates for identity types. As an application, we show a relational parametricity result for homotopy type theory. As a corollary, it follows that every closed term of type of polymorphic endofunctions on a loop space is homotopic to some iterated concatenation of a loop.