The abstract and slides for our TYPES talk "Generating morphism types using parametricity and Trocq" are now available on my website, check them out! This is joint work with Cyril Cohen and Assia Mahboubi. https://vojtechstep.eu/