CTT: Constructive Type Theory

This is a version of Constructive Type Theory (extensional equality, no universes).

Useful references on Constructive Type Theory: