Mechouet, T.; Zidani, F. Constructive Type Theory. allj 2022, 28, 31-45.