Fibred Fibration Categories

TL;DR

This paper introduces fibred type-theoretic fibration categories to model logical predicates in type theory, demonstrating a relational parametricity result in homotopy type theory with implications for polymorphic functions on loop spaces.

Contribution

It defines fibred categories for Martin-Löf type theory and applies them to establish a parametricity result in homotopy type theory.

Findings

Relational parametricity for homotopy type theory

Homotopic equivalence of polymorphic endofunctions on loop spaces

Categorical framework for logical predicates in type theory

Abstract

We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-L\"{o}f 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.