T. Mechouet and F. Zidani, “Constructive Type Theory”, allj, vol. 28, no. 1, pp. 31-45, Jun. 2022.