Impredicative Encodings of (Higher) Inductive Types. - Steve Awodey; Jonas Frey; Sam Speight (LICS, 2018)

Groupoidal realizability for intensional type theory. - Samuel L. Speight (Math. Struct. Comput. Sci., 2024)