van Dijk, E.; Ripley, D.; Gutierrez, J. Core Type Theory. B Sect Log 2023, 52, 145-186.