The very dependent recursive structure of iterated parametricity in indexed form

Hugo Herbelin, Ramkumar Ramachandra

Reynolds' parametricity originally equips types with proof-irrelevant binary propositional relations over the types. But such relations can also be taken proof-relevant or unary, a…