See https://www.nottingham.ac.uk/computerscience/people/thorsten.altenkirch
Thorsten Altenkirch is a German Professor of Computer Science at the University of Nottingham known for his research on logic, type theory, and homotopy type theory. Altenkirch was part of the 2012/2013 special year on Univalent Foundations at the Institute for Advanced Study. At Nottingham he co-chairs the Functional Programming Laboratory with Graham Hutton.