Bifibrational parametricity, from zero to two dimensions

  • Federico Orsanigo

Student thesis: Doctoral Thesis


In this thesis we use bifibrations in order to study relational parametricity. There are three main contributions in this thesis. First, through the lenses of bifibrations, we give a new framework for models of parametricity. This allows us to make some of the underlying categorical structure in Reynolds' original work clearer. Using the same approach we then give a universal property for the interpretation of forall types: they are characterized as terminal objects in a certain category. The universal property permits us to prove both Reynolds' Identity Extension Lemma and Abstraction Theorem. The third contribution consists in defining two-dimensional parametricity. The insight derived from the bifibrational approach leads to a generalization of parametricity to proof relevant relations, incorporating higher-dimensional relations between relations. We call the resulting theory two-dimensional parametricity.
Date of Award27 Jan 2017
Original languageEnglish
Awarding Institution
  • University Of Strathclyde
SupervisorNeil Ghani (Supervisor) & Clemens Kupke (Supervisor)

Cite this